refactor(Circuit): preserve intermediate synthesis targets

Cslib/Computability/Circuit/Boolean/LupanovConstruction.lean

@@ -282,7 +282,7 @@ theorem synthesis (f : BooleanFunction (k + d)) (hs : 0 < s) :
   simp only [Finset.mem_univ, true_and, hsum] at h
   change Synthesis interpretation _ {table f s} _ at h
   rw [table_eq f hs] at h
-  simpa [bound, Nat.add_assoc] using minterms_synthesis.comp
+  simpa [bound, Nat.add_assoc] using minterms_synthesis.trans
     (h.mono Set.subset_union_right Set.Subset.rfl le_rfl)
 
 end Cslib.Circuits.Boolean.Lupanov

Cslib/Computability/Circuit/Boolean/Synthesis.lean

@@ -54,38 +54,30 @@ theorem exists_mem (indices : Finset ι) (f : ι → BooleanFunction n) (cost :
     (h : ∀ i ∈ indices, Synthesis interpretation s {f i} (cost i)) :
     Synthesis interpretation s {fun x => decide (∃ i ∈ indices, f i x = true)}
       ((∑ i ∈ indices, (cost i + 1)) + 1) := by
-  have hop (f g : BooleanFunction n) :
-      Synthesis interpretation {f, g} {fun x => f x || g x} 1 := by
-    simpa [interpretation] using gate (I := interpretation) (s := {f, g}) .or
-      (fun i => if i.val = 0 then f else g) (fun i => by split <;> simp)
   have heq : (fun x => indices.fold Bool.or false (fun i => f i x)) =
       (fun x => decide (∃ i ∈ indices, f i x = true)) := by
     funext x
     apply Bool.eq_iff_iff.mpr
     simpa using Finset.fold_op_rel_iff_or (op := Bool.or)
       (r := fun _ v : Bool => v = true) (by simp) (c := true)
       (s := indices) (f := fun i => f i x) (b := false)
-  simpa only [heq] using finset_fold Bool.or 1 hop indices f cost
-    (fun _ => false) (const false) h
+  simpa only [heq] using finset_fold Bool.or 1
+    (fun _ _ => (of_mem (by simp)).or (of_mem (by simp))) indices (const false) h
 
 /-- Conjoin a finite family of functions. The extra gate supplies the empty conjunction. -/
 theorem forall_mem (indices : Finset ι) (f : ι → BooleanFunction n) (cost : ι → ℕ)
     (h : ∀ i ∈ indices, Synthesis interpretation s {f i} (cost i)) :
     Synthesis interpretation s {fun x => decide (∀ i ∈ indices, f i x = true)}
       ((∑ i ∈ indices, (cost i + 1)) + 1) := by
-  have hop (f g : BooleanFunction n) :
-      Synthesis interpretation {f, g} {fun x => f x && g x} 1 := by
-    simpa [interpretation] using gate (I := interpretation) (s := {f, g}) .and
-      (fun i => if i.val = 0 then f else g) (fun i => by split <;> simp)
   have heq : (fun x => indices.fold Bool.and true (fun i => f i x)) =
       (fun x => decide (∀ i ∈ indices, f i x = true)) := by
     funext x
     apply Bool.eq_iff_iff.mpr
     simpa using Finset.fold_op_rel_iff_and (op := Bool.and)
       (r := fun _ v : Bool => v = true) (by simp) (c := true)
       (s := indices) (f := fun i => f i x) (b := true)
-  simpa only [heq] using finset_fold Bool.and 1 hop indices f cost
-    (fun _ => true) (const true) h
+  simpa only [heq] using finset_fold Bool.and 1
+    (fun _ _ => (of_mem (by simp)).and (of_mem (by simp))) indices (const true) h
 
 end Synthesis
 
@@ -98,7 +90,7 @@ theorem synthesis_minterm {k : ℕ} (wires : Fin k → Fin n) (value : Fin k →
   have literal (i : Fin k) :
       Synthesis interpretation (inputs n) {fun x => decide (x (wires i) = value i)} 1 := by
     have h : Synthesis interpretation (inputs n) {fun x => x (wires i)} 0 :=
-      Synthesis.of_subset (Set.singleton_subset_iff.mpr ⟨wires i, rfl⟩)
+      Synthesis.of_mem ⟨wires i, rfl⟩
     cases hv : value i
     · simpa [hv] using h.not
     · simpa [hv] using h.mono Set.Subset.rfl Set.Subset.rfl (by omega : 0 ≤ 1)

Cslib/Computability/Circuit/Synthesis.lean

@@ -20,8 +20,10 @@ public import Mathlib.Data.Set.Lattice.Bounded
 starting program remains available, so successive constructions can share intermediate results.
 The signature and its carrier are arbitrary; neither needs to be finite or decidable.
 
-The core rules compose bounds, combine finite families, and apply operations of the signature.
-The fold rules accept a bound for combining two arguments, which may itself use several gates.
+The core rules compose bounds, combine finite families, and apply operations of the signature,
+either to functions that are already available or to functions synthesized in turn. Composition
+keeps everything built along the way available to later steps. The fold rules accept a bound
+for combining two arguments, which may itself use several gates.
 `Synthesis.exists_circuit_family` selects any finite family of outputs without adding gates;
 `Synthesis.exists_circuit` specializes this to a single output.
 -/
@@ -79,28 +81,35 @@ variable {s t t₁ : Set ((Fin n → U) → U)} {a b : ℕ} {f g : (Fin n → U)
 theorem of_subset (h : t ⊆ s) : Synthesis I s t 0 :=
   fun g p hp => ⟨g, p, by omega, Set.Subset.rfl, h.trans hp⟩
 
+/-- An available function requires no additional gates. -/
+theorem of_mem (hf : f ∈ s) : Synthesis I s {f} 0 :=
+  of_subset (Set.singleton_subset_iff.mpr hf)
+
 /-- Enlarge the source family, narrow the target family, or increase the budget. -/
 theorem mono (h : Synthesis I s t a) {s' t' : Set ((Fin n → U) → U)}
     (hs : s ⊆ s') (ht : t' ⊆ t) (hab : a ≤ b) : Synthesis I s' t' b := by
   intro g₁ p hp
   obtain ⟨g₂, q, hq, hkeep, hout⟩ := h g₁ p (hs.trans hp)
   exact ⟨g₂, q, by omega, hkeep, ht.trans hout⟩
 
-/-- Successive constructions add their gate budgets. -/
+/-- Successive constructions add their gate budgets. The second construction may use the
+targets of the first, and both target families remain available. -/
 theorem comp (h : Synthesis I s t a) (h' : Synthesis I (s ∪ t) t₁ b) :
-    Synthesis I s t₁ (a + b) := by
+    Synthesis I s (t ∪ t₁) (a + b) := by
   intro g₁ p hp
   obtain ⟨g₂, q, hq, hpq, ht⟩ := h g₁ p hp
   obtain ⟨g₃, r, hr, hqr, hu⟩ := h' g₂ q (Set.union_subset (hp.trans hpq) ht)
-  exact ⟨g₃, r, by omega, hpq.trans hqr, hu⟩
+  exact ⟨g₃, r, by omega, hpq.trans hqr, Set.union_subset (ht.trans hqr) hu⟩
+
+/-- Successive constructions, keeping only the final targets. -/
+theorem trans (h : Synthesis I s t a) (h' : Synthesis I (s ∪ t) t₁ b) :
+    Synthesis I s t₁ (a + b) :=
+  (h.comp h').mono Set.Subset.rfl Set.subset_union_right le_rfl
 
 /-- Combine two target families, preserving the first while constructing the second. -/
 theorem union (h : Synthesis I s t a) (h' : Synthesis I s t₁ b) :
-    Synthesis I s (t ∪ t₁) (a + b) := by
-  intro g₁ p hp
-  obtain ⟨g₂, q, hq, hpq, ht⟩ := h g₁ p hp
-  obtain ⟨g₃, r, hr, hqr, hu⟩ := h' g₂ q (hp.trans hpq)
-  exact ⟨g₃, r, by omega, hpq.trans hqr, Set.union_subset (ht.trans hqr) hu⟩
+    Synthesis I s (t ∪ t₁) (a + b) :=
+  h.comp (h'.mono Set.subset_union_left Set.Subset.rfl le_rfl)
 
 /-- Synthesize an operation whose arguments are already available. -/
 theorem gate (op : σ.Op) (args : Fin (σ.Arity op) → (Fin n → U) → U)
@@ -148,7 +157,7 @@ theorem family [Fintype ι] (f : ι → (Fin n → U) → U) (cost : ι → ℕ)
 theorem gate_of_syntheses (op : σ.Op) (args : Fin (σ.Arity op) → (Fin n → U) → U)
     (cost : Fin (σ.Arity op) → ℕ) (h : ∀ i, Synthesis I s {args i} (cost i)) :
     Synthesis I s {fun x => I op (fun i => args i x)} ((∑ i, cost i) + 1) :=
-  (family args cost h).comp (gate op args (fun i => Set.mem_union_right _ ⟨i, rfl⟩))
+  (family args cost h).trans (gate op args (fun i => Set.mem_union_right _ ⟨i, rfl⟩))
 
 /-- A nullary operation supplies its interpreted constant with one gate. -/
 theorem nullary (op : σ.Op) (arity : σ.Arity op = 0) :
@@ -159,22 +168,22 @@ theorem nullary (op : σ.Op) (arity : σ.Arity op = 0) :
 In particular, this applies a unary operation. -/
 theorem unary (h : Synthesis I s {f} a) (op : σ.Op) :
     Synthesis I s {fun x => I op (fun _ => f x)} (a + 1) :=
-  h.comp (gate op (fun _ => f) (by simp))
+  h.trans (gate op (fun _ => f) (by simp))
 
 /-- Feed `f` to argument zero and `g` to the remaining arguments, using one further gate.
 For a binary operation, these are its two arguments. -/
 theorem binary (hf : Synthesis I s {f} a) (hg : Synthesis I s {g} b) (op : σ.Op) :
     Synthesis I s {fun x => I op (fun i => if i.val = 0 then f x else g x)}
       (a + b + 1) := by
-  simpa only [ite_apply] using (hf.union hg).comp
+  simpa only [ite_apply] using (hf.union hg).trans
     (gate op (fun i => if i.val = 0 then f else g) (fun i => by split <;> simp))
 
 /-- Apply a synthesis bound to two previously synthesized arguments. The combining
 construction can use several gates and can reuse either argument. -/
 theorem combine {result : (Fin n → U) → U} {c : ℕ}
     (hf : Synthesis I s {f} a) (hg : Synthesis I s {g} b)
     (h : Synthesis I {f, g} {result} c) : Synthesis I s {result} (a + b + c) := by
-  apply (hf.union hg).comp
+  apply (hf.union hg).trans
   apply h.mono ?_ Set.Subset.rfl le_rfl
   intro k hk
   exact Set.mem_union_right _ (by simpa [or_comm] using hk)
@@ -184,8 +193,8 @@ combining operation. The seed and the combining construction have their own gate
 theorem foldr (op : U → U → U) (combineCost : ℕ)
     (hop : ∀ f g : (Fin n → U) → U,
       Synthesis I {f, g} {fun x => op (f x) (g x)} combineCost)
-    (indices : List ι) (f : ι → (Fin n → U) → U) (cost : ι → ℕ)
-    (seed : (Fin n → U) → U) (hseed : Synthesis I s {seed} a)
+    (indices : List ι) {f : ι → (Fin n → U) → U} {cost : ι → ℕ}
+    {seed : (Fin n → U) → U} (hseed : Synthesis I s {seed} a)
     (h : ∀ i ∈ indices, Synthesis I s {f i} (cost i)) :
     Synthesis I s {fun x => indices.foldr (fun i acc => op (f i x) acc) (seed x)}
       ((indices.map fun i => cost i + combineCost).sum + a) := by
@@ -202,8 +211,8 @@ several gates. -/
 theorem finset_fold (op : U → U → U) [Std.Commutative op] [Std.Associative op]
     (combineCost : ℕ) (hop : ∀ f g : (Fin n → U) → U,
       Synthesis I {f, g} {fun x => op (f x) (g x)} combineCost)
-    (indices : Finset ι) (f : ι → (Fin n → U) → U) (cost : ι → ℕ)
-    (seed : (Fin n → U) → U) (hseed : Synthesis I s {seed} a)
+    (indices : Finset ι) {f : ι → (Fin n → U) → U} {cost : ι → ℕ}
+    {seed : (Fin n → U) → U} (hseed : Synthesis I s {seed} a)
     (h : ∀ i ∈ indices, Synthesis I s {f i} (cost i)) :
     Synthesis I s {fun x => indices.fold op (seed x) (fun i => f i x)}
       ((∑ i ∈ indices, (cost i + combineCost)) + a) := by

CslibTests/BooleanCircuits.lean

@@ -36,14 +36,14 @@ example : ¬ (Circuit.id signature 1).Computes interpretation (fun x => !x 0) :=
 
 private def conjunction : BooleanFunction 2 := fun x => x 0 && x 1
 
+private theorem conjunction_synthesis : Synthesis interpretation (inputs 2) {conjunction} 1 :=
+  Synthesis.gate (I := interpretation) .and (fun i x => x i) (fun i => ⟨i, rfl⟩)
+
 example : ∃ g ≤ 2, ∃ c : Circuit signature 2 g 2,
     ∀ x, c.eval interpretation x 0 = conjunction x ∧
       c.eval interpretation x 1 = !conjunction x := by
-  have hand : Synthesis interpretation (inputs 2) {conjunction} 1 :=
-    Synthesis.gate (I := interpretation) .and (fun i x => x i) (fun i => ⟨i, rfl⟩)
-  have hkeep : Synthesis interpretation (inputs 2 ∪ {conjunction}) {conjunction} 0 :=
-    Synthesis.of_subset Set.subset_union_right
-  have h := hand.comp (hkeep.union hkeep.not)
+  have h := conjunction_synthesis.comp
+    (Synthesis.of_mem (Set.mem_union_right _ (Set.mem_singleton conjunction))).not
   have hout : Synthesis interpretation (inputs 2)
       (Set.range fun i : Fin 2 => if i = 0 then conjunction else fun x => !conjunction x) 2 :=
     h.mono Set.Subset.rfl (by rintro _ ⟨i, rfl⟩; dsimp only; split <;> simp) le_rfl

CslibTests/Synthesis.lean

@@ -23,7 +23,7 @@ universe v u
 example {σ : Signature.{v}} {U : Type u} (I : Interpretation σ U) {n : ℕ} (i : Fin n) :
     ∃ g ≤ 0, ∃ c : Circuit σ n g 1, c.Computes I (fun x => x i) := by
   have h : Synthesis I (inputs n) {fun x => x i} 0 :=
-    Synthesis.of_subset (Set.singleton_subset_iff.mpr ⟨i, rfl⟩)
+    Synthesis.of_mem ⟨i, rfl⟩
   exact h.exists_circuit
 
 example {σ : Signature.{v}} {U : Type u} (I : Interpretation σ U) :
@@ -55,17 +55,17 @@ def interpretation : Interpretation signature ℕ
 
 private theorem projection {n : ℕ} (i : Fin n) :
     Synthesis interpretation (inputs n) {fun x => x i} 0 :=
-  Synthesis.of_subset (Set.singleton_subset_iff.mpr ⟨i, rfl⟩)
+  Synthesis.of_mem ⟨i, rfl⟩
 
 private theorem add_available {n : ℕ} (f g : (Fin n → ℕ) → ℕ) :
     Synthesis interpretation {f, g} {fun x => f x + g x} 1 := by
-  simpa [interpretation] using Synthesis.gate (I := interpretation) (s := {f, g}) .add
-    (fun i => if i.val = 0 then f else g) (fun i => by split <;> simp)
+  exact Synthesis.binary (I := interpretation)
+    (Synthesis.of_mem (by simp)) (Synthesis.of_mem (by simp)) .add
 
 private theorem sub_available {n : ℕ} (f g : (Fin n → ℕ) → ℕ) :
     Synthesis interpretation {f, g} {fun x => f x - g x} 1 := by
-  simpa [interpretation] using Synthesis.gate (I := interpretation) (s := {f, g}) .sub
-    (fun i => if i.val = 0 then f else g) (fun i => by split <;> simp)
+  exact Synthesis.binary (I := interpretation)
+    (Synthesis.of_mem (by simp)) (Synthesis.of_mem (by simp)) .sub
 
 example (value : ℕ) :
     ∃ g ≤ 1, ∃ c : Circuit signature 0 g 1, c.Computes interpretation (fun _ => value) :=
@@ -88,13 +88,11 @@ example : ∃ g ≤ 2, ∃ c : Circuit signature 2 g 3,
     ∀ x i, c.eval interpretation x i = sharedOutputs i x := by
   have hproduct : Synthesis interpretation (inputs 2) {product} 1 :=
     Synthesis.gate (I := interpretation) .mul (fun i x => x i) (fun i => ⟨i, rfl⟩)
-  have hkeep : Synthesis interpretation (inputs 2 ∪ {product}) {product} 0 :=
-    Synthesis.of_subset Set.subset_union_right
-  have hinput : Synthesis interpretation (inputs 2 ∪ {product}) {fun x => x 0} 0 :=
-    (projection 0).mono Set.subset_union_left Set.Subset.rfl le_rfl
   have hsum : Synthesis interpretation (inputs 2 ∪ {product}) {fun x => product x + x 0} 1 := by
-    simpa [interpretation] using hkeep.binary hinput .add
-  have h := hproduct.comp (hkeep.union hsum)
+    exact Synthesis.binary (I := interpretation) (s := inputs 2 ∪ {product})
+      (Synthesis.of_mem (Set.mem_union_right _ (Set.mem_singleton product)))
+      (Synthesis.of_mem (Set.mem_union_left _ ⟨0, rfl⟩)) .add
+  have h := hproduct.comp hsum
   have hout : Synthesis interpretation (inputs 2) (Set.range sharedOutputs) 2 :=
     h.mono Set.Subset.rfl (by rintro _ ⟨i, rfl⟩; unfold sharedOutputs; split <;> simp) le_rfl
   exact hout.exists_circuit_family
@@ -103,24 +101,21 @@ example : ∃ g ≤ 2, ∃ c : Circuit signature 2 g 3,
 example : ∃ g ≤ 2, ∃ c : Circuit signature 2 g 1,
     c.Computes interpretation (fun x => x 0 - (x 1 - x 0)) := by
   have h := Synthesis.foldr (I := interpretation) (· - ·) 1 sub_available
-    ([0, 1] : List (Fin 2)) (fun i x => x i) (fun _ => 0)
-    (fun x => x 0) (projection 0) (fun i _ => projection i)
+    ([0, 1] : List (Fin 2)) (projection 0) (fun i _ => projection i)
   simpa using h.exists_circuit
 
 -- A finite-set fold may start from an available, nonconstant seed.
 example : ∃ g ≤ 2, ∃ c : Circuit signature 2 g 1,
     c.Computes interpretation
       (fun x => Finset.univ.fold (· + ·) (x 0) (fun i : Fin 2 => x i)) := by
   have h := Synthesis.finset_fold (I := interpretation) (· + ·) 1 add_available
-    (Finset.univ : Finset (Fin 2)) (fun i x => x i) (fun _ => 0)
-    (fun x => x 0) (projection 0) (fun i _ => projection i)
+    (Finset.univ : Finset (Fin 2)) (projection 0) (fun i _ => projection i)
   simpa using h.exists_circuit
 
 example : ∃ g ≤ 0, ∃ c : Circuit signature 1 g 1,
     c.Computes interpretation (fun x => x 0) := by
   have h := Synthesis.finset_fold (I := interpretation) (· + ·) 1 add_available
-    (∅ : Finset (Fin 1)) (fun i x => x i) (fun _ => 0)
-    (fun x => x 0) (projection 0) (fun i _ => projection i)
+    (∅ : Finset (Fin 1)) (projection 0) (fun i _ => projection i)
   simpa using h.exists_circuit
 
 end CslibTests.Synthesis