Restricting parameters and deleting constraints

The simplifications of a fair semi-circuit, each preserving well-formedness:

• SemiCircuit.restrict: restricting a parameter to a constant or to a literal of another parameter, the restrictions (UF) and (PF) of Mishra and Santhanam;
• SemiCircuit.deleteGate: deleting a gate that computes a literal of one of its inputs, or a constant, or that is unused, rerouting its uses, the deletions (D1) and (D2);
• SemiCircuit.deleteEqn: deleting an equation v = ℓ together with its auxiliary variable v, rerouting v to ℓ, the deletion (D3);
• SemiCircuit.dropEqn: deleting an equation together with an auxiliary variable occurring nowhere else, the second half of (D4), and SemiCircuit.dropTrivialEqn: deleting an equation without terms.

A consistent assignment of a restriction is consistent for the original semi-circuit once the restricted parameter takes the value of its literal (SemiCircuit.consistent_restrict), and consistent assignments of the deletions lift to the original semi-circuit (SemiCircuit.DeleteGateOK.liftsTo, SemiCircuit.DeleteEqnOK.liftsTo, SemiCircuit.DropEqnOK.liftsTo, SemiCircuit.liftsTo_dropTrivialEqn).

Main definitions

• Cslib.Circuits.Boolean.SemiCircuit.restrict, Cslib.Circuits.Boolean.SemiCircuit.deleteGate, Cslib.Circuits.Boolean.SemiCircuit.DeleteGateOK, Cslib.Circuits.Boolean.SemiCircuit.deleteEqn, Cslib.Circuits.Boolean.SemiCircuit.DeleteEqnOK, Cslib.Circuits.Boolean.SemiCircuit.dropEqn, Cslib.Circuits.Boolean.SemiCircuit.DropEqnOK, Cslib.Circuits.Boolean.SemiCircuit.dropTrivialEqn: the simplifications and their preconditions.

Main results

• Cslib.Circuits.Boolean.SemiCircuit.WellFormed.restrict, WellFormed.deleteGate, WellFormed.deleteEqn, WellFormed.dropEqn, WellFormed.dropTrivialEqn: the simplifications preserve well-formedness.

References

• O. S. Mishra and R. Santhanam, An Explicit 3.5n − o(n) Size Lower Bound against General Boolean Circuits

Restricting a parameter

def Cslib.Circuits.Boolean.SemiCircuit.restrict (C : SemiCircuit) (x : ℕ) (ℓ : Lit) : SemiCircuit

Restrict the parameter x to the literal ℓ: reroute x to ℓ and remove it from the parameters.

theorem Cslib.Circuits.Boolean.SemiCircuit.mem_live_restrict {C : SemiCircuit} {x : ℕ} {ℓ : Lit} {i : ℕ} (hi : i ∈ C.live) (hix : i ≠ x) : i ∈ (C.restrict x ℓ).live

Any live node of C distinct from x remains live in C.restrict x ℓ.

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.restrict {C : SemiCircuit} (hC : C.WellFormed) {x : ℕ} {ℓ : Lit} (hx : x ∈ C.params) (hℓ : ∀ (y : ℕ), ℓ.Reads y → y ∈ C.params ∧ y ≠ x) : (C.restrict x ℓ).WellFormed

Restricting a parameter to a literal reading at most another parameter preserves well-formedness.

theorem Cslib.Circuits.Boolean.SemiCircuit.consistent_restrict {C : SemiCircuit} (hC : C.WellFormed) {x : ℕ} {ℓ : Lit} (hx : x ∈ C.params) (hℓ : ℓ.arg ≠ Arg.node x) {val : ℕ → Bool} (h : (C.restrict x ℓ).Consistent val) : C.Consistent (Function.update val x (ℓ.eval val))

A consistent assignment of a restriction, with the restricted parameter given the value of its literal, is consistent for the original semi-circuit.

theorem Cslib.Circuits.Boolean.SemiCircuit.out_restrict {C : SemiCircuit} {x : ℕ} {ℓ : Lit} (hℓ : ℓ.arg ≠ Arg.node x) (val : ℕ → Bool) : (C.restrict x ℓ).out.eval val = C.out.eval (Function.update val x (ℓ.eval val))

Evaluating the output of C.restrict x ℓ under val equals evaluating the output of C after updating x to ℓ.eval val.

Deleting a gate

def Cslib.Circuits.Boolean.SemiCircuit.deleteGate (C : SemiCircuit) (J : ℕ) (ℓ : Lit) : SemiCircuit

Delete the gate J, rerouting its uses to the literal ℓ.

structure Cslib.Circuits.Boolean.SemiCircuit.DeleteGateOK (C : SemiCircuit) (J : ℕ) (ℓ : Lit) : Prop

The hypotheses of a gate deletion: J is a gate, ℓ reads at most an input of J, and either J computes ℓ on the solutions of the affine system or nothing reads J.

• mem : J ∈ C.gates
• reads (t : ℕ) : ℓ.Reads t → (C.gate J).Reads t
• value : (∀ (val : ℕ → Bool), C.EqnsHold val → (C.gate J).eval val = ℓ.eval val) ∨ (∀ K ∈ C.gates, ¬(C.gate K).Reads J) ∧ ¬C.out.Reads J

theorem Cslib.Circuits.Boolean.SemiCircuit.mem_live_deleteGate {C : SemiCircuit} {J : ℕ} {ℓ : Lit} {i : ℕ} (hi : i ∈ C.live) (hiJ : i ≠ J) : i ∈ (C.deleteGate J ℓ).live

Any live node of C distinct from J remains live in C.deleteGate J ℓ.

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.deleteGate {C : SemiCircuit} (hC : C.WellFormed) {J : ℕ} {ℓ : Lit} (h : C.DeleteGateOK J ℓ) : (C.deleteGate J ℓ).WellFormed

Deleting a gate preserves well-formedness.

theorem Cslib.Circuits.Boolean.SemiCircuit.DeleteGateOK.liftsTo {C : SemiCircuit} (hC : C.WellFormed) {J : ℕ} {ℓ : Lit} (h : C.DeleteGateOK J ℓ) : (C.deleteGate J ℓ).LiftsTo C

A consistent assignment of a gate deletion lifts, by giving the deleted gate its value.

Deleting an equation

def Cslib.Circuits.Boolean.SemiCircuit.deleteEqn (C : SemiCircuit) (e v : ℕ) (ℓ : Lit) : SemiCircuit

Delete the equation e, which reads v = ℓ, and the auxiliary variable v, rerouting v to ℓ.

structure Cslib.Circuits.Boolean.SemiCircuit.DeleteEqnOK (C : SemiCircuit) (e v : ℕ) (ℓ : Lit) : Prop

The hypotheses of deleting an equation: e is an equation stating v = ℓ for an auxiliary variable v and a literal ℓ reading at most another term of e.

• mem : e ∈ C.eqns
• aux : v ∈ C.aux
• holds (val : ℕ → Bool) : (C.eqn e).Holds val ↔ val v = ℓ.eval val
• reads (t : ℕ) : ℓ.Reads t → t ∈ (C.eqn e).terms ∧ t ≠ v

theorem Cslib.Circuits.Boolean.SemiCircuit.mem_live_deleteEqn {C : SemiCircuit} {e v : ℕ} {ℓ : Lit} {i : ℕ} (hi : i ∈ C.live) (hiv : i ≠ v) : i ∈ (C.deleteEqn e v ℓ).live

Any live node of C distinct from v remains live in C.deleteEqn e v ℓ.

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.deleteEqn {C : SemiCircuit} (hC : C.WellFormed) {e v : ℕ} {ℓ : Lit} (h : C.DeleteEqnOK e v ℓ) : (C.deleteEqn e v ℓ).WellFormed

Deleting an equation v = ℓ with its auxiliary variable preserves well-formedness.

theorem Cslib.Circuits.Boolean.SemiCircuit.DeleteEqnOK.liftsTo {C : SemiCircuit} (hC : C.WellFormed) {e v : ℕ} {ℓ : Lit} (h : C.DeleteEqnOK e v ℓ) : (C.deleteEqn e v ℓ).LiftsTo C

A consistent assignment after deleting v = ℓ lifts, by giving v the value of ℓ.

Dropping an equation

def Cslib.Circuits.Boolean.SemiCircuit.dropEqn (C : SemiCircuit) (e v : ℕ) : SemiCircuit

Delete the equation e together with an auxiliary variable v occurring nowhere else.

structure Cslib.Circuits.Boolean.SemiCircuit.DropEqnOK (C : SemiCircuit) (e v : ℕ) : Prop

The hypotheses of dropping an equation: the auxiliary variable v occurs in the equation e and nowhere else.

• mem : e ∈ C.eqns
• aux : v ∈ C.aux
• mem_terms : v ∈ (C.eqn e).terms
• only (e' : ℕ) : e' ∈ C.eqns → e' ≠ e → v ∉ (C.eqn e').terms
• gates (K : ℕ) : K ∈ C.gates → ¬(C.gate K).Reads v
• out : ¬C.out.Reads v

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.dropEqn {C : SemiCircuit} (hC : C.WellFormed) {e v : ℕ} (h : C.DropEqnOK e v) : (C.dropEqn e v).WellFormed

Dropping an equation with an auxiliary variable occurring only there preserves well-formedness.

theorem Cslib.Circuits.Boolean.SemiCircuit.DropEqnOK.liftsTo {C : SemiCircuit} (hC : C.WellFormed) {e v : ℕ} (h : C.DropEqnOK e v) : (C.dropEqn e v).LiftsTo C

A consistent assignment after dropping an equation lifts, by solving the equation for the dropped auxiliary variable.

def Cslib.Circuits.Boolean.SemiCircuit.dropTrivialEqn (C : SemiCircuit) (e : ℕ) : SemiCircuit

Delete an equation without terms.

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.dropTrivialEqn {C : SemiCircuit} (hC : C.WellFormed) {e : ℕ} (he : e ∈ C.eqns) (hterms : (C.eqn e).terms = ∅) : (C.dropTrivialEqn e).WellFormed

Dropping an equation with no terms preserves well-formedness.

theorem Cslib.Circuits.Boolean.SemiCircuit.liftsTo_dropTrivialEqn {C : SemiCircuit} (hC : C.WellFormed) {e : ℕ} (he : e ∈ C.eqns) (hterms : (C.eqn e).terms = ∅) : (C.dropTrivialEqn e).LiftsTo C

Every consistent assignment after dropping an equation with no terms is consistent for the original semi-circuit.