Occurrences of a formula with a first clause to Moving a walked name from \(D\) to \(E\)
TheoremOccurrences of a formula with a first clause#✓fully proved
Let \(C\) be a clause and \(\varphi\) a CNF formula, and write a literal occurrence as a pair \((i, \ell)\) of a clause index \(i\) and a literal \(\ell\). The list of literal occurrences of the formula whose first clause is \(C\) and whose remaining clauses are those of \(\varphi\) is the list of \((0, \ell)\) for the literals \(\ell\) of \(C\) in order, followed by the list of \((i + 1, \ell)\) for the occurrences \((i, \ell)\) of \(\varphi\) in order.
theorem occs_cons (C : CNFClause) (φ : CNF) :
occs (C :: φ) = C.map (fun l => (0, l)) ++ (occs φ).map fun o => (o.1 + 1, o.2)abbrev CNFClause := List (Nat × Bool)CSLibExt/Logics/Propositional/CNF/Basic.lean:30
abbrev CNF := List CNFClauseCSLibExt/Logics/Propositional/CNF/Basic.lean:33
def occs (φ : CNF) : List (ℕ × ℕ × Bool) :=
φ.zipIdx.flatMap fun p => p.1.map fun l => (p.2, l.1, l.2)CSLibExt/Computability/Complexity/Karp/Clique.lean:97
Uses 3 · Used by 3
DefinitionPolarity-first tokens of a literal#✓fully proved
For a literal \((x, p)\) with variable index \(x \in \mathbb{N}\) and polarity \(p\), the token list is the polarity marker symbol for \(p\) followed by one name-bit symbol for each bit of the canonical binary representation of \(x\) (least significant bit first, empty for \(x = 0\)), in order.
This is how the CLIQUE emitter writes a walked literal occurrence on its stack \(D\), top first.
def dTok (l : ℕ × Bool) : List Sym := .lit l.2 :: (encodeNat l.1).map .bitinductive Sym
| bit (b : Bool) | lit (p : Bool) | cl | val (b : Bool) | dead
deriving DecidableEqCSLibExt/Computability/Complexity/SatVerifierSpec.lean:41
Uses 1 · Used by 3
DefinitionTokens of an item on the walked stack#✓fully proved
An item of the stack \(D\) is either \(\mathrm{none}\), standing for a clause marker, or an occurrence \((x, p)\) of the variable \(x\) with polarity \(p\). The tokens of \(\mathrm{none}\) are the single clause-marker symbol; the tokens of \((x, p)\) are the polarity marker of \(p\) followed by the binary encoding of \(x\) as name-bit symbols.
def itemTok : Option (ℕ × Bool) → List Sym
| none => [.cl]
| some l => dTok linductive Sym
| bit (b : Bool) | lit (p : Bool) | cl | val (b : Bool) | dead
deriving DecidableEqCSLibExt/Computability/Complexity/SatVerifierSpec.lean:41
def dTok (l : ℕ × Bool) : List Sym := .lit l.2 :: (encodeNat l.1).map .bitCSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:106
Uses 2 · Used by 6
DefinitionBits pushed by a walk of the CLIQUE emitter#✓fully proved
Let \(l = (x, p)\) be a literal occurrence with name \(x \in \mathbb{N}\) and polarity \(p\), let \(f\) be a Boolean, and let \(ds\) be a list whose items are literal occurrences or clause markers. The bit list \(\mathrm{walkBits}(l, f, ds)\) is defined by recursion on \(ds\): it is empty if \(ds\) is empty; if \(ds\) is a clause marker followed by \(ds'\), it is \(\mathrm{walkBits}(l, \mathrm{true}, ds')\); and if \(ds\) is an occurrence \(l'\) followed by \(ds'\), it is the bit \(f \wedge \mathrm{adj}(l, l')\) followed by \(\mathrm{walkBits}(l, f, ds')\). Here \(\mathrm{adj}(l, l')\) is the Karp adjacency of literals: it is false exactly when \(l\) and \(l'\) have the same name and opposite polarities.
The flag \(f\) records whether a clause marker has been passed; while it is false, each occurrence contributes a false bit.
def walkBits (l : ℕ × Bool) : Bool → List (Option (ℕ × Bool)) → List Bool
| _, [] => []
| _, none :: ds => walkBits l true ds
| f, some l' :: ds => (f && adjL l l') :: walkBits l f dsdef adjL (l l' : ℕ × Bool) : Bool := !(l.1 == l'.1 && l.2 != l'.2)CSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:55
DefinitionWalked items of a formula#✓fully proved
For a CNF formula \(\varphi\) with clauses \(C_1, \dots, C_m\) in order, the items of \(\varphi\) are the list made of, for each \(i = 1, \dots, m\) in turn, the literals of \(C_i\) in order, each as an occurrence item, followed by one clause-marker item \(\mathrm{none}\). These are the items on the stack \(D\) once the clauses of \(\varphi\) are walked.
def items (φ : CNF) : List (Option (ℕ × Bool)) := φ.flatMap fun C => C.map some ++ [none]abbrev CNF := List CNFClauseCSLibExt/Logics/Propositional/CNF/Basic.lean:33
Uses 2 · Used by 6
DefinitionRows pushed for a clause's literals#✓fully proved
For a list \(I\) of items and literals \(l_1, \dots, l_k\), the rows are the concatenation, for \(i = 1, \dots, k\) in turn, of the reverse of the walk bits of \(l_i\) with flag false over the items \(l_{i+1}, \dots, l_k\) (as occurrence items) followed by \(I\). These are the bits pushed when the literals of a clause are walked above the items \(I\).
def lrows (ds : List (Option (ℕ × Bool))) : List (ℕ × Bool) → List Bool
| [] => []
| l :: Ls => (walkBits l false (Ls.map some ++ ds)).reverse ++ lrows ds Lsdef walkBits (l : ℕ × Bool) : Bool → List (Option (ℕ × Bool)) → List Bool
| _, [] => []
| _, none :: ds => walkBits l true ds
| f, some l' :: ds => (f && adjL l l') :: walkBits l f dsCSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:115
Uses 1 · Used by 6
DefinitionRow bits of a formula for the CLIQUE emitter#✓fully proved
A literal is a pair \((x, s)\) of a variable \(x \in \mathbb{N}\) and a polarity \(s\), and an item is a literal or a clause marker. For a literal \(\ell = (x, s)\), a Boolean \(f\) and a list of items, the walk bits are defined by recursion on the list: there are none for the empty list; for a list starting with a clause marker they are the walk bits of the rest with \(f\) replaced by true; for a list starting with a literal \((x', s')\) they are the bit "\(f\) and not (\(x = x'\) and \(s \ne s'\))" followed by the walk bits of the rest with the same \(f\). For a list \(\delta\) of items, the rows of a list of literals are none for the empty list, and for a list \(\ell_1, \dots, \ell_k\) with \(k \ge 1\) they are the reverse of the walk bits of \(\ell_1\) with \(f\) false over the list \(\ell_2, \dots, \ell_k\) followed by \(\delta\), then the rows of \(\ell_2, \dots, \ell_k\). The items of a CNF formula \(\psi\) are, for each clause of \(\psi\) in order, its literals followed by a clause marker. The row bits of a CNF formula are defined by recursion on its clauses: the empty formula has none, and for the formula with first clause \(C\) and remaining clauses \(\varphi\) they are the rows of the literals of \(C\) for \(\delta\) the clause marker followed by the items of \(\varphi\), followed by the row bits of \(\varphi\).
def rowsF : CNF → List Bool
| [] => []
| C :: φ => lrows (none :: items φ) C ++ rowsF φabbrev CNF := List CNFClauseCSLibExt/Logics/Propositional/CNF/Basic.lean:33
def lrows (ds : List (Option (ℕ × Bool))) : List (ℕ × Bool) → List Bool
| [] => []
| l :: Ls => (walkBits l false (Ls.map some ++ ds)).reverse ++ lrows ds LsCSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:124
def items (φ : CNF) : List (Option (ℕ × Bool)) := φ.flatMap fun C => C.map some ++ [none]CSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:121
Uses 4 · Used by 3
TheoremPair bits of a leading clause#✓fully proved
Let \(C\) be a clause and \(\varphi\) a CNF formula. Let \(O_\varphi\) be the list of literal occurrences of \(\varphi\) (clause index, variable, polarity), with every clause index increased by \(1\). Then the row-by-row pair bits of the list made of the literals of \(C\), each with clause index \(0\), followed by \(O_\varphi\), are the rows pushed for the literals of \(C\) walked above a clause marker and the items of \(\varphi\), followed by the row-by-row pair bits of \(O_\varphi\).
theorem bitsRec_clause (C : CNFClause) (φ : CNF) :
bitsRec (C.map (fun l => (0, l)) ++ (occs φ).map fun o => (o.1 + 1, o.2)) =
lrows (none :: items φ) C ++ bitsRec ((occs φ).map fun o => (o.1 + 1, o.2))abbrev CNFClause := List (Nat × Bool)CSLibExt/Logics/Propositional/CNF/Basic.lean:30
abbrev CNF := List CNFClauseCSLibExt/Logics/Propositional/CNF/Basic.lean:33
def bitsRec : List (ℕ × ℕ × Bool) → List Bool
| [] => []
| o :: os => (os.map (occAdj o)).reverse ++ bitsRec osCSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:58
def occs (φ : CNF) : List (ℕ × ℕ × Bool) :=
φ.zipIdx.flatMap fun p => p.1.map fun l => (p.2, l.1, l.2)CSLibExt/Computability/Complexity/Karp/Clique.lean:97
def lrows (ds : List (Option (ℕ × Bool))) : List (ℕ × Bool) → List Bool
| [] => []
| l :: Ls => (walkBits l false (Ls.map some ++ ds)).reverse ++ lrows ds LsCSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:124
def items (φ : CNF) : List (Option (ℕ × Bool)) := φ.flatMap fun C => C.map some ++ [none]CSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:121
Uses 10 · Used by 1
TheoremThe CLIQUE emitter's row bits are Karp's pair bits#✓fully proved
For every CNF formula \(\varphi\), the row bits of \(\varphi\) equal the pair bits of Karp's CLIQUE graph of \(\varphi\): with \(o_0, \dots, o_{m-1}\) the literal occurrences of \(\varphi\), these are, for the pairs \((i, j)\) with \(i < j < m\) in encoding order (rows \(i\) ascending, and \(j\) descending within a row), the bits telling whether \(o_i\) and \(o_j\) lie in different clauses and are not complementary.
theorem rowsF_eq (φ : CNF) : rowsF φ = cliqueBits φabbrev CNF := List CNFClauseCSLibExt/Logics/Propositional/CNF/Basic.lean:33
def rowsF : CNF → List Bool
| [] => []
| C :: φ => lrows (none :: items φ) C ++ rowsF φCSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:129
def cliqueBits (φ : CNF) : List Bool :=
(pairs (occs φ).length).map fun p => occAdj ((occs φ).getD p.1 (0, 0, false))
((occs φ).getD p.2 (0, 0, false))CSLibExt/Computability/Complexity/Karp/Clique.lean:105
Uses 13 · Used by 1
InductiveStacks of the SAT-to-CLIQUE emitter#✓fully proved
The emitter has nine stacks: \(T\) (tokens), \(O\) (output), \(A\) (the current name), \(B\) (scratch), \(D\) (walked occurrences), \(E\) (the walk's other side), \(X\) (scratch), \(C\) (the clause count) and \(N\) (the occurrence count).
inductive K | T | O | A | B | D | E | X | C | N
deriving DecidableEqUsed by 18
DefinitionStack alphabets of the CLIQUE emitter#✓fully proved
In the CLIQUE emitter, the output stack \(O\) has the Booleans as its alphabet, and every other stack has the token symbols as its alphabet.
The counter stacks \(C\) and \(N\) hold copies of the clause marker.
@[reducible] def Γ : K → Type
| .O => Bool
| _ => Syminductive K | T | O | A | B | D | E | X | C | N
deriving DecidableEqCSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:183
inductive Sym
| bit (b : Bool) | lit (p : Bool) | cl | val (b : Bool) | dead
deriving DecidableEqCSLibExt/Computability/Complexity/SatVerifierSpec.lean:41
Uses 2 · Used by 17
InductiveLabels of the SAT-to-CLIQUE emitter#✓fully proved
For bits \(p, q, f, b\) the labels are \(\mathsf{start}\), \(\mathsf{lits}\), \(\mathsf{nm}(p)\), \(\mathsf{walk}(p, f)\), \(\mathsf{cmp}(p, q)\), \(\mathsf{res}(p, b)\), \(\mathsf{rsA}(p)\), \(\mathsf{rsD}(p)\), \(\mathsf{mvN}(p, f)\), \(\mathsf{back}(p)\), \(\mathsf{put}(p)\), \(\mathsf{put2}(p)\), \(\mathsf{put3}(p)\), \(\mathsf{fin}\), \(\mathsf{finN}\), \(\mathsf{fin2}\), \(\mathsf{finC}\) and \(\mathsf{done}\). Here \(p\) is the polarity of the current occurrence. \(\mathsf{start}\) begins a clause and \(\mathsf{lits}\) pops a literal marker; \(\mathsf{nm}\) moves its name to \(A\); \(\mathsf{walk}(p, f)\) walks \(D\), where \(f\) tells whether a clause marker was passed; \(\mathsf{cmp}(p, q)\), \(\mathsf{res}\), \(\mathsf{rsA}\) and \(\mathsf{rsD}\) compare with an occurrence of polarity \(q\), push the bit \(b\) and restore; \(\mathsf{mvN}\) moves that occurrence's name to \(E\); \(\mathsf{back}\) moves \(E\) back to \(D\); \(\mathsf{put}\), \(\mathsf{put2}\) and \(\mathsf{put3}\) put the current occurrence on \(D\); \(\mathsf{fin}\) to \(\mathsf{finC}\) push the instance prefix, and \(\mathsf{done}\) halts.
inductive Lab
| start | lits | nm (p : Bool) | walk (p f : Bool) | cmp (p q : Bool) | res (p b : Bool)
| rsA (p : Bool) | rsD (p : Bool) | mvN (p f : Bool) | back (p : Bool) | put (p : Bool)
| put2 (p : Bool) | put3 (p : Bool) | fin | finN | fin2 | finC | done
deriving DecidableEqUsed by 16
DefinitionThe CLIQUE emitter machine#✓fully proved
The CLIQUE emitter is the multi-stack machine with stacks \(T, O, A, B, D, E, X, C, N\), a Boolean flag and the labels named below. The stack \(O\) holds Booleans and the others hold symbols, among them the bit symbols \(\mathrm{bit}(b)\), the literal symbols \(\mathrm{lit}(p)\) and the clause marker \(\mathrm{cl}\). Each test sets the flag to its outcome, a pop that reads a polarity or a bit sets the flag to it, and other pops leave the flag unchanged. To move the bits of \(Y\) to \(Z\) and then go to \(\lambda\) means: while the top of \(Y\) is a bit symbol, pop it and push it onto \(Z\); once \(Y\) is empty or its top is another symbol, go to \(\lambda\) (the flag serves as scratch). The instruction at each label is as follows.
At \(\mathrm{start}\): test whether \(T\) is empty; if so go to \(\mathrm{fin}\), else pop \(T\), push \(\mathrm{cl}\) onto \(D\) and onto \(C\), and go to \(\mathrm{lits}\). At \(\mathrm{lits}\): test whether the top of \(T\) is a literal symbol; if so pop it, reading the polarity \(q\) (true exactly for \(\mathrm{lit}(\mathrm{true})\)), push \(\mathrm{cl}\) onto \(N\) and go to \(\mathrm{nm}(q)\); else go to \(\mathrm{start}\). At \(\mathrm{nm}(p)\): move the bits of \(T\) to \(A\), then go to \(\mathrm{walk}(p, \mathrm{false})\). At \(\mathrm{walk}(p, f)\): test whether \(D\) is empty; if so go to \(\mathrm{back}(p)\); else test whether the top of \(D\) is \(\mathrm{cl}\); if so pop it, push \(\mathrm{cl}\) onto \(E\) and go to \(\mathrm{walk}(p, \mathrm{true})\); else pop \(D\), reading \(q\) (true exactly for \(\mathrm{lit}(\mathrm{true})\)), push \(\mathrm{lit}(q)\) onto \(E\), and if \(f\) go to \(\mathrm{cmp}(p, q)\), else push false onto \(O\) and go to \(\mathrm{mvN}(p, \mathrm{false})\). At \(\mathrm{cmp}(p, q)\): compare the bits of \(A\) and \(D\), that is, while both tops are bit symbols of the same bit, pop both and push that bit symbol onto \(X\) and onto \(B\); when both bit blocks end together go to \(\mathrm{res}(p, b)\) with \(b\) true exactly when \(p = q\), and on a mismatch (different bits, or one block ending first) go to \(\mathrm{res}(p, \mathrm{true})\) without popping (the flag serves as scratch). At \(\mathrm{res}(p, b)\): push \(b\) onto \(O\) and go to \(\mathrm{rsA}(p)\). At \(\mathrm{rsA}(p)\): move the bits of \(X\) to \(A\), then go to \(\mathrm{rsD}(p)\). At \(\mathrm{rsD}(p)\): move the bits of \(B\) to \(D\), then go to \(\mathrm{mvN}(p, \mathrm{true})\). At \(\mathrm{mvN}(p, f)\): move the bits of \(D\) to \(E\), then go to \(\mathrm{walk}(p, f)\). At \(\mathrm{back}(p)\): test whether \(E\) is empty; if so go to \(\mathrm{put}(p)\); else test whether its top is \(\mathrm{cl}\); if so pop it and push \(\mathrm{cl}\) onto \(D\); else test whether its top is a literal symbol; if so pop it, reading \(q\) (true exactly for \(\mathrm{lit}(\mathrm{true})\)), and push \(\mathrm{lit}(q)\) onto \(D\); else pop it, reading \(b\) (true exactly for \(\mathrm{bit}(\mathrm{true})\)), and push \(\mathrm{bit}(b)\) onto \(D\); in these three cases stay at \(\mathrm{back}(p)\). At \(\mathrm{put}(p)\): move the bits of \(A\) to \(B\), then go to \(\mathrm{put2}(p)\). At \(\mathrm{put2}(p)\): move the bits of \(B\) to \(D\), then go to \(\mathrm{put3}(p)\). At \(\mathrm{put3}(p)\): push \(\mathrm{lit}(p)\) onto \(D\) and go to \(\mathrm{lits}\). At \(\mathrm{fin}\): push false onto \(O\) and go to \(\mathrm{finN}\). At \(\mathrm{finN}\): pop \(N\), testing whether a symbol was popped; if so push true onto \(O\) and stay, else go to \(\mathrm{fin2}\). At \(\mathrm{fin2}\): push false onto \(O\) and go to \(\mathrm{finC}\). At \(\mathrm{finC}\): pop \(C\), testing whether a symbol was popped; if so push true onto \(O\) and stay, else go to \(\mathrm{done}\). At \(\mathrm{done}\): halt.
Cslib.Complexity.Karp.EmitClique.prog · 37 lines
def prog : Lab → TM2.Stmt Γ Lab Bool
| .start => .peek .T (fun _ o => o.isNone) <| .branch id (.goto fun _ => .fin) <|
.pop .T (fun s _ => s) <| .push .D (fun _ => Sym.cl) <| .push .C (fun _ => Sym.cl) <|
.goto fun _ => .lits
| .lits => .peek .T (fun _ o => Emit3.isLit o) <| .branch id
(.pop .T (fun _ o => o == some (.lit true)) <| .push .N (fun _ => Sym.cl) <|
.goto fun s => .nm s)
(.goto fun _ => .start)
| .nm p => moveB .T .A Sym.bit? Sym.bit (.nm p) (.walk p false)
| .walk p f => .peek .D (fun _ o => o.isNone) <| .branch id (.goto fun _ => .back p) <|
.peek .D (fun _ o => o == some .cl) <| .branch id
(.pop .D (fun s _ => s) <| .push .E (fun _ => Sym.cl) <| .goto fun _ => .walk p true)
(.pop .D (fun _ o => o == some (.lit true)) <| .push .E (fun s => Sym.lit s) <|
if f then .goto fun s => .cmp p s
else .push .O (fun _ => false) <| .goto fun _ => .mvN p false)
| .cmp p q => cmpB .A .D .X .B Sym.bit? Sym.bit? Sym.bit Sym.bit (.cmp p q) (.res p (p == q))
(.res p true)
| .res p b => .push .O (fun _ => b) <| .goto fun _ => .rsA p
| .rsA p => moveB .X .A Sym.bit? Sym.bit (.rsA p) (.rsD p)
| .rsD p => moveB .B .D Sym.bit? Sym.bit (.rsD p) (.mvN p true)
| .mvN p f => moveB .D .E Sym.bit? Sym.bit (.mvN p f) (.walk p f)
| .back p => .peek .E (fun _ o => o.isNone) <| .branch id (.goto fun _ => .put p) <|
.peek .E (fun _ o => o == some .cl) <| .branch id
(.pop .E (fun s _ => s) <| .push .D (fun _ => Sym.cl) <| .goto fun _ => .back p) <|
.peek .E (fun _ o => Emit3.isLit o) <| .branch id
(.pop .E (fun _ o => o == some (.lit true)) <| .push .D (fun s => Sym.lit s) <|
.goto fun _ => .back p)
(.pop .E (fun _ o => o == some (.bit true)) <| .push .D (fun s => Sym.bit s) <|
.goto fun _ => .back p)
| .put p => moveB .A .B Sym.bit? Sym.bit (.put p) (.put2 p)
| .put2 p => moveB .B .D Sym.bit? Sym.bit (.put2 p) (.put3 p)
| .put3 p => .push .D (fun _ => Sym.lit p) <| .goto fun _ => .lits
| .fin => .push .O (fun _ => false) <| .goto fun _ => .finN
| .finN => xferE .N .O [true] .finN .fin2
| .fin2 => .push .O (fun _ => false) <| .goto fun _ => .finC
| .finC => xferE .C .O [true] .finC .done
| .done => .haltinductive Lab
| start | lits | nm (p : Bool) | walk (p f : Bool) | cmp (p q : Bool) | res (p b : Bool)
| rsA (p : Bool) | rsD (p : Bool) | mvN (p f : Bool) | back (p : Bool) | put (p : Bool)
| put2 (p : Bool) | put3 (p : Bool) | fin | finN | fin2 | finC | done
deriving DecidableEqCSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:202
@[reducible] def Γ : K → Type
| .O => Bool
| _ => SymCSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:193
def isLit : Option Sym → Bool
| some (.lit _) => true
| _ => falseCSLibExt/Computability/Complexity/Karp/ThreeSatEmit.lean:148
def moveB (a b : K) (d : Γ a → Option Bool) (g : Bool → Γ b) (self next : Λ) :
TM2.Stmt Γ Λ σ :=
.peek a (fun _ o => Flag.tag (isBit d o))
(.branch Flag.untag
(.pop a (fun _ o => Flag.tag (bitOf d o))
(.branch Flag.untag
(.push b (fun _ => g true) (.goto fun _ => self))
(.push b (fun _ => g false) (.goto fun _ => self))))
(.goto fun _ => next))MathlibExt/Computability/TuringMachine/BitOps.lean:86
def Sym.bit? : Sym → Option Bool
| .bit b => some b
| _ => noneCSLibExt/Computability/Complexity/SatVerifierSpec.lean:46
def cmpB (a b ta tb : K) (da : Γ a → Option Bool) (db : Γ b → Option Bool)
(ea : Bool → Γ ta) (eb : Bool → Γ tb) (self eqL neL : Λ) : TM2.Stmt Γ Λ σ :=
.peek a (fun _ o => Flag.tag (isBit da o))
(.branch Flag.untag
(.peek a (fun _ o => Flag.tag (bitOf da o))
(.branch Flag.untag
(.peek b (fun _ o => Flag.tag (decide (o.bind db = some true)))
(.branch Flag.untag
(.pop a (fun s _ => s) (.pop b (fun s _ => s)
(.push ta (fun _ => ea true) (.push tb (fun _ => eb true)
(.goto fun _ => self)))))
(.goto fun _ => neL)))
⋯MathlibExt/Computability/TuringMachine/BitOps.lean:146
def xferE (k o : K) (ys : List (Γ o)) (self next : Λ) : TM2.Stmt Γ Λ σ :=
.pop k (fun _ o => Flag.tag o.isSome)
(.branch Flag.untag (pushList o ys.reverse (.goto fun _ => self)) (.goto fun _ => next))MathlibExt/Computability/TuringMachine/Program.lean:707
Uses 10 · Used by 13
DefinitionStart label of the CLIQUE emitter#✓fully proved
The start label of the CLIQUE emitter machine is its label \(\mathsf{start}\).
def start : Lab := .startinductive Lab
| start | lits | nm (p : Bool) | walk (p f : Bool) | cmp (p q : Bool) | res (p b : Bool)
| rsA (p : Bool) | rsD (p : Bool) | mvN (p f : Bool) | back (p : Bool) | put (p : Bool)
| put2 (p : Bool) | put3 (p : Bool) | fin | finN | fin2 | finC | done
deriving DecidableEqCSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:202
Uses 1 · Used by 2
DefinitionConfiguration stacks of the CLIQUE emitter#✓fully proved
For a token stack \(t\), an output stack \(o\) of bits, stacks \(a\), \(d\), \(e\) of token symbols and natural numbers \(c\) and \(n\), this assigns to each stack of the CLIQUE emitter its contents: the token stack \(T\) holds \(t\), the output stack \(O\) holds \(o\), the name stack \(A\) holds \(a\), the walked-occurrence stack \(D\) holds \(d\), the walk's other stack \(E\) holds \(e\), the clause counter \(C\) holds \(c\) copies of the clause marker, the occurrence counter \(N\) holds \(n\) copies of the clause marker, and the scratch stacks \(B\) and \(X\) are empty.
def st (t : List Sym) (o : List Bool) (a d e : List Sym) (c n : ℕ) : ∀ k, List (Γ k)
| .T => t
| .O => o
| .A => a
| .B => []
| .D => d
| .E => e
| .X => []
| .C => cnt Sym.cl c
| .N => cnt Sym.cl ninductive Sym
| bit (b : Bool) | lit (p : Bool) | cl | val (b : Bool) | dead
deriving DecidableEqCSLibExt/Computability/Complexity/SatVerifierSpec.lean:41
@[reducible] def Γ : K → Type
| .O => Bool
| _ => SymCSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:193
abbrev cnt {α : Type} (u : α) (n : ℕ) : List α := List.replicate n uMathlibExt/Computability/TuringMachine/Program.lean:115
Uses 4 · Used by 13
TheoremCLIQUE emitter: recognizing a standard state#✓fully proved
Let \(S\) assign contents to the stacks of the CLIQUE emitter and let \(c, n \in \mathbb{N}\). If the scratch stacks \(B\) and \(X\) are empty and the counters \(C\) and \(N\) hold exactly \(c\) and \(n\) clause markers, then \(S\) is the standard state whose stacks \(T\), \(O\), \(A\), \(D\), \(E\) hold what they hold in \(S\), whose stacks \(B\) and \(X\) are empty and whose counters \(C\) and \(N\) hold \(c\) and \(n\) clause markers.
theorem st_eq {S : ∀ k, List (Γ k)} {c n : ℕ} (hB : S .B = []) (hX : S .X = [])
(hC : S .C = cnt Sym.cl c) (hN : S .N = cnt Sym.cl n) :
S = st (S .T) (S .O) (S .A) (S .D) (S .E) c n@[reducible] def Γ : K → Type
| .O => Bool
| _ => SymCSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:193
abbrev cnt {α : Type} (u : α) (n : ℕ) : List α := List.replicate n uMathlibExt/Computability/TuringMachine/Program.lean:115
def st (t : List Sym) (o : List Bool) (a d e : List Sym) (c n : ℕ) : ∀ k, List (Γ k)
| .T => t
| .O => o
| .A => a
| .B => []
| .D => d
| .E => e
| .X => []
| .C => cnt Sym.cl c
| .N => cnt Sym.cl nCSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:265
DefinitionTokens moved by the walk#✓fully proved
A symbol is a token of the walk between the stacks \(D\) and \(E\) when it is a name bit, a literal marker or a clause marker; the value symbols and the dead symbol are not.
def isTok : Sym → Bool
| .bit _ | .lit _ | .cl => true
| _ => falseinductive Sym
| bit (b : Bool) | lit (p : Bool) | cl | val (b : Bool) | dead
deriving DecidableEqCSLibExt/Computability/Complexity/SatVerifierSpec.lean:41
Uses 1 · Used by 2
AbbreviationName bits of a variable in the CLIQUE emitter#✓fully proved
For \(x \in \mathbb{N}\), the name of \(x\) is the list of symbols obtained from the binary encoding of \(x\) (least significant bit first, empty for \(x = 0\)) by writing each bit \(b\) as the bit symbol \(\mathrm{bit}(b)\). This is the form in which the stacks \(A\) and \(D\) of the CLIQUE emitter hold variable names.
abbrev name (x : ℕ) : List Sym := (encodeNat x).map Sym.bitinductive Sym
| bit (b : Bool) | lit (p : Bool) | cl | val (b : Bool) | dead
deriving DecidableEqCSLibExt/Computability/Complexity/SatVerifierSpec.lean:41
Uses 1 · Used by 3
TheoremCLIQUE emitter: reading a variable name#✓fully proved
Stacks are listed top first. Let \(p\) be a Boolean, \(x \in \mathbb{N}\) with name \(w\) (its binary encoding written as bit symbols) of length \(\ell\), and \(R\) a list of symbols that is empty or whose top symbol is not a bit symbol. Let \(v\) be a flag, \(o\) a list of Booleans, \(d\) and \(e\) lists of symbols, and \(c, n \in \mathbb{N}\). Started at label \(\mathrm{nm}(p)\) with flag \(v\), the token stack \(T\) holding \(w\) reversed on top of \(R\), empty stacks \(A\), \(B\), \(X\), stacks \(O\), \(D\), \(E\) holding \(o\), \(d\), \(e\), and \(c\) and \(n\) clause markers on the counters \(C\) and \(N\), the CLIQUE emitter reaches, in exactly \(\ell + 1\) steps and with some flag, the label \(\mathrm{walk}(p, \mathrm{false})\) with \(T\) holding \(R\), \(A\) holding \(w\), and all other stacks as before.
theorem nm_run (p : Bool) (x : ℕ) (R : List Sym) (hR : R.head?.bind Sym.bit? = none) :
∃ v', Run prog ((encodeNat x).length + 1)
⟨some (.nm p), v, st ((name x).reverse ++ R) o [] d e c n⟩
⟨some (.walk p false), v', st R o (name x) d e c n⟩inductive Sym
| bit (b : Bool) | lit (p : Bool) | cl | val (b : Bool) | dead
deriving DecidableEqCSLibExt/Computability/Complexity/SatVerifierSpec.lean:41
def Sym.bit? : Sym → Option Bool
| .bit b => some b
| _ => noneCSLibExt/Computability/Complexity/SatVerifierSpec.lean:46
def Run (n : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
(flip bind (TM2.step M))^[n] (some c) = some dMathlibExt/Computability/TuringMachine/Program.lean:84
def prog : Lab → TM2.Stmt Γ Lab Bool
| .start => .peek .T (fun _ o => o.isNone) <| .branch id (.goto fun _ => .fin) <|
.pop .T (fun s _ => s) <| .push .D (fun _ => Sym.cl) <| .push .C (fun _ => Sym.cl) <|
.goto fun _ => .lits
| .lits => .peek .T (fun _ o => Emit3.isLit o) <| .branch id
(.pop .T (fun _ o => o == some (.lit true)) <| .push .N (fun _ => Sym.cl) <|
.goto fun s => .nm s)
(.goto fun _ => .start)
| .nm p => moveB .T .A Sym.bit? Sym.bit (.nm p) (.walk p false)
| .walk p f => .peek .D (fun _ o => o.isNone) <| .branch id (.goto fun _ => .back p) <|
.peek .D (fun _ o => o == some .cl) <| .branch id
(.pop .D (fun s _ => s) <| .push .E (fun _ => Sym.cl) <| .goto fun _ => .walk p true)
⋯CSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:220
def st (t : List Sym) (o : List Bool) (a d e : List Sym) (c n : ℕ) : ∀ k, List (Γ k)
| .T => t
| .O => o
| .A => a
| .B => []
| .D => d
| .E => e
| .X => []
| .C => cnt Sym.cl c
| .N => cnt Sym.cl nCSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:265
abbrev name (x : ℕ) : List Sym := (encodeNat x).map Sym.bitCSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:401
Uses 12 · Used by 1
TheoremMoving a walked name from \(D\) to \(E\)#✓fully proved
Write \(\langle \ell, v \mid t, o, a, d, e, c, n\rangle\) for the configuration of the SAT-to-CLIQUE emitter at label \(\ell\) with local bit \(v\), stacks \(T = t\), \(O = o\), \(A = a\), \(D = d\), \(E = e\), empty scratch stacks \(B\) and \(X\), and \(c\) and \(n\) marks on the counters \(C\) and \(N\); juxtaposition of lists is concatenation. Let \(p, f\) be bits, \(w\) a list of bits with \(\bar w\) the corresponding list of name-bit symbols, \(R\) a list of symbols that is empty or does not start with a name-bit symbol, and \(t, o, a, e, c, n, v\) arbitrary. Then for some bit \(v'\) the machine goes in exactly \(|w| + 1\) steps from \(\langle \mathsf{mvN}(p, f), v \mid t, o, a, \bar w R, e, c, n\rangle\) to \(\langle \mathsf{walk}(p, f), v' \mid t, o, a, R, \bar w^{\mathrm{rev}} e, c, n\rangle\), where \(\bar w^{\mathrm{rev}}\) is the reverse of \(\bar w\).
theorem mvN_run (p f : Bool) (w : List Bool) (R : List Sym) (hR : R.head?.bind Sym.bit? = none) :
∃ v', Run prog (w.length + 1) ⟨some (.mvN p f), v, st t o a (w.map Sym.bit ++ R) e c n⟩
⟨some (.walk p f), v', st t o a R ((w.map Sym.bit).reverse ++ e) c n⟩inductive Sym
| bit (b : Bool) | lit (p : Bool) | cl | val (b : Bool) | dead
deriving DecidableEqCSLibExt/Computability/Complexity/SatVerifierSpec.lean:41
def Sym.bit? : Sym → Option Bool
| .bit b => some b
| _ => noneCSLibExt/Computability/Complexity/SatVerifierSpec.lean:46
def Run (n : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
(flip bind (TM2.step M))^[n] (some c) = some dMathlibExt/Computability/TuringMachine/Program.lean:84
def prog : Lab → TM2.Stmt Γ Lab Bool
| .start => .peek .T (fun _ o => o.isNone) <| .branch id (.goto fun _ => .fin) <|
.pop .T (fun s _ => s) <| .push .D (fun _ => Sym.cl) <| .push .C (fun _ => Sym.cl) <|
.goto fun _ => .lits
| .lits => .peek .T (fun _ o => Emit3.isLit o) <| .branch id
(.pop .T (fun _ o => o == some (.lit true)) <| .push .N (fun _ => Sym.cl) <|
.goto fun s => .nm s)
(.goto fun _ => .start)
| .nm p => moveB .T .A Sym.bit? Sym.bit (.nm p) (.walk p false)
| .walk p f => .peek .D (fun _ o => o.isNone) <| .branch id (.goto fun _ => .back p) <|
.peek .D (fun _ o => o == some .cl) <| .branch id
(.pop .D (fun s _ => s) <| .push .E (fun _ => Sym.cl) <| .goto fun _ => .walk p true)
⋯CSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:220
def st (t : List Sym) (o : List Bool) (a d e : List Sym) (c n : ℕ) : ∀ k, List (Γ k)
| .T => t
| .O => o
| .A => a
| .B => []
| .D => d
| .E => e
| .X => []
| .C => cnt Sym.cl c
| .N => cnt Sym.cl nCSLibExt/Computability/Complexity/Karp/CliqueEmit.lean:265
Uses 11 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.