The scan agrees with the encoding

The clause counter reads two bits at a time and counts the token 10. This module checks that against the encoding it is meant to read: every token occupies two bits, only the clause separator is 10, and a formula's encoding carries one separator per clause.

Because tokens are two bits wide and the scan steps two bits at a time, a 10 pattern straddling two tokens is never seen.

Main results

• Complexity.sepCount_encodeTokens — the scan counts separators
• Complexity.sepCount_encode — a formula's encoding has one per clause
• Complexity.segFrom_tokenJoin — the extraction returns one segment
• Complexity.litSegFn_encode — the packaged extraction returns one literal
• Complexity.litVarFn_encode — and its variable index

theorem Complexity.length_encode_token (t : SAT.EncToken) : t.encode.length = 2

theorem Complexity.sepCount_encodeTokens (toks : List SAT.EncToken) : sepCount (SAT.encodeTokens toks) = (List.filter (fun (t : SAT.EncToken) => decide (t = SAT.EncToken.clauseSep)) toks).length

The scan counts separators.

theorem Complexity.clause_tokens_no_sep (c : SAT.Clause) : List.filter (fun (t : SAT.EncToken) => decide (t = SAT.EncToken.clauseSep)) c.tokens = []

theorem Complexity.sepCount_encode (φ : SAT.CNF) : sepCount φ.encode = List.length φ

A formula's encoding has one separator per clause.

The extraction returns one clause

theorem Complexity.hne_clauseSep (t : SAT.EncToken) : t ≠ SAT.EncToken.clauseSep → ∃ (c0 : Bool) (c1 : Bool), t.encode = [c0, c1] ∧ ¬(c0 = true ∧ c1 = false)

theorem Complexity.hne_litSep (t : SAT.EncToken) : t ≠ SAT.EncToken.litSep → ∃ (c0 : Bool) (c1 : Bool), t.encode = [c0, c1] ∧ ¬(c0 = false ∧ c1 = true)

theorem Complexity.segFrom_encodeTokens_noSep {sep : SAT.EncToken} {b0 b1 : Bool} (hne : ∀ (t : SAT.EncToken), t ≠ sep → ∃ (c0 : Bool) (c1 : Bool), t.encode = [c0, c1] ∧ ¬(c0 = b0 ∧ c1 = b1)) (toks : List SAT.EncToken) : (∀ t ∈ toks, t ≠ sep) → ∀ (v : List Bool) (t c : ℕ), segFrom b0 b1 t c (SAT.encodeTokens toks ++ v) = (if c = t then SAT.encodeTokens toks else []) ++ segFrom b0 b1 t c v

Reading past a run of non-separator tokens collects them, or not, according to whether the count matches.

theorem Complexity.segFrom_of_gt (s0 s1 : Bool) (n : ℕ) (s : List Bool) (t c : ℕ) : s.length ≤ n → t < c → segFrom s0 s1 t c s = []

def Complexity.tokenJoin (sep : SAT.EncToken) : List (List SAT.EncToken) → List SAT.EncToken

Token segments joined by a separator.

Equations

• Complexity.tokenJoin sep [] = []
• Complexity.tokenJoin sep (g :: gs) = g ++ [sep] ++ Complexity.tokenJoin sep gs

theorem Complexity.cnf_tokens_eq (φ : SAT.CNF) : φ.tokens = tokenJoin SAT.EncToken.clauseSep (List.map SAT.Clause.tokens φ)

theorem Complexity.clause_tokens_eq (c : SAT.Clause) : c.tokens = tokenJoin SAT.EncToken.litSep (List.map SAT.Lit.rawTokens c)

theorem Complexity.segFrom_tokenJoin {sep : SAT.EncToken} {b0 b1 : Bool} (hsep : sep.encode = [b0, b1]) (hne : ∀ (t : SAT.EncToken), t ≠ sep → ∃ (c0 : Bool) (c1 : Bool), t.encode = [c0, c1] ∧ ¬(c0 = b0 ∧ c1 = b1)) (segs : List (List SAT.EncToken)) : (∀ g ∈ segs, ∀ t ∈ g, t ≠ sep) → ∀ (t c : ℕ), c ≤ t → ∀ (hlt : t - c < segs.length), segFrom b0 b1 t c (SAT.encodeTokens (tokenJoin sep segs)) = SAT.encodeTokens segs[t - c]

The extraction returns one segment.

Down to a literal of a real formula

theorem Complexity.length_encodeTokens (toks : List SAT.EncToken) : (SAT.encodeTokens toks).length = 2 * toks.length

theorem Complexity.even_length_encode (φ : SAT.CNF) : Even φ.encode.length

theorem Complexity.rawTokens_no_litSep (l : SAT.Lit) (t : SAT.EncToken) : t ∈ l.rawTokens → t ≠ SAT.EncToken.litSep

theorem Complexity.segFrom_encode_clause (φ : SAT.CNF) {j : ℕ} (hj : j < List.length φ) : segFrom true false j 0 φ.encode = SAT.encodeTokens φ[j].tokens

The extraction returns one clause of a real formula.

theorem Complexity.segFrom_encode_lit (cl : SAT.Clause) {p : ℕ} (hp : p < List.length cl) : segFrom false true p 0 (SAT.encodeTokens cl.tokens) = SAT.encodeTokens cl[p].rawTokens

The extraction returns one literal of a real clause.

theorem Complexity.litSegFn_encode (φ : SAT.CNF) {j p : ℕ} (hj : j < List.length φ) (hp : p < List.length φ[j]) : litSegFn (pair (pair (List.replicate j true) (List.replicate p true)) φ.encode) = SAT.encodeTokens φ[j][p].rawTokens

The packaged extraction returns one literal.

theorem Complexity.length_rawTokens (l : SAT.Lit) : l.rawTokens.length = l.var + 1

theorem Complexity.length_litSegFn_encode (φ : SAT.CNF) {j p : ℕ} (hj : j < List.length φ) (hp : p < List.length φ[j]) : (litSegFn (pair (pair (List.replicate j true) (List.replicate p true)) φ.encode)).length = 2 * (φ[j][p].var + 1)

The extracted literal has the length its variable index dictates.

theorem Complexity.litVarFn_encode (φ : SAT.CNF) {j p : ℕ} (hj : j < List.length φ) (hp : p < List.length φ[j]) : litVarFn (pair (pair (List.replicate j true) (List.replicate p true)) φ.encode) = List.replicate φ[j][p].var true

The extraction reads off the variable index.