Evaluation lemmas for circuit cuts

@[simp]

theorem Cslib.Circuits.Program.evalCut_mem {σ : Signature} {n g : ℕ} {U : Type u_1} (p : Program σ n g) (cut : Finset (Fin g)) (I : Interpretation σ U) (x : Fin n → U) (guess : ↥cut → U) (j : ↥cut) : p.evalCut cut I x guess ↑j = guess j

Evaluation at a selected gate reads the guess.

theorem Cslib.Circuits.Program.evalCut_not_mem {σ : Signature} {n g : ℕ} {U : Type u_1} (p : Program σ n g) (cut : Finset (Fin g)) (I : Interpretation σ U) (x : Fin n → U) (guess : ↥cut → U) (j : Fin g) (hj : j ∉ cut) : p.evalCut cut I x guess j = (p.lines j).eval I x (p.evalCut cut I x guess)

An unselected gate is evaluated from its argument wires.

theorem Cslib.Circuits.Program.evalCut_eq_eval_of_agree {σ : Signature} {n g : ℕ} {U : Type u_1} (p : Program σ n g) (cut : Finset (Fin g)) (I : Interpretation σ U) (x : Fin n → U) (guess : ↥cut → U) (agree : ∀ (j : ↥cut), guess j = p.eval I x ↑j) : p.evalCut cut I x guess = p.eval I x

Supplying the actual values at the cut preserves the evaluation everywhere.