Semantic circuit normalization

Merging gates that compute the same function preserves wire values and does not increase circuit size.

def Cslib.Circuits.Program.Irredundant {σ : Signature} {n g : ℕ} {U : Type u_1} (p : Program σ n g) (i : Interpretation σ U) : Prop

Distinct gates compute distinct scalar functions. Gates may still duplicate input functions or be unused by the outputs.

def Cslib.Circuits.Circuit.Irredundant {σ : Signature} {n m : ℕ} {U : Type u_1} (c : Circuit σ n m) (i : Interpretation σ U) : Prop

A circuit is irredundant when its internal gates compute pairwise distinct functions.

theorem Cslib.Circuits.Program.exists_irredundant {σ : Signature} {n g : ℕ} {U : Type u_1} (p : Program σ n g) (i : Interpretation σ U) : ∃ k ≤ g, ∃ (q : Program σ n k) (ρ : Wire.Renaming n g k), (∀ (x : Fin n → U) (w : Wire n g), q.trace i x (ρ.apply w) = p.trace i x w) ∧ q.Irredundant i

A program can be rebuilt with distinct gate functions, preserving every wire's value.

theorem Cslib.Circuits.Circuit.exists_irredundant {σ : Signature} {n m : ℕ} {U : Type u_1} (c : Circuit σ n m) (i : Interpretation σ U) : ∃ (d : Circuit σ n m), d.eval i = c.eval i ∧ d.Irredundant i ∧ d.size ≤ c.size

Every circuit has an equivalent circuit with distinct gate functions and no more gates.