Structural facts about De Morgan restriction

This module connects the origin graph to the concrete partial evaluator. It contains no circuit-specific XOR reasoning: the results say when a fixed input turns an origin into a constant and how facts about an earlier source gate are preserved while later gates are processed.

theorem Algebraic.DeMorgan.ProgramRestriction.value_eq_constant_of_constant_origin {n g : ℕ} {source : Program signature (n + 1) g} {selected : Fin (n + 1)} {fixedValue : Bool} (restriction : ProgramRestriction source selected fixedValue) {sourceWire : Wire (n + 1) g} {value : Bool} (origin_eq : origins source sourceWire = ResidualValue.constant value) : restriction.values sourceWire = ResidualValue.constant value

Following a constant origin produces that same constant.

theorem Algebraic.DeMorgan.ProgramRestriction.value_eq_constant_of_selected_origin {n g : ℕ} {source : Program signature (n + 1) g} {selected : Fin (n + 1)} {fixedValue : Bool} (restriction : ProgramRestriction source selected fixedValue) {sourceWire : Wire (n + 1) g} {negated : Bool} (origin_eq : origins source sourceWire = ResidualValue.wire negated (Wire.input selected)) : restriction.values sourceWire = ResidualValue.constant (if negated = true then !fixedValue else fixedValue)

Following a signed occurrence of the selected input produces a constant.

theorem Algebraic.DeMorgan.ProgramRestriction.value_eq_constant_of_gate_origin {n g : ℕ} {source : Program signature (n + 1) g} {selected : Fin (n + 1)} {fixedValue : Bool} (restriction : ProgramRestriction source selected fixedValue) {sourceWire : Wire (n + 1) g} {gate : Fin g} {negated value : Bool} (origin_eq : origins source sourceWire = ResidualValue.wire negated (Wire.gate gate)) (gate_eq : restriction.values (Wire.gate gate) = ResidualValue.constant value) : restriction.values sourceWire = ResidualValue.constant (if negated = true then !value else value)

Following a signed charged-gate origin preserves a known constant value.

theorem Algebraic.DeMorgan.restrictProgram_deleted_castSucc {n g : ℕ} (source : Program signature (n + 1) g) (line : Line signature (n + 1) g) (selected : Fin (n + 1)) (fixedValue : Bool) {gate : Fin g} (deleted : gate ∈ (restrictProgram selected fixedValue source).deleted) : gate.castSucc ∈ (restrictProgram selected fixedValue (source.gate line)).deleted

Deletion of an earlier charged gate survives processing one later line.

theorem Algebraic.DeMorgan.restrictProgram_value_castSucc_eq_constant {n g : ℕ} (source : Program signature (n + 1) g) (line : Line signature (n + 1) g) (selected : Fin (n + 1)) (fixedValue value : Bool) {sourceWire : Wire (n + 1) g} (constant : (restrictProgram selected fixedValue source).values sourceWire = ResidualValue.constant value) : (restrictProgram selected fixedValue (source.gate line)).values sourceWire.castSucc = ResidualValue.constant value

A constant value of an earlier source wire remains constant after one line.

theorem Algebraic.DeMorgan.restrictProgram_value_eq_constant_of_castSucc {n g : ℕ} (source : Program signature (n + 1) g) (line : Line signature (n + 1) g) (selected : Fin (n + 1)) (fixedValue value : Bool) {sourceWire : Wire (n + 1) g} (constant : (restrictProgram selected fixedValue (source.gate line)).values sourceWire.castSucc = ResidualValue.constant value) : (restrictProgram selected fixedValue source).values sourceWire = ResidualValue.constant value

Processing a later line cannot turn an earlier nonconstant value constant.

theorem Algebraic.DeMorgan.restrictProgram_deleted_of_constant_argument {n g : ℕ} (program : Program signature (n + 1) g) (selected : Fin (n + 1)) (fixedValue : Bool) (gate : Fin g) : ChargedGate program gate → (∃ (argument : Fin (signature.Arity (program.lines gate).op)) (value : Bool), (restrictProgram selected fixedValue program).values ((program.lines gate).wires argument) = ResidualValue.constant value) → gate ∈ (restrictProgram selected fixedValue program).deleted

A charged gate is deleted whenever one of its final residual arguments is constant.

theorem Algebraic.DeMorgan.restrictProgram_deleted_of_initial_constant_left {n g : ℕ} (program : Program signature (n + 1) g) (selected : Fin (n + 1)) (fixedValue : Bool) (initial : InitialChargedGate program) {value : Bool} (origin_eq : origins program initial.left = ResidualValue.constant value) : initial.gate ∈ (restrictProgram selected fixedValue program).deleted

An initial gate with a constant left origin is deleted by every restriction.

theorem Algebraic.DeMorgan.restrictProgram_deleted_of_initial_constant_right {n g : ℕ} (program : Program signature (n + 1) g) (selected : Fin (n + 1)) (fixedValue : Bool) (initial : InitialChargedGate program) {value : Bool} (origin_eq : origins program initial.right = ResidualValue.constant value) : initial.gate ∈ (restrictProgram selected fixedValue program).deleted

An initial gate with a constant right origin is deleted by every restriction.

theorem Algebraic.DeMorgan.restrictProgram_deleted_of_readsInput {n g : ℕ} (program : Program signature (n + 1) g) (selected : Fin (n + 1)) (fixedValue : Bool) {gate : Fin g} (reads : ReadsInput program gate selected) : gate ∈ (restrictProgram selected fixedValue program).deleted

Fixing an input deletes every charged gate that reads that input directly.

theorem Algebraic.DeMorgan.restrictProgram_deleted_of_readsOnlyInput {n g : ℕ} (program : Program signature (n + 1) g) (selected : Fin (n + 1)) (fixedValue : Bool) (input : Fin (n + 1)) (gate : Fin g) : ReadsOnlyInput program gate input → gate ∈ (restrictProgram selected fixedValue program).deleted

A charged gate whose arguments are literals of one input is always deleted.

theorem Algebraic.DeMorgan.restrictProgram_deleted_of_usesGate_constant {n g : ℕ} (program : Program signature (n + 1) g) (selected : Fin (n + 1)) (fixedValue : Bool) {source target : Fin g} (uses : UsesGate program source target) {value : Bool} (sourceConstant : (restrictProgram selected fixedValue program).values (Wire.gate source) = ResidualValue.constant value) : target ∈ (restrictProgram selected fixedValue program).deleted

A constant deleted source forces every charged successor to simplify.

structure Algebraic.DeMorgan.GateAnnihilation {n g : ℕ} (source : Program signature (n + 1) g) (selected : Fin (n + 1)) (gate : Fin g) : Type

A restriction that both deletes a chosen charged gate and makes its source value constant. The latter fact is what forces a charged successor to simplify.

• fixedValue : Bool

  Value assigned to the selected input.

• outputValue : Bool

  Constant value produced by the annihilated gate.

• deleted : gate ∈ (restrictProgram selected self.fixedValue source).deleted

  The gate is recorded among the deleted charged gates.

• value_eq : (restrictProgram selected self.fixedValue source).values (Wire.gate gate) = ResidualValue.constant self.outputValue

  Its source wire is represented by the stated constant.

theorem Algebraic.DeMorgan.annihilate_of_readsInput {n g : ℕ} (program : Program signature (n + 1) g) (selected : Fin (n + 1)) (gate : Fin g) : ReadsInput program gate selected → Nonempty (GateAnnihilation program selected gate)

Every charged gate directly reading an input admits an annihilating fix.