From 87915b495463baaffaf9675a9daebf40753ff83d Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Wed, 15 Nov 2023 02:05:34 +0000
Subject: [PATCH] Added bit theorems

---
 ProvenZk/Binary.lean           | 48 ++++++++++++++++++++++++++++++++++
 ProvenZk/Ext/Vector/Basic.lean | 12 +++++++++
 ProvenZk/Misc.lean             | 13 +++++++++
 3 files changed, 73 insertions(+)

diff --git a/ProvenZk/Binary.lean b/ProvenZk/Binary.lean
index f07e241..068eaef 100644
--- a/ProvenZk/Binary.lean
+++ b/ProvenZk/Binary.lean
@@ -3,6 +3,7 @@ import Mathlib.Data.Bitvec.Defs
 
 import ProvenZk.Ext.List
 import ProvenZk.Ext.Vector
+import ProvenZk.Subvector
 
 inductive Bit : Type where
   | zero : Bit
@@ -76,6 +77,10 @@ abbrev bOne : {v : ZMod n // is_bit v} := ⟨1, by simp⟩
 
 abbrev bZero : {v : ZMod n // is_bit v} := ⟨0, by simp⟩
 
+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))
 
@@ -600,3 +605,46 @@ 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 fin_to_bits_le_recover_binary_nat {v : Vector Bit d}:
+  fin_to_bits_le ⟨recover_binary_nat v, binary_nat_lt _⟩ = v := by
+  unfold fin_to_bits_le
+  split
+  . rename_i h
+    rw [←recover_binary_nat_to_bits_le] at h
+    exact binary_nat_unique _ _ h
+  . contradiction
+
+theorem SubVector_map_cast_lower {v : SubVector α n prop} {f : α → β }:
+  (v.val.map f) = v.lower.map fun (x : Subtype prop) => f x.val := by
+  rw [←Vector.ofFn_get v.val]
+  simp only [SubVector.lower, GetElem.getElem, Vector.map_ofFn]
+
+@[simp]
+theorem recover_binary_nat_fin_to_bits_le {v : Fin (2^d)}:
+  recover_binary_nat (fin_to_bits_le v) = v.val := by
+  unfold fin_to_bits_le
+  split
+  . rename_i h
+    rw [←recover_binary_nat_to_bits_le] at h
+    assumption
+  . contradiction
+
+@[simp]
+theorem SubVector_lower_lift : SubVector.lift (SubVector.lower v) = v := by
+  unfold SubVector.lift
+  unfold SubVector.lower
+  apply Subtype.eq
+  simp [GetElem.getElem]
+
+@[simp]
+theorem SubVector_lift_lower : SubVector.lower (SubVector.lift v) = v := by
+  unfold SubVector.lift
+  unfold SubVector.lower
+  apply Subtype.eq
+  simp [GetElem.getElem]
diff --git a/ProvenZk/Ext/Vector/Basic.lean b/ProvenZk/Ext/Vector/Basic.lean
index 09cbaa6..440d511 100644
--- a/ProvenZk/Ext/Vector/Basic.lean
+++ b/ProvenZk/Ext/Vector/Basic.lean
@@ -290,4 +290,16 @@ theorem allIxes_indexed₃ {v : {v : Vector (Vector (Vector α a) b) c // allIxe
   prop (((v.val[i]'i_small)[j]'j_small)[k]'k_small) :=
   v.prop ⟨i, i_small⟩ ⟨j, j_small⟩ ⟨k, k_small⟩
 
+@[simp]
+theorem map_ofFn {f : α → β} (g : Fin n → α) :
+  Vector.map f (Vector.ofFn g) = Vector.ofFn (fun x => f (g x)) := by
+  apply Vector.eq
+  simp
+  rfl
+
+@[simp]
+theorem map_id': Vector.map (fun x => x) v = v := by
+  have : ∀α, (fun (x:α) => x) = id := by intro _; funext _; rfl
+  rw [this, Vector.map_id]
+
 end Vector
diff --git a/ProvenZk/Misc.lean b/ProvenZk/Misc.lean
index edee748..52eea7f 100644
--- a/ProvenZk/Misc.lean
+++ b/ProvenZk/Misc.lean
@@ -81,3 +81,16 @@ theorem is_bit_one_sub {a : ZMod N}: is_bit (Gates.sub 1 a) ↔ is_bit a := by
 lemma double_prop {a b c d : Prop} : (b ∧ a ∧ c ∧ a ∧ d) ↔ (b ∧ a ∧ c ∧ d) := by
   simp
   tauto
+
+lemma and_iff (P Q R : Prop): (Q ↔ R) → (P ∧ Q ↔ P ∧ R) := by
+  tauto
+
+lemma ex_iff {P Q : α → Prop}: (∀x, P x ↔ Q x) → ((∃x, P x) ↔ ∃x, Q x) := by
+  intro h;
+  apply Iff.intro <;> {
+    intro h1
+    cases h1; rename_i witness prop
+    exists witness
+    try { rw [h witness]; assumption }
+    try { rw [←h witness]; assumption }
+  }