From c41489baadd8876d7802bea7635a5f3babc1564b Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 21 Sep 2026 15:03:20 -0400 Subject: [PATCH 1/2] refactor(Circuit): preserve intermediate synthesis targets Keep both target families when composing synthesis bounds, and provide trans for retaining only the final targets. Add helpers for available unary and binary arguments, infer fold data from their proofs, and update shared-output examples and Lupanov synthesis. --- .../Circuit/Boolean/LupanovConstruction.lean | 2 +- .../Circuit/Boolean/Synthesis.lean | 38 +++++++---- Cslib/Computability/Circuit/Synthesis.lean | 67 ++++++++++++------- CslibTests/BooleanCircuits.lean | 10 +-- CslibTests/Synthesis.lean | 25 +++---- 5 files changed, 85 insertions(+), 57 deletions(-) diff --git a/Cslib/Computability/Circuit/Boolean/LupanovConstruction.lean b/Cslib/Computability/Circuit/Boolean/LupanovConstruction.lean index 9b006964f..a78bfe0d3 100644 --- a/Cslib/Computability/Circuit/Boolean/LupanovConstruction.lean +++ b/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 diff --git a/Cslib/Computability/Circuit/Boolean/Synthesis.lean b/Cslib/Computability/Circuit/Boolean/Synthesis.lean index a9e021a6c..4f4053e2a 100644 --- a/Cslib/Computability/Circuit/Boolean/Synthesis.lean +++ b/Cslib/Computability/Circuit/Boolean/Synthesis.lean @@ -34,6 +34,30 @@ variable {s : Set (BooleanFunction n)} {a b : ℕ} {f g : BooleanFunction n} theorem const (value : Bool) : Synthesis interpretation s {fun _ => value} 1 := nullary (I := interpretation) (.const value) rfl +/-- Negate an available function with one gate. -/ +theorem not_of_mem (hf : f ∈ s) : Synthesis interpretation s {fun x => !f x} 1 := + unary_of_mem (I := interpretation) hf .not + +/-- Conjoin two available functions with one gate. -/ +theorem and_of_mem (hf : f ∈ s) (hg : g ∈ s) : + Synthesis interpretation s {fun x => f x && g x} 1 := by + simpa [interpretation] using binary_of_mem (I := interpretation) hf hg .and + +/-- Disjoin two available functions with one gate. -/ +theorem or_of_mem (hf : f ∈ s) (hg : g ∈ s) : + Synthesis interpretation s {fun x => f x || g x} 1 := by + simpa [interpretation] using binary_of_mem (I := interpretation) hf hg .or + +/-- Conjoin a pair of functions with one gate: the combining step for `forall_mem`. -/ +theorem and_pair (f g : BooleanFunction n) : + Synthesis interpretation {f, g} {fun x => f x && g x} 1 := + and_of_mem (by simp) (by simp) + +/-- Disjoin a pair of functions with one gate: the combining step for `exists_mem`. -/ +theorem or_pair (f g : BooleanFunction n) : + Synthesis interpretation {f, g} {fun x => f x || g x} 1 := + or_of_mem (by simp) (by simp) + /-- Apply negation to a synthesized function. -/ theorem not (h : Synthesis interpretation s {f} a) : Synthesis interpretation s {fun x => !f x} (a + 1) := @@ -54,10 +78,6 @@ 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 @@ -65,18 +85,13 @@ theorem exists_mem (indices : Finset ι) (f : ι → BooleanFunction n) (cost : 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 or_pair 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 @@ -84,8 +99,7 @@ theorem forall_mem (indices : Finset ι) (f : ι → BooleanFunction n) (cost : 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 and_pair indices (const true) h end Synthesis diff --git a/Cslib/Computability/Circuit/Synthesis.lean b/Cslib/Computability/Circuit/Synthesis.lean index 7362f013d..6b5c3fef4 100644 --- a/Cslib/Computability/Circuit/Synthesis.lean +++ b/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. -/ @@ -86,21 +88,24 @@ theorem mono (h : Synthesis I s t a) {s' t' : Set ((Fin n → U) → U)} 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,33 +153,49 @@ 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) : Synthesis I s {fun _ => I op (fun i => Fin.elim0 (Fin.cast arity i))} 1 := gate op (fun i _ => Fin.elim0 (Fin.cast arity i)) (fun i => Fin.elim0 (Fin.cast arity i)) -/-- Feed a synthesized function to every argument of an operation, using one further gate. -In particular, this applies a unary operation. -/ +/-- Feed an available function to every argument of an operation, using one gate. In +particular, this applies a unary operation. -/ +theorem unary_of_mem (hf : f ∈ s) (op : σ.Op) : + Synthesis I s {fun x => I op (fun _ => f x)} 1 := + gate op (fun _ => f) (fun _ => hf) + +/-- Feed a synthesized function to every argument of an operation, using one further gate. -/ 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 (unary_of_mem (Set.mem_union_right _ (Set.mem_singleton f)) op) -/-- Feed `f` to argument zero and `g` to the remaining arguments, using one further gate. +/-- Feed available `f` to argument zero and `g` to the remaining arguments, using one gate. For a binary operation, these are its two arguments. -/ +theorem binary_of_mem (hf : f ∈ s) (hg : g ∈ s) (op : σ.Op) : + Synthesis I s {fun x => I op (fun i => if i.val = 0 then f x else g x)} 1 := by + simpa only [ite_apply] using + gate op (fun i => if i.val = 0 then f else g) (fun i => by split <;> assumption) + +/-- Apply an operation to a pair of functions with one gate, `f` at argument zero and `g` +elsewhere. This is the shape of the combining step in `foldr` and `finset_fold`. -/ +theorem binary_pair (op : σ.Op) (f g : (Fin n → U) → U) : + Synthesis I {f, g} {fun x => I op (fun i => if i.val = 0 then f x else g x)} 1 := + binary_of_mem (by simp) (by simp) op + +/-- Feed `f` to argument zero and `g` to the remaining arguments, using one further gate. -/ 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 - (gate op (fun i => if i.val = 0 then f else g) (fun i => by split <;> simp)) + (a + b + 1) := + (hf.union hg).trans (binary_of_mem (by simp) (by simp) op) /-- 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 +205,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 +223,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 diff --git a/CslibTests/BooleanCircuits.lean b/CslibTests/BooleanCircuits.lean index 6a8545347..b743a2eee 100644 --- a/CslibTests/BooleanCircuits.lean +++ b/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.not_of_mem (Set.mem_union_right _ (Set.mem_singleton conjunction))) 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 diff --git a/CslibTests/Synthesis.lean b/CslibTests/Synthesis.lean index de05f1718..41358b6d0 100644 --- a/CslibTests/Synthesis.lean +++ b/CslibTests/Synthesis.lean @@ -59,13 +59,11 @@ private theorem projection {n : ℕ} (i : Fin n) : 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) + simpa [interpretation] using Synthesis.binary_pair (I := interpretation) .add f g 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) + simpa [interpretation] using Synthesis.binary_pair (I := interpretation) .sub f g example (value : ℕ) : ∃ g ≤ 1, ∃ c : Circuit signature 0 g 1, c.Computes interpretation (fun _ => value) := @@ -88,13 +86,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) + simpa [interpretation] using Synthesis.binary_of_mem (I := interpretation) + (s := inputs 2 ∪ {product}) (Set.mem_union_right _ (Set.mem_singleton product)) + (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,8 +99,7 @@ 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. @@ -112,15 +107,13 @@ 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 From cd36371a552ada1e97c0ee25a9b8df5fac915f53 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 21 Sep 2026 23:49:28 -0400 Subject: [PATCH 2/2] refactor(Circuit): reuse zero-cost synthesis for available functions Replace the eight membership and pair gate helpers with Synthesis.of_mem and the existing operation combinators. Preserve intermediate targets in composition and inferred fold arguments while simplifying Boolean folds and shared-output examples. --- .../Circuit/Boolean/Synthesis.lean | 32 +++-------------- Cslib/Computability/Circuit/Synthesis.lean | 34 ++++++------------- CslibTests/BooleanCircuits.lean | 2 +- CslibTests/Synthesis.lean | 16 +++++---- 4 files changed, 26 insertions(+), 58 deletions(-) diff --git a/Cslib/Computability/Circuit/Boolean/Synthesis.lean b/Cslib/Computability/Circuit/Boolean/Synthesis.lean index 4f4053e2a..914071008 100644 --- a/Cslib/Computability/Circuit/Boolean/Synthesis.lean +++ b/Cslib/Computability/Circuit/Boolean/Synthesis.lean @@ -34,30 +34,6 @@ variable {s : Set (BooleanFunction n)} {a b : ℕ} {f g : BooleanFunction n} theorem const (value : Bool) : Synthesis interpretation s {fun _ => value} 1 := nullary (I := interpretation) (.const value) rfl -/-- Negate an available function with one gate. -/ -theorem not_of_mem (hf : f ∈ s) : Synthesis interpretation s {fun x => !f x} 1 := - unary_of_mem (I := interpretation) hf .not - -/-- Conjoin two available functions with one gate. -/ -theorem and_of_mem (hf : f ∈ s) (hg : g ∈ s) : - Synthesis interpretation s {fun x => f x && g x} 1 := by - simpa [interpretation] using binary_of_mem (I := interpretation) hf hg .and - -/-- Disjoin two available functions with one gate. -/ -theorem or_of_mem (hf : f ∈ s) (hg : g ∈ s) : - Synthesis interpretation s {fun x => f x || g x} 1 := by - simpa [interpretation] using binary_of_mem (I := interpretation) hf hg .or - -/-- Conjoin a pair of functions with one gate: the combining step for `forall_mem`. -/ -theorem and_pair (f g : BooleanFunction n) : - Synthesis interpretation {f, g} {fun x => f x && g x} 1 := - and_of_mem (by simp) (by simp) - -/-- Disjoin a pair of functions with one gate: the combining step for `exists_mem`. -/ -theorem or_pair (f g : BooleanFunction n) : - Synthesis interpretation {f, g} {fun x => f x || g x} 1 := - or_of_mem (by simp) (by simp) - /-- Apply negation to a synthesized function. -/ theorem not (h : Synthesis interpretation s {f} a) : Synthesis interpretation s {fun x => !f x} (a + 1) := @@ -85,7 +61,8 @@ theorem exists_mem (indices : Finset ι) (f : ι → BooleanFunction n) (cost : 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 or_pair indices (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 : ι → ℕ) @@ -99,7 +76,8 @@ theorem forall_mem (indices : Finset ι) (f : ι → BooleanFunction n) (cost : 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 and_pair indices (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 @@ -112,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) diff --git a/Cslib/Computability/Circuit/Synthesis.lean b/Cslib/Computability/Circuit/Synthesis.lean index 6b5c3fef4..7c4591837 100644 --- a/Cslib/Computability/Circuit/Synthesis.lean +++ b/Cslib/Computability/Circuit/Synthesis.lean @@ -81,6 +81,10 @@ 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 @@ -160,35 +164,19 @@ theorem nullary (op : σ.Op) (arity : σ.Arity op = 0) : Synthesis I s {fun _ => I op (fun i => Fin.elim0 (Fin.cast arity i))} 1 := gate op (fun i _ => Fin.elim0 (Fin.cast arity i)) (fun i => Fin.elim0 (Fin.cast arity i)) -/-- Feed an available function to every argument of an operation, using one gate. In -particular, this applies a unary operation. -/ -theorem unary_of_mem (hf : f ∈ s) (op : σ.Op) : - Synthesis I s {fun x => I op (fun _ => f x)} 1 := - gate op (fun _ => f) (fun _ => hf) - -/-- Feed a synthesized function to every argument of an operation, using one further gate. -/ +/-- Feed a synthesized function to every argument of an operation, using one further gate. +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.trans (unary_of_mem (Set.mem_union_right _ (Set.mem_singleton f)) op) + h.trans (gate op (fun _ => f) (by simp)) -/-- Feed available `f` to argument zero and `g` to the remaining arguments, using one gate. +/-- 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_of_mem (hf : f ∈ s) (hg : g ∈ s) (op : σ.Op) : - Synthesis I s {fun x => I op (fun i => if i.val = 0 then f x else g x)} 1 := by - simpa only [ite_apply] using - gate op (fun i => if i.val = 0 then f else g) (fun i => by split <;> assumption) - -/-- Apply an operation to a pair of functions with one gate, `f` at argument zero and `g` -elsewhere. This is the shape of the combining step in `foldr` and `finset_fold`. -/ -theorem binary_pair (op : σ.Op) (f g : (Fin n → U) → U) : - Synthesis I {f, g} {fun x => I op (fun i => if i.val = 0 then f x else g x)} 1 := - binary_of_mem (by simp) (by simp) op - -/-- Feed `f` to argument zero and `g` to the remaining arguments, using one further gate. -/ 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) := - (hf.union hg).trans (binary_of_mem (by simp) (by simp) op) + (a + b + 1) := by + 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. -/ diff --git a/CslibTests/BooleanCircuits.lean b/CslibTests/BooleanCircuits.lean index b743a2eee..f735d7383 100644 --- a/CslibTests/BooleanCircuits.lean +++ b/CslibTests/BooleanCircuits.lean @@ -43,7 +43,7 @@ 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 h := conjunction_synthesis.comp - (Synthesis.not_of_mem (Set.mem_union_right _ (Set.mem_singleton conjunction))) + (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 diff --git a/CslibTests/Synthesis.lean b/CslibTests/Synthesis.lean index 41358b6d0..63293fc91 100644 --- a/CslibTests/Synthesis.lean +++ b/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,15 +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.binary_pair (I := interpretation) .add f g + 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.binary_pair (I := interpretation) .sub f g + 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) := @@ -87,9 +89,9 @@ example : ∃ g ≤ 2, ∃ c : Circuit signature 2 g 3, have hproduct : Synthesis interpretation (inputs 2) {product} 1 := Synthesis.gate (I := interpretation) .mul (fun i x => x i) (fun i => ⟨i, rfl⟩) have hsum : Synthesis interpretation (inputs 2 ∪ {product}) {fun x => product x + x 0} 1 := by - simpa [interpretation] using Synthesis.binary_of_mem (I := interpretation) - (s := inputs 2 ∪ {product}) (Set.mem_union_right _ (Set.mem_singleton product)) - (Set.mem_union_left _ ⟨0, rfl⟩) .add + 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