From 4ef392d9b29bc040c17d97f39ed6e66b51d8b6cc Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Sun, 31 Dec 2023 17:14:30 +0000
Subject: [PATCH] Finished le equivalence proof

---
 ProvenZk/Binary.lean           |  2 +-
 ProvenZk/GatesEquivalence.lean | 67 ++++++++++++----------------------
 2 files changed, 24 insertions(+), 45 deletions(-)

diff --git a/ProvenZk/Binary.lean b/ProvenZk/Binary.lean
index fb2e7c0..df98045 100644
--- a/ProvenZk/Binary.lean
+++ b/ProvenZk/Binary.lean
@@ -77,7 +77,7 @@ def nat_to_bits_le_full : Nat → List Bit
       apply Nat.div_le_self
     bit_mod_two (n+2) :: nat_to_bits_le_full ((n+2) / 2)
 
-def binary_length (n : Nat) : Nat := List.length (nat_to_bits_le_full n)
+def binary_length (n : Nat) : Nat := (Nat.log 2 n).succ
 
 def nat_to_bit (x : Nat) : Bit := match x with
   | 0 => Bit.zero
diff --git a/ProvenZk/GatesEquivalence.lean b/ProvenZk/GatesEquivalence.lean
index 0aa1315..6d9dd05 100644
--- a/ProvenZk/GatesEquivalence.lean
+++ b/ProvenZk/GatesEquivalence.lean
@@ -86,6 +86,29 @@ def nat_to_binary_self {d : Nat} :
         contradiction
       )
 
+lemma one_plus_one : x+1+1 = x+2 := by simp_arith
+
+lemma nat_succ_div_two : n.succ.succ / 2 = Nat.succ (n/2) := by
+  simp_arith
+
+lemma log2_mul {n} : 2 * 2 ^ Nat.log 2 n > n := by
+  rw [<-pow_succ]
+  rw [add_comm]
+  rw [<-Nat.succ_eq_one_add]
+  simp
+  apply Nat.lt_pow_succ_log_self
+  simp
+
+lemma binary_lt_two_pow_length {n : Nat} : 2^(binary_length n) > n := by
+  induction n with
+  | zero => simp
+  | succ n' _ =>
+    conv => rhs; rw [Nat.succ_eq_one_add]
+    rw [binary_length]
+    conv => lhs; arg 2; arg 1; rw [Nat.succ_eq_one_add]
+    rw [Nat.succ_eq_one_add, add_comm, pow_succ]
+    apply log2_mul
+
 @[simp]
 lemma is_bool_equivalence {a : ZMod N} :
   GatesDef.is_bool a ↔ a = 0 ∨ a = 1 := by
@@ -341,50 +364,6 @@ lemma is_zero_equivalence' {a out: ZMod N} :
       . tauto
       . tauto
 
-lemma one_plus_one : x+1+1 = x+2 := by simp_arith
-
-lemma nat_succ_div_two : n.succ.succ / 2 = Nat.succ (n/2) := by
-  simp_arith
-
-lemma mul_lt_div {x y a : Nat} : x < a * y ↔ x/a < y := by
-  sorry
-
-lemma binary_lt_two_pow_length {n : Nat} : 2^(binary_length n) > n := by
-  induction n with
-  | zero => simp
-  | succ n' ih =>
-    induction n' with
-    | zero => simp
-    | succ n'' ih' =>
-      simp [binary_length]
-      simp [nat_to_bits_le_full]
-      rw [<-binary_length]
-      simp [pow_succ]
-      simp at *
-      have hc : 0 < 2 := by
-        simp_arith
-
-      rw [mul_lt_div]
-      rw [nat_succ_div_two]
-
-      -- rw [Nat.succ_eq_add_one]
-      -- rw [one_plus_one]
-      -- conv => lhs; rw [<-mul_one (a := n''+2)]
-      -- conv => rhs; rw [mul_comm]
-      -- rw [<-div_lt_div_iff']
-
-      --rw [<-@div_lt_iff' (a := a) (b := b) (c := c) (hc := by subst_vars; simp [hc]; sorry)]
-      sorry
-
-lemma testNat : x.succ <= 2^x → (x/2).succ <= 2^(x/2) := by
-  intro h
-  induction x with
-  | zero =>
-    simp_arith
-  | succ n ih =>
-
-    sorry
-
 @[simp]
 lemma le_equivalence {a b : ZMod N} :
   GatesDef.le_9 a b ↔ a.val <= b.val := by