The drawn instance has a match exactly when the machine accepts

The combinatorial half of the correctness of the reduction from DescriptiveComplexity.HALT to DescriptiveComplexity.PCP, over any Language.pcp-structure whose four relations read as the semantic predicates of DescriptiveComplexity.Problems.Pcp.Hardness.Draw (DescriptiveComplexity.HaltPcp.Reads) – which is exactly what the interpretation of the sibling Interp file provides.

Words by tables

Everything a word of the drawn instance says is of the form “the pair (position, letter) is an entry of a zipped table”, with the position side strictly increasing. Two abstract lemmas turn such a table into the unique word of a domino (DescriptiveComplexity.HaltPcp.isWord_of_zip, DescriptiveComplexity.HaltPcp.eq_of_isWord_zip): the enumeration of the used positions is pinned by sortedness, and the letters by functionality of the zip. The short words instantiate them at the shared position prefix; the start domino's bottom word at its own layout, whose table DescriptiveComplexity.HaltPcp.startBotAt_iff_zip is proved by walking the input page along the enumeration of the positions.

The two directions

A match of DescriptiveComplexity.Pcp.History maps to a solution of the instance by encoding each abstract domino (DescriptiveComplexity.HaltPcp.exists_encode) and reading the tables forward; a solution maps back by decoding each marked element (DescriptiveComplexity.HaltPcp.decodeDom) and using uniqueness of the words, injectivity of the letter map turning the equality of the two concatenations back into the equality of the abstract words. Chained with DescriptiveComplexity.HaltPcp.acceptsU_iff_hasMatch, this gives the correctness statement DescriptiveComplexity.HaltPcp.pcpOn_iff_of_reads the Interp file consumes.

Sorted lists, zips and tables

theorem DescriptiveComplexity.HaltPcp.sorted_eq {α : Type} {Lt : α → α → Prop} (hasym : ∀ (a b : α), Lt a b → Lt b a → False) {l₁ l₂ : List α} : List.Pairwise Lt l₁ → List.Pairwise Lt l₂ → (∀ (x : α), x ∈ l₁ ↔ x ∈ l₂) → l₁ = l₂

Two strictly sorted lists with the same members are equal.

theorem DescriptiveComplexity.HaltPcp.mem_zip_iff {α β : Type} {l : List α} {w : List β} (hlen : l.length = w.length) {p : α} {c : β} : (p, c) ∈ l.zip w ↔ ∃ (i : ℕ) (h : i < l.length), l[i] = p ∧ w[i] = c

The entries of a zip of two lists of equal length, by index.

theorem DescriptiveComplexity.HaltPcp.zip_fun {α β : Type} {l : List α} {w : List β} (hlen : l.length = w.length) (hnd : l.Nodup) {p : α} {c c' : β} (h : (p, c) ∈ l.zip w) (h' : (p, c') ∈ l.zip w) : c = c'

With a duplicate-free position side, a zip is functional.

theorem DescriptiveComplexity.HaltPcp.exists_mem_zip {α β : Type} {l : List α} {w : List β} (hlen : l.length = w.length) {p : α} : (∃ (c : β), (p, c) ∈ l.zip w) ↔ p ∈ l

A position of the table carries a letter exactly when it is on the position side.

theorem DescriptiveComplexity.HaltPcp.forall₂_zip_self {α β : Type} {l : List α} {w : List β} : l.length = w.length → List.Forall₂ (fun (p : α) (c : β) => (p, c) ∈ l.zip w) l w

A zip relates its two sides entry by entry.

theorem DescriptiveComplexity.HaltPcp.forall₂_unique {α β : Type} {R : α → β → Prop} {l : List α} {w w' : List β} : (∀ a ∈ l, ∀ (b b' : β), R a b → R a b' → b = b') → List.Forall₂ R l w → List.Forall₂ R l w' → w = w'

A functional List.Forall₂ determines its right list.

Reading the instance

structure DescriptiveComplexity.HaltPcp.Reads {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {B : Type} [FirstOrder.Language.pcp.Structure B] (e : B ≃ PV A) : Prop

The four relations of the instance read as the drawn predicates, along an equivalence of the universes. This is what the defining formulas of the interpretation are proved to realize.

• ord (x y : B) : Pcp.Ord x y ↔ PLe (e x) (e y)

  The order of the positions is the drawn order.

• dom (x : B) : Pcp.DomG x ↔ PDom (e x)

  The marked dominoes are the drawn dominoes.

• uAt (d p c : B) : Pcp.UAt d p c ↔ PUAt (e d) (e p) (e c)

  The top words read off the top tables.

• vAt (d p c : B) : Pcp.VAt d p c ↔ PVAt (e d) (e p) (e c)

  The bottom words read off the bottom tables.

theorem DescriptiveComplexity.HaltPcp.Reads.ordLt {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {B : Type} [FirstOrder.Language.pcp.Structure B] {e : B ≃ PV A} (h : Reads e) (x y : B) : Pcp.OrdLt x y ↔ PLt (e x) (e y)

Tables are words

DescriptiveComplexity.Pcp.IsWordU/IsWordV both have the shape “some strictly increasing enumeration of the used positions carries the word”; the two lemmas below handle any letter relation given by a zipped table with a strictly increasing position side.

theorem DescriptiveComplexity.HaltPcp.isWord_of_zip {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {B : Type} [FirstOrder.Language.pcp.Structure B] {e : B ≃ PV A} {R : B → B → Prop} {P W : List (PV A)} (h : Reads e) (hlen : P.length = W.length) (hsort : List.Pairwise PLt P) (htab : ∀ (p c : B), R p c ↔ (e p, e c) ∈ P.zip W) : ∃ (ps : List B), List.Pairwise Pcp.OrdLt ps ∧ (∀ (p : B), p ∈ ps ↔ ∃ (c : B), R p c) ∧ List.Forall₂ R ps (List.map (⇑e.symm) W)

A table is a word: the position side, transported, enumerates the used positions in order and carries the letter side.

theorem DescriptiveComplexity.HaltPcp.eq_of_isWord_zip {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {B : Type} [FirstOrder.Language.pcp.Structure B] {e : B ≃ PV A} {R : B → B → Prop} {P W : List (PV A)} (h : Reads e) (hasym : ∀ (x y : B), Pcp.OrdLt x y → Pcp.OrdLt y x → False) (hlen : P.length = W.length) (hsort : List.Pairwise PLt P) (htab : ∀ (p c : B), R p c ↔ (e p, e c) ∈ P.zip W) {ps w : List B} (hps : List.Pairwise Pcp.OrdLt ps) (hmem : ∀ (p : B), p ∈ ps ↔ ∃ (c : B), R p c) (hf : List.Forall₂ R ps w) : w = List.map (⇑e.symm) W

The word of a table is unique: any word of the letter relation is the letter side of the table.

The tables of the dominoes

theorem DescriptiveComplexity.HaltPcp.uSpec_length_le (t : PTag) : (uSpec t).length ≤ 8

Every short word fits in the shared positions.

theorem DescriptiveComplexity.HaltPcp.vSpec_length_le (t : PTag) : (vSpec t).length ≤ 8

Every short bottom word fits in the shared positions.

theorem DescriptiveComplexity.HaltPcp.pVAt_of_ne {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {d p c : PV A} (hne : d.1 ≠ PTag.dStart) : PVAt d p c ↔ (p, c) ∈ (posPrefix (vSpec d.1).length).zip (vWord d)

Away from the start domino, the bottom relation is its table.

theorem DescriptiveComplexity.HaltPcp.pVAt_start {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {d p c : PV A} (hd : d.1 = PTag.dStart) : PVAt d p c ↔ StartBotAt p c

At the start domino, the bottom relation is the page layout.

theorem DescriptiveComplexity.HaltPcp.length_posPrefix {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (n : ℕ) : (posPrefix n).length = n

The lengths of the two sides of a short top table agree.

The start domino's table

theorem DescriptiveComplexity.HaltPcp.posPrefix_seven {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : posPrefix 7 = [cstE PTag.pos0, cstE PTag.pos1, cstE PTag.pos2, cstE PTag.pos3, cstE PTag.pos4, cstE PTag.pos5, cstE PTag.pos6]

The shared position prefix, spelt out.

theorem DescriptiveComplexity.HaltPcp.mem_zip_page {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : (tmData A).WellFormed) {ps inp : List A} (hinp : List.Forall₂ (tmData A).InitTape ps inp) {p c : PV A} : (p, c) ∈ (pagePos ps).zip (pageBot inp) ↔ ∃ (q : A) (a : A), q ∈ ps ∧ (tmData A).InitTape q a ∧ (p = idxE PTag.pairSym q ∧ c = idxE PTag.ltSym a ∨ p = idxE PTag.pairStar q ∧ c = cstE PTag.ltStar)

The entries of the page block of the start table.

theorem DescriptiveComplexity.HaltPcp.startBotAt_iff_zip {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : (tmData A).WellFormed) {ps inp : List A} (hps : IsPosEnum (tmData A) ps) (hinp : List.Forall₂ (tmData A).InitTape ps inp) {p c : PV A} : StartBotAt p c ↔ (p, c) ∈ (startPos ps).zip (startBot inp)

The layout of the start domino's bottom word is its table: the letter relation of the start domino says exactly that the pair is an entry of the zipped layout.

More Forall₂ plumbing

theorem DescriptiveComplexity.HaltPcp.eq_map_of_forall₂ {α β : Type} {f : α → β} {l : List α} {w : List β} : List.Forall₂ (fun (a : α) (b : β) => b = f a) l w → w = List.map f l

theorem DescriptiveComplexity.HaltPcp.forall₂_imp_mem {α β : Type} {R S : α → β → Prop} {l : List α} {w : List β} : (∀ a ∈ l, ∀ (b : β), R a b → S a b) → List.Forall₂ R l w → List.Forall₂ S l w

theorem DescriptiveComplexity.HaltPcp.forall₂_mem_right {α β : Type} {R : α → β → Prop} {l : List α} {w : List β} : List.Forall₂ R l w → ∀ {b : β}, b ∈ w → ∃ a ∈ l, R a b

theorem DescriptiveComplexity.HaltPcp.flatten_map {δ ε ζ : Type} (f : δ → List ε) (g : ε → ζ) (l : List δ) : (List.map (fun (d : δ) => List.map g (f d)) l).flatten = List.map g (List.map f l).flatten

The words of the drawn dominoes

theorem DescriptiveComplexity.HaltPcp.initTape_exists {A : Type} [FirstOrder.Language.turing.Structure A] (hwf : (tmData A).WellFormed) (p : A) : ∃ (a : A), (tmData A).InitTape p a

Every input cell holds something: its input symbol or the blank.

theorem DescriptiveComplexity.HaltPcp.isWordU_elem {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {B : Type} [FirstOrder.Language.pcp.Structure B] {e : B ≃ PV A} (h : Reads e) (d : B) : Pcp.IsWordU d (List.map (⇑e.symm) (uWord (e d)))

The top word of any element is its top table.

theorem DescriptiveComplexity.HaltPcp.eq_of_isWordU {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {B : Type} [FirstOrder.Language.pcp.Structure B] {e : B ≃ PV A} (h : Reads e) (hwfB : Pcp.IsWF B) {d : B} {w : List B} (hw : Pcp.IsWordU d w) : w = List.map (⇑e.symm) (uWord (e d))

The top word of any element is only its top table.

theorem DescriptiveComplexity.HaltPcp.isWordV_elem_ne {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {B : Type} [FirstOrder.Language.pcp.Structure B] {e : B ≃ PV A} (h : Reads e) {d : B} (hne : (e d).1 ≠ PTag.dStart) : Pcp.IsWordV d (List.map (⇑e.symm) (vWord (e d)))

The bottom word of an element other than the start domino is its bottom table.

theorem DescriptiveComplexity.HaltPcp.eq_of_isWordV_ne {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {B : Type} [FirstOrder.Language.pcp.Structure B] {e : B ≃ PV A} (h : Reads e) (hwfB : Pcp.IsWF B) {d : B} (hne : (e d).1 ≠ PTag.dStart) {w : List B} (hw : Pcp.IsWordV d w) : w = List.map (⇑e.symm) (vWord (e d))

theorem DescriptiveComplexity.HaltPcp.isWordV_elem_start {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {B : Type} [FirstOrder.Language.pcp.Structure B] {e : B ≃ PV A} (h : Reads e) (hwf : (tmData A).WellFormed) {ps inp : List A} (hps : IsPosEnum (tmData A) ps) (hinp : List.Forall₂ (tmData A).InitTape ps inp) {d : B} (hd : (e d).1 = PTag.dStart) : Pcp.IsWordV d (List.map (⇑e.symm) (startBot inp))

The bottom word of the start domino is its layout.

theorem DescriptiveComplexity.HaltPcp.eq_of_isWordV_start {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {B : Type} [FirstOrder.Language.pcp.Structure B] {e : B ≃ PV A} (h : Reads e) (hwfB : Pcp.IsWF B) (hwf : (tmData A).WellFormed) {ps inp : List A} (hps : IsPosEnum (tmData A) ps) (hinp : List.Forall₂ (tmData A).InitTape ps inp) {d : B} (hd : (e d).1 = PTag.dStart) {w : List B} (hw : Pcp.IsWordV d w) : w = List.map (⇑e.symm) (startBot inp)

theorem DescriptiveComplexity.HaltPcp.decode_of_tag_start {A : Type} {x : PV A} (hx : x.1 = PTag.dStart) : decodeDom x = Pcp.History.Dom.start

The start tag decodes to the abstract start domino.

theorem DescriptiveComplexity.HaltPcp.tag_of_decode_start {A : Type} [FirstOrder.Language.turing.Structure A] {x : PV A} (hx : PDom x) (hd : decodeDom x = Pcp.History.Dom.start) : x.1 = PTag.dStart

Only the start domino decodes to the abstract start domino.

theorem DescriptiveComplexity.HaltPcp.startBotAt_fun {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : (tmData A).WellFormed) {p c c' : PV A} (h₁ : StartBotAt p c) (h₂ : StartBotAt p c') : c = c'

The start layout is functional in the position.

Well-formedness of the drawn instance

theorem DescriptiveComplexity.HaltPcp.isWF_of_reads {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {B : Type} [FirstOrder.Language.pcp.Structure B] {e : B ≃ PV A} (h : Reads e) (hwf : (tmData A).WellFormed) : Pcp.IsWF B

The equivalence

theorem DescriptiveComplexity.HaltPcp.pcpOn_iff_of_reads {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {B : Type} [FirstOrder.Language.pcp.Structure B] {e : B ≃ PV A} (h : Reads e) : Pcp.PcpOn B ↔ (tmData A).WellFormed ∧ (tmData A).AcceptsU

Correctness of the drawn instance: it is a yes-instance of PCP exactly when the machine is well-formed and accepts.