refactor(Circuit): generalize FanIn input support bounds to weighted gate costs (#884)

Complexity/Computability/Circuit/Boolean/BinaryCost.lean

@@ -7,6 +7,7 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
+import Complexity.Computability.Circuit.FanIn
 public import Complexity.Computability.Circuit.Simulation
 public import Complexity.Computability.Circuit.Support
 public import Cslib.Computability.Circuit.Boolean.Basic
@@ -142,102 +143,12 @@ theorem Program.cost_binaryCost_le (p : Program Boolean.signature n g) :
     p.cost Boolean.binaryCost ≤ g :=
   (p.cost_le_mul Boolean.binaryCost_le_one).trans_eq (one_mul g)
 
-private theorem wire_castSucc_injective' :
-    Function.Injective (Wire.castSucc : Wire n g → Wire n (g + 1)) := by
-  intro a b h
-  cases a <;> cases b <;> simp_all [Wire.castSucc]
-
 /-- In a De Morgan program, the number of inputs supporting a frontier of wires is at most the size
 of the frontier plus the number of binary (AND/OR) gates in the program. -/
 theorem Program.card_biUnion_wireSupport_le_cost_binaryCost
     (p : Program signature n g) (frontier : Finset (Wire n g)) :
-    (frontier.biUnion p.wireSupport).card ≤ frontier.card + p.cost binaryCost := by
-  induction p with
-  | empty =>
-    simp only [Program.cost_empty, Nat.add_zero]
-    have hsub : frontier.biUnion (Program.empty (σ := signature)).wireSupport ⊆
-        Finset.univ.filter fun i : Fin n => Wire.input i ∈ frontier := by
-      intro i hi
-      rw [Finset.mem_biUnion] at hi
-      obtain ⟨w, hw, hi⟩ := hi
-      cases w with
-      | input j =>
-        simp only [Program.wireSupport_input, Finset.mem_singleton] at hi
-        subst hi
-        exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, hw⟩
-      | gate j => exact j.elim0
-    refine (Finset.card_le_card hsub).trans ?_
-    apply Finset.card_le_card_of_injOn Wire.input
-    · intro i hi
-      simpa using hi
-    · intro a _ b _ h
-      cases h
-      rfl
-  | @gate g p line ih =>
-    let prior := Finset.univ.filter fun w : Wire n g => w.castSucc ∈ frontier
-    let lineInputs := Finset.univ.image line.wires
-    let opened :=
-      if Wire.gate (Fin.last g) ∈ frontier then prior ∪ lineInputs else prior
-    have hsub : frontier.biUnion (p.gate line).wireSupport ⊆ opened.biUnion p.wireSupport := by
-      intro i hi
-      rw [Finset.mem_biUnion] at hi ⊢
-      obtain ⟨w, hw, hi⟩ := hi
-      revert hw hi
-      induction w using Wire.lastCases with
-      | last =>
-        intro hlast hi
-        rw [Program.wireSupport_gate_last] at hi
-        obtain ⟨arg, hi⟩ := Line.mem_inputSupport.mp hi
-        exact ⟨line.wires arg, by simp [opened, lineInputs, hlast], hi⟩
-      | castSucc w =>
-        intro hw hi
-        rw [Program.wireSupport_gate_castSucc] at hi
-        refine ⟨w, ?_, hi⟩
-        by_cases hlast : Wire.gate (Fin.last g) ∈ frontier <;>
-          simp [opened, hlast, prior, hw]
-    have hline : lineInputs.card ≤ 1 + binaryCost line.op := by
-      calc lineInputs.card ≤ (Finset.univ : Finset (Fin (signature.Arity line.op))).card :=
-            Finset.card_image_le
-        _ = signature.Arity line.op := by simp
-        _ ≤ 1 + binaryCost line.op := Boolean.arity_le_one_add_binaryCost line.op
-    have hopened : opened.card ≤ frontier.card + binaryCost line.op := by
-      by_cases hlast : Wire.gate (Fin.last g) ∈ frontier
-      · have hprior : prior.card ≤ (frontier.erase (Wire.gate (Fin.last g))).card := by
-          apply Finset.card_le_card_of_injOn Wire.castSucc
-          · intro w hw
-            change Wire.castSucc w ∈ frontier.erase (Wire.gate (Fin.last g))
-            rw [Finset.mem_erase]
-            refine ⟨?_, by simpa [prior] using hw⟩
-            cases w with
-            | input _ => simp
-            | gate _ => simp [Fin.castSucc_ne_last]
-          · exact wire_castSucc_injective'.injOn
-        have herase := Finset.card_erase_of_mem hlast
-        have hpos : 1 ≤ frontier.card := Finset.one_le_card.mpr ⟨_, hlast⟩
-        have hopened_eq : opened = prior ∪ lineInputs := by simp [opened, hlast]
-        rw [hopened_eq]
-        calc (prior ∪ lineInputs).card ≤ prior.card + lineInputs.card :=
-              Finset.card_union_le _ _
-          _ ≤ (frontier.erase (Wire.gate (Fin.last g))).card + (1 + binaryCost line.op) :=
-              Nat.add_le_add hprior hline
-          _ = frontier.card - 1 + (1 + binaryCost line.op) := by rw [herase]
-          _ = frontier.card + binaryCost line.op := by omega
-      · have hprior : prior.card ≤ frontier.card := by
-          apply Finset.card_le_card_of_injOn Wire.castSucc
-          · intro w hw
-            simpa [prior] using hw
-          · exact wire_castSucc_injective'.injOn
-        have hopened_eq : opened = prior := by simp [opened, hlast]
-        rw [hopened_eq]
-        omega
-    calc (frontier.biUnion (p.gate line).wireSupport).card
-        ≤ (opened.biUnion p.wireSupport).card := Finset.card_le_card hsub
-      _ ≤ opened.card + p.cost binaryCost := ih opened
-      _ ≤ frontier.card + binaryCost line.op + p.cost binaryCost :=
-          Nat.add_le_add_right hopened _
-      _ = frontier.card + (p.gate line).cost binaryCost := by
-          rw [Program.cost_gate]
-          omega
+    (frontier.biUnion p.wireSupport).card ≤ frontier.card + p.cost binaryCost :=
+  p.card_biUnion_wireSupport_le_cost binaryCost arity_le_one_add_binaryCost frontier
 
 /-- A De Morgan circuit with `m` outputs has at most `m + c.program.cost binaryCost` supporting
 inputs, since only binary AND and OR gates increase the number of reachable inputs. -/

Complexity/Computability/Circuit/Boolean/ReadOnce.lean

@@ -9,6 +9,7 @@ module
 
 public import Complexity.Computability.Circuit.Boolean.BinaryCost
 public import Complexity.Computability.Circuit.Monotone.Formula
+import Complexity.Computability.Circuit.FanIn
 
 /-!
 # Positive and read-once Boolean formulas from tight binary-cost circuits
@@ -673,11 +674,6 @@ end Boolean
 
 /-! ### Unfolding tight binary-cost De Morgan programs into formulas -/
 
-private theorem wire_castSucc_injective'' :
-    Function.Injective (Wire.castSucc : Wire n g → Wire n (g + 1)) := by
-  intro a b h
-  cases a <;> cases b <;> simp_all [Wire.castSucc]
-
 @[simp] private theorem wire_lastCases_last {α : Sort*} (last : α) (castSucc : Wire n g → α) :
     Wire.lastCases (motive := fun _ => α) last castSucc (.gate (Fin.last g)) = last := by
   simp [Wire.lastCases]
@@ -770,7 +766,7 @@ theorem Program.exists_litFormula_of_card_biUnion_wireSupport_ge (hn : 0 < n)
         | last => exact absurd rfl hne
         | castSucc w' => exact ⟨w', hw, rfl⟩
     have hprior_card : prior.card = (frontier.erase (Wire.gate (Fin.last g))).card := by
-      rw [← hprior_image, Finset.card_image_of_injective _ wire_castSucc_injective'']
+      rw [← hprior_image, Finset.card_image_of_injective _ Wire.castSucc_injective]
     have hopened_le : opened.card ≤ frontier.card + binaryCost op := by
       by_cases hlast : Wire.gate (Fin.last g) ∈ frontier
       · have herase := Finset.card_erase_of_mem hlast
@@ -838,7 +834,7 @@ theorem Program.exists_litFormula_of_card_biUnion_wireSupport_ge (hn : 0 < n)
     · have hsum_prior :
           ∑ w ∈ frontier.erase (Wire.gate (Fin.last g)), (F w).leafSize =
             ∑ w' ∈ prior, (F' w').leafSize := by
-        rw [← hprior_image, Finset.sum_image fun a _ b _ hab => wire_castSucc_injective'' hab]
+        rw [← hprior_image, Finset.sum_image fun a _ b _ hab => Wire.castSucc_injective hab]
         exact Finset.sum_congr rfl fun w' _ => by
           rw [show F w'.castSucc = F' w' from wire_lastCases_castSucc lastFormula F' w']
       by_cases hlast : Wire.gate (Fin.last g) ∈ frontier

Complexity/Computability/Circuit/FanIn.lean

@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 public import Complexity.Computability.Circuit.Support
 public import Cslib.Computability.Circuit.Depth
+public import Cslib.Computability.Circuit.Simulation
 public import Mathlib.Algebra.Order.BigOperators.Group.Finset
 
 /-!
@@ -19,6 +20,8 @@ lower bound on circuit size.
 
 ## Main results
 
+* `Cslib.Circuits.Program.card_biUnion_wireSupport_le_cost`: supporting inputs are bounded by the
+  frontier size plus the program cost under any weight bounding arities by `1 + w op`.
 * `Cslib.Circuits.Circuit.card_inputSupport_le_size`: a circuit of fan-in `r` with `m` outputs has
   at most `m + (r - 1) size` supporting inputs.
 * `Cslib.Circuits.Circuit.essential_le_size`: the same bound for essential inputs of the computed
@@ -33,6 +36,7 @@ namespace Cslib.Circuits
 
 variable {σ : Signature} {U V : Type*} {n m g : ℕ}
 
+/-- The original circuit inputs reachable backwards from a frontier of wires in a program. -/
 private def Program.reachableInputs :
     ∀ {g : ℕ}, Program σ n g → Finset (Wire n g) → Finset (Fin n)
   | _, .empty, frontier => Finset.univ.filter fun input => Wire.input input ∈ frontier
@@ -45,7 +49,8 @@ private def Program.reachableInputs :
           prior
       program.reachableInputs opened
 
-private theorem wire_castSucc_injective :
+/-- Embedding a wire into a widened program by `Wire.castSucc` is injective. -/
+theorem Wire.castSucc_injective :
     Function.Injective (Wire.castSucc : Wire n g → Wire n (g + 1)) := by
   intro a b h
   cases a <;> cases b <;> simp_all [Wire.castSucc]
@@ -65,6 +70,7 @@ private def Circuit.reachableInputs (c : Circuit σ n m) :
     Finset (Fin n) :=
   c.program.reachableInputs c.frontier
 
+/-- Every input supporting a wire in the frontier is reachable from the frontier. -/
 private theorem Program.support_subset_reachableInputs
     (program : Program σ n g) :
     ∀ frontier : Finset (Wire n g),
@@ -118,25 +124,26 @@ private theorem Circuit.inputSupport_subset_reachableInputs
   obtain ⟨output, supported⟩ := present
   exact ⟨c.outputs output, ⟨output, rfl⟩, supported⟩
 
-private theorem Program.card_reachableInputs_le
+/-- In any circuit program, the number of reachable inputs from a frontier of wires is bounded
+by the size of the frontier plus the cost of the program, for any weight function that bounds gate
+arities by `1 + w op`. -/
+private theorem Program.card_reachableInputs_le_cost
     (program : Program σ n g)
-    (r : Nat) :
-    ∀ (_bounded : program.FanInAtMost r) (frontier : Finset (Wire n g)),
-      (program.reachableInputs frontier).card ≤
-        frontier.card + (r - 1) * g := by
+    (w : σ.Op → ℕ)
+    (hw : ∀ op, σ.Arity op ≤ 1 + w op)
+    (frontier : Finset (Wire n g)) :
+    (program.reachableInputs frontier).card ≤
+      frontier.card + program.cost w := by
   induction program with
   | empty =>
-      intro _ frontier
-      simp only [Cslib.Circuits.Program.reachableInputs, Nat.mul_zero, Nat.add_zero]
+      simp only [Program.reachableInputs, Program.cost_empty, Nat.add_zero]
       apply Finset.card_le_card_of_injOn Wire.input
       · intro input present
         simpa using present
       · intro a _ b _ h
         cases h
         rfl
   | @gate g program line ih =>
-      intro bounded frontier
-      obtain ⟨programBounded, lineBounded⟩ := bounded
       let prior := Finset.univ.filter fun wire : Wire n g => wire.castSucc ∈ frontier
       let lineInputs := Finset.univ.image line.wires
       let opened :=
@@ -145,14 +152,14 @@ private theorem Program.card_reachableInputs_le
         apply Finset.card_le_card_of_injOn Wire.castSucc
         · intro wire present
           simpa [prior] using present
-        · exact wire_castSucc_injective.injOn
-      have lineBound : lineInputs.card ≤ r := by
+        · exact Wire.castSucc_injective.injOn
+      have lineBound : lineInputs.card ≤ 1 + w line.op := by
         calc
           lineInputs.card ≤ (Finset.univ : Finset (Fin (σ.Arity line.op))).card :=
             Finset.card_image_le
           _ = σ.Arity line.op := by simp
-          _ ≤ r := lineBounded
-      have openedBound : opened.card ≤ frontier.card + (r - 1) := by
+          _ ≤ 1 + w line.op := hw line.op
+      have openedBound : opened.card ≤ frontier.card + w line.op := by
         by_cases lastSelected : Wire.gate (Fin.last g) ∈ frontier
         · have priorEraseBound : prior.card ≤
               (frontier.erase (Wire.gate (Fin.last g))).card := by
@@ -164,18 +171,18 @@ private theorem Program.card_reachableInputs_le
               cases wire with
               | input i => simp
               | gate j => simp [Fin.castSucc_ne_last]
-            · exact wire_castSucc_injective.injOn
+            · exact Wire.castSucc_injective.injOn
           have erased := Finset.card_erase_of_mem lastSelected
           have openedEq : opened = prior ∪ lineInputs := by
             simp [opened, lastSelected]
           rw [openedEq]
           calc
             (prior ∪ lineInputs).card ≤ prior.card + lineInputs.card :=
               Finset.card_union_le _ _
-            _ ≤ (frontier.erase (Wire.gate (Fin.last g))).card + r :=
+            _ ≤ (frontier.erase (Wire.gate (Fin.last g))).card + (1 + w line.op) :=
               Nat.add_le_add priorEraseBound lineBound
-            _ = frontier.card - 1 + r := by rw [erased]
-            _ ≤ frontier.card + (r - 1) := by
+            _ = frontier.card - 1 + (1 + w line.op) := by rw [erased]
+            _ = frontier.card + w line.op := by
               have frontierPositive : 1 ≤ frontier.card :=
                 Finset.one_le_card.mpr ⟨_, lastSelected⟩
               omega
@@ -185,12 +192,48 @@ private theorem Program.card_reachableInputs_le
           omega
       change (program.reachableInputs opened).card ≤ _
       calc
-        (program.reachableInputs opened).card ≤ opened.card + (r - 1) * g :=
-          ih programBounded opened
-        _ ≤ frontier.card + (r - 1) * (g + 1) := by
-          rw [Nat.mul_succ]
+        (program.reachableInputs opened).card ≤ opened.card + program.cost w :=
+          ih opened
+        _ ≤ frontier.card + w line.op + program.cost w :=
+          Nat.add_le_add_right openedBound _
+        _ = frontier.card + (program.gate line).cost w := by
+          rw [Program.cost_gate]
           omega
 
+/-- The inputs supporting a frontier of wires in a program are bounded by the size of the frontier
+plus the cost of the program, for any weight function that bounds gate arities by `1 + w op`. -/
+theorem Program.card_biUnion_wireSupport_le_cost
+    (program : Program σ n g)
+    (w : σ.Op → ℕ)
+    (hw : ∀ op, σ.Arity op ≤ 1 + w op)
+    (frontier : Finset (Wire n g)) :
+    (frontier.biUnion program.wireSupport).card ≤
+      frontier.card + program.cost w :=
+  (Finset.card_le_card (program.support_subset_reachableInputs frontier)).trans
+    (program.card_reachableInputs_le_cost w hw frontier)
+
+private theorem Program.cost_le_of_fanInAtMost (p : Program σ n g) {r : ℕ} (h : p.FanInAtMost r) :
+    p.cost (fun op => max (r - 1) (σ.Arity op - 1)) ≤ (r - 1) * g := by
+  induction p with
+  | empty => simp
+  | gate p line ih =>
+    obtain ⟨hp, hline⟩ := h
+    rw [Program.cost_gate, Nat.mul_succ]
+    have hw : max (r - 1) (σ.Arity line.op - 1) = r - 1 := by omega
+    rw [hw]
+    exact Nat.add_le_add (ih hp) le_rfl
+
+private theorem Program.card_reachableInputs_le
+    (program : Program σ n g)
+    (r : Nat) :
+    ∀ (_bounded : program.FanInAtMost r) (frontier : Finset (Wire n g)),
+      (program.reachableInputs frontier).card ≤
+        frontier.card + (r - 1) * g := by
+  intro bounded frontier
+  have hw : ∀ op, σ.Arity op ≤ 1 + max (r - 1) (σ.Arity op - 1) := fun op => by omega
+  exact (program.card_reachableInputs_le_cost _ hw frontier).trans
+    (Nat.add_le_add_left (program.cost_le_of_fanInAtMost bounded) _)
+
 private theorem Circuit.card_reachableInputs_le_size
     (c : Circuit σ n m)
     (r : Nat)