x

ProvenZk/Binary.lean

@@ -1,10 +1,16 @@
 import Mathlib.Data.ZMod.Basic
 import Mathlib.Data.Bitvec.Defs
+import Mathlib.Data.Vector.Mem
 
 import ProvenZk.Ext.List
 import ProvenZk.Ext.Vector
 import ProvenZk.Subvector
 
+open BigOperators
+
+@[reducible]
+def is_bit (a : ZMod N): Prop := a = 0 ∨ a = 1
+
 inductive Bit : Type where
   | zero : Bit
   | one : Bit
@@ -19,11 +25,11 @@ def toZMod {n} : Bit -> ZMod n := fun b => match b with
   | Bit.zero => 0
   | Bit.one => 1
 
-instance : Coe Bit Nat where
-  coe := toNat
+-- instance : Coe Bit Nat where
+--   coe := toNat
 
-instance {n} : Coe Bit (ZMod n) where
-  coe := toZMod
+-- instance {n} : Coe Bit (ZMod n) where
+--   coe := toZMod
 
 instance : OfNat Bit 0 where
   ofNat := zero
@@ -34,6 +40,15 @@ instance : OfNat Bit 1 where
 instance : Inhabited Bit where
   default := zero
 
+instance [semiring : Semiring α] : Coe Bit α where
+  coe b := match b with
+  | Bit.zero => semiring.zero
+  | Bit.one => semiring.one
+
+@[simp]
+lemma is_bit_toZMod {N} {b:Bit} : is_bit (toZMod b : ZMod N) := by
+  cases b <;> simp [is_bit, toZMod]
+
 end Bit
 
 def bit_mod_two (inp : Nat) : Bit := match h:inp%2 with
@@ -64,9 +79,6 @@ def zmod_to_bit {n} (x : ZMod n) : Bit := match ZMod.val x with
   | 1 => Bit.one
   | Nat.succ (Nat.succ _) => panic "Bit can only be 0 or 1"
 
-@[reducible]
-def is_bit (a : ZMod N): Prop := a = 0 ∨ a = 1
-
 @[simp]
 theorem is_bit_zero : is_bit (0 : ZMod n) := by tauto
 
@@ -81,36 +93,35 @@ def embedBit {n : Nat} : Bit → {x : (ZMod n) // is_bit x}
 | Bit.zero => bZero
 | Bit.one => bOne
 
-def is_vector_binary {d n} (x : Vector (ZMod n) d) : Prop :=
-  (List.foldr (fun a r => is_bit a ∧ r) True (Vector.toList x))
+def is_vector_binary {d n} (x : Vector (ZMod n) d) : Prop := ∀ a ∈ x, is_bit a
+
+def recoverBinary [Semiring α] {n} (x : Vector Bit n): α :=
+  ∑i, 2^i.val * ↑(x.get i)
+
+-- @[simp]
+-- theorem is_vector_binary_def : is_vector_binary v ↔ ∀ a ∈ v.toList, is_bit a := by
+--   simp [is_vector_binary, Vector.instMembershipVector]
 
 @[simp]
 lemma is_vector_binary_reverse {depth} (ix : Vector (ZMod n) depth):
   is_vector_binary ix.reverse ↔ is_vector_binary ix := by
-  simp only [is_vector_binary, Vector.toList_reverse]
-  rw [List.foldr_reverse_assoc]
-  { simp }
-  { intros; simp; tauto }
+  simp [is_vector_binary ,Vector.toList_reverse]
 
 theorem is_vector_binary_cons {a : ZMod n} {vec : Vector (ZMod n) d}:
   is_vector_binary (a ::ᵥ vec) ↔ is_bit a ∧ is_vector_binary vec := by
-  unfold is_vector_binary
-  conv => lhs; unfold List.foldr; simp
+  simp [is_vector_binary]
 
-theorem is_vector_binary_dropLast {d n : Nat} {gate_0 : Vector (ZMod n) d} :
-  is_vector_binary gate_0 → is_vector_binary (Vector.dropLast gate_0) := by
-  simp [is_vector_binary, Vector.toList_dropLast]
-  intro h
-  induction gate_0 using Vector.inductionOn with
-  | h_nil => simp [List.dropLast]
-  | h_cons ih =>
-    rename_i x xs
-    cases xs using Vector.casesOn
-    simp
-    rw [Vector.toList_cons, Vector.toList_cons, List.dropLast_cons]
-    simp [h]
-    cases h
-    tauto
+lemma is_vector_binary_snoc {vs : Vector (ZMod (Nat.succ p)) n} {v}: is_vector_binary (vs.snoc v) ↔ is_vector_binary vs ∧ is_bit v := by
+  simp [is_vector_binary]
+  apply Iff.intro
+  . intro h
+    exact ⟨(fun a ha => h a (Or.inl ha)), h v (Or.inr rfl)⟩
+  . intro h
+    rcases h with ⟨hl, hr⟩
+    intro a ha
+    cases ha
+    . apply hl; assumption
+    . subst_vars; assumption
 
 lemma dropLast_symm {n} {xs : Vector Bit d} :
   Vector.map (fun i => @Bit.toZMod n i) (Vector.dropLast xs) = (Vector.map (fun i => @Bit.toZMod n i) xs).dropLast := by
@@ -417,28 +428,7 @@ theorem zmod_to_bit_coe {n : Nat} [Fact (n > 1)] {w : Vector Bit d} :
     }
 
 theorem vector_binary_of_bit_to_zmod {n : Nat} [Fact (n > 1)] {w : Vector Bit d }:
-  is_vector_binary (w.map (Bit.toZMod (n := n))) := by
-  induction w using Vector.inductionOn with
-  | h_nil => trivial
-  | h_cons ih =>
-    simp [is_vector_binary_cons]
-    apply And.intro
-    . unfold Bit.toZMod
-      split <;> {
-        have : n > 1 := (inferInstance : Fact (n > 1)).elim
-        induction n with
-        | zero =>
-          apply absurd this
-          simp
-        | succ n =>
-          induction n with
-          | zero =>
-            apply absurd this
-            simp
-          | succ =>
-            simp [is_bit]
-      }
-    . apply ih
+  is_vector_binary (w.map (Bit.toZMod (n := n))) := by simp [is_vector_binary]
 
 theorem recover_binary_of_to_bits {n : Nat} [Fact (n > 1)] {w : Vector Bit d} {v : ZMod n}:
   nat_to_bits_le d v.val = some w →
@@ -606,10 +596,9 @@ lemma bitCases_bZero {n:Nat}: bitCases (@bZero (n + 2)) = Bit.zero := by rfl
 @[simp]
 lemma bitCases_bOne {n:Nat}: bitCases (@bOne (n+2)) = Bit.one := by rfl
 
-theorem is_vector_binary_iff_allIxes_is_bit {n : Nat} {v : Vector (ZMod n) d}: Vector.allIxes is_bit v ↔ is_vector_binary v := by
-  induction v using Vector.inductionOn with
-  | h_nil => simp [is_vector_binary]
-  | h_cons ih => conv => lhs; simp [ih]
+-- theorem is_vector_binary_iff_allIxes_is_bit {n : Nat} {v : Vector (ZMod n) d}: Vector.allIxes is_bit v ↔ is_vector_binary v := by
+--   rw [Vector.allIxes_iff_allElems]
+--   rfl
 
 theorem fin_to_bits_le_recover_binary_nat {v : Vector Bit d}:
   fin_to_bits_le ⟨recover_binary_nat v, binary_nat_lt _⟩ = v := by

ProvenZk/Ext/Vector/Basic.lean

@@ -1,4 +1,5 @@
 import Mathlib.Data.Vector.Snoc
+import Mathlib.Data.Vector.Mem
 import Mathlib.Data.Matrix.Basic
 import Mathlib.Data.List.Defs
 
@@ -251,44 +252,65 @@ theorem ofFn_snoc' { fn : Fin (Nat.succ n) → α }:
     congr
     simp [Nat.mod_eq_of_lt]
 
-def allIxes (f : α → Prop) : Vector α n → Prop := fun v => ∀(i : Fin n), f v[i]
+instance : Membership α (Vector α n) := ⟨fun x xs => x ∈ xs.toList⟩
 
 @[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]
+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 allIxes_nil : allIxes f Vector.nil := by
-  simp [allIxes]
+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]
 
-theorem getElem_allIxes {v : { v: Vector α n // allIxes prop v  }} {i : Nat} { i_small : i < n}:
-  v.val[i]'i_small = ↑(Subtype.mk (v.val.get ⟨i, i_small⟩) (v.prop ⟨i, i_small⟩)) := by rfl
+-- @[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]
 
-theorem getElem_allIxes₂ {v : { v: Vector (Vector α m) n // allIxes (allIxes prop) v  }} {i j: Nat} { i_small : i < n} { j_small : j < m}:
-  (v.val[i]'i_small)[j]'j_small = ↑(Subtype.mk ((v.val.get ⟨i, i_small⟩).get ⟨j, j_small⟩) (v.prop ⟨i, i_small⟩ ⟨j, j_small⟩)) := by rfl
+-- @[simp]
+-- theorem allIxes_nil : allIxes f Vector.nil := by
+--   simp [allIxes]
 
-theorem allIxes_indexed {v : {v : Vector α n // allIxes prop v}} {i : Nat} {i_small : i < n}:
-  prop (v.val[i]'i_small) := v.prop ⟨i, i_small⟩
+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 allIxes_indexed₂ {v : {v : Vector (Vector (Vector α a) b) c // allIxes (allIxes prop) v}}
+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) :=
-  v.prop ⟨i, i_small⟩ ⟨j, j_small⟩
+  prop ((v.val[i]'i_small)[j]'j_small) := by
+  apply v.prop (v.val[i]'i_small) <;> simp [getElem]
 
-theorem allIxes_indexed₃ {v : {v : Vector (Vector (Vector α a) b) c // allIxes (allIxes (allIxes prop)) v}}
+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) :=
-  v.prop ⟨i, i_small⟩ ⟨j, j_small⟩ ⟨k, k_small⟩
+  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 → α) :
@@ -333,59 +355,71 @@ theorem append_inj {v₁ w₁ : Vector α d₁} {v₂ w₂ : Vector α d₂}:
     subst_vars
     apply And.intro <;> rfl
 
-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 allIxes_append {v₁ : Vector α n₁} {v₂ : Vector α n₂} : Vector.allIxes prop (v₁ ++ v₂) ↔ Vector.allIxes prop v₁ ∧ Vector.allIxes prop v₂ := by
-  simp [allIxes_toList]
-  apply Iff.intro
-  . intro h
-    apply And.intro
-    . intro i
-      rcases i with ⟨i, hp⟩
-      simp at hp
-      rw [←List.get_append]
-      exact h ⟨i, (by simp; apply Nat.lt_add_right; assumption)⟩
-    . intro i
-      rcases i with ⟨i, hp⟩
-      simp at hp
-      have := h ⟨n₁ + i, (by simpa)⟩
-      rw [List.get_append_right] at this
-      simp at this
-      exact this
-      . simp
-      . simpa
-  . intro ⟨l, r⟩
-    intro ⟨i, hi⟩
-    simp at hi
-    cases lt_or_ge i n₁ with
-    | inl hp =>
-      rw [List.get_append _ (by simpa)]
-      exact l ⟨i, (by simpa)⟩
-    | inr hp =>
-      rw [List.get_append_right]
-      have := r ⟨i - n₁, (by simp; apply Nat.sub_lt_left_of_lt_add; exact LE.le.ge hp; assumption )⟩
-      simp at this
-      simpa
-      . simp; exact LE.le.ge hp
-      . simp; apply Nat.sub_lt_left_of_lt_add; exact LE.le.ge hp; assumption
-
-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_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 allIxes_append {v₁ : Vector α n₁} {v₂ : Vector α n₂} : Vector.allIxes prop (v₁ ++ v₂) ↔ Vector.allIxes prop v₁ ∧ Vector.allIxes prop v₂ := by
+--   simp [allIxes_toList]
+--   apply Iff.intro
+--   . intro h
+--     apply And.intro
+--     . intro i
+--       rcases i with ⟨i, hp⟩
+--       simp at hp
+--       rw [←List.get_append]
+--       exact h ⟨i, (by simp; apply Nat.lt_add_right; assumption)⟩
+--     . intro i
+--       rcases i with ⟨i, hp⟩
+--       simp at hp
+--       have := h ⟨n₁ + i, (by simpa)⟩
+--       rw [List.get_append_right] at this
+--       simp at this
+--       exact this
+--       . simp
+--       . simpa
+--   . intro ⟨l, r⟩
+--     intro ⟨i, hi⟩
+--     simp at hi
+--     cases lt_or_ge i n₁ with
+--     | inl hp =>
+--       rw [List.get_append _ (by simpa)]
+--       exact l ⟨i, (by simpa)⟩
+--     | inr hp =>
+--       rw [List.get_append_right]
+--       have := r ⟨i - n₁, (by simp; apply Nat.sub_lt_left_of_lt_add; exact LE.le.ge hp; assumption )⟩
+--       simp at this
+--       simpa
+--       . simp; exact LE.le.ge hp
+--       . simp; apply Nat.sub_lt_left_of_lt_add; exact LE.le.ge hp; assumption
+
+-- 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
 
 end Vector