Added to_binary and from_binary

ProvenZk/Binary.lean

@@ -178,6 +178,50 @@ def vector_zmod_to_bit {n d : Nat} (a : Vector (ZMod n) d) : Vector Bit d :=
 def vector_bit_to_zmod {n d : Nat} (a : Vector Bit d) : Vector (ZMod n) d :=
   Vector.map (fun x => Bit.toZMod x) a
 
+lemma bit_to_zmod_equiv {d} [Fact (n > 1)] (x : Vector Bit d) (y : Vector (ZMod n) d) (h : is_vector_binary y):
+  vector_bit_to_zmod x = y ↔ x = vector_zmod_to_bit y := by
+  apply Iff.intro
+  . intro hv
+    rename_i d
+    rw [<-hv]
+    induction x, y using Vector.inductionOn₂ with
+    | nil => simp
+    | cons ih=>
+      rename_i x y xs ys
+      simp [vector_bit_to_zmod, vector_zmod_to_bit]
+      simp [Vector.vector_eq_cons]
+      refine ⟨?_, ?_⟩
+      . simp [bit_to_zmod_to_bit]
+      . rw [<-vector_bit_to_zmod, <-vector_zmod_to_bit]
+        apply ih
+        . simp [is_vector_binary_cons] at h
+          tauto
+        . simp [vector_bit_to_zmod] at hv
+          simp [Vector.vector_eq_cons] at hv
+          rw [<-vector_bit_to_zmod] at hv
+          tauto
+  . intro hv
+    rename_i d
+    rw [hv]
+    induction x, y using Vector.inductionOn₂ with
+    | nil => simp
+    | cons ih=>
+      rename_i x y xs ys
+      simp [vector_bit_to_zmod, vector_zmod_to_bit]
+      simp [Vector.vector_eq_cons]
+      refine ⟨?_, ?_⟩
+      . rw [zmod_to_bit_to_zmod]
+        . simp [is_vector_binary_cons] at h
+          tauto
+      . rw [<-vector_bit_to_zmod, <-vector_zmod_to_bit]
+        apply ih
+        . simp [is_vector_binary_cons] at h
+          tauto
+        . simp [vector_zmod_to_bit] at hv
+          simp [Vector.vector_eq_cons] at hv
+          rw [<-vector_zmod_to_bit] at hv
+          tauto
+
 lemma vector_zmod_to_bit_last {n d : Nat} {xs : Vector (ZMod n) (d+1)} :
   (vector_zmod_to_bit xs).last = (zmod_to_bit xs.last) := by
   simp [vector_zmod_to_bit, Vector.last]
@@ -297,19 +341,21 @@ lemma parity_bit_unique (a b : Bit) (c d : Nat) : a + 2 * c = b + 2 * d -> a = b
   . assumption
 
 theorem binary_nat_unique {d} (rep1 rep2 : Vector Bit d):
-  recover_binary_nat rep1 = recover_binary_nat rep2 -> rep1 = rep2 := by
-  intro h
-  induction d with
-  | zero => apply Vector.zero_subsingleton.allEq;
-  | succ d1 ih =>
-    simp [recover_binary_nat] at h
-    rw [←Vector.cons_head_tail rep1]
-    rw [←Vector.cons_head_tail rep2]
-    have h := parity_bit_unique _ _ _ _ h
-    cases h
-    apply congr
-    . apply congrArg; assumption
-    . apply ih; assumption
+  recover_binary_nat rep1 = recover_binary_nat rep2 ↔ rep1 = rep2 := by
+  apply Iff.intro
+  . intro h
+    induction d with
+    | zero => apply Vector.zero_subsingleton.allEq;
+    | succ d1 ih =>
+      simp [recover_binary_nat] at h
+      rw [←Vector.cons_head_tail rep1]
+      rw [←Vector.cons_head_tail rep2]
+      have h := parity_bit_unique _ _ _ _ h
+      cases h
+      apply congr
+      . apply congrArg; assumption
+      . apply ih; assumption
+  . tauto
 
 theorem binary_nat_lt {d} (rep : Vector Bit d): recover_binary_nat rep < 2 ^ d := by
   induction d with
@@ -363,7 +409,8 @@ theorem binary_zmod_unique {n d} (rep1 rep2 : Vector Bit d):
     rw [same_recs]
   rw [binary_zmod_same_as_nat rep1 d_small] at same_vals
   rw [binary_zmod_same_as_nat rep2 d_small] at same_vals
-  exact binary_nat_unique _ _ same_vals
+  simp [binary_nat_unique] at same_vals
+  tauto
 
 theorem recover_binary_nat_to_bits_le {w : Vector Bit d}:
   recover_binary_nat w = v ↔
@@ -646,7 +693,8 @@ theorem fin_to_bits_le_recover_binary_nat {v : Vector Bit d}:
   split
   . rename_i h
     rw [←recover_binary_nat_to_bits_le] at h
-    exact binary_nat_unique _ _ h
+    simp [binary_nat_unique] at h
+    tauto
   . contradiction
 
 theorem SubVector_map_cast_lower {v : SubVector α n prop} {f : α → β }:

ProvenZk/Gates.lean

@@ -117,3 +117,40 @@ def GatesGnark_9 (N : Nat) [Fact (Nat.Prime N)] : Gates_base (ZMod N) := {
     cmp := GatesDef.cmp_9
     le := GatesDef.le_9
 }
+
+lemma recover_nat_unique (N : Nat) [Fact (Nat.Prime N)] (i1 i2 : Vector Bit (binary_length N)) :
+  i1 = i2 ↔ recover_binary_nat i1 = recover_binary_nat i2 := by
+  apply Iff.intro
+  . apply congr_arg
+  . simp [binary_nat_unique]
+
+lemma recover_nat_different (N : Nat) [Fact (Nat.Prime N)] (i1 i2 : Vector Bit (binary_length N)) :
+  i1 ≠ i2 ↔ recover_binary_nat i1 ≠ recover_binary_nat i2 := by
+  simp [recover_nat_unique]
+
+-- Given a Vector of size `binary_length N`, there are at least two numbers with length `binary_length N`
+-- whose `mod N` returns the same value.
+lemma recover_mod_not_unique (N : Nat) [Fact (Nat.Prime N)] (i1 i2 : Vector Bit (binary_length N)) :
+  (recover_binary_nat i2) % N = (recover_binary_nat i1) % N →
+  ((recover_binary_nat i2) + N) % N = (recover_binary_nat i1) % N:= by
+  intros
+  simp [Nat.mod_eq_sub_mod]
+  tauto
+
+lemma recover_unique (N : Nat) [Fact (Nat.Prime N)] (i1 : Vector Bit (binary_length N)) :
+  ∃i2 : Vector Bit (binary_length N),
+  (recover_binary_nat i2) = (recover_binary_nat i1) →
+  i2 = i1 := by
+  apply Exists.intro
+  rotate_left
+  . assumption
+  . tauto
+
+/-
+Given three numbers
+`i1` `i2` and `i3 = i2 + N`
+→
+le i1 i2 = le i1 i3
+although
+i1 < i2 ≠ i1 < i3
+-/

ProvenZk/GatesEquivalence.lean

@@ -35,6 +35,18 @@ theorem eq_mul_sides (a b out: ZMod N) : b ≠ 0 → ((out = a * b⁻¹) ↔ (ou
       . tauto
       . contradiction
 
+lemma split_vector_eq_cons {x : α} {xs : Vector α d} {y : Vector α d.succ} :
+  x ::ᵥ xs = y ↔ x = y.head ∧ xs = y.tail := by
+  apply Iff.intro
+  . intro h
+    rw [<-h]
+    simp
+  . intro h
+    casesm* (_ ∧ _)
+    rename_i hx hxs
+    rw [hx, hxs]
+    simp
+
 @[simp]
 lemma is_bool_equivalence {a : ZMod N} :
   GatesDef.is_bool a ↔ a = 0 ∨ a = 1 := by
@@ -233,7 +245,9 @@ lemma lookup_equivalence {b0 b1 i0 i1 i2 i3 out : ZMod N} :
     )
 
 @[simp]
-lemma cmp_equivalence : sorry := by sorry -- TODO
+lemma cmp_equivalence {a b out : ZMod N} :
+  GatesDef.cmp_9 a b out ↔ if a = b then out = 0 else (if a.val < b.val then out = -1 else out = 1) := by
+  sorry -- TODO
 
 @[simp]
 lemma is_zero_equivalence {a out: ZMod N} :
@@ -289,12 +303,114 @@ lemma is_zero_equivalence' {a out: ZMod N} :
       . tauto
 
 @[simp]
-lemma le_equivalence : sorry := by sorry -- TODO
+lemma le_equivalence {a b : ZMod N} :
+  GatesDef.le_9 a b ↔ a.val < b.val := by
+  sorry -- TODO
 
+def nat_to_binary_self {d : Nat} {h : d >= 1} :
+  recover_binary_nat (nat_to_bits_le_full_n d x) = x % 2^d := by
+  induction d generalizing x with
+  | zero =>
+    contradiction
+  | succ d' ih =>
+    simp [recover_binary_nat, nat_to_bits_le_full_n]
+    have : recover_binary_nat (nat_to_bits_le_full_n d' (x / 2)) = (x/2) % 2^d' := by
+      if 1 <= d' then
+        rw [ih (x := x/2)]
+        rw [Nat.succ_eq_add_one] at h
+        rw [ge_iff_le, le_add_iff_nonneg_left] at h
+        linarith
+      else
+        have : d' = 0 := by
+          linarith
+        subst_vars
+        simp [nat_to_bits_le_full_n, recover_binary_nat, Nat.mod_one]
+    rw [this]
+    rw [<-Nat.div2_val]
+    simp [bit_mod_two]
+    split
+    . rename_i h
+      simp only [Bit.toNat]
+      rw [Nat.mod_pow_succ]
+      rw [<-Nat.div2_val]
+      rw [h]
+      simp_arith
+    . rename_i h
+      simp only [Bit.toNat]
+      rw [Nat.mod_pow_succ]
+      rw [<-Nat.div2_val]
+      rw [h]
+      simp_arith
+    . rename_i h
+      apply False.elim (by
+        have := Nat.mod_lt x (y := 2)
+        rw [h] at this
+        simp at this
+        contradiction
+      )
+
+-- Should `hd : 2^d < N` be a hypothesis?
 @[simp]
-lemma to_binary_equivalence : sorry := by sorry -- TODO
+lemma to_binary_equivalence {a : ZMod N} {d : Nat} {out : Vector (ZMod N) d} (hd : 2^d < N) :
+  GatesDef.to_binary a d out ↔ vector_bit_to_zmod (nat_to_bits_le_full_n d a.val) = out := by
+  apply Iff.intro
+  . intro h
+    unfold GatesDef.to_binary at h
+    casesm* (_ ∧ _)
+    rename_i h hbin
+    rw [recover_binary_zmod_bit] at h
+    rw [binary_nat_zmod_equiv_mod_p] at h
+    rw [<-ZMod.val_nat_cast] at h
+    rw [ZMod.val_nat_cast_of_lt] at h
+    . induction d generalizing a with
+      | zero => simp
+      | succ d' _ =>
+        rw [<-nat_to_binary_self] at h
+        . simp [binary_nat_unique] at h
+          rw [bit_to_zmod_equiv]
+          rw [h]
+          simp [hbin]
+        . rw [<-Nat.add_one]
+          linarith
+    . rw [<-@binary_zmod_same_as_nat (n := N) (d := d) (rep := vector_zmod_to_bit out)]
+      . apply ZMod.val_lt
+      . simp [hd]
+    . simp [hbin]
+  . unfold GatesDef.to_binary
+    intro h
+    have hbin : is_vector_binary out := by
+      rw [<-h]
+      rw [vector_bit_to_zmod]
+      simp [vector_binary_of_bit_to_zmod]
+    rw [recover_binary_zmod_bit]
+    rw [binary_nat_zmod_equiv_mod_p]
+    rw [<-ZMod.val_nat_cast]
+    rw [ZMod.val_nat_cast_of_lt]
+    refine ⟨?_, ?_⟩
+    . induction d generalizing a with
+      | zero =>
+        simp [Nat.mod_one]
+        simp [vector_zmod_to_bit, recover_binary_nat]
+      | succ d' _ =>
+        rw [<-nat_to_binary_self]
+        . simp [binary_nat_unique]
+          apply Eq.symm
+          rw [<-bit_to_zmod_equiv]
+          . rw [h]
+          . simp [hbin]
+        . rw [<-Nat.add_one]
+          linarith
+    . simp [hbin]
+    . rw [<-@binary_zmod_same_as_nat (n := N) (d := d) (rep := vector_zmod_to_bit out)]
+      . apply ZMod.val_lt
+      . simp [hd]
+    . simp [hbin]
 
 @[simp]
-lemma from_binary_equivalence : sorry := by sorry -- TODO
+lemma from_binary_equivalence {d} {a : Vector (ZMod N) d} {out : ZMod N} (hd : 2^d < N)  :
+  GatesDef.from_binary a out ↔ vector_bit_to_zmod (nat_to_bits_le_full_n d out.val) = a := by
+  unfold GatesDef.from_binary
+  rw [<-GatesDef.to_binary]
+  apply to_binary_equivalence (hd := hd)
 
 end GatesEquivalence