Fixing misc theorems

ProvenZk/Misc.lean

@@ -1,53 +1,66 @@
 import ProvenZk.Gates
 import ProvenZk.Binary
 
+open  GatesEquivalence
+
 variable {N : Nat}
 variable [Fact (Nat.Prime N)]
 
 theorem or_rw (a b out : (ZMod N)) : Gates.or a b out ↔
   (Gates.is_bool a ∧ Gates.is_bool b ∧
   ( (out = 1 ∧ (a = 1 ∨ b = 1) ∨
     (out = 0 ∧ a = 0 ∧ b = 0)))) := by
-  unfold Gates.or
-  unfold Gates.is_bool
-  simp
-  intro ha hb
-  cases ha <;> cases hb <;> { subst_vars; simp }
+  rw [or_equivalence]
+  rw [is_bool_equivalence]
+  rw [is_bool_equivalence]
+  apply Iff.intro
+  . intro h
+    casesm* (_ ∨ _)
+    repeat (
+      casesm* (_ ∧ _)
+      subst_vars
+      simp
+    )
+  . intro h
+    casesm* (_ ∧ _)
+    rename_i ha hb hout
+    cases ha <;> cases hb <;> {
+      subst_vars
+      simp at hout
+      simp
+      tauto
+    }
 
 lemma select_rw {b i1 i2 out : (ZMod N)} : (Gates.select b i1 i2 out) ↔ is_bit b ∧ match zmod_to_bit b with
   | Bit.zero => out = i2
   | Bit.one => out = i1 := by
-  unfold Gates.select
-  unfold Gates.is_bool
-  apply Iff.intro <;> {
-    intro h; rcases h with ⟨is_b, _⟩
-    refine ⟨is_b, ?_⟩
-    cases is_b
-    case inl => {
-      simp [*, zmod_to_bit] at *
-      assumption
-    }
-    case inr => {
-      simp [*, zmod_to_bit] at *
-      have : Nat.Prime N := (inferInstance : Fact (Nat.Prime N)).elim
-      have : N > 1 := by
-        apply Nat.Prime.one_lt
-        assumption
-      cases N
-      case zero => simp [ZMod.val] at *
-      case succ n _ _ _ _=> {
-        cases n
-        case zero => simp [ZMod.val] at *
-        case succ => {
-          simp [ZMod.val] at *
-          assumption
-        }
-      }
-    }
-  }
+  rw [select_equivalence]
+  apply Iff.intro
+  . intro h
+    casesm* (_ ∧ _)
+    rename_i hb hout
+    cases hb
+    repeat (
+      subst_vars
+      simp at hout
+      simp [zmod_to_bit, ZMod.val_one]
+      tauto
+    )
+  . intro h
+    simp [is_bit] at h
+    casesm* (_ ∧ _)
+    rename_i hb hout
+    cases hb
+    repeat (
+      subst_vars
+      simp [zmod_to_bit, ZMod.val_one] at hout
+      simp
+      tauto
+    )
 
 @[simp]
-theorem is_bool_is_bit (a : ZMod n) [Fact (Nat.Prime n)]: Gates.is_bool a = is_bit a := by rfl
+theorem is_bool_is_bit (a : ZMod n) [Fact (Nat.Prime n)]: Gates.is_bool a = is_bit a := by
+  rw [is_bool_equivalence]
 
 @[simp]
 theorem select_zero {a b r : ZMod N}: Gates.select 0 a b r = (r = b) := by