Documentation

DescriptiveComplexity.Problems.Pcp.Hardness.Draw

Drawing the domino system of a machine #

The elements of the PCP instance the reduction from DescriptiveComplexity.HALT writes, and what its relations are to say about them – everything semantic, no formula in sight. The sibling Interp file writes first-order formulas realizing exactly the predicates of this file, and the Match file proves that an instance reading this way has a match exactly when the machine accepts.

The universe #

An element is a tag with a 5-tuple of source elements (DescriptiveComplexity.HaltPcp.PV); the dimension is set by the move dominoes, whose rules of DescriptiveComplexity.HaltPcp.MRule are indexed by up to five attribute values. Tags fall into three groups:

letters – the alphabet DescriptiveComplexity.Pcp.History.Letter over DescriptiveComplexity.HaltPcp.TapeLetter, drawn by DescriptiveComplexity.HaltPcp.letterElem: one constant tag per constant letter, and a tag carrying one source element for the symbol and state letters;
positions – eight shared constants carrying the short words of every domino, the interleaved page block pairSym p < pairStar p < pairSym p' … carrying the input page of the start domino's bottom word, and four high constants closing it;
dominoes – one tag per shape of DescriptiveComplexity.Pcp.History.Dom at the rules of the machine, the rule dominoes carrying their attribute values in the tuple.

The word tables #

Every short word is a static list of letter specifications (DescriptiveComplexity.HaltPcp.LSpec): each letter is a constant or is indexed by one coordinate of the domino. uSpec/vSpec give the table of each domino tag, and the letter relations PUAt/PVAt say exactly “the pair (position, letter) is an entry of the zipped table” – one uniform definition, one uniform sortedness argument, one uniform reading lemma, instead of one per domino. Only the start domino's bottom word – the one word whose length grows with the instance – has its own relation, StartBotAt.

The order #

One uniform lexicographic key orders the whole universe: the static block index of the tag, then the first coordinate in the machine's own order – which is what interleaves the page block correctly – then the static sub-index (letter before star inside the page block), then the remaining coordinates in the ambient order. On a well-formed machine this is a linear order on all of PV A, junk included.

The tags #

inductive DescriptiveComplexity.HaltPcp.PTag :

The tags of the drawn PCP instance: letters, positions and dominoes.

ltStar : PTag
The decoration letter.
ltSep : PTag
The separator letter between configurations.
ltTri : PTag
The letter opening a history.
ltDia : PTag
The letter closing a match.
ltLft : PTag
The left endmarker, as a letter.
ltRgt : PTag
The right endmarker, as a letter.
ltBoot : PTag
The boot letter.
ltHalt : PTag
The halting letter.
ltSym : PTag
A tape symbol, carrying its element.
ltState : PTag
A state, carrying its element.
pos0 : PTag
The eight shared positions of the short words.
pos1 : PTag
pos2 : PTag
pos3 : PTag
pos4 : PTag
pos5 : PTag
pos6 : PTag
pos7 : PTag
pairSym : PTag
The page block: the position carrying the input symbol of a source position.
pairStar : PTag
The page block: the decoration position after a source position.
hi0 : PTag
The four positions closing the start domino's bottom word.
hi1 : PTag
hi2 : PTag
hi3 : PTag
dStart : PTag
The start domino.
dClose : PTag
The closing domino.
dCopySep : PTag
The domino copying the separator.
dCopyLft : PTag
The dominoes copying the constant letters of the alphabet.
dCopyRgt : PTag
dCopyBoot : PTag
dCopyHalt : PTag
dCopySym : PTag
The domino copying a tape symbol, carrying its element.
dCopyState : PTag
The domino copying a state letter, carrying its element.
dBoot : PTag
The boot rule, carrying its start state.
dAcc : PTag
The halting rule, carrying its accepting state.
dMoveR : PTag
The four move rules, carrying (q, a, b, q', c) respectively (q, a, b, q', blank).
dMoveREnd : PTag
dMoveL : PTag
dMoveLEnd : PTag
dEraseSymL : PTag
The four erasers, the symbol ones carrying their element.
dEraseLft : PTag
dEraseSymR : PTag
dEraseRgt : PTag

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.HaltPcp.instDecidableEqPTag :

DecidableEq PTag

Equations

DescriptiveComplexity.HaltPcp.instDecidableEqPTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Dependency graph

instance DescriptiveComplexity.HaltPcp.instNonemptyPTag :

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.HaltPcp.instFintypePTag :

Equations

One or more equations did not get rendered due to their size.

Dependency graph

def DescriptiveComplexity.HaltPcp.PTag.bIdx :

The block index of a tag: the primary key of the order of the universe. The page block is the only block shared by two tags.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.HaltPcp.PTag.sIdx :

The sub-index inside a block: the input symbol comes before the decoration that follows it.

Equations

DescriptiveComplexity.HaltPcp.PTag.pairStar.sIdx = 1
x✝.sIdx = 0

Instances For

Dependency graph

theorem DescriptiveComplexity.HaltPcp.PTag.bIdx_sIdx_inj {t t' : PTag} :

t.bIdx = t'.bIdx → t.sIdx = t'.sIdx → t = t'

The pair of indices identifies the tag.

Dependency graph

The universe and its distinguished elements #

@[reducible, inline]

abbrev DescriptiveComplexity.HaltPcp.PV (A : Type) :

The universe of the drawn instance: a tag and a 5-tuple of source elements.

Equations

DescriptiveComplexity.HaltPcp.PV A = (DescriptiveComplexity.HaltPcp.PTag × (Fin 5 → A))

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HaltPcp.pbot {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

A

The least source element, the padding of the unused coordinates.

Equations

DescriptiveComplexity.HaltPcp.pbot = ⋯.choose

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HaltPcp.cstE {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : PTag) :

PV A

The constant element of a tag.

Equations

DescriptiveComplexity.HaltPcp.cstE t = (t, fun (x : Fin 5) => DescriptiveComplexity.HaltPcp.pbot)

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HaltPcp.idxE {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : PTag) (a : A) :

PV A

The element of a tag carrying one source element.

Equations

DescriptiveComplexity.HaltPcp.idxE t a = (t, fun (i : Fin 5) => if i = 0 then a else DescriptiveComplexity.HaltPcp.pbot)

Instances For

Dependency graph

@[simp]

theorem DescriptiveComplexity.HaltPcp.cstE_fst {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : PTag) :

(cstE t).1 = t

Dependency graph

@[simp]

theorem DescriptiveComplexity.HaltPcp.idxE_fst {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : PTag) (a : A) :

(idxE t a).1 = t

Dependency graph

@[simp]

theorem DescriptiveComplexity.HaltPcp.idxE_snd_zero {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : PTag) (a : A) :

(idxE t a).2 0 = a

Dependency graph

The order of the universe #

One lexicographic key: the static block index, the first coordinate in the machine's order, the static sub-index, the remaining coordinates in the ambient order.

def DescriptiveComplexity.HaltPcp.MLt {A : Type} [FirstOrder.Language.turing.Structure A] (a b : A) :

Strictly below, in the machine's order.

Equations

DescriptiveComplexity.HaltPcp.MLt a b = (DescriptiveComplexity.TMLe a b ∧ a ≠ b)

Instances For

Dependency graph

def DescriptiveComplexity.HaltPcp.TupLe {A : Type} [LinearOrder A] (w w' : Fin 5 → A) :

The ambient lexicographic order on the last four coordinates.

Equations

DescriptiveComplexity.HaltPcp.TupLe w w' = (w 1 < w' 1 ∨ w 1 = w' 1 ∧ (w 2 < w' 2 ∨ w 2 = w' 2 ∧ (w 3 < w' 3 ∨ w 3 = w' 3 ∧ w 4 ≤ w' 4)))

Instances For

Dependency graph

def DescriptiveComplexity.HaltPcp.PLe {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (x y : PV A) :

The order of the drawn instance: block index, first coordinate in the machine's order, sub-index, remaining coordinates. On a well-formed machine this is a linear order on the whole universe.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

def DescriptiveComplexity.HaltPcp.PLt {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (x y : PV A) :

The strict part of the order of the drawn instance.

Equations

DescriptiveComplexity.HaltPcp.PLt x y = (DescriptiveComplexity.HaltPcp.PLe x y ∧ x ≠ y)

Instances For

Dependency graph

theorem DescriptiveComplexity.HaltPcp.tupLe_refl {A : Type} [LinearOrder A] (w : Fin 5 → A) :

Dependency graph

theorem DescriptiveComplexity.HaltPcp.tupLe_trans {A : Type} [LinearOrder A] {u v w : Fin 5 → A} (h1 : TupLe u v) (h2 : TupLe v w) :

Dependency graph

theorem DescriptiveComplexity.HaltPcp.tupLe_antisymm {A : Type} [LinearOrder A] {u v : Fin 5 → A} (h1 : TupLe u v) (h2 : TupLe v u) :

u 1 = v 1 ∧ u 2 = v 2 ∧ u 3 = v 3 ∧ u 4 = v 4

Dependency graph

theorem DescriptiveComplexity.HaltPcp.tupLe_total {A : Type} [LinearOrder A] (u v : Fin 5 → A) :

TupLe u v ∨ TupLe v u

Dependency graph

theorem DescriptiveComplexity.HaltPcp.mLt_trans {A : Type} [FirstOrder.Language.turing.Structure A] (hlin : IsLinOrd TMLe) {a b c : A} (h1 : MLt a b) (h2 : MLt b c) :

MLt a c

Dependency graph

The word tables #

inductive DescriptiveComplexity.HaltPcp.LSpec :

A letter of a short word: a constant, or a letter carrying one coordinate of its domino.

cst : PTag → LSpec
A constant letter.
idx : PTag → Fin 5 → LSpec
A letter carrying the given coordinate of the domino.

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HaltPcp.LSpec.eval {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (w : Fin 5 → A) :

LSpec → PV A

The letter an entry of the table stands for, at a domino's tuple.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HaltPcp.posE {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

ℕ → PV A

The eight shared positions of the short words.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HaltPcp.posPrefix {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (n : ℕ) :

The first n of the shared positions, in order.

Equations

DescriptiveComplexity.HaltPcp.posPrefix n = List.map DescriptiveComplexity.HaltPcp.posE (List.range n)

Instances For

Dependency graph

def DescriptiveComplexity.HaltPcp.uSpec :

PTag → List LSpec

The top words, as tables: the decorated left-hand sides of the rules, and the tops of the bookkeeping dominoes.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.HaltPcp.uSpec x✝ = []

Instances For

Dependency graph

def DescriptiveComplexity.HaltPcp.vSpec :

PTag → List LSpec

The bottom words, as tables – all but the start domino's, which has its own layout.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.HaltPcp.vSpec DescriptiveComplexity.HaltPcp.PTag.dClose = [DescriptiveComplexity.HaltPcp.LSpec.cst DescriptiveComplexity.HaltPcp.PTag.ltDia]
DescriptiveComplexity.HaltPcp.vSpec x✝ = []

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HaltPcp.uWord {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : PV A) :

The top word of a domino element.

Equations

DescriptiveComplexity.HaltPcp.uWord x = List.map (DescriptiveComplexity.HaltPcp.LSpec.eval x.2) (DescriptiveComplexity.HaltPcp.uSpec x.1)

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HaltPcp.vWord {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : PV A) :

The bottom word of a domino element other than the start domino.

Equations

DescriptiveComplexity.HaltPcp.vWord x = List.map (DescriptiveComplexity.HaltPcp.LSpec.eval x.2) (DescriptiveComplexity.HaltPcp.vSpec x.1)

Instances For

Dependency graph

def DescriptiveComplexity.HaltPcp.PUAt {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (d p c : PV A) :

The top letter relation: the pair is an entry of the zipped table.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

def DescriptiveComplexity.HaltPcp.StartBotAt {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p c : PV A) :

The bottom word of the start domino: seven low constants, the interleaved page block carrying the input, four high constants.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

def DescriptiveComplexity.HaltPcp.PVAt {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (d p c : PV A) :

The bottom letter relation: the start domino reads its own layout, every other domino its table.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

The dominoes #

def DescriptiveComplexity.HaltPcp.DomGuard {A : Type} [FirstOrder.Language.turing.Structure A] (x : PV A) :

The side condition a domino tag places on its tuple: the promises of the rule it stands for.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

def DescriptiveComplexity.HaltPcp.PDom {A : Type} [FirstOrder.Language.turing.Structure A] (x : PV A) :

Being a domino of the drawn instance: the machine is well-formed and the tag's side condition holds.

Equations

DescriptiveComplexity.HaltPcp.PDom x = ((DescriptiveComplexity.tmData A).WellFormed ∧ DescriptiveComplexity.HaltPcp.DomGuard x)

Instances For

Dependency graph

def DescriptiveComplexity.HaltPcp.decodeDom {A : Type} (x : PV A) :

Pcp.History.Dom (TapeLetter A)

The abstract domino an element stands for.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

theorem DescriptiveComplexity.HaltPcp.exists_encode {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : (tmData A).WellFormed) {d : Pcp.History.Dom (TapeLetter A)} (hok : Pcp.History.Ok (MRule (tmData A)) d) :

∃ (x : PV A), PDom x ∧ decodeDom x = d

Every legitimate domino is drawn: an element with the right guard stands for it.

Dependency graph

The positions, in order #

noncomputable def DescriptiveComplexity.HaltPcp.pagePos {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (ps : List A) :

The page block of the start domino's bottom word: the input position and its decoration, per source position.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HaltPcp.startPos {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (ps : List A) :

The positions of the start domino's bottom word.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HaltPcp.pageBot {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (inp : List A) :

The letters of the page block: the input symbol and the decoration.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.HaltPcp.startBot {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (inp : List A) :

The letters of the start domino's bottom word.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

@[simp]

theorem DescriptiveComplexity.HaltPcp.length_pagePos {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (ps : List A) :

(pagePos ps).length = 2 * ps.length

Dependency graph

@[simp]

theorem DescriptiveComplexity.HaltPcp.length_pageBot {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (inp : List A) :

(pageBot inp).length = 2 * inp.length

Dependency graph