Proofs improvements

reilabs · Nov 25, 2023 · e9350ed · e9350ed
1 parent 96f5f77
commit e9350ed
Showing 1 changed file with 16 additions and 44 deletions.
diff --git a/ProvenZk/Gates.lean b/ProvenZk/Gates.lean
@@ -134,17 +134,10 @@ lemma xor_equivalence {a b out : ZMod N} :
     simp at h
     casesm* (_ ∧ _)
     rename_i ha hb _
-    cases ha
-    . cases hb
-      repeat (
-        subst_vars
-        simp
-      )
-    . cases hb
-      repeat (
-        subst_vars
-        simp
-      )
+    cases ha <;> cases hb <;> {
+      subst_vars
+      simp
+    }
   . intro h
     casesm* (_ ∨ _)
     repeat (
@@ -166,17 +159,10 @@ lemma or_equivalence {a b out : ZMod N} :
     simp at h
     casesm* (_ ∧ _)
     rename_i ha hb _
-    cases ha
-    . cases hb
-      repeat (
-        subst_vars
-        simp
-      )
-    . cases hb
-      repeat (
-        subst_vars
-        simp
-      )
+    cases ha <;> cases hb <;> {
+      subst_vars
+      simp
+    }
   . intro h
     casesm* (_ ∨ _)
     repeat (
@@ -200,17 +186,10 @@ lemma and_equivalence {a b out : ZMod N} :
     simp at h
     casesm* (_ ∧ _)
     rename_i ha hb _
-    cases ha
-    . cases hb
-      repeat (
-        subst_vars
-        simp
-      )
-    . cases hb
-      repeat (
-        subst_vars
-        simp
-      )
+    cases ha <;> cases hb <;> {
+      subst_vars
+      simp
+    }
   . intro h
     casesm* (_ ∨ _)
     repeat (
@@ -280,17 +259,10 @@ lemma lookup_equivalence {b0 b1 i0 i1 i2 i3 out : ZMod N} :
   . intro h
     casesm* (_ ∧ _)
     rename_i hb0 hb1 _
-    cases hb0
-    . cases hb1
-      . subst_vars
-        simp
-      . subst_vars
-        simp
-    . cases hb1
-      . subst_vars
-        simp
-      . subst_vars
-        simp [add_assoc]
+    cases hb0 <;> cases hb1 <;> {
+      subst_vars
+      simp [add_assoc]
+    }
   . intro h
     casesm* (_ ∨ _)
     repeat (