Flattening a formula to a circuit, in polynomial time

A formula is encoded as its post-order serialization (Fml.rpn), and the circuit of a formula (Fml.flattenAt 0) is computed from that serialization by a single left-to-right scan with a stack of gate indices (flStep, flatten): an input or constant node emits its gate and pushes the gate's index; a connective pops the indices of its arguments, emits the gate and pushes the new index. The scan is a fold, so the program is a PolyTimeFun.foldl of the step (PolyTimeFun.casesNode dispatches on the node), and Fml.toCircuitF is the circuit of a formula on a given number of inputs as a polynomial-time function (planning/succinct-cook-levin.md, S3).

The scan

@[reducible, inline]

abbrev MIPRE.SAT.FlState : Type

The state of the scan: the stack of gate indices, the gates so far (reversed), and the number of gates so far.

Equations

• MIPRE.SAT.FlState = (List ℕ × List MIPRE.SAT.Gate × ℕ)

def MIPRE.SAT.flStep (s : FlState) : Fml.Node → FlState

One step of the scan.

Equations

• MIPRE.SAT.flStep s (MIPRE.SAT.Fml.Node.inp i) = (s.2.2 :: s.1, MIPRE.SAT.Gate.input i :: s.2.1, s.2.2 + 1)
• MIPRE.SAT.flStep s (MIPRE.SAT.Fml.Node.const b) = (s.2.2 :: s.1, MIPRE.SAT.Gate.const b :: s.2.1, s.2.2 + 1)
• MIPRE.SAT.flStep s MIPRE.SAT.Fml.Node.and = match s.1 with | g :: f :: vs => (s.2.2 :: vs, MIPRE.SAT.Gate.and f g :: s.2.1, s.2.2 + 1) | x => s
• MIPRE.SAT.flStep s MIPRE.SAT.Fml.Node.or = match s.1 with | g :: f :: vs => (s.2.2 :: vs, MIPRE.SAT.Gate.or f g :: s.2.1, s.2.2 + 1) | x => s
• MIPRE.SAT.flStep s MIPRE.SAT.Fml.Node.not = match s.1 with | f :: vs => (s.2.2 :: vs, MIPRE.SAT.Gate.not f :: s.2.1, s.2.2 + 1) | x => s

theorem MIPRE.SAT.foldl_flStep_rpn (f : Fml) (rest : List Fml.Node) (vs : List ℕ) (out : List Gate) (cnt : ℕ) : List.foldl flStep (vs, out, cnt) (f.rpn ++ rest) = List.foldl flStep ((cnt + f.size - 1) :: vs, (Fml.flattenAt cnt f).reverse ++ out, cnt + f.size) rest

The scan of the serialization of f from a state pushes the output index of f and emits its gates.

def MIPRE.SAT.flatten (l : List Fml.Node) : List Gate

The gates of a serialization.

Equations

• MIPRE.SAT.flatten l = (List.foldl MIPRE.SAT.flStep ([], [], 0) l).2.1.reverse

theorem MIPRE.SAT.flatten_rpn (f : Fml) : flatten f.rpn = Fml.flattenAt 0 f

The size of the state along the scan

def MIPRE.SAT.Gate.payload : Gate → ℕ

The payload of a gate: the input index of an input gate.

Equations

• (MIPRE.SAT.Gate.input i).payload = MIPRE.Cost.esize i
• x✝.payload = 0

theorem MIPRE.SAT.esize_gate_le (g : Gate) : Cost.esize g ≤ (List.map Cost.esize g.refs).sum + g.payload + 12

theorem MIPRE.SAT.esize_inp_node (i : ℕ) : Cost.esize (Fml.Node.inp i) = Cost.esize i + 2

theorem MIPRE.SAT.esize_nat_add_le (n k : ℕ) : Cost.esize (n + k) ≤ Cost.esize n + 4 * k

theorem MIPRE.SAT.flStep_bounded (l : List Fml.Node) (E : ℕ) (hE : ∀ nd ∈ l, Cost.esize nd ≤ E) (vs : List ℕ) (out : List Gate) (cnt D : ℕ) : (∀ v ∈ vs, Cost.esize v ≤ D) → Cost.esize cnt ≤ D → have s := List.foldl flStep (vs, out, cnt) l; (∀ v ∈ s.1, Cost.esize v ≤ D + 4 * l.length) ∧ Cost.esize s.2.2 ≤ D + 4 * l.length ∧ Cost.esize s.1 ≤ Cost.esize vs + l.length * (D + 4 * l.length + 1) ∧ Cost.esize s.2.1 ≤ Cost.esize out + l.length * (2 * (D + 4 * l.length) + E + 13)

Along the scan, every index on the stack is bounded, and so is the state.

Dispatch on a node

def MIPRE.SAT.FlProg.cnInp (Fi : Cost.Prog) : Cost.Prog

The branches of casesNodeProg, in the environments described there.

Equations

• MIPRE.SAT.FlProg.cnInp Fi = ((MIPRE.Cost.Prog.var 2).cons (MIPRE.Cost.Prog.var 1)).let_ Fi

def MIPRE.SAT.FlProg.cnConst (Fc : Cost.Prog) : Cost.Prog

Equations

• MIPRE.SAT.FlProg.cnConst Fc = ((MIPRE.Cost.Prog.var 4).cons (MIPRE.Cost.Prog.var 3)).let_ Fc

def MIPRE.SAT.FlProg.cnRest3 (Fo Fn : Cost.Prog) : Cost.Prog

Equations

• MIPRE.SAT.FlProg.cnRest3 Fo Fn = MIPRE.Cost.Prog.elim 1 (MIPRE.Cost.Prog.callVar 8 Fo) (MIPRE.Cost.Prog.callVar 10 Fn)

def MIPRE.SAT.FlProg.cnRest2 (Fa Fo Fn : Cost.Prog) : Cost.Prog

Equations

• MIPRE.SAT.FlProg.cnRest2 Fa Fo Fn = MIPRE.Cost.Prog.elim 1 (MIPRE.Cost.Prog.callVar 6 Fa) (MIPRE.SAT.FlProg.cnRest3 Fo Fn)

def MIPRE.SAT.FlProg.cnRest1 (Fc Fa Fo Fn : Cost.Prog) : Cost.Prog

Equations

• MIPRE.SAT.FlProg.cnRest1 Fc Fa Fo Fn = MIPRE.Cost.Prog.elim 1 (MIPRE.SAT.FlProg.cnConst Fc) (MIPRE.SAT.FlProg.cnRest2 Fa Fo Fn)

def MIPRE.SAT.FlProg.cnTag (Fi Fc Fa Fo Fn : Cost.Prog) : Cost.Prog

Equations

• MIPRE.SAT.FlProg.cnTag Fi Fc Fa Fo Fn = MIPRE.Cost.Prog.elim 0 (MIPRE.SAT.FlProg.cnInp Fi) (MIPRE.SAT.FlProg.cnRest1 Fc Fa Fo Fn)

def MIPRE.SAT.FlProg.casesNodeProg (Fi Fc Fa Fo Fn : Cost.Prog) : Cost.Prog

Dispatch on the node of an input (a, nd): the environment after the two elims is [tag, payload, a, nd, input], and the unary tag is inspected one nil at a time.

Equations

• MIPRE.SAT.FlProg.casesNodeProg Fi Fc Fa Fo Fn = MIPRE.Cost.Prog.elim 0 MIPRE.Cost.Prog.nil (MIPRE.Cost.Prog.elim 1 MIPRE.Cost.Prog.nil (MIPRE.SAT.FlProg.cnTag Fi Fc Fa Fo Fn))

theorem MIPRE.SAT.FlProg.casesNodeProg_wellScoped {Fi Fc Fa Fo Fn : Cost.Prog} (hi : Cost.Prog.WellScoped 1 Fi) (hc : Cost.Prog.WellScoped 1 Fc) (ha : Cost.Prog.WellScoped 1 Fa) (ho : Cost.Prog.WellScoped 1 Fo) (hn : Cost.Prog.WellScoped 1 Fn) : Cost.Prog.WellScoped 1 (casesNodeProg Fi Fc Fa Fo Fn)

theorem MIPRE.SAT.FlProg.casesNodeProg_inp {Fi Fc Fa Fo Fn : Cost.Prog} (hi : Cost.Prog.WellScoped 1 Fi) (ea : Cost.Data) (i : ℕ) {r : Cost.Data} {t : ℕ} (h : Cost.Eval [ea.cons (Cost.encode i)] Fi r t) : Cost.Eval [ea.cons (Cost.encode (Fml.Node.inp i))] (casesNodeProg Fi Fc Fa Fo Fn) r (ea.size + Cost.esize i + t + 7)

theorem MIPRE.SAT.FlProg.casesNodeProg_const {Fi Fc Fa Fo Fn : Cost.Prog} (hc : Cost.Prog.WellScoped 1 Fc) (ea : Cost.Data) (b : Bool) {r : Cost.Data} {t : ℕ} (h : Cost.Eval [ea.cons (Cost.encode b)] Fc r t) : Cost.Eval [ea.cons (Cost.encode (Fml.Node.const b))] (casesNodeProg Fi Fc Fa Fo Fn) r (ea.size + Cost.esize b + t + 8)

theorem MIPRE.SAT.FlProg.casesNodeProg_and {Fi Fc Fa Fo Fn : Cost.Prog} (ha : Cost.Prog.WellScoped 1 Fa) (ea : Cost.Data) {r : Cost.Data} {t : ℕ} (h : Cost.Eval [ea] Fa r t) : Cost.Eval [ea.cons (Cost.encode Fml.Node.and)] (casesNodeProg Fi Fc Fa Fo Fn) r (ea.size + t + 7)

theorem MIPRE.SAT.FlProg.casesNodeProg_or {Fi Fc Fa Fo Fn : Cost.Prog} (ho : Cost.Prog.WellScoped 1 Fo) (ea : Cost.Data) {r : Cost.Data} {t : ℕ} (h : Cost.Eval [ea] Fo r t) : Cost.Eval [ea.cons (Cost.encode Fml.Node.or)] (casesNodeProg Fi Fc Fa Fo Fn) r (ea.size + t + 8)

theorem MIPRE.SAT.FlProg.casesNodeProg_not {Fi Fc Fa Fo Fn : Cost.Prog} (hn : Cost.Prog.WellScoped 1 Fn) (ea : Cost.Data) {r : Cost.Data} {t : ℕ} (h : Cost.Eval [ea] Fn r t) : Cost.Eval [ea.cons (Cost.encode Fml.Node.not)] (casesNodeProg Fi Fc Fa Fo Fn) r (ea.size + t + 8)

theorem MIPRE.SAT.esize_node_inp (i : ℕ) : Cost.esize (Fml.Node.inp i) = Cost.esize i + 2

theorem MIPRE.SAT.esize_node_const (b : Bool) : Cost.esize (Fml.Node.const b) = Cost.esize b + 4

def MIPRE.SAT.PolyTimeFun.casesNodeFun {α : Type u_1} {β : Type u_2} (Fi : α × ℕ → β) (Fc : α × Bool → β) (Fa Fo Fn : α → β) : α × Fml.Node → β

The function of casesNode.

Equations

• MIPRE.SAT.PolyTimeFun.casesNodeFun Fi Fc Fa Fo Fn (a, MIPRE.SAT.Fml.Node.inp i) = Fi (a, i)
• MIPRE.SAT.PolyTimeFun.casesNodeFun Fi Fc Fa Fo Fn (a, MIPRE.SAT.Fml.Node.const b) = Fc (a, b)
• MIPRE.SAT.PolyTimeFun.casesNodeFun Fi Fc Fa Fo Fn (a, MIPRE.SAT.Fml.Node.and) = Fa a
• MIPRE.SAT.PolyTimeFun.casesNodeFun Fi Fc Fa Fo Fn (a, MIPRE.SAT.Fml.Node.or) = Fo a
• MIPRE.SAT.PolyTimeFun.casesNodeFun Fi Fc Fa Fo Fn (a, MIPRE.SAT.Fml.Node.not) = Fn a

noncomputable def MIPRE.SAT.PolyTimeFun.casesNode {α : Type u_1} {β : Type u_2} [Cost.SizedEncoding α] [Cost.SizedEncoding β] (Fi : Cost.PolyTimeFun (α × ℕ) β) (Fc : Cost.PolyTimeFun (α × Bool) β) (Fa Fo Fn : Cost.PolyTimeFun α β) : Cost.PolyTimeFun (α × Fml.Node) β

Case analysis on a node component.

Equations

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

@[simp]

theorem MIPRE.SAT.PolyTimeFun.casesNode_inp {α : Type u_1} {β : Type u_2} [Cost.SizedEncoding α] [Cost.SizedEncoding β] (Fi : Cost.PolyTimeFun (α × ℕ) β) (Fc : Cost.PolyTimeFun (α × Bool) β) (Fa Fo Fn : Cost.PolyTimeFun α β) (a : α) (i : ℕ) : (casesNode Fi Fc Fa Fo Fn).toFun (a, Fml.Node.inp i) = Fi.toFun (a, i)

@[simp]

theorem MIPRE.SAT.PolyTimeFun.casesNode_const {α : Type u_1} {β : Type u_2} [Cost.SizedEncoding α] [Cost.SizedEncoding β] (Fi : Cost.PolyTimeFun (α × ℕ) β) (Fc : Cost.PolyTimeFun (α × Bool) β) (Fa Fo Fn : Cost.PolyTimeFun α β) (a : α) (b : Bool) : (casesNode Fi Fc Fa Fo Fn).toFun (a, Fml.Node.const b) = Fc.toFun (a, b)

@[simp]

theorem MIPRE.SAT.PolyTimeFun.casesNode_and {α : Type u_1} {β : Type u_2} [Cost.SizedEncoding α] [Cost.SizedEncoding β] (Fi : Cost.PolyTimeFun (α × ℕ) β) (Fc : Cost.PolyTimeFun (α × Bool) β) (Fa Fo Fn : Cost.PolyTimeFun α β) (a : α) : (casesNode Fi Fc Fa Fo Fn).toFun (a, Fml.Node.and) = Fa.toFun a

@[simp]

theorem MIPRE.SAT.PolyTimeFun.casesNode_or {α : Type u_1} {β : Type u_2} [Cost.SizedEncoding α] [Cost.SizedEncoding β] (Fi : Cost.PolyTimeFun (α × ℕ) β) (Fc : Cost.PolyTimeFun (α × Bool) β) (Fa Fo Fn : Cost.PolyTimeFun α β) (a : α) : (casesNode Fi Fc Fa Fo Fn).toFun (a, Fml.Node.or) = Fo.toFun a

@[simp]

theorem MIPRE.SAT.PolyTimeFun.casesNode_not {α : Type u_1} {β : Type u_2} [Cost.SizedEncoding α] [Cost.SizedEncoding β] (Fi : Cost.PolyTimeFun (α × ℕ) β) (Fc : Cost.PolyTimeFun (α × Bool) β) (Fa Fo Fn : Cost.PolyTimeFun α β) (a : α) : (casesNode Fi Fc Fa Fo Fn).toFun (a, Fml.Node.not) = Fn.toFun a

The scan as a polynomial-time function

noncomputable def MIPRE.SAT.Gate.inputF : Cost.PolyTimeFun ℕ Gate

The gate constructors as polynomial-time functions.

Equations

• MIPRE.SAT.Gate.inputF = MIPRE.Cost.PolyTimeFun.tagged 0 MIPRE.SAT.Gate.input MIPRE.SAT.Gate.inputF._proof_1

noncomputable def MIPRE.SAT.Gate.constF : Cost.PolyTimeFun Bool Gate

Equations

• MIPRE.SAT.Gate.constF = MIPRE.Cost.PolyTimeFun.tagged 1 MIPRE.SAT.Gate.const MIPRE.SAT.Gate.constF._proof_1

noncomputable def MIPRE.SAT.Gate.andF : Cost.PolyTimeFun (ℕ × ℕ) Gate

Equations

• MIPRE.SAT.Gate.andF = MIPRE.Cost.PolyTimeFun.tagged 2 (fun (p : ℕ × ℕ) => MIPRE.SAT.Gate.and p.1 p.2) MIPRE.SAT.Gate.andF._proof_1

noncomputable def MIPRE.SAT.Gate.orF : Cost.PolyTimeFun (ℕ × ℕ) Gate

Equations

• MIPRE.SAT.Gate.orF = MIPRE.Cost.PolyTimeFun.tagged 3 (fun (p : ℕ × ℕ) => MIPRE.SAT.Gate.or p.1 p.2) MIPRE.SAT.Gate.orF._proof_1

noncomputable def MIPRE.SAT.Gate.notF : Cost.PolyTimeFun ℕ Gate

Equations

• MIPRE.SAT.Gate.notF = MIPRE.Cost.PolyTimeFun.tagged 4 MIPRE.SAT.Gate.not MIPRE.SAT.Gate.notF._proof_1

noncomputable def MIPRE.SAT.flLeafF {γ : Type u_1} [Cost.SizedEncoding γ] (G : Cost.PolyTimeFun γ Gate) : Cost.PolyTimeFun (FlState × γ) FlState

The step of the scan on a leaf: push the counter, emit the gate, increment.

Equations

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

noncomputable def MIPRE.SAT.flBinF (G : Cost.PolyTimeFun (ℕ × ℕ) Gate) : Cost.PolyTimeFun FlState FlState

The step of the scan on a binary connective: pop two indices, emit the gate, push. The state is presented as ((out, cnt), vs) to casesList.

Equations

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

noncomputable def MIPRE.SAT.flNotF : Cost.PolyTimeFun FlState FlState

The step of the scan on a negation.

Equations

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

theorem MIPRE.SAT.flBinF_apply_and (s : FlState) : (flBinF Gate.andF).toFun s = flStep s Fml.Node.and

theorem MIPRE.SAT.flBinF_apply_or (s : FlState) : (flBinF Gate.orF).toFun s = flStep s Fml.Node.or

theorem MIPRE.SAT.flNotF_apply (s : FlState) : flNotF.toFun s = flStep s Fml.Node.not

noncomputable def MIPRE.SAT.flStepF : Cost.PolyTimeFun (FlState × Fml.Node) FlState

The step of the scan, as a polynomial-time function.

Equations

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

@[simp]

theorem MIPRE.SAT.flStepF_apply (p : FlState × Fml.Node) : flStepF.toFun p = flStep p.1 p.2

theorem MIPRE.SAT.esize_flState (vs : List ℕ) (out : List Gate) (cnt : ℕ) : Cost.esize (vs, out, cnt) = Cost.esize vs + (Cost.esize out + Cost.esize cnt + 1) + 1

theorem MIPRE.SAT.flStepF_bounded : flStepF.FoldBounded (Polynomial.C 40 * (Polynomial.X + 1) * (Polynomial.X + 1))

The Cobham condition of the scan.

noncomputable def MIPRE.SAT.flattenF : Cost.PolyTimeFun (List Fml.Node) (List Gate)

The gates of a serialization, in polynomial time.

Equations

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

@[simp]

theorem MIPRE.SAT.flattenF_apply (l : List Fml.Node) : flattenF.toFun l = flatten l

noncomputable def MIPRE.SAT.Fml.toCircuitF : Cost.PolyTimeFun (ℕ × Fml) Circuit

The circuit of a formula on n inputs, in polynomial time.

Equations

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

@[simp]

theorem MIPRE.SAT.Fml.toCircuitF_apply (p : ℕ × Fml) : toCircuitF.toFun p = toCircuit p.1 p.2