Replace optimality_proof.v with mux.v - exact enumeration

optimality_proof.v → mux.v

@@ -1,12 +1,3 @@
-(*
-   MUX Magnitude Discovery
-
-   We search for the minimum magnitude that can compute 2:1 MUX.
-   MUX(a, b, s) = a if s=0, b if s=1
-
-   The result is discovered through exhaustive computation.
-*)
-
 Require Import ZArith.
 Require Import Bool.
 Require Import List.
@@ -14,45 +5,34 @@ Import ListNotations.
 
 Open Scope Z_scope.
 
-(* Threshold gate with 3 inputs *)
 Definition threshold3 (w1 w2 w3 b : Z) (x1 x2 x3 : bool) : bool :=
   Z.geb (w1 * (if x1 then 1 else 0) +
          w2 * (if x2 then 1 else 0) +
          w3 * (if x3 then 1 else 0) + b) 0.
 
-(* Threshold gate with 2 inputs *)
 Definition threshold2 (w1 w2 b : Z) (x1 x2 : bool) : bool :=
   Z.geb (w1 * (if x1 then 1 else 0) +
          w2 * (if x2 then 1 else 0) + b) 0.
 
-(* 3-neuron circuit: 2 hidden + 1 output *)
 Definition circuit (w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo : Z)
                    (a b s : bool) : bool :=
   let h1 := threshold3 w1a w1b w1s b1 a b s in
   let h2 := threshold3 w2a w2b w2s b2 a b s in
   threshold2 wo1 wo2 bo h1 h2.
 
-(* MUX specification: output = a when s=false, b when s=true *)
-(* circuit args: w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo a b s *)
-Definition is_mux_b (w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo : Z) : bool :=
-  (* s=false: output should equal a *)
-  negb (circuit w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo false false false) &&  (* a=0,b=0,s=0 -> 0 *)
-  negb (circuit w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo false true  false) &&  (* a=0,b=1,s=0 -> 0 *)
-       (circuit w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo true  false false) &&  (* a=1,b=0,s=0 -> 1 *)
-       (circuit w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo true  true  false) &&  (* a=1,b=1,s=0 -> 1 *)
-  (* s=true: output should equal b *)
-  negb (circuit w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo false false true) &&   (* a=0,b=0,s=1 -> 0 *)
-       (circuit w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo false true  true) &&   (* a=0,b=1,s=1 -> 1 *)
-  negb (circuit w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo true  false true) &&   (* a=1,b=0,s=1 -> 0 *)
-       (circuit w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo true  true  true).     (* a=1,b=1,s=1 -> 1 *)
-
-(* Magnitude *)
-Definition magnitude (w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo : Z) : Z :=
-  Z.abs w1a + Z.abs w1b + Z.abs w1s + Z.abs b1 +
-  Z.abs w2a + Z.abs w2b + Z.abs w2s + Z.abs b2 +
-  Z.abs wo1 + Z.abs wo2 + Z.abs bo.
-
-(* Generate signed variants *)
+Definition is_mux (w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo : Z) : bool :=
+  negb (circuit w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo false false false) &&
+  negb (circuit w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo false true  false) &&
+       (circuit w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo true  false false) &&
+       (circuit w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo true  true  false) &&
+  negb (circuit w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo false false true) &&
+       (circuit w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo false true  true) &&
+  negb (circuit w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo true  false true) &&
+       (circuit w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo true  true  true).
+
+Definition mag (c : list Z) : Z :=
+  fold_left (fun acc x => acc + Z.abs x) c 0.
+
 Fixpoint all_signs (abs_vals : list Z) : list (list Z) :=
   match abs_vals with
   | [] => [[]]
@@ -64,7 +44,6 @@ Fixpoint all_signs (abs_vals : list Z) : list (list Z) :=
         map (cons a) signed_rest ++ map (cons (-a)) signed_rest
   end.
 
-(* Partition magnitude across positions *)
 Fixpoint partitions (remaining : Z) (positions : nat) (max_val : Z) : list (list Z) :=
   match positions with
   | O => if Z.eqb remaining 0 then [[]] else []
@@ -74,50 +53,66 @@ Fixpoint partitions (remaining : Z) (positions : nat) (max_val : Z) : list (list
       ) (map Z.of_nat (seq 0 (Z.to_nat (Z.min remaining max_val) + 1)))
   end.
 
-(* All signed configs at magnitude M *)
 Definition configs_at_mag (m : Z) : list (list Z) :=
   flat_map all_signs (partitions m 11 m).
 
-(* Check if any config computes MUX *)
-Definition any_mux (configs : list (list Z)) : bool :=
-  existsb (fun c =>
+Definition filter_mux (configs : list (list Z)) : list (list Z) :=
+  filter (fun c =>
     match c with
     | [w1a; w1b; w1s; b1; w2a; w2b; w2s; b2; wo1; wo2; bo] =>
-        is_mux_b w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo
+        is_mux w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo
     | _ => false
     end
   ) configs.
 
-(* === DISCOVERY === *)
+Definition solutions_at_mag (m : Z) : list (list Z) :=
+  filter_mux (configs_at_mag m).
+
+Definition count (m : Z) : nat :=
+  length (solutions_at_mag m).
 
-(* Does MUX exist at magnitude 0? *)
-Theorem mag_0 : any_mux (configs_at_mag 0) = false.
-Proof. native_compute. reflexivity. Qed.
+Theorem count_0 : count 0 = 0%nat.
+Proof. vm_compute. reflexivity. Qed.
 
-(* Does MUX exist at magnitude 1? *)
-Theorem mag_1 : any_mux (configs_at_mag 1) = false.
-Proof. native_compute. reflexivity. Qed.
+Theorem count_1 : count 1 = 0%nat.
+Proof. vm_compute. reflexivity. Qed.
 
-(* Does MUX exist at magnitude 2? *)
-Theorem mag_2 : any_mux (configs_at_mag 2) = false.
-Proof. native_compute. reflexivity. Qed.
+Theorem count_2 : count 2 = 0%nat.
+Proof. vm_compute. reflexivity. Qed.
 
-(* Does MUX exist at magnitude 3? *)
-Theorem mag_3 : any_mux (configs_at_mag 3) = false.
-Proof. native_compute. reflexivity. Qed.
+Theorem count_3 : count 3 = 0%nat.
+Proof. vm_compute. reflexivity. Qed.
 
-(* Does MUX exist at magnitude 4? *)
-Theorem mag_4 : any_mux (configs_at_mag 4) = false.
-Proof. native_compute. reflexivity. Qed.
+Theorem count_4 : count 4 = 0%nat.
+Proof. vm_compute. reflexivity. Qed.
 
-(* Does MUX exist at magnitude 5? *)
-Theorem mag_5 : any_mux (configs_at_mag 5) = false.
-Proof. native_compute. reflexivity. Qed.
+Theorem count_5 : count 5 = 0%nat.
+Proof. vm_compute. reflexivity. Qed.
+
+Theorem count_6 : count 6 = 0%nat.
+Proof. vm_compute. reflexivity. Qed.
+
+Theorem count_7 : count 7 = 4%nat.
+Proof. vm_compute. reflexivity. Qed.
+
+Definition solutions : list (list Z) :=
+  [[0; 1; -1; 0; -1; 0; -1; 0; 1; -1; -1];
+   [0; -1; 1; -1; -1; 0; -1; 0; -1; -1; 0];
+   [-1; 0; -1; 0; 0; 1; -1; 0; -1; 1; -1];
+   [-1; 0; -1; 0; 0; -1; 1; -1; -1; -1; 0]].
+
+Theorem solutions_eq : solutions_at_mag 7 = solutions.
+Proof. vm_compute. reflexivity. Qed.
+
+Definition check (c : list Z) : bool :=
+  match c with
+  | [w1a; w1b; w1s; b1; w2a; w2b; w2s; b2; wo1; wo2; bo] =>
+      is_mux w1a w1b w1s b1 w2a w2b w2s b2 wo1 wo2 bo
+  | _ => false
+  end.
 
-(* Does MUX exist at magnitude 6? *)
-Theorem mag_6 : any_mux (configs_at_mag 6) = false.
-Proof. native_compute. reflexivity. Qed.
+Theorem solutions_valid : forallb check solutions = true.
+Proof. vm_compute. reflexivity. Qed.
 
-(* Does MUX exist at magnitude 7? *)
-Theorem mag_7 : any_mux (configs_at_mag 7) = true.
-Proof. native_compute. reflexivity. Qed.
+Theorem solutions_mag : forallb (fun c => Z.eqb (mag c) 7) solutions = true.
+Proof. vm_compute. reflexivity. Qed.