Dense CNF encoding of SAT
AbbreviationDense clause#✓fully proved
A clause is a finite list of slots, where slot \(j\) records how the variable \(x_j\) occurs: the slot is either empty (the variable is absent) or holds a Boolean \(b\), meaning the literal \(x_j = b\); so \(b\) true gives \(x_j\) and \(b\) false gives \(\lnot x_j\).
Used by 79
AbbreviationDense CNF formula#✓fully proved
A CNF formula is a finite list of dense clauses, read as the conjunction of its clauses.
abbrev CNF := List Clauseabbrev Clause := List (Option Bool)CSLibExt/Computability/Complexity/DenseSAT.lean:56
Uses 1 · Used by 64
DefinitionSatisfaction of a dense clause#✓fully proved
A finite bit sequence \(a = (a_0, \dots, a_{n-1})\) satisfies a clause \(c\) when there are an index \(j\) and a Boolean \(b\) such that slot \(j\) of \(c\) holds the literal \(x_j = b\), \(j < n\), and \(a_j = b\). Variables \(x_j\) with \(j \ge n\) are unassigned and satisfy no literal.
def clauseSat (c : Clause) (a : List Bool) : Prop :=
∃ (j : ℕ) (b : Bool), c[j]? = some (some b) ∧ a[j]? = some babbrev Clause := List (Option Bool)CSLibExt/Computability/Complexity/DenseSAT.lean:56
Uses 1 · Used by 15
DefinitionSatisfaction of a dense CNF formula#✓fully proved
A finite bit sequence \(a\) satisfies a CNF formula \(\varphi\) when \(a\) satisfies every clause of \(\varphi\).
def cnfSat (φ : CNF) (a : List Bool) : Prop :=
∀ c ∈ φ, clauseSat c aabbrev CNF := List ClauseCSLibExt/Computability/Complexity/DenseSAT.lean:59
def clauseSat (c : Clause) (a : List Bool) : Prop :=
∃ (j : ℕ) (b : Bool), c[j]? = some (some b) ∧ a[j]? = some bCSLibExt/Computability/Complexity/DenseSAT.lean:63
Uses 3 · Used by 50
DefinitionDense decoding with an accumulator#✓fully proved
Given a bit string \(w\) and the list \(c\) of slots read so far for the current clause, stored in reverse order, the result is the CNF formula obtained by reading \(w\) two bits at a time: \(00\) outputs the current clause in reading order and continues with no slots read; \(01\) adds an empty slot to the current clause; and \(1s\), for a bit \(s\), adds a slot holding the Boolean \(\lnot s\), so \(10\) adds a positive and \(11\) a negative literal. When fewer than two bits remain, decoding stops and outputs no further clauses, so a trailing unterminated clause and a dangling odd bit are ignored and decoding is total.
def decodeAux : List Bool → Clause → CNF
| false :: false :: r, cur => cur.reverse :: decodeAux r []
| false :: true :: r, cur => decodeAux r (none :: cur)
| true :: s :: r, cur => decodeAux r (some (!s) :: cur)
| _, _ => []abbrev Clause := List (Option Bool)CSLibExt/Computability/Complexity/DenseSAT.lean:56
abbrev CNF := List ClauseCSLibExt/Computability/Complexity/DenseSAT.lean:59
Uses 2 · Used by 4
DefinitionDense decoding of CNF formulas#✓fully proved
The CNF formula decoded from a bit string \(w\) is the result of the accumulator decoding of \(w\) started with no slots read for the current clause: \(w\) is read two bits at a time, \(00\) ends a clause, \(01\) is an empty slot, \(10\) a positive and \(11\) a negative literal, and a trailing unterminated clause and a dangling odd bit are ignored.
def decodeCNF (w : List Bool) : CNF := decodeAux w []abbrev CNF := List ClauseCSLibExt/Computability/Complexity/DenseSAT.lean:59
def decodeAux : List Bool → Clause → CNF
| false :: false :: r, cur => cur.reverse :: decodeAux r []
| false :: true :: r, cur => decodeAux r (none :: cur)
| true :: s :: r, cur => decodeAux r (some (!s) :: cur)
| _, _ => []CSLibExt/Computability/Complexity/DenseSAT.lean:72
Uses 2 · Used by 6
DefinitionTwo-bit code of a slot#✓fully proved
Slot \(j\) of a dense clause is empty (variable \(x_j\) is absent), holds the positive literal \(x_j\), or holds the negative literal \(\neg x_j\). Its code is \(01\) when empty, \(10\) for the positive literal and \(11\) for the negative literal.
Used by 22
DefinitionDense encoding of a clause#✓fully proved
The bit string encoding a clause is the concatenation of the two-bit codes of its slots, in order (empty slot \(01\), positive literal \(10\), negative literal \(11\)), followed by the terminator \(00\).
def encodeClause (c : Clause) : List Bool := c.flatMap encodeSlot ++ [false, false]abbrev Clause := List (Option Bool)CSLibExt/Computability/Complexity/DenseSAT.lean:56
def encodeSlot : Option Bool → List Bool
| none => [false, true]
| some b => [true, !b]CSLibExt/Computability/Complexity/DenseSAT.lean:82
Uses 2 · Used by 32
DefinitionDense encoding of a CNF formula#✓fully proved
The dense encoding of a CNF formula \(\varphi\) is the bit string obtained by concatenating, in order, the encodings of the clauses of \(\varphi\), where a clause is encoded as the two-bit codes of its slots followed by the terminator \(00\).
def encodeCNF (φ : CNF) : List Bool := φ.flatMap encodeClauseabbrev CNF := List ClauseCSLibExt/Computability/Complexity/DenseSAT.lean:59
def encodeClause (c : Clause) : List Bool := c.flatMap encodeSlot ++ [false, false]CSLibExt/Computability/Complexity/DenseSAT.lean:87
Uses 3 · Used by 34
TheoremDecoding inverts the dense encoding#✓fully proved
For every CNF formula \(\varphi\), decoding the bit string that encodes \(\varphi\) gives back \(\varphi\). In particular, every CNF formula is the decoding of some bit string.
theorem decodeCNF_encodeCNF (φ : CNF) : decodeCNF (encodeCNF φ) = φabbrev CNF := List ClauseCSLibExt/Computability/Complexity/DenseSAT.lean:59
def decodeCNF (w : List Bool) : CNF := decodeAux w []CSLibExt/Computability/Complexity/DenseSAT.lean:79
def encodeCNF (φ : CNF) : List Bool := φ.flatMap encodeClauseCSLibExt/Computability/Complexity/DenseSAT.lean:90
Uses 7 · Used by 2
DefinitionDense CNF-SAT#✓fully proved
A bit string \(w\) belongs to dense CNF-SAT when the CNF formula obtained by decoding \(w\) in the dense clause encoding is satisfiable, that is, some assignment (a list of booleans) satisfies every clause of the decoded formula.
def SAT (w : List Bool) : Prop := ∃ a : List Bool, cnfSat (decodeCNF w) adef cnfSat (φ : CNF) (a : List Bool) : Prop :=
∀ c ∈ φ, clauseSat c aCSLibExt/Computability/Complexity/DenseSAT.lean:67
def decodeCNF (w : List Bool) : CNF := decodeAux w []CSLibExt/Computability/Complexity/DenseSAT.lean:79
Uses 2 · Used by 6
DefinitionSingle-pass evaluation of a dense CNF encoding#✓fully proved
The scan \(E(r, u, v, f)\) takes the formula bits \(r\) still to be read, the assignment bits \(u\) not yet used by the current clause, the bits \(v\) already used by it (most recent first) and a boolean \(f\) recording whether the current clause is already satisfied; write \(x u'\) for the list with first bit \(x\) followed by the list \(u'\). It reads \(r\) two bits at a time; let \(r'\) be the bits after the pair read. On \(00\) (end of clause) the result is \(f \wedge E(r', \overline{v}\,u, [\,], \mathrm{false})\), where \(\overline{v}\,u\) is the reversal of \(v\) followed by \(u\). On \(01\) (an empty slot) the result is \(E(r', u', x v, f)\) when \(u = x u'\), and \(E(r', [\,], v, f)\) when \(u\) is empty. On \(1s\) (a literal with sign bit \(s\)) the result is \(E(r', u', x v, f \vee (x = \neg s))\) when \(u = x u'\), and \(E(r', [\,], v, f)\) when \(u\) is empty. When fewer than two bits remain, the result is true.
The scan mirrors the verifier machine step by step.
def evalCNF : List Bool → List Bool → List Bool → Bool → Bool
| false :: false :: r, bs, as, fl => fl && evalCNF r (as.reverse ++ bs) [] false
| false :: true :: r, [], as, fl => evalCNF r [] as fl
| false :: true :: r, x :: bs, as, fl => evalCNF r bs (x :: as) fl
| true :: _ :: r, [], as, fl => evalCNF r [] as fl
| true :: s :: r, x :: bs, as, fl => evalCNF r bs (x :: as) (fl || x == !s)
| _, _, _, _ => trueDefinitionIndexed evaluation of a dense CNF encoding#✓fully proved
The scan \(I(r, a, j, f)\) takes the formula bits \(r\) still to be read, an assignment \(a\) (a list of booleans), the position \(j\) of the next slot in the current clause and a boolean \(f\) recording whether the current clause is already satisfied. It reads \(r\) two bits at a time; let \(r'\) be the bits after the pair read. On \(00\) (end of clause) the result is \(f \wedge I(r', a, 0, \mathrm{false})\). On \(01\) (an empty slot) the result is \(I(r', a, j + 1, f)\). On \(1s\) (a literal with sign bit \(s\)) the result is \(I(r', a, j + 1, f')\), where \(f'\) is true when \(f\) is true, or when \(j < |a|\) and the entry \(a_j\) of \(a\) (counting from \(0\)) equals \(\neg s\). When fewer than two bits remain, the result is true.
def evalIdx : List Bool → List Bool → ℕ → Bool → Bool
| false :: false :: r, a, _, fl => fl && evalIdx r a 0 false
| false :: true :: r, a, j, fl => evalIdx r a (j + 1) fl
| true :: s :: r, a, j, fl => evalIdx r a (j + 1) (fl || a[j]? == some (!s))
| _, _, _, _ => trueUsed by 1
DefinitionDense CNF-SAT certificate check#✓fully proved
For bit strings \(w\) (the encoded formula) and \(y\) (the certificate), the check of \(y\) against \(w\) is the Boolean result of the verifier's left-to-right scan of the formula bits \(w\), started with \(y\) as the assignment bits not yet used by the current clause, no used bits, and the current clause not yet satisfied.
def check (w y : List Bool) : Bool := evalCNF w y [] falsedef evalCNF : List Bool → List Bool → List Bool → Bool → Bool
| false :: false :: r, bs, as, fl => fl && evalCNF r (as.reverse ++ bs) [] false
| false :: true :: r, [], as, fl => evalCNF r [] as fl
| false :: true :: r, x :: bs, as, fl => evalCNF r bs (x :: as) fl
| true :: _ :: r, [], as, fl => evalCNF r [] as fl
| true :: s :: r, x :: bs, as, fl => evalCNF r bs (x :: as) (fl || x == !s)
| _, _, _, _ => trueCSLibExt/Computability/Complexity/DenseSAT.lean:118
TheoremDecoded clauses are no longer than the input#✓fully proved
For every bit string \(r\) and every clause \(c_0\), every clause produced by the auxiliary decoder run on \(r\) with accumulated partial clause \(c_0\) has length at most \(|c_0| + |r|\).
theorem length_le_of_mem_decodeAux (r : List Bool) (cur : Clause) :
∀ c ∈ decodeAux r cur, c.length ≤ cur.length + r.lengthabbrev Clause := List (Option Bool)CSLibExt/Computability/Complexity/DenseSAT.lean:56
def decodeAux : List Bool → Clause → CNF
| false :: false :: r, cur => cur.reverse :: decodeAux r []
| false :: true :: r, cur => decodeAux r (none :: cur)
| true :: s :: r, cur => decodeAux r (some (!s) :: cur)
| _, _ => []CSLibExt/Computability/Complexity/DenseSAT.lean:72
Uses 3 · Used by 1
TheoremTruncating a satisfying assignment#✓fully proved
Let \(w\) be a bit string and \(\varphi\) the CNF formula decoded from \(w\). If a finite bit sequence \(a\) satisfies \(\varphi\), then so does the prefix of \(a\) of length \(|w|\) (all of \(a\) when \(a\) has at most \(|w|\) bits).
theorem cnfSat_take (w a : List Bool) (h : cnfSat (decodeCNF w) a) :
cnfSat (decodeCNF w) (a.take w.length)def cnfSat (φ : CNF) (a : List Bool) : Prop :=
∀ c ∈ φ, clauseSat c aCSLibExt/Computability/Complexity/DenseSAT.lean:67
def decodeCNF (w : List Bool) : CNF := decodeAux w []CSLibExt/Computability/Complexity/DenseSAT.lean:79
Uses 6 · Used by 1
TheoremCertificate characterization of dense CNF-SAT#✓fully proved
A bit string \(w\) belongs to dense CNF-SAT if and only if there is a bit string \(y\) with \(|y| \le |w|\) that the certificate check accepts on formula bits \(w\) and assignment bits \(y\).
theorem sat_iff_check (w : List Bool) :
SAT w ↔ ∃ y : List Bool, y.length ≤ w.length ^ 1 ∧ check w y = truedef SAT (w : List Bool) : Prop := ∃ a : List Bool, cnfSat (decodeCNF w) aCSLibExt/Computability/Complexity/DenseSAT.lean:111
def check (w y : List Bool) : Bool := evalCNF w y [] falseCSLibExt/Computability/Complexity/DenseSAT.lean:223
Uses 11 · Used by 1
InductiveWork stacks of the dense CNF-SAT verifier#✓fully proved
The verifier has four work stacks: the input stack, a stack \(F\) that stashes the formula, and two stacks \(A\) and \(B\) for the assignment.
inductive W | inp | F | A | B
deriving DecidableEqUsed by 14
AbbreviationWork alphabet of the dense-SAT verifier#✓fully proved
The work alphabet \(G\) is the disjoint union of the Booleans and the optional Booleans. Its elements are the left symbols \(\mathrm{inl}(b)\) and the right symbols \(\mathrm{inr}(o)\), where \(b\) is a Boolean and \(o\) is either \(\mathrm{some}\ b\) or \(\mathrm{none}\). This is the alphabet of the pair encoding, in which \(\mathrm{inr}(\mathrm{none})\) is the separator \(\#\).
Formula and assignment bits are stored on the work stacks as left symbols \(\mathrm{inl}(b)\).
Used by 61
TM2 SAT verifier · Reading a bit of \(w\) · Reading a bit of \(x\) · The verifier host embeds the component · Verifier host, canonical form · Verifier host · Verifier host program · The verifier host's run · The verifier host machineDefinitionPair encoding \(w \# y\)#✓fully proved
For bit strings \(w\) and \(y\), the word over the pair alphabet \(G = \mathrm{Bool} \oplus \mathrm{Option}\,\mathrm{Bool}\) consisting of the bits \(b\) of \(w\) in order, each tagged on the left as \(\mathrm{inl}\,b\), then the separator \(\# = \mathrm{inr}\,\mathrm{none}\), then the bits \(b\) of \(y\) in order, each tagged on the right as \(\mathrm{inr}(\mathrm{some}\,b)\). This is the input of the dense CNF-SAT verifier.
def pairEncode (p : List Bool × List Bool) : List G :=
p.1.map Sum.inl ++ Sum.inr none :: p.2.map fun b => Sum.inr (some b)abbrev G := Bool ⊕ Option BoolCSLibExt/Computability/Complexity/DenseSATVerifier.lean:67
Uses 1 · Used by 28
TM2 SAT verifier · Verifier host, canonical form · Verifier host · The verifier host's runDefinitionStack alphabets of the dense CNF-SAT verifier#✓fully proved
The stacks of the verifier are the output stack and one stack for each work stack name (input, formula stash \(F\), assignment stacks \(A\) and \(B\)). The output stack has the Booleans as alphabet, and every work stack has the alphabet \(G\), the disjoint union of the Booleans and the Booleans extended by a separator \(\#\).
@[reducible] def Γ : Option W → Type
| none => Bool
| some _ => Ginductive W | inp | F | A | B
deriving DecidableEqCSLibExt/Computability/Complexity/DenseSATVerifier.lean:59
abbrev G := Bool ⊕ Option BoolCSLibExt/Computability/Complexity/DenseSATVerifier.lean:67
Uses 2 · Used by 11
InductiveLabels of the dense-SAT verifier#✓fully proved
The labels of the verifier's program are \(\mathrm{read1}\), \(\mathrm{read2}\), \(\mathrm{back1}\) and \(\mathrm{back2}\); \(\mathrm{c0}(f)\) and \(\mathrm{c1}(f, b)\) for Booleans \(f\) and \(b\); \(\mathrm{adv}(f, o)\) for a Boolean \(f\) and an optional Boolean \(o\); \(\mathrm{restore}(f)\) for a Boolean \(f\); and \(\mathrm{drainI}(a)\), \(\mathrm{drainA}(a)\), \(\mathrm{drainB}(a)\) and \(\mathrm{finish}(a)\) for a Boolean \(a\). There are finitely many labels, and equality of labels is decidable.
The labels \(\mathrm{c0}(f)\) and \(\mathrm{c1}(f, b)\) read the two bits of a token, with \(f\) recording whether the current clause is already satisfied. \(\mathrm{adv}(f, o)\) moves one assignment bit from stack \(B\) to stack \(A\) (\(o = \mathrm{some}\ s\) for the literal token \(1s\)), and \(\mathrm{restore}(f)\) moves the used assignment bits back from \(A\) to \(B\).
inductive Lab
| read1 | read2 | back1 | back2
| c0 (fl : Bool) | c1 (fl b : Bool) | adv (fl : Bool) (o : Option Bool) | restore (fl : Bool)
| drainI (ans : Bool) | drainA (ans : Bool) | drainB (ans : Bool) | finish (ans : Bool)
deriving DecidableEq, FintypeUsed by 10
AbbreviationMachine states of the verifier#✓fully proved
The machine state of the dense CNF-SAT verifier is an element of \(\mathrm{Option}\,G\): either nothing or a work symbol in \(G\).
The program uses it to hold the last popped symbol.
abbrev St := Option Gabbrev G := Bool ⊕ Option BoolCSLibExt/Computability/Complexity/DenseSATVerifier.lean:67
Uses 1 · Used by 10
AbbreviationStatements of the dense CNF-SAT verifier#✓fully proved
The statements of the verifier are the statements of Mathlib's multi-stack Turing machine model with stack alphabets \(\Gamma\), labels in the verifier's label type and machine states in \(\mathrm{Option}\,G\).
abbrev Stmt := TM2.Stmt Γ Lab St@[reducible] def Γ : Option W → Type
| none => Bool
| some _ => GCSLibExt/Computability/Complexity/DenseSATVerifier.lean:75
inductive Lab
| read1 | read2 | back1 | back2
| c0 (fl : Bool) | c1 (fl b : Bool) | adv (fl : Bool) (o : Option Bool) | restore (fl : Bool)
| drainI (ans : Bool) | drainA (ans : Bool) | drainB (ans : Bool) | finish (ans : Bool)
deriving DecidableEq, FintypeCSLibExt/Computability/Complexity/DenseSATVerifier.lean:82
abbrev St := Option GCSLibExt/Computability/Complexity/DenseSATVerifier.lean:89
Uses 4 · Used by 6
AbbreviationConfigurations of the dense-SAT verifier#✓fully proved
A configuration of the verifier is a configuration of the multi-stack Turing machine model with the verifier's labels, states and stack alphabets. It consists of an optional current label (absent once the machine has halted), a state, which is either a symbol of the work alphabet \(G\) or nothing, and for each stack the list of symbols on it: Booleans on the output stack and symbols of \(G\) on each of the four work stacks.
abbrev Cfg := TM2.Cfg Γ Lab St@[reducible] def Γ : Option W → Type
| none => Bool
| some _ => GCSLibExt/Computability/Complexity/DenseSATVerifier.lean:75
inductive Lab
| read1 | read2 | back1 | back2
| c0 (fl : Bool) | c1 (fl b : Bool) | adv (fl : Bool) (o : Option Bool) | restore (fl : Bool)
| drainI (ans : Bool) | drainA (ans : Bool) | drainB (ans : Bool) | finish (ans : Bool)
deriving DecidableEq, FintypeCSLibExt/Computability/Complexity/DenseSATVerifier.lean:82
abbrev St := Option GCSLibExt/Computability/Complexity/DenseSATVerifier.lean:89
DefinitionGeneric copy loop of the dense-SAT verifier#✓fully proved
For a work stack \(s\), a partial map \(g\) on the work alphabet \(G\), an optional target work stack \(t\), and labels \(\ell\) (the loop's own label) and \(\ell'\) (its exit), the generic loop is the program statement that does the following. It pops the top of \(s\) and stores the popped symbol \(x\) as the machine state (nothing if \(s\) is empty). If \(x\) exists and \(g(x) = y\) is defined, it pushes \(y\) onto \(t\) (or pushes nothing when there is no target stack) and jumps to \(\ell\). Otherwise, when \(s\) was empty or \(g\) is undefined at \(x\), it jumps to \(\ell'\).
def loop (s : W) (g : G → Option G) (t : Option W) (self next : Lab) : Stmt :=
.pop (some s) (fun _ o => o) <|
.branch (fun v => (v.bind g).isSome)
(match t with
| some t => .push (some t) (fun v => (v.bind g).getD (.inl false)) (.goto fun _ => self)
| none => .goto fun _ => self)
(.goto fun _ => next)inductive W | inp | F | A | B
deriving DecidableEqCSLibExt/Computability/Complexity/DenseSATVerifier.lean:59
abbrev G := Bool ⊕ Option BoolCSLibExt/Computability/Complexity/DenseSATVerifier.lean:67
inductive Lab
| read1 | read2 | back1 | back2
| c0 (fl : Bool) | c1 (fl b : Bool) | adv (fl : Bool) (o : Option Bool) | restore (fl : Bool)
| drainI (ans : Bool) | drainA (ans : Bool) | drainB (ans : Bool) | finish (ans : Bool)
deriving DecidableEq, FintypeCSLibExt/Computability/Complexity/DenseSATVerifier.lean:82
abbrev Stmt := TM2.Stmt Γ Lab StCSLibExt/Computability/Complexity/DenseSATVerifier.lean:92
DefinitionFormula filter of the dense-SAT verifier#✓fully proved
The partial map on the work alphabet \(G\) that sends each left symbol \(\mathrm{inl}(b)\) to itself and is undefined on every right symbol \(\mathrm{inr}(o)\), including the separator \(\mathrm{inr}(\mathrm{none})\), written \(\#\).
The verifier's first copying loop uses it, so on the pair encoding of a formula and a certificate it stops at the separator \(\#\).
def gRead1 : G → Option G
| .inl b => some (.inl b)
| .inr _ => noneabbrev G := Bool ⊕ Option BoolCSLibExt/Computability/Complexity/DenseSATVerifier.lean:67
Uses 1 · Used by 2
DefinitionCertificate filter of the dense-SAT verifier#✓fully proved
The partial map on the work alphabet \(G\) that sends each right symbol \(\mathrm{inr}(\mathrm{some}\ b)\) to the left symbol \(\mathrm{inl}(b)\) and is undefined on every other symbol, that is on the left symbols and on the separator \(\mathrm{inr}(\mathrm{none})\).
def gRead2 : G → Option G
| .inr (some b) => some (.inl b)
| _ => noneabbrev G := Bool ⊕ Option BoolCSLibExt/Computability/Complexity/DenseSATVerifier.lean:67
Uses 1 · Used by 2
DefinitionThe dense CNF-SAT verifier program#✓fully proved
The program assigns a statement to each label. Every pop stores the popped symbol, or nothing if the stack was empty, as the machine state.
- \(\mathsf{read1}\): pop the input stack; while the popped symbol is some \(\mathrm{inl}\,b\), push \(\mathrm{inl}\,b\) onto \(F\) and pop again; otherwise go to \(\mathsf{read2}\).
- \(\mathsf{read2}\): pop the input stack; while the popped symbol is some \(\mathrm{inr}(\mathrm{some}\,b)\), push \(\mathrm{inl}\,b\) onto \(A\) and pop again; otherwise go to \(\mathsf{back1}\).
- \(\mathsf{back1}\): pop \(F\) and push each popped symbol onto the input stack until \(F\) is empty, then go to \(\mathsf{back2}\).
- \(\mathsf{back2}\): pop \(A\) and push each popped symbol onto \(B\) until \(A\) is empty, then go to \(\mathsf{c0}(\mathrm{false})\).
- \(\mathsf{c0}(fl)\): pop the input stack; if the popped symbol is \(\mathrm{inl}\,b\), go to \(\mathsf{c1}(fl, b)\), otherwise go to \(\mathsf{drainI}(\mathrm{true})\).
- \(\mathsf{c1}(fl, \mathrm{false})\): pop the input stack; on \(\mathrm{inl}\,\mathrm{false}\) go to \(\mathsf{restore}(fl)\), on \(\mathrm{inl}\,\mathrm{true}\) go to \(\mathsf{adv}(fl, \mathrm{none})\), otherwise go to \(\mathsf{drainI}(\mathrm{true})\).
- \(\mathsf{c1}(fl, \mathrm{true})\): pop the input stack; on \(\mathrm{inl}\,s\) go to \(\mathsf{adv}(fl, \mathrm{some}\,s)\), otherwise go to \(\mathsf{drainI}(\mathrm{true})\).
- \(\mathsf{adv}(fl, o)\): pop \(B\); if a symbol \(x\) was popped, push \(x\) onto \(A\) and go to \(\mathsf{c0}(fl')\), where \(fl'\) is true when \(fl\) is true, or when \(o = \mathrm{some}\,s\) for a bit \(s\) with \(x = \mathrm{inl}(\lnot s)\); if \(B\) was empty, go to \(\mathsf{c0}(fl)\).
- \(\mathsf{restore}(fl)\): pop \(A\) and push each popped symbol onto \(B\) until \(A\) is empty, then go to \(\mathsf{c0}(\mathrm{false})\) if \(fl\) is true and to \(\mathsf{drainI}(\mathrm{false})\) otherwise.
- \(\mathsf{drainI}(ans)\), \(\mathsf{drainA}(ans)\), \(\mathsf{drainB}(ans)\): pop and discard the input stack, \(A\), \(B\) respectively until it is empty, then go to \(\mathsf{drainA}(ans)\), \(\mathsf{drainB}(ans)\), \(\mathsf{finish}(ans)\) respectively.
- \(\mathsf{finish}(ans)\): push \(ans\) onto the output stack, clear the machine state and halt.
Cslib.Complexity.DenseSAT.Verifier.prog · 25 lines
def prog : Lab → Stmt
| .read1 => loop .inp gRead1 (some .F) .read1 .read2
| .read2 => loop .inp gRead2 (some .A) .read2 .back1
| .back1 => loop .F some (some .inp) .back1 .back2
| .back2 => loop .A some (some .B) .back2 (.c0 false)
| .c0 fl => .pop (some .inp) (fun _ o => o) <| .goto fun v => match v with
| some (.inl b) => .c1 fl b
| _ => .drainI true
| .c1 fl false => .pop (some .inp) (fun _ o => o) <| .goto fun v => match v with
| some (.inl false) => .restore fl
| some (.inl true) => .adv fl none
| _ => .drainI true
| .c1 fl true => .pop (some .inp) (fun _ o => o) <| .goto fun v => match v with
| some (.inl s) => .adv fl (some s)
| _ => .drainI true
| .adv fl o => .pop (some .B) (fun _ o => o) <|
.branch (fun v => v.isSome)
(.push (some .A) (fun v => v.getD (.inl false)) <|
.goto fun v => .c0 (fl || decide (v = o.map fun s => .inl (!s))))
(.goto fun _ => .c0 fl)
| .restore fl => loop .A some (some .B) (.restore fl) (if fl then .c0 false else .drainI false)
| .drainI ans => loop .inp some none (.drainI ans) (.drainA ans)
| .drainA ans => loop .A some none (.drainA ans) (.drainB ans)
| .drainB ans => loop .B some none (.drainB ans) (.finish ans)
| .finish ans => .push none (fun _ => ans) <| .load (fun _ => none) .haltinductive Lab
| read1 | read2 | back1 | back2
| c0 (fl : Bool) | c1 (fl b : Bool) | adv (fl : Bool) (o : Option Bool) | restore (fl : Bool)
| drainI (ans : Bool) | drainA (ans : Bool) | drainB (ans : Bool) | finish (ans : Bool)
deriving DecidableEq, FintypeCSLibExt/Computability/Complexity/DenseSATVerifier.lean:82
abbrev Stmt := TM2.Stmt Γ Lab StCSLibExt/Computability/Complexity/DenseSATVerifier.lean:92
def loop (s : W) (g : G → Option G) (t : Option W) (self next : Lab) : Stmt :=
.pop (some s) (fun _ o => o) <|
.branch (fun v => (v.bind g).isSome)
(match t with
| some t => .push (some t) (fun v => (v.bind g).getD (.inl false)) (.goto fun _ => self)
| none => .goto fun _ => self)
(.goto fun _ => next)CSLibExt/Computability/Complexity/DenseSATVerifier.lean:98
def gRead1 : G → Option G
| .inl b => some (.inl b)
| .inr _ => noneCSLibExt/Computability/Complexity/DenseSATVerifier.lean:107
def gRead2 : G → Option G
| .inr (some b) => some (.inl b)
| _ => noneCSLibExt/Computability/Complexity/DenseSATVerifier.lean:112
Uses 9 · Used by 6
DefinitionThe dense CNF-SAT verifier machine#✓fully proved
The finite multi-stack Turing machine with an output stack over the Booleans and four work stacks (the input stack, a formula stash \(F\) and two assignment stacks \(A\) and \(B\)) over the alphabet \(G\), the disjoint union of the Booleans and the Booleans extended by a separator \(\#\). It reads its input from the input stack, writes its result to the output stack, starts at the first label of the verifier program with empty internal state, and runs that program: on input \(w \# y\) it moves the formula bits \(w\) onto \(F\) and the assignment bits \(y\) onto \(A\), moves them back so that \(w\) is on the input stack and \(y\) on \(B\), then scans \(w\) clause by clause, moving assignment bits from \(B\) to \(A\) to test the literals of a clause and back from \(A\) to \(B\) at the end of the clause, and finally empties the work stacks and pushes the computed bit onto the output stack.
def tm : FinTM2 where
K := Option W
k₀ := some .inp
k₁ := none
Γ := Γ
Λ := Lab
main := .read1
σ := St
initialState := none
Γk₀Fin := (inferInstance : Fintype G)
m := proginductive W | inp | F | A | B
deriving DecidableEqCSLibExt/Computability/Complexity/DenseSATVerifier.lean:59
@[reducible] def Γ : Option W → Type
| none => Bool
| some _ => GCSLibExt/Computability/Complexity/DenseSATVerifier.lean:75
inductive Lab
| read1 | read2 | back1 | back2
| c0 (fl : Bool) | c1 (fl b : Bool) | adv (fl : Bool) (o : Option Bool) | restore (fl : Bool)
| drainI (ans : Bool) | drainA (ans : Bool) | drainB (ans : Bool) | finish (ans : Bool)
deriving DecidableEq, FintypeCSLibExt/Computability/Complexity/DenseSATVerifier.lean:82
abbrev St := Option GCSLibExt/Computability/Complexity/DenseSATVerifier.lean:89
abbrev G := Bool ⊕ Option BoolCSLibExt/Computability/Complexity/DenseSATVerifier.lean:67
def prog : Lab → Stmt
| .read1 => loop .inp gRead1 (some .F) .read1 .read2
| .read2 => loop .inp gRead2 (some .A) .read2 .back1
| .back1 => loop .F some (some .inp) .back1 .back2
| .back2 => loop .A some (some .B) .back2 (.c0 false)
| .c0 fl => .pop (some .inp) (fun _ o => o) <| .goto fun v => match v with
| some (.inl b) => .c1 fl b
| _ => .drainI true
| .c1 fl false => .pop (some .inp) (fun _ o => o) <| .goto fun v => match v with
| some (.inl false) => .restore fl
| some (.inl true) => .adv fl none
| _ => .drainI true
⋯CSLibExt/Computability/Complexity/DenseSATVerifier.lean:117
DefinitionAll stacks of the verifier from work stacks and output#✓fully proved
Given work-stack contents \(V\) (a list \(V(s)\) of work symbols for each work stack \(s\)) and a list \(o\) of bits, the stack contents of the verifier that give the output stack \(o\) and each work stack \(s\) the list \(V(s)\).
def stk (V : W → List G) (o : List Bool) : ∀ k, List (Γ k)
| none => o
| some w => V winductive W | inp | F | A | B
deriving DecidableEqCSLibExt/Computability/Complexity/DenseSATVerifier.lean:59
abbrev G := Bool ⊕ Option BoolCSLibExt/Computability/Complexity/DenseSATVerifier.lean:67
@[reducible] def Γ : Option W → Type
| none => Bool
| some _ => GCSLibExt/Computability/Complexity/DenseSATVerifier.lean:75
Uses 3 · Used by 5
DefinitionWork stacks from four lists#✓fully proved
Given four lists \(i\), \(f\), \(a\), \(b\) of work symbols in \(G\), the contents of the verifier's work stacks in which the input stack holds \(i\), the formula stash \(F\) holds \(f\), and the assignment stacks \(A\) and \(B\) hold \(a\) and \(b\).
DefinitionPushing a list onto a verifier work stack#✓fully proved
Given an optional work stack \(t\), a list \(ys\) of work symbols and work-stack contents \(V\) (a list \(V(s)\) of symbols for each work stack \(s\)), the contents obtained by pushing the elements of \(ys\) one at a time onto \(t\): if \(t\) is a work stack, \(V(t)\) is replaced by the reverse of \(ys\) followed by \(V(t)\) and every other stack is unchanged; if \(t\) is none, the result is \(V\).
def pushAll : Option W → List G → (W → List G) → W → List G
| none, _, V => V
| some t, ys, V => update V t (ys.reverse ++ V t)inductive W | inp | F | A | B
deriving DecidableEqCSLibExt/Computability/Complexity/DenseSATVerifier.lean:59
abbrev G := Bool ⊕ Option BoolCSLibExt/Computability/Complexity/DenseSATVerifier.lean:67
TheoremRunning the generic copy loop of the dense-SAT verifier#✓fully proved
Let \(s\) be a work stack, \(g\) a partial map on the work alphabet \(G\), \(t\) an optional target work stack other than \(s\), and \(\ell\), \(\ell'\) labels such that the verifier's program at \(\ell\) is the generic loop with source \(s\), map \(g\), target \(t\), own label \(\ell\) and exit \(\ell'\). Let \(o\) be a list of output bits. Let \(x = x_1 \dots x_n\), \(y = y_1 \dots y_n\) and \(r\) be lists of symbols of \(G\) with \(g(x_j) = y_j\) defined for every \(j\), and with \(r\) empty or \(g\) undefined at the first symbol of \(r\). Let \(V\) be work-stack contents with \(V(s) = x r\), and let \(v\) be any state. Started at \(\ell\) in state \(v\) with work stacks \(V\) and output stack \(o\), the program runs for exactly \(n + 1\) steps and reaches the label \(\ell'\). Its state is then the first symbol of \(r\) (nothing if \(r\) is empty) and its output stack is still \(o\). Its work stacks are obtained from \(V\) by replacing stack \(s\) with \(r\) minus its first symbol (empty if \(r\) is empty) and then, if \(t\) is a stack, pushing \(y_1, \dots, y_n\) onto \(t\) one at a time.
theorem loop_run (s : W) (g : G → Option G) (t : Option W) (self next : Lab)
(hp : prog self = loop s g t self next) (hst : t ≠ some s) (o : List Bool) :
∀ (xs ys rest : List G) (v : St) (V : W → List G),
xs.map g = ys.map some → rest.head?.bind g = none → V s = xs ++ rest →
TM2Program.Run prog (xs.length + 1) ⟨some self, v, stk V o⟩
⟨some next, rest.head?, stk (pushAll t ys (update V s rest.tail)) o⟩inductive W | inp | F | A | B
deriving DecidableEqCSLibExt/Computability/Complexity/DenseSATVerifier.lean:59
abbrev G := Bool ⊕ Option BoolCSLibExt/Computability/Complexity/DenseSATVerifier.lean:67
inductive Lab
| read1 | read2 | back1 | back2
| c0 (fl : Bool) | c1 (fl b : Bool) | adv (fl : Bool) (o : Option Bool) | restore (fl : Bool)
| drainI (ans : Bool) | drainA (ans : Bool) | drainB (ans : Bool) | finish (ans : Bool)
deriving DecidableEq, FintypeCSLibExt/Computability/Complexity/DenseSATVerifier.lean:82
def prog : Lab → Stmt
| .read1 => loop .inp gRead1 (some .F) .read1 .read2
| .read2 => loop .inp gRead2 (some .A) .read2 .back1
| .back1 => loop .F some (some .inp) .back1 .back2
| .back2 => loop .A some (some .B) .back2 (.c0 false)
| .c0 fl => .pop (some .inp) (fun _ o => o) <| .goto fun v => match v with
| some (.inl b) => .c1 fl b
| _ => .drainI true
| .c1 fl false => .pop (some .inp) (fun _ o => o) <| .goto fun v => match v with
| some (.inl false) => .restore fl
| some (.inl true) => .adv fl none
| _ => .drainI true
⋯CSLibExt/Computability/Complexity/DenseSATVerifier.lean:117
def loop (s : W) (g : G → Option G) (t : Option W) (self next : Lab) : Stmt :=
.pop (some s) (fun _ o => o) <|
.branch (fun v => (v.bind g).isSome)
(match t with
| some t => .push (some t) (fun v => (v.bind g).getD (.inl false)) (.goto fun _ => self)
| none => .goto fun _ => self)
(.goto fun _ => next)CSLibExt/Computability/Complexity/DenseSATVerifier.lean:98
abbrev St := Option GCSLibExt/Computability/Complexity/DenseSATVerifier.lean:89
def Run (n : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
(flip bind (TM2.step M))^[n] (some c) = some dMathlibExt/Computability/TuringMachine/Program.lean:84
def stk (V : W → List G) (o : List Bool) : ∀ k, List (Γ k)
| none => o
| some w => V wCSLibExt/Computability/Complexity/DenseSATVerifier.lean:159
def pushAll : Option W → List G → (W → List G) → W → List G
| none, _, V => V
| some t, ys, V => update V t (ys.reverse ++ V t)CSLibExt/Computability/Complexity/DenseSATVerifier.lean:201
Uses 11 · Used by 3
TheoremDraining the work stacks of the dense-SAT verifier#✓fully proved
Let \(\mathit{ans}\) be a Boolean, let \(i\), \(a\), \(b\) be lists of symbols of the work alphabet \(G\), and let \(v\) be any state. Start the verifier's program at the label \(\mathrm{drainI}(\mathit{ans})\) in state \(v\), with the input stack holding \(i\), the formula stash empty, the assignment stacks \(A\) and \(B\) holding \(a\) and \(b\), and the output stack empty. It then runs for exactly \(|i| + |a| + |b| + 3\) steps and reaches the label \(\mathrm{finish}(\mathit{ans})\) with no symbol in its state, all four work stacks empty and the output stack still empty.
theorem drain_run (ans : Bool) (i a b : List G) (v : St) :
TM2Program.Run prog (i.length + a.length + b.length + 3)
⟨some (.drainI ans), v, stk (mkV i [] a b) []⟩
⟨some (.finish ans), none, stk (mkV [] [] [] []) []⟩abbrev G := Bool ⊕ Option BoolCSLibExt/Computability/Complexity/DenseSATVerifier.lean:67
abbrev St := Option GCSLibExt/Computability/Complexity/DenseSATVerifier.lean:89
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 → Stmt
| .read1 => loop .inp gRead1 (some .F) .read1 .read2
| .read2 => loop .inp gRead2 (some .A) .read2 .back1
| .back1 => loop .F some (some .inp) .back1 .back2
| .back2 => loop .A some (some .B) .back2 (.c0 false)
| .c0 fl => .pop (some .inp) (fun _ o => o) <| .goto fun v => match v with
| some (.inl b) => .c1 fl b
| _ => .drainI true
| .c1 fl false => .pop (some .inp) (fun _ o => o) <| .goto fun v => match v with
| some (.inl false) => .restore fl
| some (.inl true) => .adv fl none
| _ => .drainI true
⋯CSLibExt/Computability/Complexity/DenseSATVerifier.lean:117
def stk (V : W → List G) (o : List Bool) : ∀ k, List (Γ k)
| none => o
| some w => V wCSLibExt/Computability/Complexity/DenseSATVerifier.lean:159
def mkV (i f a b : List G) : W → List G
| .inp => i
| .F => f
| .A => a
| .B => bCSLibExt/Computability/Complexity/DenseSATVerifier.lean:181
Uses 12 · Used by 1
DefinitionLeft-tagged encoding of a bit list#✓fully proved
For a list \(l\) of bits, its encoding on a work stack of the dense-SAT verifier is the list of symbols of the work alphabet \(G\) obtained by replacing each bit \(b\) of \(l\) with the left symbol \(\mathrm{inl}(b)\).
def enc (l : List Bool) : List G := l.map Sum.inlabbrev G := Bool ⊕ Option BoolCSLibExt/Computability/Complexity/DenseSATVerifier.lean:67
Uses 1 · Used by 3
DefinitionStep count of the verifier's main scan#✓fully proved
The number \(T(r, bs, as, fl) \in \mathbb{N}\), for bit strings \(r\), \(bs\), \(as\) and a flag \(fl\), is defined by recursion on \(r\), where \(0\) is false and \(1\) is true, juxtaposition denotes concatenation (so \(b\,r\) is \(r\) with the bit \(b\) prepended), \([\,]\) is the empty string, \(\mathrm{rev}\) reverses a string and \(|\cdot|\) is length:
- \(T(0\,0\,r, bs, as, fl) = |as| + 3 + T(r, \mathrm{rev}(as)\,bs, [\,], \mathrm{false})\) if \(fl\) is true, and \(|as| + 3 + (|r| + (|as| + |bs|) + 3)\) otherwise;
- \(T(0\,1\,r, [\,], as, fl) = 3 + T(r, [\,], as, fl)\);
- \(T(0\,1\,r, x\,bs, as, fl) = 3 + T(r, bs, x\,as, fl)\);
- \(T(1\,s\,r, [\,], as, fl) = 3 + T(r, [\,], as, fl)\);
- \(T(1\,s\,r, x\,bs, as, fl) = 3 + T(r, bs, x\,as, fl \lor (x = \lnot s))\);
- \(T(r, bs, as, fl) = |r| + |as| + |bs| + 4\) when \(r\) has fewer than two bits.
The recursion mirrors the dense CNF evaluation scan.
def T : List Bool → List Bool → List Bool → Bool → ℕ
| false :: false :: r, bs, as, fl =>
as.length + 3 +
if fl then T r (as.reverse ++ bs) [] false else r.length + (as.length + bs.length) + 3
| false :: true :: r, [], as, fl => 3 + T r [] as fl
| false :: true :: r, x :: bs, as, fl => 3 + T r bs (x :: as) fl
| true :: _ :: r, [], as, fl => 3 + T r [] as fl
| true :: s :: r, x :: bs, as, fl => 3 + T r bs (x :: as) (fl || x == !s)
| r, bs, as, _ => r.length + as.length + bs.length + 4TheoremThe verifier's main scan#✓fully proved
For all bit strings \(r\), \(bs\), \(as\), every flag \(fl\) and every machine state \(v\), the verifier program leads in exactly \(T(r, bs, as, fl)\) steps from the configuration at label \(\mathsf{c0}(fl)\) with machine state \(v\), the input stack holding the bits of \(r\), the stack \(A\) holding the bits of \(as\) and the stack \(B\) holding the bits of \(bs\) (each bit \(b\) stored as \(\mathrm{inl}\,b\), from the top in order), and the stack \(F\) and the output stack empty, to the configuration at label \(\mathsf{finish}(\operatorname{evalCNF}(r, bs, as, fl))\) with empty machine state and all stacks empty.
theorem scan (r bs as : List Bool) (fl : Bool) (v : St) :
TM2Program.Run prog (T r bs as fl) ⟨some (.c0 fl), v, stk (mkV (enc r) [] (enc as) (enc bs)) []⟩
⟨some (.finish (evalCNF r bs as fl)), none, stk (mkV [] [] [] []) []⟩abbrev St := Option GCSLibExt/Computability/Complexity/DenseSATVerifier.lean:89
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 → Stmt
| .read1 => loop .inp gRead1 (some .F) .read1 .read2
| .read2 => loop .inp gRead2 (some .A) .read2 .back1
| .back1 => loop .F some (some .inp) .back1 .back2
| .back2 => loop .A some (some .B) .back2 (.c0 false)
| .c0 fl => .pop (some .inp) (fun _ o => o) <| .goto fun v => match v with
| some (.inl b) => .c1 fl b
| _ => .drainI true
| .c1 fl false => .pop (some .inp) (fun _ o => o) <| .goto fun v => match v with
| some (.inl false) => .restore fl
| some (.inl true) => .adv fl none
| _ => .drainI true
⋯CSLibExt/Computability/Complexity/DenseSATVerifier.lean:117
def T : List Bool → List Bool → List Bool → Bool → ℕ
| false :: false :: r, bs, as, fl =>
as.length + 3 +
if fl then T r (as.reverse ++ bs) [] false else r.length + (as.length + bs.length) + 3
| false :: true :: r, [], as, fl => 3 + T r [] as fl
| false :: true :: r, x :: bs, as, fl => 3 + T r bs (x :: as) fl
| true :: _ :: r, [], as, fl => 3 + T r [] as fl
| true :: s :: r, x :: bs, as, fl => 3 + T r bs (x :: as) (fl || x == !s)
| r, bs, as, _ => r.length + as.length + bs.length + 4CSLibExt/Computability/Complexity/DenseSATVerifier.lean:363
def stk (V : W → List G) (o : List Bool) : ∀ k, List (Γ k)
| none => o
| some w => V wCSLibExt/Computability/Complexity/DenseSATVerifier.lean:159
def mkV (i f a b : List G) : W → List G
| .inp => i
| .F => f
| .A => a
| .B => bCSLibExt/Computability/Complexity/DenseSATVerifier.lean:181
def enc (l : List Bool) : List G := l.map Sum.inlCSLibExt/Computability/Complexity/DenseSATVerifier.lean:287
def evalCNF : List Bool → List Bool → List Bool → Bool → Bool
| false :: false :: r, bs, as, fl => fl && evalCNF r (as.reverse ++ bs) [] false
| false :: true :: r, [], as, fl => evalCNF r [] as fl
| false :: true :: r, x :: bs, as, fl => evalCNF r bs (x :: as) fl
| true :: _ :: r, [], as, fl => evalCNF r [] as fl
| true :: s :: r, x :: bs, as, fl => evalCNF r bs (x :: as) (fl || x == !s)
| _, _, _, _ => trueCSLibExt/Computability/Complexity/DenseSAT.lean:118
Uses 16 · Used by 1
DefinitionRight-tagged encoding of a certificate#✓fully proved
For a list \(y\) of bits, its right-tagged encoding is the list of symbols of the work alphabet \(G\) obtained by replacing each bit \(b\) of \(y\) with the right symbol \(\mathrm{inr}(\mathrm{some}\ b)\). This is how the certificate appears after the separator in the pair encoding of a formula and a certificate.
def encR (y : List Bool) : List G := y.map fun b => .inr (some b)abbrev G := Bool ⊕ Option BoolCSLibExt/Computability/Complexity/DenseSATVerifier.lean:67
Uses 1 · Used by 2
TheoremSplitting the verifier input#✓fully proved
For all bit strings \(w\) and \(y\), the verifier program leads in exactly \((|w| + 1) + (|y| + 1) + (|w| + 1) + (|y| + 1)\) steps from the configuration at label \(\mathsf{read1}\) with empty machine state, the input stack holding (from the top) the bits \(b\) of \(w\) as \(\mathrm{inl}\,b\), the separator \(\mathrm{inr}\,\mathrm{none}\) and the bits \(b\) of \(y\) as \(\mathrm{inr}(\mathrm{some}\,b)\), and all other stacks empty, to the configuration at label \(\mathsf{c0}(\mathrm{false})\) with empty machine state, the input stack holding the bits \(b\) of \(w\) as \(\mathrm{inl}\,b\), the stack \(B\) holding the bits \(b\) of \(y\) as \(\mathrm{inl}\,b\) (both from the top in order), and the stacks \(F\), \(A\) and the output stack empty.
The four phases stash \(w\) on \(F\) and \(y\) on \(A\), then move them back onto the input stack and \(B\).
theorem prefix_run (w y : List Bool) :
TM2Program.Run prog (w.length + 1 + (y.length + 1) + (w.length + 1) + (y.length + 1))
⟨some .read1, none, stk (mkV (enc w ++ .inr none :: encR y) [] [] []) []⟩
⟨some (.c0 false), none, stk (mkV (enc w) [] [] (enc y)) []⟩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 → Stmt
| .read1 => loop .inp gRead1 (some .F) .read1 .read2
| .read2 => loop .inp gRead2 (some .A) .read2 .back1
| .back1 => loop .F some (some .inp) .back1 .back2
| .back2 => loop .A some (some .B) .back2 (.c0 false)
| .c0 fl => .pop (some .inp) (fun _ o => o) <| .goto fun v => match v with
| some (.inl b) => .c1 fl b
| _ => .drainI true
| .c1 fl false => .pop (some .inp) (fun _ o => o) <| .goto fun v => match v with
| some (.inl false) => .restore fl
| some (.inl true) => .adv fl none
| _ => .drainI true
⋯CSLibExt/Computability/Complexity/DenseSATVerifier.lean:117
def stk (V : W → List G) (o : List Bool) : ∀ k, List (Γ k)
| none => o
| some w => V wCSLibExt/Computability/Complexity/DenseSATVerifier.lean:159
def mkV (i f a b : List G) : W → List G
| .inp => i
| .F => f
| .A => a
| .B => bCSLibExt/Computability/Complexity/DenseSATVerifier.lean:181
def enc (l : List Bool) : List G := l.map Sum.inlCSLibExt/Computability/Complexity/DenseSATVerifier.lean:287
def encR (y : List Bool) : List G := y.map fun b => .inr (some b)CSLibExt/Computability/Complexity/DenseSATVerifier.lean:472
Uses 16 · Used by 1
DefinitionStep count of the dense CNF-SAT verifier#✓fully proved
For bit lists \(w\) (a formula) and \(y\) (an assignment), the number \((|w| + 1) + (|y| + 1) + (|w| + 1) + (|y| + 1) + T + 1\), where \(T\) is the step count of the main scan on \(w\) started with all of \(y\) unused, no assignment bits used and the clause flag false.
This is the exact number of steps of the verifier machine on input \(w \# y\): four passes that stash and restore \(w\) and \(y\), the main scan, and one output step.
def totalSteps (w y : List Bool) : ℕ :=
w.length + 1 + (y.length + 1) + (w.length + 1) + (y.length + 1) + T w y [] false + 1def T : List Bool → List Bool → List Bool → Bool → ℕ
| false :: false :: r, bs, as, fl =>
as.length + 3 +
if fl then T r (as.reverse ++ bs) [] false else r.length + (as.length + bs.length) + 3
| false :: true :: r, [], as, fl => 3 + T r [] as fl
| false :: true :: r, x :: bs, as, fl => 3 + T r bs (x :: as) fl
| true :: _ :: r, [], as, fl => 3 + T r [] as fl
| true :: s :: r, x :: bs, as, fl => 3 + T r bs (x :: as) (fl || x == !s)
| r, bs, as, _ => r.length + as.length + bs.length + 4CSLibExt/Computability/Complexity/DenseSATVerifier.lean:363
Uses 1 · Used by 1
DefinitionTime bound of the dense CNF-SAT verifier#✓fully proved
The polynomial \(2(n + 5)^2\) over \(\mathbb{N}\) in one variable \(n\). It bounds the running time of the verifier on inputs of length \(n\); for a formula \(w\) and an assignment \(y\), the input \(w \# y\) has length \(n = |w| + 1 + |y|\).
noncomputable def time : Polynomial ℕ :=
Polynomial.C 2 * (Polynomial.X + Polynomial.C 5) ^ 2Used by 1
DefinitionPolynomial-time verifier for dense CNF-SAT#✓fully proved
The verifier machine computes, in polynomial time, the map sending a pair \((w, y)\) of bit lists to the Boolean \(\mathrm{check}(w, y)\), which is true exactly when \(y\) satisfies the CNF formula decoded from \(w\). The pair is given as the input \(w \# y\) (the bits of \(w\), a separator \(\#\), then the bits of \(y\)), the output is the single bit \(\mathrm{check}(w, y)\), and the machine halts within \(2(n + 5)^2\) steps on an input of length \(n\).
Cslib.Complexity.DenseSAT.Verifier.verifier · 26 lines
noncomputable def verifier :
TM2ComputableInPolyTime pairEncode (fun b : Bool => [b]) (fun p => check p.1 p.2) where
tm := tm
inputAlphabet := Equiv.refl G
outputAlphabet := Equiv.refl Bool
time := time
outputsFun := fun p => by
obtain ⟨w, y⟩ := p
have hin : List.map (Equiv.refl G).invFun (pairEncode (w, y)) =
enc w ++ .inr none :: encR y := by
simp [pairEncode, enc, encR]
have hlen : (pairEncode (w, y)).length = w.length + 1 + y.length := by
simp only [pairEncode, List.length_append, List.length_map, List.length_cons]
omega
have hrun := ((prefix_run w y).trans (scan w y [] false none)).trans (finish_run (check w y))
unfold TM2OutputsInTime
refine { steps := totalSteps w y, evals_in_steps := ?_, steps_le_m := ?_ }
· change (flip bind (TM2.step prog))^[_] (some (initList tm _)) =
Option.map (haltList tm) (some _)
erw [hin, initList_tm, Option.map_some, haltList_tm]
exact hrun
· rw [hlen, totalSteps]
have hT := T_le w y [] false
simp only [time, Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_pow,
Polynomial.eval_add, Polynomial.eval_X, List.length_nil] at hT ⊢
nlinarithdef pairEncode (p : List Bool × List Bool) : List G :=
p.1.map Sum.inl ++ Sum.inr none :: p.2.map fun b => Sum.inr (some b)CSLibExt/Computability/Complexity/DenseSATVerifier.lean:71
def check (w y : List Bool) : Bool := evalCNF w y [] falseCSLibExt/Computability/Complexity/DenseSAT.lean:223
def tm : FinTM2 where
K := Option W
k₀ := some .inp
k₁ := none
Γ := Γ
Λ := Lab
main := .read1
σ := St
initialState := none
Γk₀Fin := (inferInstance : Fintype G)
m := progCSLibExt/Computability/Complexity/DenseSATVerifier.lean:144
abbrev G := Bool ⊕ Option BoolCSLibExt/Computability/Complexity/DenseSATVerifier.lean:67
noncomputable def time : Polynomial ℕ :=
Polynomial.C 2 * (Polynomial.X + Polynomial.C 5) ^ 2CSLibExt/Computability/Complexity/DenseSATVerifier.lean:517
Uses 20 · Used by 1
DefinitionDense CNF-SAT as a decision problem#✓fully proved
The decision problem of dense CNF-SAT accepts a bit string \(w\) exactly when \(w\) belongs to dense CNF-SAT, that is, when the formula decoded from \(w\) in the dense clause encoding has a satisfying assignment.
noncomputable def denseSatDec : DecisionProblem := fun w => decide (SAT w)abbrev DecisionProblem := List Bool → BoolMathlibExt/Computability/Complexity.lean:170
def SAT (w : List Bool) : Prop := ∃ a : List Bool, cnfSat (decodeCNF w) aCSLibExt/Computability/Complexity/DenseSAT.lean:111
Uses 2 · Used by 3
TheoremThe dense certificate check runs in polynomial time#✓fully proved
The map sending a pair \((w, y)\) of bit strings to the result of the certificate check on formula bits \(w\) and assignment bits \(y\) is polynomial-time computable, where pairs of bit strings carry their canonical bitstring encoding.
theorem isPolyTime_check : IsPolyTime (fun p : List Bool × List Bool => check p.1 p.2)def IsPolyTime {α β : Type} [BitstringEncoding α] [BitstringEncoding β]
(f : α → β) : Prop :=
IsPolyTimeWithEncoding (BitstringEncoding.toEncoding (α := α))
(BitstringEncoding.toEncoding (α := β)) fMathlibExt/Computability/Complexity.lean:186
def check (w y : List Bool) : Bool := evalCNF w y [] falseCSLibExt/Computability/Complexity/DenseSAT.lean:223
Uses 15 · Used by 1
TheoremDense CNF-SAT is in NP#✓fully proved
Dense CNF-SAT is in NP.
theorem denseSatDec_mem_NP : denseSatDec ∈ NPnoncomputable def denseSatDec : DecisionProblem := fun w => decide (SAT w)CSLibExt/Computability/Complexity/DenseSATInNP.lean:37
def NP : DecisionComplexityClass :=
{ L | ∃ (p : Polynomial ℕ), ∃ R : (List Bool × List Bool) → Bool,
IsPolyTime R ∧
∀ x, L x ↔ ∃ w : List Bool, w.length ≤ p.eval x.length ∧ R (x, w) }MathlibExt/Computability/Complexity.lean:200
Uses 17 · Used by 1
TheoremThe binary code of \(2^k - 1\)#✓fully proved
For every natural number \(k\), the binary code of \(2^k - 1\) (Mathlib's encoding of natural numbers as bit lists, least significant bit first) is the list of \(k\) ones.
theorem encodeNat_two_pow_sub_one (k : ℕ) : encodeNat (2 ^ k - 1) = List.replicate k trueUsed by 1
TheoremSelf-delimiting code of a block of ones#✓fully proved
For every \(k \in \mathbb{N}\), the self-delimiting form of the bit string of \(k\) ones is \(k\) copies of \(11\) followed by a single \(0\).
theorem delimit_replicate (k : ℕ) :
BitstringEncoding.delimit (List.replicate k true) =
TM2Program.rep [true, true] k ++ [false]def delimit : List Bool → List Bool
| [] => [false]
| b :: l => true :: b :: delimit lMathlibExt/Computability/Complexity.lean:68
def rep {α : Type} (ys : List α) (n : ℕ) : List α := (List.replicate n ys).flattenMathlibExt/Computability/TuringMachine/Program.lean:682
Uses 2 · Used by 1
TheoremBinary codes of literals on variables one less than a power of two#✓fully proved
For every \(k \in \mathbb{N}\) and every truth value \(b\), the binary code of the literal of polarity \(b\) on variable \(2^k - 1\) is \(k\) copies of \(11\), followed by \(0\), followed by the bit \(b\).
theorem encodeLit_two_pow (k : ℕ) (b : Bool) :
Cslib.CookLevin.encodeLit (2 ^ k - 1, b) = TM2Program.rep [true, true] k ++ [false, b]def encodeLit (l : Nat × Bool) : List Bool :=
encodeNatPrefix l.1 ++ [l.2]CSLibExt/Computability/CookLevin.lean:63
def rep {α : Type} (ys : List α) (n : ℕ) : List α := (List.replicate n ys).flattenMathlibExt/Computability/TuringMachine/Program.lean:682
Uses 6 · Used by 1
DefinitionBinary-index translation of a dense clause#✓fully proved
Let \(k_0 \in \mathbb{N}\) and let \(c\) be a dense clause with slots \(s_0, \dots, s_{L-1}\). Its binary-index translation with offset \(k_0\) is the clause that has, for each slot \(j\) holding a literal of polarity \(b\), the literal of polarity \(b\) on variable \(2^{k_0 + L - 1 - j} - 1\), listed in increasing order of \(j\); absent slots contribute no literal.
def binClause (k₀ : ℕ) : Clause → Cslib.CookLevin.CNFClause
| [] => []
| none :: c => binClause k₀ c
| some b :: c => (2 ^ (k₀ + c.length) - 1, b) :: binClause k₀ cabbrev Clause := List (Option Bool)CSLibExt/Computability/Complexity/DenseSAT.lean:56
Uses 2 · Used by 6
DefinitionBinary-index translation of a dense formula#✓fully proved
The translation of a dense CNF formula \(\varphi\) replaces each clause \(c\) of \(\varphi\), keeping their order, by its binary-index translation with offset \(0\): if \(c\) has length \(L\), each slot \(j\) of \(c\) holding a literal of polarity \(b\) becomes the literal of polarity \(b\) on variable \(2^{L - 1 - j} - 1\), and absent slots are dropped.
def binCNF (φ : CNF) : Cslib.CookLevin.CNF := φ.map (binClause 0)abbrev CNF := List ClauseCSLibExt/Computability/Complexity/DenseSAT.lean:59
def binClause (k₀ : ℕ) : Clause → Cslib.CookLevin.CNFClause
| [] => []
| none :: c => binClause k₀ c
| some b :: c => (2 ^ (k₀ + c.length) - 1, b) :: binClause k₀ cCSLibExt/Computability/Complexity/DenseToBinary.lean:90
Uses 5 · Used by 3
TheoremThe binary-index translation preserves satisfiability when all clauses have equal length#✓fully proved
Let \(\varphi\) be a dense CNF formula all of whose clauses have the same length \(V\). Then the binary-index translation of \(\varphi\) is satisfiable (some assignment of truth values to the variables satisfies every clause) if and only if some finite list of truth values satisfies \(\varphi\).
theorem cnfSat_binCNF_iff {φ : CNF} {V : ℕ} (hV : ∀ c ∈ φ, c.length = V) :
Cslib.CookLevin.CNFSat (binCNF φ) ↔ ∃ a, cnfSat φ aabbrev CNF := List ClauseCSLibExt/Computability/Complexity/DenseSAT.lean:59
def binCNF (φ : CNF) : Cslib.CookLevin.CNF := φ.map (binClause 0)CSLibExt/Computability/Complexity/DenseToBinary.lean:96
def cnfSat (φ : CNF) (a : List Bool) : Prop :=
∀ c ∈ φ, clauseSat c aCSLibExt/Computability/Complexity/DenseSAT.lean:67
Uses 9 · Used by 1
DefinitionClosing a clause in the translated output#✓fully proved
For a natural number \(n\) and a bit string \(o\), closing a clause with \(n\) literals in front of \(o\) gives the bit string consisting of \(n\) ones, then a zero, then \(o\); that is, the unary count of \(n\) is prepended to \(o\).
In the translation, \(o\) starts with the codes of the clause's \(n\) literals, already emitted.
Used by 7
DefinitionThe dense-to-binary translation on the reversed bit string#✓fully proved
The function \(\mathrm{conv}(w, \iota, n, k, m, o)\) consumes the bit string \(w\) two bits at a time and prepends to the output bit string \(o\). The truth value \(\iota\) records whether a clause is open, \(n\) counts the literals of the open clause, \(k\) counts slots and \(m\) counts clauses. Juxtaposition of bit strings is concatenation, \(1^n\) is \(n\) ones, \((11)^k\) is \(k\) copies of \(11\), \(\bar s\) is the negation of a bit \(s\), and \(C\) is \(1^n 0\, o\) if \(\iota\) is true and \(o\) otherwise. For every bit \(s\) and bit string \(r\):
- \(\mathrm{conv}(00\, r, \iota, n, k, m, o) = \mathrm{conv}(r, \mathrm{true}, 0, 0, m + 1, C)\);
- \(\mathrm{conv}(10\, r, \iota, n, k, m, o) = \mathrm{conv}(r, \iota, n, k + 1, m, o)\);
- \(\mathrm{conv}(s1\, r, \iota, n, k, m, o)\) is \(\mathrm{conv}(r, \mathrm{true}, n + 1, k + 1, m, (11)^k 0 \bar s\, o)\) if \(\iota\) is true and \(\mathrm{conv}(r, \mathrm{false}, n, k, m, o)\) otherwise;
- if \(w\) has fewer than two bits, \(\mathrm{conv}(w, \iota, n, k, m, o) = 1^m 0\, C\).
On the reversed dense encoding a slot \(s_1 s_2\) is read as \(s_2 s_1\): \(00\) is a terminator, which closes the open clause and opens the next, \(10\) is an absent slot, and \(s1\) is a present slot, whose literal \((2^k - 1, \bar s)\) is emitted (its binary code is \((11)^k 0 \bar s\)) inside a clause and skipped outside one. At the end the open clause is closed and the unary clause count is emitted.
def conv : List Bool → Bool → ℕ → ℕ → ℕ → List Bool → List Bool
| false :: false :: r, ins, n, _, m, o =>
conv r true 0 0 (m + 1) (if ins then endClause n o else o)
| true :: false :: r, ins, n, k, m, o => conv r ins n (k + 1) m o
| s :: true :: r, ins, n, k, m, o =>
if ins then conv r true (n + 1) (k + 1) m (TM2Program.rep [true,
true] k ++ false :: (!s) :: o)
else conv r false n k m o
| _, ins, n, _, m, o => List.replicate m true ++ false :: (if ins then endClause n o else o)def endClause (n : ℕ) (o : List Bool) : List Bool := List.replicate n true ++ false :: oCSLibExt/Computability/Complexity/DenseToBinary.lean:161
def rep {α : Type} (ys : List α) (n : ℕ) : List α := (List.replicate n ys).flattenMathlibExt/Computability/TuringMachine/Program.lean:682
Uses 2 · Used by 6
TheoremThe translation on the slots of a clause#✓fully proved
Write \(\mathrm{conv}(w, \iota, n, k, m, o)\) for the reversed-string translation run on the bit string \(w\) with open-clause flag \(\iota\), literal count \(n\), slot count \(k\), clause count \(m\) and output \(o\); juxtaposition of bit strings is concatenation, \(w^R\) is the reversal of \(w\) and \(|x|\) is the length of a list \(x\). Let \(c\) be a dense clause, \(r\) and \(o\) bit strings and \(n, k, m \in \mathbb{N}\). Let \(s(c)\) be the concatenation of the two-bit codes of the slots of \(c\), let \(c'\) be the binary-index translation of \(c\) with offset \(k\), and let \(e\) be the concatenation of the binary codes of the literals of \(c'\). Then \(\mathrm{conv}(s(c)^R r, \mathrm{true}, n, k, m, o) = \mathrm{conv}(r, \mathrm{true}, n + |c'|, k + |c|, m, e\, o)\).
theorem conv_slots (c : Clause) (r : List Bool) (n k m : ℕ) (o : List Bool) :
conv ((c.flatMap encodeSlot).reverse ++ r) true n k m o =
conv r true (n + (binClause k c).length) (k + c.length) m
((binClause k c).flatMap Cslib.CookLevin.encodeLit ++ o)abbrev Clause := List (Option Bool)CSLibExt/Computability/Complexity/DenseSAT.lean:56
def conv : List Bool → Bool → ℕ → ℕ → ℕ → List Bool → List Bool
| false :: false :: r, ins, n, _, m, o =>
conv r true 0 0 (m + 1) (if ins then endClause n o else o)
| true :: false :: r, ins, n, k, m, o => conv r ins n (k + 1) m o
| s :: true :: r, ins, n, k, m, o =>
if ins then conv r true (n + 1) (k + 1) m (TM2Program.rep [true,
true] k ++ false :: (!s) :: o)
else conv r false n k m o
| _, ins, n, _, m, o => List.replicate m true ++ false :: (if ins then endClause n o else o)CSLibExt/Computability/Complexity/DenseToBinary.lean:169
def encodeSlot : Option Bool → List Bool
| none => [false, true]
| some b => [true, !b]CSLibExt/Computability/Complexity/DenseSAT.lean:82
def binClause (k₀ : ℕ) : Clause → Cslib.CookLevin.CNFClause
| [] => []
| none :: c => binClause k₀ c
| some b :: c => (2 ^ (k₀ + c.length) - 1, b) :: binClause k₀ cCSLibExt/Computability/Complexity/DenseToBinary.lean:90
def encodeLit (l : Nat × Bool) : List Bool :=
encodeNatPrefix l.1 ++ [l.2]CSLibExt/Computability/CookLevin.lean:63
Uses 8 · Used by 1
TheoremThe translation on a whole clause#✓fully proved
Write \(\mathrm{conv}(w, \iota, n, k, m, o)\) for the reversed-string translation run on the bit string \(w\) with open-clause flag \(\iota\), literal count \(n\), slot count \(k\), clause count \(m\) and output \(o\); juxtaposition of bit strings is concatenation, \(w^R\) is the reversal of \(w\), \(1^n\) is \(n\) ones and \(|x|\) is the length of a list \(x\). Let \(c\) be a dense clause, \(r\) and \(o\) bit strings, \(\iota\) a truth value and \(n, k, m \in \mathbb{N}\). Let \(E(c)\) be the dense encoding of \(c\) (its slot codes followed by the terminator \(00\)), \(c'\) the binary-index translation of \(c\) with offset \(0\), and \(e\) the concatenation of the binary codes of the literals of \(c'\). Put \(o' = 1^n 0\, o\) if \(\iota\) is true and \(o' = o\) otherwise. Then \(\mathrm{conv}(E(c)^R r, \iota, n, k, m, o) = \mathrm{conv}(r, \mathrm{true}, |c'|, |c|, m + 1, e\, o')\).
theorem conv_clause (c : Clause) (r : List Bool) (ins : Bool) (n k m : ℕ) (o : List Bool) :
conv ((encodeClause c).reverse ++ r) ins n k m o =
conv r true (binClause 0 c).length c.length (m + 1)
((binClause 0 c).flatMap Cslib.CookLevin.encodeLit ++
(if ins then endClause n o else o))abbrev Clause := List (Option Bool)CSLibExt/Computability/Complexity/DenseSAT.lean:56
def conv : List Bool → Bool → ℕ → ℕ → ℕ → List Bool → List Bool
| false :: false :: r, ins, n, _, m, o =>
conv r true 0 0 (m + 1) (if ins then endClause n o else o)
| true :: false :: r, ins, n, k, m, o => conv r ins n (k + 1) m o
| s :: true :: r, ins, n, k, m, o =>
if ins then conv r true (n + 1) (k + 1) m (TM2Program.rep [true,
true] k ++ false :: (!s) :: o)
else conv r false n k m o
| _, ins, n, _, m, o => List.replicate m true ++ false :: (if ins then endClause n o else o)CSLibExt/Computability/Complexity/DenseToBinary.lean:169
def encodeClause (c : Clause) : List Bool := c.flatMap encodeSlot ++ [false, false]CSLibExt/Computability/Complexity/DenseSAT.lean:87
def binClause (k₀ : ℕ) : Clause → Cslib.CookLevin.CNFClause
| [] => []
| none :: c => binClause k₀ c
| some b :: c => (2 ^ (k₀ + c.length) - 1, b) :: binClause k₀ cCSLibExt/Computability/Complexity/DenseToBinary.lean:90
def encodeLit (l : Nat × Bool) : List Bool :=
encodeNatPrefix l.1 ++ [l.2]CSLibExt/Computability/CookLevin.lean:63
def endClause (n : ℕ) (o : List Bool) : List Bool := List.replicate n true ++ false :: oCSLibExt/Computability/Complexity/DenseToBinary.lean:161
TheoremThe translation on the remaining clauses#✓fully proved
Write \(\mathrm{conv}(w, \iota, n, k, m, o)\) for the reversed-string translation run on the bit string \(w\) with open-clause flag \(\iota\), literal count \(n\), slot count \(k\), clause count \(m\) and output \(o\); juxtaposition of bit strings is concatenation, \(w^R\) is the reversal of \(w\), \(1^n\) is \(n\) ones and \(|x|\) is the length of a list \(x\). For a dense clause \(c\), let \(E(c)\) be its dense encoding, \(c'\) its binary-index translation with offset \(0\), \(e(c)\) the concatenation of the binary codes of the literals of \(c'\), and \(B(c)\) the binary code of the clause \(c'\). Let \(p, k, m \in \mathbb{N}\), let \(c_0, c_1, \dots, c_p\) be dense clauses and let \(D\) be a bit string. Then \(\mathrm{conv}(E(c_1)^R \cdots E(c_p)^R, \mathrm{true}, |c_0'|, k, m, e(c_0)\, D) = 1^{m + p} 0\, B(c_p) \cdots B(c_1) B(c_0) D\).
theorem conv_clauses (ψ : List Clause) (c₀ : Clause) (k m : ℕ) (D : List Bool) :
conv (ψ.flatMap fun c => (encodeClause c).reverse) true (binClause 0 c₀).length k m
((binClause 0 c₀).flatMap Cslib.CookLevin.encodeLit ++ D) =
List.replicate (m + ψ.length) true ++ false ::
((ψ.reverse.flatMap fun c => Cslib.CookLevin.encodeClause (binClause 0 c)) ++
Cslib.CookLevin.encodeClause (binClause 0 c₀) ++ D)abbrev Clause := List (Option Bool)CSLibExt/Computability/Complexity/DenseSAT.lean:56
def conv : List Bool → Bool → ℕ → ℕ → ℕ → List Bool → List Bool
| false :: false :: r, ins, n, _, m, o =>
conv r true 0 0 (m + 1) (if ins then endClause n o else o)
| true :: false :: r, ins, n, k, m, o => conv r ins n (k + 1) m o
| s :: true :: r, ins, n, k, m, o =>
if ins then conv r true (n + 1) (k + 1) m (TM2Program.rep [true,
true] k ++ false :: (!s) :: o)
else conv r false n k m o
| _, ins, n, _, m, o => List.replicate m true ++ false :: (if ins then endClause n o else o)CSLibExt/Computability/Complexity/DenseToBinary.lean:169
def encodeClause (c : Clause) : List Bool := c.flatMap encodeSlot ++ [false, false]CSLibExt/Computability/Complexity/DenseSAT.lean:87
def binClause (k₀ : ℕ) : Clause → Cslib.CookLevin.CNFClause
| [] => []
| none :: c => binClause k₀ c
| some b :: c => (2 ^ (k₀ + c.length) - 1, b) :: binClause k₀ cCSLibExt/Computability/Complexity/DenseToBinary.lean:90
def encodeLit (l : Nat × Bool) : List Bool :=
encodeNatPrefix l.1 ++ [l.2]CSLibExt/Computability/CookLevin.lean:63
def encodeClause (C : CNFClause) : List Bool :=
List.replicate C.length true ++ false :: C.flatMap encodeLitCSLibExt/Computability/CookLevin.lean:82
Uses 9 · Used by 1
TheoremThe translation computes the binary encoding#✓fully proved
Let \(\varphi\) be a dense CNF formula. Run the reversed-string translation on the reversal of the dense encoding of \(\varphi\), starting with no clause open, literal count \(0\), slot count \(0\), clause count \(0\) and empty output. The result is the binary encoding of the binary-index translation of \(\varphi\).
theorem conv_encodeCNF (φ : CNF) :
conv (encodeCNF φ).reverse false 0 0 0 [] = Cslib.CookLevin.encodeCNF (binCNF φ)abbrev CNF := List ClauseCSLibExt/Computability/Complexity/DenseSAT.lean:59
def conv : List Bool → Bool → ℕ → ℕ → ℕ → List Bool → List Bool
| false :: false :: r, ins, n, _, m, o =>
conv r true 0 0 (m + 1) (if ins then endClause n o else o)
| true :: false :: r, ins, n, k, m, o => conv r ins n (k + 1) m o
| s :: true :: r, ins, n, k, m, o =>
if ins then conv r true (n + 1) (k + 1) m (TM2Program.rep [true,
true] k ++ false :: (!s) :: o)
else conv r false n k m o
| _, ins, n, _, m, o => List.replicate m true ++ false :: (if ins then endClause n o else o)CSLibExt/Computability/Complexity/DenseToBinary.lean:169
def encodeCNF (φ : CNF) : List Bool := φ.flatMap encodeClauseCSLibExt/Computability/Complexity/DenseSAT.lean:90
def encodeCNF (φ : CNF) : List Bool :=
List.replicate φ.length true ++ false :: φ.flatMap encodeClauseCSLibExt/Computability/CookLevin.lean:99
def binCNF (φ : CNF) : Cslib.CookLevin.CNF := φ.map (binClause 0)CSLibExt/Computability/Complexity/DenseToBinary.lean:96
Uses 16 · Used by 1
TheoremSAT accepts the code of a formula exactly when it is satisfiable#✓fully proved
For every CNF formula \(\psi\), the SAT decision problem returns true on the length-prefixed binary code of \(\psi\) if and only if \(\psi\) is satisfiable.
theorem satDec_encodeCNF (ψ : Cslib.CookLevin.CNF) :
Cslib.CookLevin.satDec (Cslib.CookLevin.encodeCNF ψ) = true ↔
Cslib.CookLevin.CNFSat ψnoncomputable def satDec : MetaMathlibExt.ComplexityTheory.DecisionProblem :=
fun x => if x ∈ SATLang then true else falseCSLibExt/Computability/CookLevin.lean:391
def encodeCNF (φ : CNF) : List Bool :=
List.replicate φ.length true ++ false :: φ.flatMap encodeClauseCSLibExt/Computability/CookLevin.lean:99
Uses 19 · Used by 6
TheoremUnparsable input is not in SAT#✓fully proved
If the decoder for binary-encoded CNF formulas fails on a bit string \(x\), then the SAT decision problem rejects \(x\).
theorem satDec_of_decodeCNF_eq_none {x : List Bool} (h : Cslib.CookLevin.decodeCNF x = none) :
Cslib.CookLevin.satDec x = falsedef decodeCNF (input : List Bool) : Option CNF := do
let (φ, rest) ← decodeCNFAux input
if rest.isEmpty then some φ else noneCSLibExt/Computability/CookLevin.lean:108
noncomputable def satDec : MetaMathlibExt.ComplexityTheory.DecisionProblem :=
fun x => if x ∈ SATLang then true else falseCSLibExt/Computability/CookLevin.lean:391
Uses 19 · Used by 4
DefinitionThe dense-to-binary translation on bit strings#✓fully proved
The translation of a bit string \(w\) is the backwards dense-to-binary translation applied to the reversal of \(w\), started with no clause open, with its literal, slot and clause counters all equal to \(0\), and with empty output.
def binConv (w : List Bool) : List Bool := conv w.reverse false 0 0 0 []def conv : List Bool → Bool → ℕ → ℕ → ℕ → List Bool → List Bool
| false :: false :: r, ins, n, _, m, o =>
conv r true 0 0 (m + 1) (if ins then endClause n o else o)
| true :: false :: r, ins, n, k, m, o => conv r ins n (k + 1) m o
| s :: true :: r, ins, n, k, m, o =>
if ins then conv r true (n + 1) (k + 1) m (TM2Program.rep [true,
true] k ++ false :: (!s) :: o)
else conv r false n k m o
| _, ins, n, _, m, o => List.replicate m true ++ false :: (if ins then endClause n o else o)CSLibExt/Computability/Complexity/DenseToBinary.lean:169
InductiveStacks of the dense-to-binary machine#✓fully proved
The stack names of the Turing machine for the dense-to-binary translation form a type with exactly seven elements: the input, a stash, the output, the three counters \(n\), \(k\) and \(m\), and a scratch stack \(t\).
inductive Stk | inp | stash | out | N | K | M | T
deriving DecidableEqInductiveLabels of the dense-to-binary converter#✓fully proved
The labels of the dense-to-binary converter program are the moving label \(\mathrm{mv}\); the reading label \(\mathrm{rd}(\iota)\) for a Boolean \(\iota\); the second-read label \(\mathrm{rd2}(\iota, s)\) for Booleans \(\iota\) and \(s\); the two literal labels \(\mathrm{litA}\) and \(\mathrm{litB}\); the two closing labels \(\mathrm{eN}\) and \(\mathrm{eK}\); the clearing label \(\mathrm{fK}(\iota)\) for a Boolean \(\iota\); the literal-count label \(\mathrm{fN}\); and the clause-count label \(\mathrm{fM}\). Equality of labels is decidable.
Here \(\iota\) records whether a clause is open, and \(s\) is the first bit read of a slot.
inductive Lab
| mv
| rd (ins : Bool)
| rd2 (ins s : Bool)
| litA
| litB
| eN
| eK
| fK (ins : Bool)
| fN
| fM
deriving DecidableEqDefinitionStack contents of the converter#✓fully proved
For bit strings \(i\), \(a\), \(o\) and natural numbers \(n, k, m, t\), this stack assignment gives the input stack \(i\), the stash \(a\), the output stack \(o\), and the counter stacks \(N\), \(K\), \(M\) and the scratch stack \(T\) respectively \(n\), \(k\), \(m\) and \(t\) copies of \(1\) (true).
def stk (i a o : List Bool) (n k m t : ℕ) : Stk → List Bool
| .inp => i
| .stash => a
| .out => o
| .N => List.replicate n true
| .K => List.replicate k true
| .M => List.replicate m true
| .T => List.replicate t trueinductive Stk | inp | stash | out | N | K | M | T
deriving DecidableEqCSLibExt/Computability/Complexity/DenseToBinaryConverter.lean:34
Uses 1 · Used by 3
DefinitionThe dense-to-binary converter program#✓fully proved
The program uses an input stack, a stash, an output stack, unary counter stacks \(N\), \(K\), \(M\) and a scratch stack \(T\); each label first pops one stack and keeps the popped bit (or nothing, if the stack was empty) as its internal state. Below, \(\iota\) says whether a clause is open, \(0\) is false and \(1\) is true.
Moving: pop the input; if a bit \(b\) was popped, push \(b\) onto the stash and repeat, otherwise go to reading with \(\iota\) false.
Reading with \(\iota\): pop the stash; if a bit \(s\) was popped, go to the second read with \(\iota\) and \(s\), otherwise go to clearing with \(\iota\).
Second read with \(\iota\) and \(s\): pop the stash. If it was empty, go to clearing with \(\iota\). If it gave \(0\): when \(s = 1\), push \(1\) onto \(K\) and go to reading with \(\iota\); when \(s = 0\) and \(\iota\) is true, push \(0\) onto the output and go to the first closing label; when \(s = 0\) and \(\iota\) is false, go to the second closing label. If it gave \(1\): when \(\iota\) is true, push \(\lnot s\) and then \(0\) onto the output and go to the first literal label; otherwise go to reading with \(\iota\) false.
First literal label: pop \(K\); if a bit was popped, push \(1\) twice onto the output and \(1\) onto \(T\) and repeat, otherwise go to the second literal label.
Second literal label: pop \(T\); if a bit was popped, push \(1\) onto \(K\) and repeat, otherwise push \(1\) onto \(N\), then \(1\) onto \(K\), and go to reading with \(\iota\) true.
First closing label: pop \(N\); if a bit was popped, push \(1\) onto the output and repeat, otherwise go to the second closing label.
Second closing label: pop \(K\); if a bit was popped, repeat, otherwise push \(1\) onto \(M\) and go to reading with \(\iota\) true.
Clearing with \(\iota\): pop \(K\); if a bit was popped, repeat, otherwise push \(0\) onto the output and go to the literal-count label if \(\iota\) is true and to the clause-count label otherwise.
Literal-count label: pop \(N\); if a bit was popped, push \(1\) onto the output and repeat, otherwise push \(0\) onto the output and go to the clause-count label.
Clause-count label: pop \(M\); if a bit was popped, push \(1\) onto the output and repeat, otherwise halt.
Cslib.Complexity.DenseSAT.ToBinary.prog · 31 lines
def prog : Lab → TM2.Stmt (fun _ : Stk => Bool) Lab (Option Bool)
| .mv => pop .inp (fun _ o => o) <| branch (fun s => s.isSome)
(push .stash (fun s => s.getD false) <| goto fun _ => .mv) (goto fun _ => .rd false)
| .rd ins => pop .stash (fun _ o => o) <| branch (fun s => s.isSome)
(goto fun s => .rd2 ins (s.getD false)) (goto fun _ => .fK ins)
| .rd2 ins s => pop .stash (fun _ o => o) <| branch (fun v => v.isNone) (goto fun _ => .fK ins) <|
branch (fun v => v == some false)
(if s then (push .K (fun _ => true) <| goto fun _ => .rd ins)
else if ins then (push .out (fun _ => false) <| goto fun _ => .eN)
else goto fun _ => .eK)
(if ins then (push .out (fun _ => !s) <| push .out (fun _ => false) <| goto fun _ => .litA)
else goto fun _ => .rd false)
| .litA => pop .K (fun _ o => o) <| branch (fun v => v.isSome)
(push .out (fun _ => true) <| push .out (fun _ => true) <| push .T (fun _ => true) <|
goto fun _ => .litA)
(goto fun _ => .litB)
| .litB => pop .T (fun _ o => o) <| branch (fun v => v.isSome)
(push .K (fun _ => true) <| goto fun _ => .litB)
(push .N (fun _ => true) <| push .K (fun _ => true) <| goto fun _ => .rd true)
| .eN => pop .N (fun _ o => o) <| branch (fun v => v.isSome)
(push .out (fun _ => true) <| goto fun _ => .eN) (goto fun _ => .eK)
| .eK => pop .K (fun _ o => o) <| branch (fun v => v.isSome)
(goto fun _ => .eK) (push .M (fun _ => true) <| goto fun _ => .rd true)
| .fK ins => pop .K (fun _ o => o) <| branch (fun v => v.isSome)
(goto fun _ => .fK ins)
(push .out (fun _ => false) <| goto fun _ => if ins then .fN else .fM)
| .fN => pop .N (fun _ o => o) <| branch (fun v => v.isSome)
(push .out (fun _ => true) <| goto fun _ => .fN)
(push .out (fun _ => false) <| goto fun _ => .fM)
| .fM => pop .M (fun _ o => o) <| branch (fun v => v.isSome)
(push .out (fun _ => true) <| goto fun _ => .fM) haltinductive Lab
| mv
| rd (ins : Bool)
| rd2 (ins s : Bool)
| litA
| litB
| eN
| eK
| fK (ins : Bool)
| fN
| fM
deriving DecidableEqCSLibExt/Computability/Complexity/DenseToBinaryConverter.lean:42
inductive Stk | inp | stash | out | N | K | M | T
deriving DecidableEqCSLibExt/Computability/Complexity/DenseToBinaryConverter.lean:34
Uses 2 · Used by 5
AbbreviationExact runs of the dense-to-binary converter#✓fully proved
For a natural number \(n\) and configurations \(c\) and \(d\) of the converter program, \(c\) leads to \(d\) in exactly \(n\) steps when the program, started at \(c\), is at configuration \(d\) after exactly \(n\) steps.
abbrev Run (n : ℕ) (c d : TM2.Cfg (fun _ : Stk => Bool) Lab (Option Bool)) : Prop :=
TM2Program.Run prog n c dinductive Stk | inp | stash | out | N | K | M | T
deriving DecidableEqCSLibExt/Computability/Complexity/DenseToBinaryConverter.lean:34
inductive Lab
| mv
| rd (ins : Bool)
| rd2 (ins s : Bool)
| litA
| litB
| eN
| eK
| fK (ins : Bool)
| fN
| fM
deriving DecidableEqCSLibExt/Computability/Complexity/DenseToBinaryConverter.lean:42
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 (fun _ : Stk => Bool) Lab (Option Bool)
| .mv => pop .inp (fun _ o => o) <| branch (fun s => s.isSome)
(push .stash (fun s => s.getD false) <| goto fun _ => .mv) (goto fun _ => .rd false)
| .rd ins => pop .stash (fun _ o => o) <| branch (fun s => s.isSome)
(goto fun s => .rd2 ins (s.getD false)) (goto fun _ => .fK ins)
| .rd2 ins s => pop .stash (fun _ o => o) <| branch (fun v => v.isNone) (goto fun _ => .fK ins) <|
branch (fun v => v == some false)
(if s then (push .K (fun _ => true) <| goto fun _ => .rd ins)
else if ins then (push .out (fun _ => false) <| goto fun _ => .eN)
else goto fun _ => .eK)
(if ins then (push .out (fun _ => !s) <| push .out (fun _ => false) <| goto fun _ => .litA)
else goto fun _ => .rd false)
⋯CSLibExt/Computability/Complexity/DenseToBinaryConverter.lean:123
Uses 4 · Used by 3
TheoremMoving the input onto the stash#✓fully proved
Let \(l\), \(a\), \(o\) be bit strings and \(v\) an optional bit, and list stacks top first. Started at the moving label with internal state \(v\), input stack \(l\), stash \(a\), output stack \(o\), empty counter stacks \(N\), \(K\), \(M\) and empty scratch stack \(T\), the dense-to-binary converter reaches, in exactly \(|l| + 1\) steps, the label for reading with no clause open, with no internal state, an empty input stack, the reversal of \(l\) followed by \(a\) on the stash, output stack \(o\), and \(N\), \(K\), \(M\), \(T\) still empty.
theorem mv_run (l : List Bool) : ∀ (a o : List Bool) (v : Option Bool),
Run (l.length + 1) ⟨some .mv, v, stk l a o 0 0 0 0⟩
⟨some (.rd false), none, stk [] (l.reverse ++ a) o 0 0 0 0⟩abbrev Run (n : ℕ) (c d : TM2.Cfg (fun _ : Stk => Bool) Lab (Option Bool)) : Prop :=
TM2Program.Run prog n c dCSLibExt/Computability/Complexity/DenseToBinaryConverter.lean:156
def stk (i a o : List Bool) (n k m t : ℕ) : Stk → List Bool
| .inp => i
| .stash => a
| .out => o
| .N => List.replicate n true
| .K => List.replicate k true
| .M => List.replicate m true
| .T => List.replicate t trueCSLibExt/Computability/Complexity/DenseToBinaryConverter.lean:66
Uses 7 · Used by 1
TheoremThe converter's final phase#✓fully proved
Write \(0\) for false, \(1\) for true and \(1^j\) for \(j\) copies of \(1\). Let \(o\) be a bit string, \(\iota\) a flag saying whether a clause is open, and \(n, k, m\) natural numbers with \(n = 0\) if no clause is open; let \(c = n + 1\) if a clause is open and \(c = 0\) otherwise. Started at the label that clears the slot counter at the end, for the flag \(\iota\), with empty internal state, empty input and stash, output \(o\), literal, slot and clause counter stacks holding \(n\), \(k\) and \(m\) ones respectively, and an empty scratch stack, the converter reaches in exactly \((k + 1) + c + (m + 1)\) steps the halting configuration with empty internal state, every stack but the output empty, and output \(1^m 0 1^n 0 o\) if a clause is open and \(1^m 0 o\) otherwise (listed from the top of the stack).
theorem fin_run (o : List Bool) (ins : Bool) (n k m : ℕ) (hn : ins = false → n = 0) :
Run ((k + 1) + (if ins then n + 1 else 0) + (m + 1))
⟨some (.fK ins), none, stk [] [] o n k m 0⟩
⟨none, none, stk [] [] (List.replicate m true ++ false ::
(if ins then endClause n o else o)) 0 0 0 0⟩abbrev Run (n : ℕ) (c d : TM2.Cfg (fun _ : Stk => Bool) Lab (Option Bool)) : Prop :=
TM2Program.Run prog n c dCSLibExt/Computability/Complexity/DenseToBinaryConverter.lean:156
def stk (i a o : List Bool) (n k m t : ℕ) : Stk → List Bool
| .inp => i
| .stash => a
| .out => o
| .N => List.replicate n true
| .K => List.replicate k true
| .M => List.replicate m true
| .T => List.replicate t trueCSLibExt/Computability/Complexity/DenseToBinaryConverter.lean:66
def endClause (n : ℕ) (o : List Bool) : List Bool := List.replicate n true ++ false :: oCSLibExt/Computability/Complexity/DenseToBinary.lean:161
Uses 8 · Used by 1
DefinitionStep count of the main loop#✓fully proved
Write \(0\) for false, \(1\) for true, and \(xyr\) for the bit string whose first two bits are \(x, y\) followed by \(r\). For a bit string \(l\), a flag \(\iota\) (whether a clause is open) and natural numbers \(n, k, m\), let \(c = n + 1\) if \(\iota\) is true and \(c = 0\) otherwise. The step count \(T(l, \iota, n, k, m)\) is defined by recursion on \(l\): \(T(00r, \iota, n, k, m) = 2 + c + (k + 1) + T(r, 1, 0, 0, m + 1)\); \(T(10r, \iota, n, k, m) = 2 + T(r, \iota, n, k + 1, m)\); for every bit \(s\), \(T(s1r, \iota, n, k, m)\) is \(2 + 2(k + 1) + T(r, 1, n + 1, k + 1, m)\) if \(\iota\) is true and \(2 + T(r, 0, n, k, m)\) otherwise; on a one-bit string \(T = 2 + (k + 1) + c + (m + 1)\); and on the empty string \(T = 1 + (k + 1) + c + (m + 1)\).
def convT : List Bool → Bool → ℕ → ℕ → ℕ → ℕ
| false :: false :: r, ins, n, k, m =>
2 + (if ins then n + 1 else 0) + (k + 1) + convT r true 0 0 (m + 1)
| true :: false :: r, ins, n, k, m => 2 + convT r ins n (k + 1) m
| _ :: true :: r, ins, n, k, m =>
if ins then 2 + 2 * (k + 1) + convT r true (n + 1) (k + 1) m else 2 + convT r false n k m
| [_], ins, n, k, m => 2 + ((k + 1) + (if ins then n + 1 else 0) + (m + 1))
| _, ins, n, k, m => 1 + ((k + 1) + (if ins then n + 1 else 0) + (m + 1))TheoremStep bound for the main loop#✓fully proved
For every bit string \(l\), whether or not a clause is open, and all natural numbers \(n, k, m, Q\) with \(|l| + n + k + m \le Q\), the exact step count of the main loop on stash \(l\) with literal, slot and clause counters \(n, k, m\) is at most \((|l| + 1)(2Q + 6) + Q + 4\).
theorem convT_le : ∀ (l : List Bool) (ins : Bool) (n k m Q : ℕ),
l.length + n + k + m ≤ Q → convT l ins n k m ≤ (l.length + 1) * (2 * Q + 6) + Q + 4def convT : List Bool → Bool → ℕ → ℕ → ℕ → ℕ
| false :: false :: r, ins, n, k, m =>
2 + (if ins then n + 1 else 0) + (k + 1) + convT r true 0 0 (m + 1)
| true :: false :: r, ins, n, k, m => 2 + convT r ins n (k + 1) m
| _ :: true :: r, ins, n, k, m =>
if ins then 2 + 2 * (k + 1) + convT r true (n + 1) (k + 1) m else 2 + convT r false n k m
| [_], ins, n, k, m => 2 + ((k + 1) + (if ins then n + 1 else 0) + (m + 1))
| _, ins, n, k, m => 1 + ((k + 1) + (if ins then n + 1 else 0) + (m + 1))CSLibExt/Computability/Complexity/DenseToBinaryConverter.lean:277
Uses 1 · Used by 1
DefinitionThe dense-to-binary machine#✓fully proved
The multi-stack Turing machine whose stacks are indexed by the stack names (input, stash, output, the counters \(n\), \(k\), \(m\) and the scratch \(t\)), each with the Booleans as alphabet. It reads its input from the input stack and leaves its output on the output stack; its labels are the program labels, starting at the label that moves the input onto the stash; its internal state is an optional Boolean, initially empty; and each label runs the corresponding statement of the program.
def tm : FinTM2 where
K := Stk
k₀ := .inp
k₁ := .out
Γ := fun _ => Bool
Λ := Lab
main := .mv
σ := Option Bool
initialState := none
Γk₀Fin := (inferInstance : Fintype Bool)
m := proginductive Stk | inp | stash | out | N | K | M | T
deriving DecidableEqCSLibExt/Computability/Complexity/DenseToBinaryConverter.lean:34
inductive Lab
| mv
| rd (ins : Bool)
| rd2 (ins s : Bool)
| litA
| litB
| eN
| eK
| fK (ins : Bool)
| fN
| fM
deriving DecidableEqCSLibExt/Computability/Complexity/DenseToBinaryConverter.lean:42
def prog : Lab → TM2.Stmt (fun _ : Stk => Bool) Lab (Option Bool)
| .mv => pop .inp (fun _ o => o) <| branch (fun s => s.isSome)
(push .stash (fun s => s.getD false) <| goto fun _ => .mv) (goto fun _ => .rd false)
| .rd ins => pop .stash (fun _ o => o) <| branch (fun s => s.isSome)
(goto fun s => .rd2 ins (s.getD false)) (goto fun _ => .fK ins)
| .rd2 ins s => pop .stash (fun _ o => o) <| branch (fun v => v.isNone) (goto fun _ => .fK ins) <|
branch (fun v => v == some false)
(if s then (push .K (fun _ => true) <| goto fun _ => .rd ins)
else if ins then (push .out (fun _ => false) <| goto fun _ => .eN)
else goto fun _ => .eK)
(if ins then (push .out (fun _ => !s) <| push .out (fun _ => false) <| goto fun _ => .litA)
else goto fun _ => .rd false)
⋯CSLibExt/Computability/Complexity/DenseToBinaryConverter.lean:123
Uses 3 · Used by 1
DefinitionThe dense-to-binary translation on raw bits is polynomial-time#✓fully proved
There is a finite multi-stack Turing machine whose input and output alphabets are the bits such that, for every bit string \(w\) of length \(L\), the machine started on input \(w\) halts within \(2L^2 + 10L + 11\) steps with the dense-to-binary translation of \(w\) on its output stack and all other stacks empty.
Cslib.Complexity.DenseSAT.ToBinary.computable · 23 lines
noncomputable def computable :
TM2ComputableInPolyTime (fun l : List Bool => l) (fun l : List Bool => l) binConv where
tm := tm
inputAlphabet := Equiv.refl Bool
outputAlphabet := Equiv.refl Bool
time := Polynomial.C 2 * Polynomial.X ^ 2 + Polynomial.C 10 * Polynomial.X + Polynomial.C 11
outputsFun := fun w => by
unfold TM2OutputsInTime
refine ⟨⟨w.length + 1 + convT w.reverse false 0 0 0, ?_⟩, ?_⟩
· change (flip bind (TM2.step prog))^[_] (some (initList tm _)) =
Option.map (haltList tm) (some _)
erw [List.map_id, List.map_id, initList_tm, Option.map_some, haltList_tm]
have h1 := mv_run w [] [] none
rw [List.append_nil] at h1
exact h1.trans (main_run w.reverse false 0 0 0 [] none (fun _ => rfl))
· have h := convT_le w.reverse false 0 0 0 w.length (by simp)
have e : (w.length + 1) * (2 * w.length + 6) = 2 * w.length ^ 2 + 8 * w.length + 6 := by
ring
simp only [List.length_reverse, e] at h
simp only [Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_pow, Polynomial.eval_X,
Polynomial.eval_C]
generalize w.length ^ 2 = S at h ⊢
omegadef binConv (w : List Bool) : List Bool := conv w.reverse false 0 0 0 []CSLibExt/Computability/Complexity/DenseToBinaryConverter.lean:31
def tm : FinTM2 where
K := Stk
k₀ := .inp
k₁ := .out
Γ := fun _ => Bool
Λ := Lab
main := .mv
σ := Option Bool
initialState := none
Γk₀Fin := (inferInstance : Fintype Bool)
m := progCSLibExt/Computability/Complexity/DenseToBinaryConverter.lean:406
Uses 16 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.