From 96f5f77b429ed33c71ef252ed8cb724a84fc0dfd Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Sat, 25 Nov 2023 18:33:31 +0000
Subject: [PATCH] Fixing misc theorems

---
 ProvenZk/Misc.lean | 81 +++++++++++++++++++++++++++-------------------
 1 file changed, 47 insertions(+), 34 deletions(-)

diff --git a/ProvenZk/Misc.lean b/ProvenZk/Misc.lean
index 52eea7f..471c6b5 100644
--- a/ProvenZk/Misc.lean
+++ b/ProvenZk/Misc.lean
@@ -1,6 +1,8 @@
 import ProvenZk.Gates
 import ProvenZk.Binary
 
+open  GatesEquivalence
+
 variable {N : Nat}
 variable [Fact (Nat.Prime N)]
 
@@ -8,46 +10,57 @@ 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