Sorted enumerations, and matchings between them

The list layer under DescriptiveComplexity.PCP ∈ RE. A word of a Post instance is a partial map from a finite linear order to letters (DescriptiveComplexity.Pcp.IsWordU), so everything the semantics reads is mediated by the strictly increasing list enumerating the positions used. This file is that mediation, stated for arbitrary relations and lists:

• DescriptiveComplexity.Pcp.IsEnum – being the strictly increasing enumeration of a predicate, and DescriptiveComplexity.Pcp.exists_isEnum, which produces one over a finite type carrying a linear order relation (DescriptiveComplexity.IsLinOrd), by sorting;
• the two ways a parse of a concatenation is built out of the parses of its blocks: DescriptiveComplexity.Pcp.forall₂_flatMap for the letters and List.pairwise_flatMap for the order;
• DescriptiveComplexity.Pcp.forall₂_of_matching, the lemma of the file: a relation between the members of two strictly sorted lists that is total on both sides and reflects the order is the pairing of their entries index by index. This is what makes a matching between the two parses – a relation variable, hence first-order-checkable – as good as the equality of the two concatenations, which is not.

The converse pairing, DescriptiveComplexity.Pcp.IdxMatch, is the matching two lists of the same length carry for free; it is the certificate a yes-instance hands back.

Strictly increasing enumerations

def DescriptiveComplexity.Pcp.IsEnum {α : Type} (Lt : α → α → Prop) (S : α → Prop) (ps : List α) : Prop

ps enumerates S in increasing order: it is strictly sorted for Lt, and its members are exactly the elements satisfying S. Such a list is unique when it exists, but nothing below needs the uniqueness.

Equations

• DescriptiveComplexity.Pcp.IsEnum Lt S ps = (List.Pairwise Lt ps ∧ ∀ (p : α), p ∈ ps ↔ S p)

theorem DescriptiveComplexity.Pcp.exists_isEnum {α : Type} [Finite α] {Le : α → α → Prop} (h : IsLinOrd Le) (S : α → Prop) : ∃ (ps : List α), IsEnum (fun (a b : α) => Le a b ∧ a ≠ b) S ps

Over a finite type ordered by a linear order relation, every predicate has a strictly increasing enumeration: sort the elements satisfying it.

Indices of a strictly sorted list

A strictly sorted list has no repetitions, so its order is the order of its indices: that is the only property of the two parses the matching lemma below uses.

Lists built block by block

theorem DescriptiveComplexity.Pcp.forall₂_flatMap {γ α β : Type} {R : α → β → Prop} {f : γ → List α} {g : γ → List β} {l : List γ} : (∀ c ∈ l, List.Forall₂ R (f c) (g c)) → List.Forall₂ R (List.flatMap f l) (List.flatMap g l)

Two flatMaps over the same list are related entry by entry as soon as their blocks are: the parse of a concatenation is the concatenation of the parses.

The lexicographic order on blocks and positions

The index list of a parse

A parse of a concatenation is indexed by the pairs (block, position inside the block), in lexicographic order: the common word is never invented, only the two ways of cutting it into blocks are.

def DescriptiveComplexity.Pcp.parseIx {D α : Type} (slots : List D) (ps : D → List α) : List (D × α)

The index list of a parse: the pairs (block, position used inside it), block by block.

Equations

• DescriptiveComplexity.Pcp.parseIx slots ps = List.flatMap (fun (s : D) => List.map (fun (p : α) => (s, p)) (ps s)) slots

@[simp]

theorem DescriptiveComplexity.Pcp.mem_parseIx {D α : Type} {slots : List D} {ps : D → List α} {x : D × α} : x ∈ parseIx slots ps ↔ x.1 ∈ slots ∧ x.2 ∈ ps x.1

Reading a Forall₂ as a function

The certificate of a yes-instance indexes its slots by Fin n, while the semantics hands the words over as a List.Forall₂; this turns the one into the other, once.

Matchings between two sorted lists

theorem DescriptiveComplexity.Pcp.forall₂_of_matching {α β : Type} {Lt₁ : α → α → Prop} {Lt₂ : β → β → Prop} (has₁ : ∀ (a b : α), Lt₁ a b → Lt₁ b a → False) (has₂ : ∀ (a b : β), Lt₂ a b → Lt₂ b a → False) {L₁ : List α} {L₂ : List β} {M : α → β → Prop} : List.Pairwise Lt₁ L₁ → List.Pairwise Lt₂ L₂ → (∀ (x : α) (y : β), M x y → x ∈ L₁ ∧ y ∈ L₂) → (∀ x ∈ L₁, ∃ (y : β), M x y) → (∀ y ∈ L₂, ∃ (x : α), M x y) → (∀ (x : α) (y : β) (x' : α) (y' : β), M x y → M x' y' → (Lt₁ x x' ↔ Lt₂ y y')) → List.Forall₂ M L₁ L₂

A matching between two strictly sorted lists pairs their entries index by index. The relation is asked only for what a first-order kernel can check of a relation variable – that it lands in the two lists, that it is defined everywhere on both, and that it reflects the two orders – and this is already enough to make it the unique order isomorphism, hence to identify the two lists entry by entry. Functionality and injectivity are not hypotheses: they follow from reflecting the order.

The matching two lists of the same length carry