Cook-Levin: the counter-machine view shared by the clause generators
InductiveStages of the multiplication routine#✓fully proved
The stages of the counter-machine multiplication routine form the four-element type with elements head, body, l2 and rest.
inductive MS | head | body | l2 | rest
deriving DecidableEqUsed by 65
InductiveStacks of a counter machine#✓fully proved
For a type \(C\), the stacks of a counter machine with counters indexed by \(C\) are an output stack \(\mathrm{out}\) and one counter stack \(c_x\) for each \(x \in C\).
inductive SK (C : Type)
| out
| c (x : C)
deriving DecidableEq, FintypeUsed by 114
for loop in the counter view · Host stack renaming for the accept generator · Host stack renaming for the shift generator · Host stack renaming for the init generator · Host stack renaming for the situation-definition generator · Host stack renaming for the update generator · Embedding of the accept generator into the host · Embedding of the shift generator into the host · Embedding of the init generator into the host · Embedding of the situation-definition generator into the host · Embedding of the update generator's stacks into the host · The host as a finite multi-stack Turing machine · The host program · The assembled generator, after the precomputation · Sequencing · The counter program · The counter program's run · Stack renaming of the counter program · Embedding of the counter program's stacks · The full program · One Horner round · The statements of one Horner round · Horner rounds · The power loop · Power-loop program · The precomputation · Unit targets of a multi-target transfer · Multi-target transferAbbreviationAlphabets of a counter machine#✓fully proved
For a type \(C\), the output stack \(\mathrm{out}\) of a counter machine with counters indexed by \(C\) has the Booleans as its alphabet, and each counter stack \(c_x\) has a one-element alphabet.
abbrev SΓ (C : Type) : SK C → Type
| .out => Bool
| .c _ => Unitinductive SK (C : Type)
| out
| c (x : C)
deriving DecidableEq, FintypeCSLibExt/Computability/Complexity/CookLevin/CounterView.lean:57
Uses 1 · Used by 90
for loop in the counter view · Embedding of the accept generator into the host · Embedding of the shift generator into the host · The host as a finite multi-stack Turing machine · The host program · The assembled generator, after the precomputation · Sequencing · The counter program · The counter program's run · Embedding of the counter program's stacks · The full program · One Horner round · The statements of one Horner round · Horner rounds · The power loop · Power-loop program · The precomputation · Unit targets of a multi-target transfer · Multi-target transferDefinitionStacks holding given counter values#✓fully proved
For a type \(C\), counter values \(f : C \to \mathbb{N}\) and a list \(o\) of Booleans, \(\mathrm{st}(f, o)\) is the stack contents of a counter machine whose output stack \(\mathrm{out}\) holds \(o\) and whose counter stack \(c_x\) holds exactly \(f(x)\) copies of the unit symbol, for each \(x \in C\).
def st (f : C → ℕ) (o : List Bool) : ∀ k, List (SΓ C k)
| .out => o
| .c x => cnt () (f x)abbrev SΓ (C : Type) : SK C → Type
| .out => Bool
| .c _ => UnitCSLibExt/Computability/Complexity/CookLevin/CounterView.lean:63
abbrev cnt {α : Type} (u : α) (n : ℕ) : List α := List.replicate n uMathlibExt/Computability/TuringMachine/Program.lean:115
Uses 3 · Used by 65
for loop in the counter view · Sequencing · The counter program's run · One Horner round · Horner rounds · The power loop · The precomputation · Multi-target transferDefinitionThe multiplication routine of a counter machine#✓fully proved
Let \(a, a_d, b, c, t\) be counters, let \(\mathrm{mk}\) assign a label to each stage of the multiplication routine, and let \(\mathrm{next}\) be a label. The routine assigns to each stage the following counter-machine instruction. At head: pop a unit from \(a\), then push a unit onto \(a_d\) and go to \(\mathrm{mk}(\mathrm{body})\), or go to \(\mathrm{mk}(\mathrm{rest})\) if \(a\) was empty. At body: pop a unit from \(b\), then push a unit onto each of \(c\) and \(t\) and go to \(\mathrm{mk}(\mathrm{body})\), or go to \(\mathrm{mk}(\mathrm{l2})\) if \(b\) was empty. At l2: pop a unit from \(t\), then push a unit onto \(b\) and go to \(\mathrm{mk}(\mathrm{l2})\), or go to \(\mathrm{mk}(\mathrm{head})\) if \(t\) was empty. At rest: pop a unit from \(a_d\), then push a unit onto \(a\) and go to \(\mathrm{mk}(\mathrm{rest})\), or go to \(\mathrm{next}\) if \(a_d\) was empty. In each instruction the pop sets the flag to true if a unit was popped and to false if the counter was empty, and the pushes leave the flag unchanged.
Started at head with \(a, a_d, b, c, t\) distinct and \(a_d\) and \(t\) empty, the routine ends at \(\mathrm{next}\) having added \(a \cdot b\) to \(c\), with every other counter unchanged; \(a_d\) serves as the loop index and \(t\) as scratch.
def mulS (a ad b c t : C) (mk : MS → Λ) (next : Λ) : MS → TM2.Stmt (SΓ C) Λ Bool
| .head => forHead (.c a) (.c ad) () (mk .body) (mk .rest)
| .body => xfer (.c b) [⟨.c c, ()⟩, ⟨.c t, ()⟩] (mk .body) (mk .l2)
| .l2 => xfer (.c t) [⟨.c b, ()⟩] (mk .l2) (mk .head)
| .rest => xfer (.c ad) [⟨.c a, ()⟩] (mk .rest) nextinductive MS | head | body | l2 | rest
deriving DecidableEqCSLibExt/Computability/Complexity/CookLevin/CounterView.lean:49
abbrev SΓ (C : Type) : SK C → Type
| .out => Bool
| .c _ => UnitCSLibExt/Computability/Complexity/CookLevin/CounterView.lean:63
def forHead (c cd : K) (ucd : Γ cd) (body rest : Λ) : TM2.Stmt Γ Λ σ :=
.pop c (fun _ o => Flag.tag o.isSome) <| .branch Flag.untag
(.push cd (fun _ => ucd) <| .goto fun _ => body) (.goto fun _ => rest)MathlibExt/Computability/TuringMachine/Program.lean:461
def xfer (k : K) (ps : List (Σ k, Γ k)) (self next : Λ) : TM2.Stmt Γ Λ σ :=
.pop k (fun _ o => Flag.tag o.isSome)
(.branch Flag.untag (pushAll ps (.goto fun _ => self)) (.goto fun _ => next))MathlibExt/Computability/TuringMachine/Program.lean:232
Uses 6 · Used by 27
TheoremGap emission in the counter view#✓fully proved
Let \(M\) be a counter machine, let \(P, Q, T_1, T_2\) be pairwise distinct counters, let \(y\) be a list of Booleans, let \(\mathrm{dec}\), \(\mathrm{cmp}\), \(\mathrm{emit}\), \(z\), \(\mathrm{next}\) be labels, and let \(r\), \(r'\), \(\mathrm{out}\) assign a label to each comparison outcome \(\omega\), which is one of \(\mathrm{lt}\), \(\mathrm{eq}\), \(\mathrm{gt}\). In the instructions below, every pop sets the flag to true if a unit was popped and to false if the stack was empty, and pushing or prepending leaves the flag unchanged. Suppose that at \(\mathrm{dec}\), \(M\) pops a unit from \(P\) and goes to \(\mathrm{cmp}\), or to \(z\) if \(P\) was empty; at \(\mathrm{cmp}\), \(M\) pops a unit from each of \(P\) and \(Q\), pushes a unit onto \(T_1\) if \(P\) was nonempty and onto \(T_2\) if \(Q\) was nonempty, and goes back to \(\mathrm{cmp}\) if both were nonempty, and otherwise to \(r(\mathrm{lt})\), \(r(\mathrm{eq})\) or \(r(\mathrm{gt})\) according as only \(Q\), neither, or only \(P\) was nonempty; for each \(\omega\), at \(r(\omega)\), \(M\) pops a unit from \(T_1\), then pushes a unit onto \(P\) and stays at \(r(\omega)\), or goes to \(r'(\omega)\) if \(T_1\) was empty; at \(r'(\omega)\), \(M\) pops a unit from \(T_2\), then pushes a unit onto \(Q\) and stays at \(r'(\omega)\), or goes to \(\mathrm{out}(\omega)\) if \(T_2\) was empty; \(\mathrm{out}(\mathrm{eq}) = \mathrm{next}\) and \(\mathrm{out}(\mathrm{lt}) = \mathrm{out}(\mathrm{gt}) = \mathrm{emit}\); and at \(\mathrm{emit}\), \(M\) prepends \(y\) to the output stack and goes to \(\mathrm{dec}\). Let \(q, g \in \mathbb{N}\) and let \(F\) be counter values with \(F(P) = q + g + 1\), \(F(Q) = q\) and \(F(T_1) = F(T_2) = 0\). Then for every flag \(v\) and every list \(o\) of Booleans, \(M\) goes in exactly \(g(3q + 6) + 3q + 4\) steps from label \(\mathrm{dec}\), flag \(v\) and stacks \(\mathrm{st}(F, o)\) to label \(\mathrm{next}\), flag false and stacks \(\mathrm{st}(F', y^g o)\), where \(F'\) agrees with \(F\) except that \(F'(P) = q\), and \(y^g o\) is \(g\) copies of \(y\) followed by \(o\).
theorem gapS {P Q T1 T2 : C} {ys : List Bool} {dec cmpL emitL ifZero next : Λ}
{r rB out : Ordering → Λ}
(hdec : M dec = decr (.c P) ifZero cmpL)
(hcmp : M cmpL = cmpStep (.c P) (.c Q) (.c T1) (.c T2) () () cmpL (r .lt) (r .eq) (r .gt))
(hr : ∀ o, M (r o) = xfer (.c T1) [⟨.c P, ()⟩] (r o) (rB o))
(hrB : ∀ o, M (rB o) = xfer (.c T2) [⟨.c Q, ()⟩] (rB o) (out o))
(hout : ∀ o, out o = if o = .eq then next else emitL)
(hemit : M emitL = emitR .out ys dec)
(hnd : ([.c P, .c Q, .c T1, .c T2, .out] : List (SK C)).Nodup) (q gap : ℕ) (F : C → ℕ)
(hP : F P = q + gap + 1) (hQ : F Q = q) (h1 : F T1 = 0) (h2 : F T2 = 0) (v : Bool)
(o : List Bool) :
Run M (gap * (3 * q + 6) + 3 * q + 4) ⟨some dec, v, st F o⟩
⟨some next, false, st (update F P q) (rep ys gap ++ o)⟩def decr (k : K) (ifZero ifPos : Λ) : TM2.Stmt Γ Λ σ :=
.pop k (fun _ o => Flag.tag o.isSome)
(.branch Flag.untag (.goto fun _ => ifPos) (.goto fun _ => ifZero))MathlibExt/Computability/TuringMachine/Program.lean:141
def cmpStep (a b ta tb : K) (uta : Γ ta) (utb : Γ tb)
(self lt eq gt : Λ) : TM2.Stmt Γ Λ σ :=
.pop a (fun _ o => Flag.tag o.isSome) <| .branch Flag.untag
(.pop b (fun _ o => Flag.tag o.isSome) <| .branch Flag.untag
(.push ta (fun _ => uta) <| .push tb (fun _ => utb) <| .goto fun _ => self)
(.push ta (fun _ => uta) <| .goto fun _ => gt))
(.pop b (fun _ o => Flag.tag o.isSome) <| .branch Flag.untag
(.push tb (fun _ => utb) <| .goto fun _ => lt)
(.goto fun _ => eq))MathlibExt/Computability/TuringMachine/Program.lean:291
def xfer (k : K) (ps : List (Σ k, Γ k)) (self next : Λ) : TM2.Stmt Γ Λ σ :=
.pop k (fun _ o => Flag.tag o.isSome)
(.branch Flag.untag (pushAll ps (.goto fun _ => self)) (.goto fun _ => next))MathlibExt/Computability/TuringMachine/Program.lean:232
def emitR (k : K) (ys : List (Γ k)) (next : Λ) : TM2.Stmt Γ Λ σ := emit k ys.reverse nextMathlibExt/Computability/TuringMachine/Program.lean:698
inductive SK (C : Type)
| out
| c (x : C)
deriving DecidableEq, FintypeCSLibExt/Computability/Complexity/CookLevin/CounterView.lean:57
def Run (n : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
(flip bind (TM2.step M))^[n] (some c) = some dMathlibExt/Computability/TuringMachine/Program.lean:84
def st (f : C → ℕ) (o : List Bool) : ∀ k, List (SΓ C k)
| .out => o
| .c x => cnt () (f x)CSLibExt/Computability/Complexity/CookLevin/CounterView.lean:72
def rep {α : Type} (ys : List α) (n : ℕ) : List α := (List.replicate n ys).flattenMathlibExt/Computability/TuringMachine/Program.lean:682
Uses 12 · Used by 4
TheoremBudgeted runs transport along equal counter values#✓fully proved
Let \(M\) be a counter machine, let \(K, X \in \mathbb{N}\), let \(F\) and \(F'\) be counter values with \(F = F'\), let \(l\) be a label or the halting state, \(v\) a flag, \(o\) a list of Booleans and \(d\) a configuration. If there is \(n\) with \(K + n \le X\) such that \(M\) goes in exactly \(n\) steps from the configuration with label \(l\), flag \(v\) and stacks \(\mathrm{st}(F', o)\) to \(d\), then the same holds from the configuration with label \(l\), flag \(v\) and stacks \(\mathrm{st}(F, o)\).
theorem bud_st {K X : ℕ} {F F' : C → ℕ} {l : Option Λ} {v : Bool} {o : List Bool}
{d : TM2.Cfg (SΓ C) Λ Bool} (h : F = F') (h' : Bud M K X ⟨l, v, st F' o⟩ d) :
Bud M K X ⟨l, v, st F o⟩ dabbrev SΓ (C : Type) : SK C → Type
| .out => Bool
| .c _ => UnitCSLibExt/Computability/Complexity/CookLevin/CounterView.lean:63
def Bud (M : Λ → TM2.Stmt Γ Λ σ) (K X : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
∃ n, K + n ≤ X ∧ Run M n c dMathlibExt/Computability/TuringMachine/Program.lean:907
def st (f : C → ℕ) (o : List Bool) : ∀ k, List (SΓ C k)
| .out => o
| .c x => cnt () (f x)CSLibExt/Computability/Complexity/CookLevin/CounterView.lean:72
Uses 4 · Used by 13
TheoremA runtime for loop in the counter view#✓fully proved
Let \(M\) be a counter machine, let \(c \ne c_d\) be counters, and let \(\mathrm{head}\), \(\mathrm{body}\), \(\mathrm{rest}\), \(\mathrm{next}\) be labels such that at \(\mathrm{head}\), \(M\) pops a unit from \(c\), then pushes a unit onto \(c_d\) and goes to \(\mathrm{body}\), or goes to \(\mathrm{rest}\) if \(c\) was empty; and at \(\mathrm{rest}\), \(M\) pops a unit from \(c_d\), then pushes a unit onto \(c\) and stays at \(\mathrm{rest}\), or goes to \(\mathrm{next}\) if \(c_d\) was empty. Each of these pops sets the flag to true if a unit was popped and to false if the stack was empty, and the pushes leave the flag unchanged. Let \(n, B \in \mathbb{N}\), let \(\mathrm{blk}\) assign a list of Booleans to each natural number, and let \(f\) be counter values with \(f(c) = n\) and \(f(c_d) = 0\); for \(t < n\) write \(g_t\) for the counter values that agree with \(f\) except that \(g_t(c) = t\) and \(g_t(c_d) = n - t\), and write juxtaposition of lists for concatenation. Suppose that for every \(t < n\) and every list \(o\) of Booleans, \(M\) goes in at most \(B\) steps from label \(\mathrm{body}\), flag true and stacks \(\mathrm{st}(g_t, o)\) to label \(\mathrm{head}\), some flag and stacks \(\mathrm{st}(g_t, \mathrm{blk}(t)\, o)\). Then for every flag \(v\) and every list \(o\) of Booleans, \(M\) goes in at most \(n(B + 1) + n + 2\) steps from label \(\mathrm{head}\), flag \(v\) and stacks \(\mathrm{st}(f, o)\) to label \(\mathrm{next}\), flag false and stacks \(\mathrm{st}(f, \mathrm{blk}(0)\, \mathrm{blk}(1) \cdots \mathrm{blk}(n-1)\, o)\).
The body runs with \(c\) holding \(t = n - 1, \dots, 0\) in that order, so the blocks end up in ascending order.
theorem stLoop {c cd : C} {head body rest next : Λ}
(hHead : M head = forHead (.c c) (.c cd) () body rest)
(hRest : M rest = xfer (.c cd) [⟨.c c, ()⟩] rest next) (hc : c ≠ cd) (n B : ℕ)
(blk : ℕ → List Bool) (f : C → ℕ) (hfc : f c = n) (hfcd : f cd = 0)
(hbody : ∀ t < n, ∀ o, ∃ v', RunLe M B
⟨some body, true, st (update (update f c t) cd (n - t)) o⟩
⟨some head, v', st (update (update f c t) cd (n - t)) (blk t ++ o)⟩)
(v : Bool) (o : List Bool) :
RunLe M (n * (B + 1) + n + 2) ⟨some head, v, st f o⟩
⟨some next, false, st f ((List.range n).flatMap blk ++ o)⟩def forHead (c cd : K) (ucd : Γ cd) (body rest : Λ) : TM2.Stmt Γ Λ σ :=
.pop c (fun _ o => Flag.tag o.isSome) <| .branch Flag.untag
(.push cd (fun _ => ucd) <| .goto fun _ => body) (.goto fun _ => rest)MathlibExt/Computability/TuringMachine/Program.lean:461
def xfer (k : K) (ps : List (Σ k, Γ k)) (self next : Λ) : TM2.Stmt Γ Λ σ :=
.pop k (fun _ o => Flag.tag o.isSome)
(.branch Flag.untag (pushAll ps (.goto fun _ => self)) (.goto fun _ => next))MathlibExt/Computability/TuringMachine/Program.lean:232
def RunLe (M : Λ → TM2.Stmt Γ Λ σ) (B : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
∃ n, n ≤ B ∧ Run M n c dMathlibExt/Computability/TuringMachine/Program.lean:901
def st (f : C → ℕ) (o : List Bool) : ∀ k, List (SΓ C k)
| .out => o
| .c x => cnt () (f x)CSLibExt/Computability/Complexity/CookLevin/CounterView.lean:72
Uses 9 · Used by 6
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.