Cutting out one clause of an encoded formula

Reading the j-th clause of an encoded formula is the same two-bit scan that counts the clauses, with two additions: a target index to compare against, and a buffer that collects tokens while the count matches.

The state is pair (pair target count) (pair collected unread).

Main definitions

• Complexity.segStep — one two-bit step of the extraction
• Complexity.segFrom — the tokens of one segment

Main results

• Complexity.segStep_mem_FP — the extraction is polynomial time
• Complexity.segAtFn_mem_FP, Complexity.segAtFn_eq — the packaged extraction
• Complexity.litSegFn_eq — the p-th literal of the j-th clause
• Complexity.litVarFn_eq, Complexity.litSignFn_eq — its variable and sign

def Complexity.segFrom (s0 s1 : Bool) (t c : ℕ) : List Bool → List Bool

The tokens of the segment with index t, having already passed c separators, where the separator is the token s0 s1.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.segFrom s0 s1 t c x✝ = []

@[simp]

theorem Complexity.segFrom_nil (s0 s1 : Bool) (t c : ℕ) : segFrom s0 s1 t c [] = []

theorem Complexity.segFrom_cons₂ (s0 s1 : Bool) (t c : ℕ) (b0 b1 : Bool) (r : List Bool) : segFrom s0 s1 t c (b0 :: b1 :: r) = if b0 = s0 ∧ b1 = s1 then segFrom s0 s1 t (c + 1) r else if c = t then b0 :: b1 :: segFrom s0 s1 t c r else segFrom s0 s1 t c r

def Complexity.segTgt (z : List Bool) : List Bool

The target index carried by the state.

Equations

• Complexity.segTgt z = Complexity.pairFst (Complexity.pairFst z)

def Complexity.segCnt (z : List Bool) : List Bool

The number of separators already passed.

Equations

• Complexity.segCnt z = Complexity.pairSnd (Complexity.pairFst z)

def Complexity.segColl (z : List Bool) : List Bool

The tokens collected so far.

Equations

• Complexity.segColl z = Complexity.pairFst (Complexity.pairSnd z)

def Complexity.segRest (z : List Bool) : List Bool

The unread suffix.

Equations

• Complexity.segRest z = Complexity.pairSnd (Complexity.pairSnd z)

def Complexity.matchBit (b : Bool) (s : List Bool) : List Bool

Does the string begin with the bit b, as a flag?

Equations

• Complexity.matchBit b s = if b = true then Complexity.Cobham.selectHead s [true] [false] else Complexity.Cobham.selectHead s [false] [true]

theorem Complexity.matchBit_mem_FP (b : Bool) {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => matchBit b (a z)) ∈ FP

theorem Complexity.matchBit_cons (b c : Bool) (t : List Bool) : matchBit b (c :: t) = if c = b then [true] else [false]

def Complexity.segIsSep (s0 s1 : Bool) (z : List Bool) : List Bool

Is this token the separator?

Equations

• Complexity.segIsSep s0 s1 z = Complexity.andBit (Complexity.matchBit s0 (Complexity.segRest z)) (Complexity.matchBit s1 (Complexity.dropOne (Complexity.segRest z)))

def Complexity.segHere (z : List Bool) : List Bool

Are we inside the segment we want?

Equations

• Complexity.segHere z = Complexity.Cobham.lenEqFlag (Complexity.segCnt z) (Complexity.segTgt z)

def Complexity.segStep (s0 s1 : Bool) (z : List Bool) : List Bool

One two-bit step of the extraction.

Equations

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

theorem Complexity.segTgt_mem_FP : segTgt ∈ FP

theorem Complexity.segCnt_mem_FP : segCnt ∈ FP

theorem Complexity.segColl_mem_FP : segColl ∈ FP

theorem Complexity.segRest_mem_FP : segRest ∈ FP

theorem Complexity.segIsSep_mem_FP (s0 s1 : Bool) : segIsSep s0 s1 ∈ FP

theorem Complexity.segHere_mem_FP : segHere ∈ FP

theorem Complexity.segStep_mem_FP (s0 s1 : Bool) : segStep s0 s1 ∈ FP

What the scan collects

@[simp]

theorem Complexity.segStep_nil (s0 s1 : Bool) (tgt cnt coll : List Bool) : segStep s0 s1 (pair (pair tgt cnt) (pair coll [])) = pair (pair tgt cnt) (pair coll [])

theorem Complexity.segStep_cons₂ (s0 s1 : Bool) (tgt cnt coll : List Bool) (b0 b1 : Bool) (r : List Bool) : segStep s0 s1 (pair (pair tgt cnt) (pair coll (b0 :: b1 :: r))) = if b0 = s0 ∧ b1 = s1 then pair (pair tgt (true :: cnt)) (pair coll r) else pair (pair tgt cnt) (pair (if cnt.length = tgt.length then coll ++ [b0, b1] else coll) r)

theorem Complexity.segStep_iterate (s0 s1 : Bool) (k : ℕ) (tgt cnt coll s : List Bool) : s.length ≤ 2 * k → Even s.length → segColl ((segStep s0 s1)^[k] (pair (pair tgt cnt) (pair coll s))) = coll ++ segFrom s0 s1 tgt.length cnt.length s

The scan collects the segment.

theorem Complexity.even_length_segFrom (s0 s1 : Bool) (t n : ℕ) (s : List Bool) (c : ℕ) : s.length ≤ n → Even s.length → Even (segFrom s0 s1 t c s).length

The scan as one function

theorem Complexity.segStep_one (s0 s1 : Bool) (tgt cnt coll s : List Bool) : ∃ (cnt' : List Bool) (coll' : List Bool) (s' : List Bool), segStep s0 s1 (pair (pair tgt cnt) (pair coll s)) = pair (pair tgt cnt') (pair coll' s') ∧ cnt'.length ≤ cnt.length + 1 ∧ coll'.length ≤ coll.length + 2 ∧ s'.length ≤ s.length

theorem Complexity.segStep_shape (s0 s1 : Bool) (k : ℕ) (tgt cnt coll s : List Bool) : ∃ (cnt' : List Bool) (coll' : List Bool) (s' : List Bool), (segStep s0 s1)^[k] (pair (pair tgt cnt) (pair coll s)) = pair (pair tgt cnt') (pair coll' s') ∧ cnt'.length ≤ cnt.length + k ∧ coll'.length ≤ coll.length + 2 * k ∧ s'.length ≤ s.length

noncomputable def Complexity.segAtFn (s0 s1 : Bool) (z : List Bool) : List Bool

The packaged extraction, on pair (unary index) encoding.

Equations

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

theorem Complexity.segAtFn_mem_FP (s0 s1 : Bool) : segAtFn s0 s1 ∈ FP

theorem Complexity.segAtFn_eq (s0 s1 : Bool) {j : ℕ} {e : List Bool} (h : Even e.length) : segAtFn s0 s1 (pair (List.replicate j true) e) = segFrom s0 s1 j 0 e

Down to a literal

noncomputable def Complexity.litSegFn (z : List Bool) : List Bool

The p-th literal of the j-th clause, on pair (pair (unary j) (unary p)) encoding.

Equations

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

theorem Complexity.litSegFn_mem_FP : litSegFn ∈ FP

theorem Complexity.litSegFn_eq {j p : ℕ} {e : List Bool} (h : Even e.length) : litSegFn (pair (pair (List.replicate j true) (List.replicate p true)) e) = segFrom false true p 0 (segFrom true false j 0 e)

noncomputable def Complexity.litVarFn (z : List Bool) : List Bool

The variable a literal names, in unary.

Equations

• Complexity.litVarFn z = Complexity.halfFn (List.drop 2 (Complexity.litSegFn z))

theorem Complexity.litVarFn_mem_FP : litVarFn ∈ FP

theorem Complexity.litVarFn_eq {j p : ℕ} {e : List Bool} (h : Even e.length) : litVarFn (pair (pair (List.replicate j true) (List.replicate p true)) e) = List.replicate (((segFrom false true p 0 (segFrom true false j 0 e)).length - 2) / 2) true

noncomputable def Complexity.litSignFn (z : List Bool) : List Bool

The sign a literal carries, as a flag.

Equations

• Complexity.litSignFn z = Complexity.Cobham.selectHead (Complexity.litSegFn z) [true] [false]

theorem Complexity.litSignFn_mem_FP : litSignFn ∈ FP

theorem Complexity.litSignFn_eq {j p : ℕ} {e : List Bool} (h : Even e.length) : litSignFn (pair (pair (List.replicate j true) (List.replicate p true)) e) = Cobham.selectHead (segFrom false true p 0 (segFrom true false j 0 e)) [true] [false]