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.

theorem DescriptiveComplexity.Pcp.irrefl_of_asymm {α : Type} {Lt : α → α → Prop} (has : ∀ (a b : α), Lt a b → Lt b a → False) (a : α) : ¬Lt a a

An asymmetric relation is irreflexive.

theorem DescriptiveComplexity.Pcp.lt_getElem_iff {α : Type} {Lt : α → α → Prop} (has : ∀ (a b : α), Lt a b → Lt b a → False) {l : List α} (hl : List.Pairwise Lt l) {i j : ℕ} (hi : i < l.length) (hj : j < l.length) : Lt l[i] l[j] ↔ i < j

In a strictly sorted list, one entry precedes another exactly when its index is smaller.

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.

theorem DescriptiveComplexity.Pcp.exists_forall₂ {α β : Type} {R : α → β → Prop} {l : List α} : (∀ a ∈ l, ∃ (b : β), R a b) → ∃ (w : List β), List.Forall₂ R l w

A list of witnesses for a list of existentials.

theorem DescriptiveComplexity.Pcp.eq_of_forall₂ {α β : Type} {M : α → β → Prop} {δ : Type} {RU : α → δ → Prop} {RV : β → δ → Prop} (hcomp : ∀ (x : α) (y : β) (ℓ ℓ' : δ), M x y → RU x ℓ → RV y ℓ' → ℓ = ℓ') {L₁ : List α} {L₂ : List β} (hM : List.Forall₂ M L₁ L₂) {U V : List δ} : List.Forall₂ RU L₁ U → List.Forall₂ RV L₂ V → U = V

Two lists read off entry by entry along a matching agree, as soon as the matched entries carry the same letter.

The lexicographic order on blocks and positions

def DescriptiveComplexity.Pcp.LexOf {D α : Type} (R : D → D → Prop) (S : α → α → Prop) : D × α → D × α → Prop

The lexicographic order on pairs (block, position inside it), for two strict orders.

Equations

• DescriptiveComplexity.Pcp.LexOf R S x y = (R x.1 y.1 ∨ x.1 = y.1 ∧ S x.2 y.2)

theorem DescriptiveComplexity.Pcp.asymm_strict {D : Type} {Le : D → D → Prop} (h : IsLinOrd Le) (a b : D) (hab : Le a b ∧ a ≠ b) (hba : Le b a ∧ b ≠ a) : False

The strict part of a linear order relation is asymmetric.

theorem DescriptiveComplexity.Pcp.asymm_lexOf {D α : Type} {R : D → D → Prop} {S : α → α → Prop} (hR : ∀ (a b : D), R a b → R b a → False) (hS : ∀ (a b : α), S a b → S b a → False) (x y : D × α) (hxy : LexOf R S x y) (hyx : LexOf R S y x) : False

The lexicographic order of two asymmetric relations is asymmetric.

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

theorem DescriptiveComplexity.Pcp.pairwise_parseIx {D α : Type} {slots : List D} {ps : D → List α} {R : D → D → Prop} {S : α → α → Prop} (hs : List.Pairwise R slots) (hp : ∀ (s : D), List.Pairwise S (ps s)) : List.Pairwise (LexOf R S) (parseIx slots ps)

The index list of a parse is sorted lexicographically: the blocks come in order, and the positions inside a block come in order.

theorem DescriptiveComplexity.Pcp.forall₂_parseIx {D α β : Type} {slots : List D} {ps : D → List α} {T : D → α → β → Prop} {ws : D → List β} (h : ∀ s ∈ slots, List.Forall₂ (T s) (ps s) (ws s)) : List.Forall₂ (fun (x : D × α) (ℓ : β) => T x.1 x.2 ℓ) (parseIx slots ps) (List.flatMap ws slots)

The letters of a parse, read along its index list, are the letters of the concatenation.

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.

theorem DescriptiveComplexity.Pcp.forall₂_getElem {α β : Type} {R : α → β → Prop} {l₁ : List α} {l₂ : List β} (h : List.Forall₂ R l₁ l₂) {i : ℕ} (h₁ : i < l₁.length) (h₂ : i < l₂.length) : R l₁[i] l₂[i]

Entries of two lists related by List.Forall₂ are related index by index.

theorem DescriptiveComplexity.Pcp.exists_fun_of_forall₂ {α β : Type} {R : α → β → Prop} {l₁ : List α} {l₂ : List β} (h : List.Forall₂ R l₁ l₂) : ∃ (g : Fin l₁.length → β), List.map g (List.finRange l₁.length) = l₂ ∧ ∀ (i : Fin l₁.length), R (l₁.get i) (g i)

A List.Forall₂ is a function on the indices of its left list.

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

def DescriptiveComplexity.Pcp.IdxMatch {α β : Type} (L₁ : List α) (L₂ : List β) (x : α) (y : β) : Prop

The pairing of two lists index by index, as a relation: the matching a yes-instance hands back once its two parses are known to be the same word.

Equations

• DescriptiveComplexity.Pcp.IdxMatch L₁ L₂ x y = ∃ (i : ℕ) (h₁ : i < L₁.length) (h₂ : i < L₂.length), L₁[i] = x ∧ L₂[i] = y

theorem DescriptiveComplexity.Pcp.idxMatch_mem {α β : Type} {L₁ : List α} {L₂ : List β} {x : α} {y : β} (h : IdxMatch L₁ L₂ x y) : x ∈ L₁ ∧ y ∈ L₂

The index pairing relates members of the two lists.

theorem DescriptiveComplexity.Pcp.idxMatch_left {α β : Type} {L₁ : List α} {L₂ : List β} (hlen : L₁.length = L₂.length) {x : α} (hx : x ∈ L₁) : ∃ (y : β), IdxMatch L₁ L₂ x y

The index pairing is defined on every member of the left list.

theorem DescriptiveComplexity.Pcp.idxMatch_right {α β : Type} {L₁ : List α} {L₂ : List β} (hlen : L₁.length = L₂.length) {y : β} (hy : y ∈ L₂) : ∃ (x : α), IdxMatch L₁ L₂ x y

The index pairing is defined on every member of the right list.

theorem DescriptiveComplexity.Pcp.idxMatch_mono {α β : Type} {L₁ : List α} {L₂ : List β} {Lt₁ : α → α → Prop} {Lt₂ : β → β → Prop} (has₁ : ∀ (a b : α), Lt₁ a b → Lt₁ b a → False) (has₂ : ∀ (a b : β), Lt₂ a b → Lt₂ b a → False) (hp₁ : List.Pairwise Lt₁ L₁) (hp₂ : List.Pairwise Lt₂ L₂) {x : α} {y : β} {x' : α} {y' : β} (h : IdxMatch L₁ L₂ x y) (h' : IdxMatch L₁ L₂ x' y') : Lt₁ x x' ↔ Lt₂ y y'

The index pairing reflects the orders of two strictly sorted lists: both read as the order of the indices.