The formula builders as programs

Every builder of FmlLib.lean as a polynomial-time function of the ambient model, with its toFun the builder itself. Nothing here reasons about post-order lists: the encoding of a formula is the encoding of its post-order list (SizedEncoding Fml), so the constructors are appends (andF, orF, notF of Formula.lean) and each builder is a foldl over a list, whose Cobham condition is the additivity of esize under the constructors (esize_and_fml and friends) (planning/succinct-cook-levin.md, S3).

The size of a constructed formula

theorem MIPRE.SAT.esize_and_fml (f g : Fml) : Cost.esize (f.and g) = Cost.esize f + Cost.esize g + 7

theorem MIPRE.SAT.esize_or_fml (f g : Fml) : Cost.esize (f.or g) = Cost.esize f + Cost.esize g + 9

theorem MIPRE.SAT.esize_not_fml (f : Fml) : Cost.esize f.not = Cost.esize f + 12

Folding with a constructor

noncomputable def MIPRE.SAT.andListP : Cost.PolyTimeFun (List Fml) Fml

Fml.andList.

Equations

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

@[simp]

theorem MIPRE.SAT.andListP_apply (l : List Fml) : andListP.toFun l = Fml.andList l

noncomputable def MIPRE.SAT.orListP : Cost.PolyTimeFun (List Fml) Fml

Fml.orList.

Equations

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

@[simp]

theorem MIPRE.SAT.orListP_apply (l : List Fml) : orListP.toFun l = Fml.orList l

Equality and comparison with a constant

noncomputable def MIPRE.SAT.eqStepP : Cost.PolyTimeFun (Fml × Fml × Bool) Fml

Fml.eqStep.

Equations

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

@[simp]

theorem MIPRE.SAT.eqStepP_apply (p : Fml × Fml × Bool) : eqStepP.toFun p = p.1.eqStep p.2

theorem MIPRE.SAT.eqStepP_bound (s : Fml) (a : Fml × Bool) : Cost.esize (eqStepP.toFun (s, a)) ≤ Cost.esize s + Polynomial.eval (Cost.esize a) (Polynomial.X + Polynomial.C 20)

The step of eqConst grows the accumulator by at most the size of the pair plus 20.

noncomputable def MIPRE.SAT.eqConstP : Cost.PolyTimeFun (List Fml × Cost.BitStr) Fml

Fml.eqConst.

Equations

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

@[simp]

theorem MIPRE.SAT.eqConstP_apply (p : List Fml × Cost.BitStr) : eqConstP.toFun p = Fml.eqConst p.1 p.2

Sizes of the derived builders

theorem MIPRE.SAT.esize_constFml_le (b : Bool) : Cost.esize (Fml.const b) ≤ 9

theorem MIPRE.SAT.esize_xnor_fml (f g : Fml) : Cost.esize (f.xnor g) = 2 * Cost.esize f + 2 * Cost.esize g + 47

The derived combinators

noncomputable def MIPRE.SAT.xnorP : Cost.PolyTimeFun (Fml × Fml) Fml

Fml.xnor.

Equations

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

@[simp]

theorem MIPRE.SAT.xnorP_apply (p : Fml × Fml) : xnorP.toFun p = p.1.xnor p.2

noncomputable def MIPRE.SAT.xorP : Cost.PolyTimeFun (Fml × Fml) Fml

Fml.xor.

Equations

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

@[simp]

theorem MIPRE.SAT.xorP_apply (p : Fml × Fml) : xorP.toFun p = p.1.xor p.2

noncomputable def MIPRE.SAT.muxP : Cost.PolyTimeFun (Fml × Fml × Fml) Fml

Fml.mux.

Equations

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

@[simp]

theorem MIPRE.SAT.muxP_apply (p : Fml × Fml × Fml) : muxP.toFun p = p.1.mux p.2.1 p.2.2

noncomputable def MIPRE.SAT.sum3P : Cost.PolyTimeFun (Fml × Fml × Fml) Fml

Fml.sum3.

Equations

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

@[simp]

theorem MIPRE.SAT.sum3P_apply (p : Fml × Fml × Fml) : sum3P.toFun p = p.1.sum3 p.2.1 p.2.2

noncomputable def MIPRE.SAT.maj3P : Cost.PolyTimeFun (Fml × Fml × Fml) Fml

Fml.maj3.

Equations

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

@[simp]

theorem MIPRE.SAT.maj3P_apply (p : Fml × Fml × Fml) : maj3P.toFun p = p.1.maj3 p.2.1 p.2.2

Comparison with a constant

noncomputable def MIPRE.SAT.ltStepP : Cost.PolyTimeFun (Fml × Fml × Bool) Fml

Fml.ltStep.

Equations

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

@[simp]

theorem MIPRE.SAT.ltStepP_apply (p : Fml × Fml × Bool) : ltStepP.toFun p = p.1.ltStep p.2

theorem MIPRE.SAT.ltStepP_bound (s : Fml) (a : Fml × Bool) : Cost.esize (ltStepP.toFun (s, a)) ≤ Cost.esize s + Polynomial.eval (Cost.esize a) (Polynomial.C 3 * Polynomial.X + Polynomial.C 200)

noncomputable def MIPRE.SAT.ltConstP : Cost.PolyTimeFun (List Fml × Cost.BitStr) Fml

Fml.ltConst.

Equations

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

@[simp]

theorem MIPRE.SAT.ltConstP_apply (p : List Fml × Cost.BitStr) : ltConstP.toFun p = Fml.ltConst p.1 p.2

Comparison of two fields

noncomputable def MIPRE.SAT.eqFStepP : Cost.PolyTimeFun (Fml × Fml × Fml) Fml

Fml.eqFStep.

Equations

• MIPRE.SAT.eqFStepP = MIPRE.SAT.Fml.andF.comp (MIPRE.Cost.PolyTimeFun.fst.pair (MIPRE.SAT.xnorP.comp MIPRE.Cost.PolyTimeFun.snd))

@[simp]

theorem MIPRE.SAT.eqFStepP_apply (p : Fml × Fml × Fml) : eqFStepP.toFun p = p.1.eqFStep p.2

theorem MIPRE.SAT.eqFStepP_bound (s : Fml) (a : Fml × Fml) : Cost.esize (eqFStepP.toFun (s, a)) ≤ Cost.esize s + Polynomial.eval (Cost.esize a) (Polynomial.C 2 * Polynomial.X + Polynomial.C 60)

noncomputable def MIPRE.SAT.eqFieldsP : Cost.PolyTimeFun (List Fml × List Fml) Fml

Fml.eqFields.

Equations

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

@[simp]

theorem MIPRE.SAT.eqFieldsP_apply (p : List Fml × List Fml) : eqFieldsP.toFun p = Fml.eqFields p.1 p.2

noncomputable def MIPRE.SAT.ltFStepP : Cost.PolyTimeFun (Fml × Fml × Fml) Fml

Fml.ltFStep.

Equations

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

@[simp]

theorem MIPRE.SAT.ltFStepP_apply (p : Fml × Fml × Fml) : ltFStepP.toFun p = p.1.ltFStep p.2

theorem MIPRE.SAT.ltFStepP_bound (s : Fml) (a : Fml × Fml) : Cost.esize (ltFStepP.toFun (s, a)) ≤ Cost.esize s + Polynomial.eval (Cost.esize a) (Polynomial.C 4 * Polynomial.X + Polynomial.C 100)

noncomputable def MIPRE.SAT.ltFieldsP : Cost.PolyTimeFun (List Fml × List Fml) Fml

Fml.ltFields.

Equations

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

@[simp]

theorem MIPRE.SAT.ltFieldsP_apply (p : List Fml × List Fml) : ltFieldsP.toFun p = Fml.ltFields p.1 p.2

Constant and input vectors

noncomputable def MIPRE.SAT.constBitsP : Cost.PolyTimeFun Cost.BitStr (List Fml)

Fml.constBits.

Equations

• MIPRE.SAT.constBitsP = MIPRE.SAT.Fml.constF.map.congr MIPRE.SAT.Fml.constBits MIPRE.SAT.constBitsP._proof_1

@[simp]

theorem MIPRE.SAT.constBitsP_apply (c : Cost.BitStr) : constBitsP.toFun c = Fml.constBits c

The vector of input formulas

theorem MIPRE.SAT.esize_list_le_of_forall {α : Type u_1} [Cost.SizedEncoding α] (k : ℕ) (l : List α) : (∀ a ∈ l, Cost.esize a ≤ k) → Cost.esize l ≤ l.length * (k + 1) + 1

theorem MIPRE.SAT.esize_mem_range'_le {a n x : ℕ} (h : x ∈ List.range' a n) : Cost.esize x ≤ 4 * Cost.esize (a + n) + 1

def MIPRE.SAT.rangeStep (st : ℕ × List ℕ) : Unit → ℕ × List ℕ

The step building a range of indices, from the top down.

Equations

• MIPRE.SAT.rangeStep st x✝ = (st.1 + 1, st.1 :: st.2)

theorem MIPRE.SAT.foldl_rangeStep (u : Cost.Unary) (a : ℕ) (acc : List ℕ) : List.foldl rangeStep (a, acc) u = (a + List.length u, (List.range' a (List.length u)).reverse ++ acc)

noncomputable def MIPRE.SAT.rangeStepF : Cost.PolyTimeFun ((ℕ × List ℕ) × Unit) (ℕ × List ℕ)

The step of the range, as a program.

Equations

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

@[simp]

theorem MIPRE.SAT.rangeStepF_apply (p : (ℕ × List ℕ) × Unit) : rangeStepF.toFun p = rangeStep p.1 p.2

theorem MIPRE.SAT.rangeStepF_bounded : rangeStepF.FoldBounded (Polynomial.C 30 * (Polynomial.X + 1) * (Polynomial.X + 1))

noncomputable def MIPRE.SAT.range'P : Cost.PolyTimeFun (ℕ × Cost.Unary) (List ℕ)

List.range', the length in unary.

Equations

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

@[simp]

theorem MIPRE.SAT.range'P_apply (p : ℕ × Cost.Unary) : range'P.toFun p = List.range' p.1 (List.length p.2)

noncomputable def MIPRE.SAT.fieldP : Cost.PolyTimeFun (ℕ × Cost.Unary) (List Fml)

Fml.field, the width in unary.

Equations

• MIPRE.SAT.fieldP = (MIPRE.SAT.Fml.inpF.map.comp MIPRE.SAT.range'P).congr (fun (p : ℕ × MIPRE.Cost.Unary) => MIPRE.SAT.Fml.field p.1 (List.length p.2)) MIPRE.SAT.fieldP._proof_1

@[simp]

theorem MIPRE.SAT.fieldP_apply (p : ℕ × Cost.Unary) : fieldP.toFun p = Fml.field p.1 (List.length p.2)

The adder

theorem MIPRE.SAT.esize_xor_fml (f g : Fml) : Cost.esize (f.xor g) = 2 * Cost.esize f + 2 * Cost.esize g + 47

theorem MIPRE.SAT.esize_maj3_fml (f g h : Fml) : Cost.esize (f.maj3 g h) = 2 * Cost.esize f + 2 * Cost.esize g + Cost.esize h + 32

theorem MIPRE.SAT.esize_sum3_fml (f g h : Fml) : Cost.esize (f.sum3 g h) = 4 * Cost.esize f + 4 * Cost.esize g + 2 * Cost.esize h + 141

theorem MIPRE.SAT.addBits_carry_le (E : ℕ) (fs : List Fml) (c : Cost.BitStr) (cin : Fml) : (∀ f ∈ fs, Cost.esize f ≤ E) → Cost.esize (Fml.addBits fs c cin).2 ≤ Cost.esize cin + fs.length * (2 * E + 50)

The carry out of the adder grows linearly in the width.

theorem MIPRE.SAT.addBits_mem_le (E : ℕ) (fs : List Fml) (c : Cost.BitStr) (cin : Fml) : (∀ f ∈ fs, Cost.esize f ≤ E) → ∀ s ∈ (Fml.addBits fs c cin).1, Cost.esize s ≤ 4 * E + 2 * (Cost.esize cin + fs.length * (2 * E + 50)) + 200

Every sum bit of the adder is bounded by the carry bound.

def MIPRE.SAT.addStep (st : Fml × List Fml) (p : Fml × Bool) : Fml × List Fml

The step of the adder: the carry and the reversed sum bits.

Equations

• MIPRE.SAT.addStep st p = (p.1.maj3 (MIPRE.SAT.Fml.const p.2) st.1, p.1.sum3 (MIPRE.SAT.Fml.const p.2) st.1 :: st.2)

theorem MIPRE.SAT.foldl_addStep (fs : List Fml) (c : Cost.BitStr) (cin : Fml) (acc : List Fml) : List.foldl addStep (cin, acc) (fs.zip c) = ((Fml.addBits fs c cin).2, (Fml.addBits fs c cin).1.reverse ++ acc)

noncomputable def MIPRE.SAT.addStepF : Cost.PolyTimeFun ((Fml × List Fml) × Fml × Bool) (Fml × List Fml)

The step of the adder, as a program.

Equations

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

@[simp]

theorem MIPRE.SAT.addStepF_apply (p : (Fml × List Fml) × Fml × Bool) : addStepF.toFun p = addStep p.1 p.2

theorem MIPRE.SAT.zip_map_fst_snd {α : Type u_1} {β : Type u_2} (l : List (α × β)) : (List.map Prod.fst l).zip (List.map Prod.snd l) = l

theorem MIPRE.SAT.length_addBits_le (fs : List Fml) (c : Cost.BitStr) (cin : Fml) : (Fml.addBits fs c cin).1.length ≤ fs.length

theorem MIPRE.SAT.addStepF_bounded : addStepF.FoldBounded (Polynomial.C 400 * (Polynomial.X + 1) * (Polynomial.X + 1) * (Polynomial.X + 1))

noncomputable def MIPRE.SAT.addBitsP : Cost.PolyTimeFun ((List Fml × Cost.BitStr) × Fml) (List Fml × Fml)

Fml.addBits.

Equations

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

@[simp]

theorem MIPRE.SAT.addBitsP_apply (p : (List Fml × Cost.BitStr) × Fml) : addBitsP.toFun p = Fml.addBits p.1.1 p.1.2 p.2

noncomputable def MIPRE.SAT.addConstBitsP : Cost.PolyTimeFun (List Fml × Cost.BitStr) (List Fml)

Fml.addConstBits.

Equations

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

@[simp]

theorem MIPRE.SAT.addConstBitsP_apply (p : List Fml × Cost.BitStr) : addConstBitsP.toFun p = Fml.addConstBits p.1 p.2

noncomputable def MIPRE.SAT.addConstCarryP : Cost.PolyTimeFun (List Fml × Cost.BitStr) Fml

Fml.addConstCarry.

Equations

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

@[simp]

theorem MIPRE.SAT.addConstCarryP_apply (p : List Fml × Cost.BitStr) : addConstCarryP.toFun p = Fml.addConstCarry p.1 p.2

noncomputable def MIPRE.SAT.addConstRelP : Cost.PolyTimeFun ((List Fml × List Fml) × Cost.BitStr) Fml

Fml.addConstRel.

Equations

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

@[simp]

theorem MIPRE.SAT.addConstRelP_apply (p : (List Fml × List Fml) × Cost.BitStr) : addConstRelP.toFun p = Fml.addConstRel p.1.1 p.1.2 p.2

Padding

noncomputable def MIPRE.SAT.padP : Cost.PolyTimeFun (Cost.Unary × Cost.BitStr) Cost.BitStr

padBits, the width in unary.

Equations

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

@[simp]

theorem MIPRE.SAT.padP_apply (p : Cost.Unary × Cost.BitStr) : padP.toFun p = padBits (List.length p.1) p.2

The two's complement

noncomputable def MIPRE.SAT.incBitsP : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

The successor on bit strings.

Equations

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

@[simp]

theorem MIPRE.SAT.incBitsP_apply (l : Cost.BitStr) : incBitsP.toFun l = Cost.incBits l

noncomputable def MIPRE.SAT.notBoolP : Cost.PolyTimeFun Bool Bool

Negation on booleans.

Equations

• MIPRE.SAT.notBoolP = ((MIPRE.Cost.PolyTimeFun.id Bool).ite (MIPRE.Cost.PolyTimeFun.const false) (MIPRE.Cost.PolyTimeFun.const true)).congr not MIPRE.SAT.notBoolP._proof_1

@[simp]

theorem MIPRE.SAT.notBoolP_apply (b : Bool) : notBoolP.toFun b = !b

noncomputable def MIPRE.SAT.twosCompP : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

twosComp.

Equations

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

@[simp]

theorem MIPRE.SAT.twosCompP_apply (c : Cost.BitStr) : twosCompP.toFun c = twosComp c

noncomputable def MIPRE.SAT.subConstBitsP : Cost.PolyTimeFun (List Fml × Cost.BitStr) (List Fml)

Fml.subConstBits.

Equations

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

@[simp]

theorem MIPRE.SAT.subConstBitsP_apply (p : List Fml × Cost.BitStr) : subConstBitsP.toFun p = Fml.subConstBits p.1 p.2