cleanup

ProvenZk/Binary.lean

@@ -34,6 +34,15 @@ lemma Bool.toZMod_one {N} : Bool.toZMod true = (1  : ZMod N) := by
 lemma Bool.toZMod_is_bit {N} : is_bit (toZMod (N:=N) b) := by
   cases b <;> simp [is_bit, toZMod, toNat]
 
+
+@[simp]
+theorem Bool.toZMod_eq_one_iff_eq_true {n:ℕ} [Fact (n > 1)] : (Bool.toZMod a : ZMod n) = 1 ↔ a = true := by
+  cases a <;> simp
+
+@[simp]
+theorem Bool.toZMod_eq_one_iff_eq_false {n:ℕ} [Fact (n > 1)] : (Bool.toZMod a : ZMod n) = 0 ↔ a = false := by
+  cases a <;> simp
+
 @[simp]
 lemma Bool.ofZMod_toZMod_eq_self {b} [Fact (N > 1)]: Bool.ofZMod (Bool.toZMod (N:=N) b) = b := by
   cases b <;> simp [toZMod, ofZMod, ofNat, toNat]

ProvenZk/Ext/GetElem.lean

@@ -7,6 +7,15 @@ theorem getElem?_eq_some_getElem_of_valid_index [GetElem cont idx elem domain] [
   . rfl
   . contradiction
 
+theorem getElem!_eq_getElem_of_valid_index [GetElem cont idx elem domain] [Decidable (domain container index)] [Inhabited elem] (h : domain container index):
+  container[index]! = container[index] := by
+  simp [getElem!, h]
+
+theorem getElem_of_getElem! [GetElem cont idx elem domain] [Decidable (domain container index)] [Inhabited elem] (ix_ok : domain container index) (h : container[index]! = element):
+  container[index] = element := by
+  simp [getElem!, ix_ok] at h
+  assumption
+
 theorem getElem?_none_of_invalid_index [GetElem cont idx elem domain] [Decidable (domain container index)] (h : ¬ domain container index):
   container[index]? = none := by
   unfold getElem?

ProvenZk/Ext/Vector/Basic.lean

@@ -252,61 +252,6 @@ instance : Membership α (Vector α n) := ⟨fun x xs => x ∈ xs.toList⟩
 @[simp]
 theorem mem_def {xs : Vector α n} {x} : x ∈ xs ↔ x ∈ xs.toList := by rfl
 
--- def allElems (f : α → Prop) : Vector α n → Prop := fun v => ∀(a : α), a ∈ v → f a
-
--- @[simp]
--- theorem allElems_cons : Vector.allElems prop (v ::ᵥ vs) ↔ prop v ∧ allElems prop vs := by
---   simp [allElems]
-
--- @[simp]
--- theorem allElems_nil : Vector.allElems prop Vector.nil := by simp [allElems]
-
--- def allIxes (f : α → Prop) : Vector α n → Prop := fun v => ∀(i : Fin n), f v[i]
-
--- @[simp]
--- theorem allIxes_cons : allIxes f (v ::ᵥ vs) ↔ f v ∧ allIxes f vs := by
---   simp [allIxes, GetElem.getElem]
---   apply Iff.intro
---   . intro h
---     exact ⟨h 0, fun i => h i.succ⟩
---   . intro h i
---     cases i using Fin.cases
---     . simp [h.1]
---     . simp [h.2]
-
--- @[simp]
--- theorem allIxes_nil : allIxes f Vector.nil := by
---   simp [allIxes]
-
--- theorem getElem_allElems {v : { v: Vector α n // allElems prop v  }} {i : Nat} { i_small : i < n}:
---   v.val[i]'i_small = ↑(Subtype.mk (p := prop) (v.val.get ⟨i, i_small⟩) (by apply v.prop; simp)) := by rfl
-
--- theorem getElem_allElems₂ {v : { v: Vector (Vector α m) n // allElems (allElems prop) v  }} {i j: Nat} { i_small : i < n} { j_small : j < m}:
---   (v.val[i]'i_small)[j]'j_small = ↑(Subtype.mk (p := prop) ((v.val.get ⟨i, i_small⟩).get ⟨j, j_small⟩) (by apply v.prop; rotate_right; exact v.val.get ⟨i, i_small⟩; all_goals simp)) := by rfl
-
--- theorem allElems_indexed {v : {v : Vector α n // allElems prop v}} {i : Nat} {i_small : i < n}:
---   prop (v.val[i]'i_small) := by
---   apply v.prop
---   simp [getElem]
-
--- theorem allElems_indexed₂ {v : {v : Vector (Vector (Vector α a) b) c // allElems (allElems prop) v}}
---   {i : Nat} {i_small : i < c}
---   {j : Nat} {j_small : j < b}:
---   prop ((v.val[i]'i_small)[j]'j_small) := by
---   apply v.prop (v.val[i]'i_small) <;> simp [getElem]
-
--- theorem allElems_indexed₃ {v : {v : Vector (Vector (Vector α a) b) c // allElems (allElems (allElems prop)) v}}
---   {i : Nat} {i_small : i < c}
---   {j : Nat} {j_small : j < b}
---   {k : Nat} {k_small : k < a}:
---   prop (((v.val[i]'i_small)[j]'j_small)[k]'k_small) := by
---   apply v.prop
---   rotate_right
---   . exact (v.val[i]'i_small)[j]'j_small
---   rotate_right
---   . exact (v.val[i]'i_small)
---   all_goals simp [getElem]
-
 @[simp]
 theorem map_ofFn {f : α → β} (g : Fin n → α) :
   Vector.map f (Vector.ofFn g) = Vector.ofFn (fun x => f (g x)) := by
@@ -367,47 +312,6 @@ theorem append_inj_iff {v₁ w₁ : Vector α d₁} {v₂ w₂ : Vector α d₂}
   . intro ⟨_, _⟩
     simp [*]
 
--- theorem allIxes_toList : Vector.allIxes prop v ↔ ∀ i, prop (v.toList.get i) := by
---   unfold Vector.allIxes
---   apply Iff.intro
---   . intro h i
---     rcases i with ⟨i, p⟩
---     simp at p
---     simp [GetElem.getElem, Vector.get] at h
---     have := h ⟨i, p⟩
---     conv at this => arg 1; whnf
---     exact this
---   . intro h i
---     simp [GetElem.getElem, Vector.get]
---     rcases i with ⟨i, p⟩
---     have := h ⟨i, by simpa⟩
---     conv at this => arg 1; whnf
---     exact this
-
--- theorem allElems_append {v₁ : Vector α n₁} {v₂ : Vector α n₂} : Vector.allElems prop (v₁ ++ v₂) ↔ Vector.allElems prop v₁ ∧ Vector.allElems prop v₂ := by
---   simp [allElems]
---   apply Iff.intro
---   . intro h
---     apply And.intro
---     . exact fun a hp => h a (Or.inl hp)
---     . exact fun a hp => h a (Or.inr hp)
---   . rintro ⟨_,_⟩ _ _ ; tauto
-
--- theorem SubVector_append {v₁ : Vector α d₁} {prop₁ : Vector.allIxes prop v₁ } {v₂ : Vector α d₂} {prop₂ : Vector.allIxes prop v₂}:
---   (Subtype.mk v₁ prop₁).val ++ (Subtype.mk v₂ prop₂).val =
---   (Subtype.mk (v₁ ++ v₂) (allIxes_append.mpr ⟨prop₁, prop₂⟩)).val := by eq_refl
-
-
--- theorem allIxes_iff_allElems : allIxes prop v ↔ ∀ a ∈ v, prop a := by
---   apply Iff.intro
---   . intro hp a ain
---     have := (Vector.mem_iff_get a v).mp ain
---     rcases this with ⟨i, h⟩
---     cases h
---     apply hp
---   . intro hp i
---     apply hp
---     apply Vector.get_mem
 
 @[simp]
 theorem getElem_map {i n : ℕ} {h : i < n} {v : Vector α n} : (Vector.map f v)[i]'h = f (v[i]'h) := by
@@ -449,4 +353,41 @@ theorem map_permute {p : Fin m → Fin n} {f : α → β} {v : Vector α n}:
   Vector.map f (permute p v) = permute p (v.map f) := by
   simp [permute]
 
+theorem exists_succ_iff_exists_snoc {α d} {pred : Vector α (Nat.succ d) → Prop}:
+  (∃v, pred v) ↔ ∃vs v, pred (Vector.snoc vs v) := by
+  apply Iff.intro
+  . rintro ⟨v, hp⟩
+    cases v using Vector.revCasesOn
+    apply Exists.intro
+    apply Exists.intro
+    assumption
+  . rintro ⟨vs, v, hp⟩
+    exists vs.snoc v
+
+theorem exists_succ_iff_exists_cons {α d} {pred : Vector α (Nat.succ d) → Prop}:
+  (∃v, pred v) ↔ ∃v vs, pred (v ::ᵥ vs) := by
+  apply Iff.intro
+  . rintro ⟨v, hp⟩
+    cases v using Vector.casesOn
+    apply Exists.intro
+    apply Exists.intro
+    assumption
+  . rintro ⟨v, vs, hp⟩
+    exists (v ::ᵥ vs)
+
+@[simp]
+theorem snoc_eq : Vector.snoc xs x = Vector.snoc ys y ↔ xs = ys ∧ x = y := by
+  apply Iff.intro
+  . intro h
+    have := congrArg Vector.reverse h
+    simp at this
+    injection this with this
+    injection this with h t
+    simp [*]
+    apply Vector.eq
+    have := congrArg List.reverse t
+    simpa [this]
+  . intro ⟨_, _⟩
+    simp [*]
+
 end Vector

ProvenZk/Gates.lean

@@ -6,7 +6,6 @@ open BigOperators
 
 namespace Gates
 variable {N : Nat}
--- variable [Fact (Nat.Prime N)]
 def is_bool (a : ZMod N): Prop := a = 0 ∨ a = 1
 def add (a b : ZMod N): ZMod N := a + b
 def mul_acc (a b c : ZMod N): ZMod N := a + (b * c)

ProvenZk/Lemmas.lean

@@ -9,35 +9,66 @@ variable [Fact (Nat.Prime N)]
 
 instance : Fact (N > 1) := ⟨Nat.Prime.one_lt Fact.out⟩
 
+theorem ZMod.eq_of_veq {a b : ZMod N} (h : a.val = b.val) : a = b := by
+  have : N ≠ 0 := by apply Nat.Prime.ne_zero Fact.out
+  have : ∃n, N = Nat.succ n := by exists N.pred; simp [Nat.succ_pred this]
+  rcases this with ⟨_, ⟨_⟩⟩
+  simp [val] at h
+  exact Fin.eq_of_veq h
+
+
+theorem ZMod.val_fin {n : ℕ} {i : ZMod (Nat.succ n)} : i.val = Fin.val i := by
+  simp [ZMod.val]
+
+@[simp]
+theorem exists_eq_left₂ {pred : α → β → Prop}:
+  (∃a b, (a = c ∧ b = d) ∧ pred a b) ↔ pred c d := by
+  simp [and_assoc]
+
 @[simp]
 theorem is_bool_is_bit (a : ZMod n) [Fact (Nat.Prime n)]: Gates.is_bool a = is_bit a := by rfl
 
 @[simp]
-theorem select_zero {a b r : ZMod N}: Gates.select 0 a b r = (r = b) := by
+theorem Gates.eq_def : Gates.eq a b ↔ a = b := by simp [Gates.eq]
+
+@[simp]
+theorem Gates.sub_def {N} {a b : ZMod N} : Gates.sub a b = a - b := by simp [Gates.sub]
+
+@[simp]
+theorem Gates.is_zero_def {N} {a out : ZMod N} : Gates.is_zero a out ↔ out = Bool.toZMod (a = 0) := by
+  simp [Gates.is_zero]
+  apply Iff.intro
+  . rintro (_ | _) <;> simp [*]
+  . rintro ⟨_⟩
+    simp [Bool.toZMod, Bool.toNat]
+    tauto
+
+@[simp]
+theorem Gates.select_zero {a b r : ZMod N}: Gates.select 0 a b r = (r = b) := by
   simp [Gates.select]
 
 @[simp]
-theorem select_one {a b r : ZMod N}: Gates.select 1 a b r = (r = a) := by
+theorem Gates.select_one {a b r : ZMod N}: Gates.select 1 a b r = (r = a) := by
   simp [Gates.select]
 
 @[simp]
-theorem or_zero { a r : ZMod N}: Gates.or a 0 r = (is_bit a ∧ r = a) := by
+theorem Gates.or_zero { a r : ZMod N}: Gates.or a 0 r = (is_bit a ∧ r = a) := by
   simp [Gates.or]
 
 @[simp]
-theorem zero_or { a r : ZMod N}: Gates.or 0 a r = (is_bit a ∧ r = a) := by
+theorem Gates.zero_or { a r : ZMod N}: Gates.or 0 a r = (is_bit a ∧ r = a) := by
   simp [Gates.or]
 
 @[simp]
-theorem one_or { a r : ZMod N}: Gates.or 1 a r = (is_bit a ∧ r = 1) := by
+theorem Gates.one_or { a r : ZMod N}: Gates.or 1 a r = (is_bit a ∧ r = 1) := by
   simp [Gates.or]
 
 @[simp]
-theorem or_one { a r : ZMod N}: Gates.or a 1 r = (is_bit a ∧ r = 1) := by
+theorem Gates.or_one { a r : ZMod N}: Gates.or a 1 r = (is_bit a ∧ r = 1) := by
   simp [Gates.or]
 
 @[simp]
-theorem is_bit_one_sub {a : ZMod N}: is_bit (Gates.sub 1 a) ↔ is_bit a := by
+theorem Gates.is_bit_one_sub {a : ZMod N}: is_bit (Gates.sub 1 a) ↔ is_bit a := by
   simp [Gates.sub, is_bit, sub_eq_zero]
   tauto
 
@@ -64,7 +95,7 @@ theorem Gates.or_bool {N} [Fact (N>1)] {a b : Bool} {c : ZMod N} : Gates.or a.to
   }
 
 @[simp]
-theorem Gates.not_bool {N} [Fact (N>1)] {a : Bool} : Gates.sub (1 : ZMod N) a.toZMod = (!a).toZMod := by
+theorem Gates.not_bool {N} [Fact (N>1)] {a : Bool} : (1 : ZMod N) - a.toZMod = (!a).toZMod := by
   cases a <;> simp [sub]
 
 @[simp]