Stack-free streams for finite Boolean folds

Finite conjunctions and disjunctions are right-associated formula trees, but their exact raw compilation does not require a run-time formula stack. It is a forward stream of member fragments, one identity constant, and a reverse stream of connector gates. These identities are the proof interface used by the log-space direct-unrolling serializer.

This module proves the exact proof-level list decomposition. The future transducer will realize its reverse suffix with an indexed cursor and recomputation; no executable cursor is claimed here.

Main results

• BoolFormula.compileRaw_conjs_eq_rightFold gives the exact conjunction stream.
• BoolFormula.compileRaw_disjs_eq_rightFold gives the exact disjunction stream.
• BoolFormula.length_compileRawRightFold gives its exact gate count.

@[simp]

theorem Complexity.BoolFormula.rightFoldSize_nil : rightFoldSize [] = 1

@[simp]

theorem Complexity.BoolFormula.rightFoldSize_cons (formula : BoolFormula) (formulas : List BoolFormula) : rightFoldSize (formula :: formulas) = formula.size + rightFoldSize formulas + 1

theorem Complexity.BoolFormula.rightFoldSize_eq_size_conjs (formulas : List BoolFormula) : rightFoldSize formulas = (conjs formulas).size

theorem Complexity.BoolFormula.rightFoldSize_eq_size_disjs (formulas : List BoolFormula) : rightFoldSize formulas = (disjs formulas).size

theorem Complexity.BoolFormula.compileRaw_conjs_eq_rightFold (available : ℕ) (formulas : List BoolFormula) : compileRaw available (conjs formulas) = compileRawRightFold AndOrOp.and true available formulas

Exact raw compilation of a finite conjunction as a stack-free gate stream.

theorem Complexity.BoolFormula.compileRaw_disjs_eq_rightFold (available : ℕ) (formulas : List BoolFormula) : compileRaw available (disjs formulas) = compileRawRightFold AndOrOp.or false available formulas

Exact raw compilation of a finite disjunction as a stack-free gate stream.

@[simp]

theorem Complexity.BoolFormula.length_rightFoldConnectors (op : AndOrOp) (available : ℕ) (formulas : List BoolFormula) : List.length (rightFoldConnectors op available formulas) = formulas.length

@[simp]

theorem Complexity.BoolFormula.length_compileRawRightFold (op : AndOrOp) (identity : Bool) (available : ℕ) (formulas : List BoolFormula) : List.length (compileRawRightFold op identity available formulas) = rightFoldSize formulas