Partial cleanup of Heap

1 files changed, 25 insertions, 119 deletions

diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean
index 922e9bf..741318b 100644
--- a/Common/BinaryHeap.lean
+++ b/Common/BinaryHeap.lean
@@ -1,3 +1,5 @@
+import Common.Nat
+
 namespace BinaryHeap
 
 /--A heap, represented as a binary indexed tree. The heap predicate is a type parameter, the index is the element count.-/
@@ -39,122 +41,11 @@ def BinaryHeap.length : BinaryHeap α lt n → Nat := λ_ ↦ n
 /--Creates an empty BinaryHeap. Needs the heap predicate as parameter.-/
 abbrev BinaryHeap.empty {α : Type u} (lt : α → α → Bool ) := BinaryHeap.leaf (α := α) (lt := lt)
 
-private theorem eq_power_of_two_power_of_two (n : Nat) : (n.nextPowerOfTwo = n) → n.isPowerOfTwo := by
-  have h₂ := Nat.isPowerOfTwo_nextPowerOfTwo n
-  intro h₁
-  revert h₂
-  rewrite[h₁]
-  intro
-  assumption
-
-private theorem power_of_two_go_eq_eq (n : Nat) (p : n >0) : Nat.nextPowerOfTwo.go n n p = n := by
-  unfold Nat.nextPowerOfTwo.go
-  simp_arith
-
-private theorem smaller_smaller_exp {n m : Nat} (p : 2 ^ n < 2 ^ m) : n < m :=
-  if h₁ : m ≤ n  then
-    by have h₂ := Nat.pow_le_pow_of_le_right (by decide : 2 > 0) h₁
-       have h₃ := Nat.lt_of_le_of_lt h₂ p
-       simp_arith at h₃
-  else
-    by rewrite[Nat.not_ge_eq] at h₁
-       trivial
-
-
-
-private theorem mul2_isPowerOfTwo_smaller_smaller_equal (n : Nat) (power : Nat) (h₁ : n.isPowerOfTwo) (h₂ : power.isPowerOfTwo) (h₃ : power < n) : power * 2 ≤ n := by
-  unfold Nat.isPowerOfTwo at h₁ h₂
-  have ⟨k, h₄⟩ := h₁
-  have ⟨l, h₅⟩ := h₂
-  rewrite [h₅]
-  rewrite[←Nat.pow_succ 2 l]
-  rewrite[h₄]
-  have h₆ : 2 > 0 := by decide
-  apply (Nat.pow_le_pow_of_le_right h₆)
-  rewrite [h₅] at h₃
-  rewrite [h₄] at h₃
-  have h₃ := smaller_smaller_exp h₃
-  simp_arith at h₃
-  assumption
-
-
-private theorem power_of_two_go_one_eq (n : Nat) (power : Nat) (h₁ : n.isPowerOfTwo) (h₂ : power.isPowerOfTwo) (h₃ : power ≤ n) : Nat.nextPowerOfTwo.go n power (Nat.pos_of_isPowerOfTwo h₂) = n := by
-  unfold Nat.nextPowerOfTwo.go
-  split
-  case inl h₄ => exact power_of_two_go_one_eq n (power*2) (h₁) (Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₂) (mul2_isPowerOfTwo_smaller_smaller_equal n power h₁ h₂ h₄)
-  case inr h₄ => rewrite[Nat.not_lt_eq power n] at h₄
-                 exact Nat.le_antisymm h₃ h₄
-termination_by power_of_two_go_one_eq _ p _ _ _ => n - p
-decreasing_by
-  simp_wf
-  have := Nat.pos_of_isPowerOfTwo h₂
-  apply Nat.nextPowerOfTwo_dec <;> assumption
-
-private theorem power_of_two_eq_power_of_two (n : Nat) : n.isPowerOfTwo → (n.nextPowerOfTwo = n) := by
-  intro h₁
-  unfold Nat.nextPowerOfTwo
-  apply power_of_two_go_one_eq
-  case h₁ => assumption
-  case h₂ => exact Nat.one_isPowerOfTwo
-  case h₃ => exact (Nat.pos_of_isPowerOfTwo h₁)
-
-theorem power_of_two_iff_next_power_eq (n : Nat) : n.isPowerOfTwo ↔ (n.nextPowerOfTwo = n) :=
-  Iff.intro (power_of_two_eq_power_of_two n) (eq_power_of_two_power_of_two n)
-
-theorem power_of_two_mul_two_lt {n m : Nat} (h₁ : m.isPowerOfTwo) (h₂ : n < 2*m) (h₃ : ¬(n+1).isPowerOfTwo) : n+1 < 2*m :=
-  if h₄ : n+1 > 2*m then by
-    have h₂ := Nat.succ_le_of_lt h₂
-    rewrite[←Nat.not_ge_eq] at h₂
-    simp_arith at h₄
-    contradiction
-  else if h₅ : n+1 = 2*m then by
-    have h₆ := Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₁
-    rewrite[Nat.mul_comm 2 m] at h₅
-    rewrite[←h₅] at h₆
-    contradiction
-  else by
-    simp_arith at h₄
-    exact Nat.lt_of_le_of_ne h₄ h₅
-
-theorem Nat.mul2_ispowerOfTwo_iff_isPowerOfTwo (n : Nat) : n.isPowerOfTwo ↔ (2*n).isPowerOfTwo :=
-  have h₁ : n.isPowerOfTwo → (2*n).isPowerOfTwo := by
-    simp[Nat.mul_comm]
-    apply Nat.mul2_isPowerOfTwo_of_isPowerOfTwo
-  have h₂ : (2*n).isPowerOfTwo → n.isPowerOfTwo :=
-    if h₂ : n.nextPowerOfTwo = n then by
-      simp[power_of_two_iff_next_power_eq,h₂]
-    else by
-      intro h₃
-      simp[←power_of_two_iff_next_power_eq] at h₂
-      have h₅ := h₃
-      unfold Nat.isPowerOfTwo at h₃
-      let ⟨k,h₄⟩ := h₃
-      cases n with
-      | zero => contradiction
-      | succ m => cases k with
-        | zero => simp_arith at h₄
-                  have h₆ (m : Nat) : 2*m+2 > 2^0 := by
-                    induction m with
-                    | zero => decide
-                    | succ o o_ih => simp_arith at *
-                                     have h₆ := Nat.le_step $ Nat.le_step o_ih
-                                     simp_arith at h₆
-                                     assumption
-                  have h₆ := Nat.ne_of_lt (h₆ m)
-                  simp_arith at h₆
-                  rewrite[h₄] at h₆ --why is this needed?!?
-                  contradiction
-        | succ l => rewrite[Nat.pow_succ 2 l] at h₄
-                    rewrite[Nat.mul_comm (2^l) 2] at h₄
-                    have h₄ := Nat.eq_of_mul_eq_mul_left (by decide : 0<2) h₄
-                    exists l
-  Iff.intro h₁ h₂
-
 mutual
-  def Nat.isEven : Nat → Bool
+  def Nat.isEven : Nat → Prop
   | .zero => True
   | .succ n => Nat.isOdd n
-  def Nat.isOdd : Nat → Bool
+  def Nat.isOdd : Nat → Prop
   | .zero => False
   | .succ n => Nat.isEven n
 end
@@ -210,6 +101,21 @@ theorem Nat.pred_even_odd {n : Nat} (h₁ : Nat.isEven n) (h₂ : n > 0) : Nat.i
   | succ o => simp[Nat.isEven] at h₁
               assumption
 
+theorem power_of_two_mul_two_lt {n m : Nat} (h₁ : m.isPowerOfTwo) (h₂ : n < 2*m) (h₃ : ¬(n+1).isPowerOfTwo) : n+1 < 2*m :=
+  if h₄ : n+1 > 2*m then by
+    have h₂ := Nat.succ_le_of_lt h₂
+    rewrite[←Nat.not_ge_eq] at h₂
+    simp_arith at h₄
+    contradiction
+  else if h₅ : n+1 = 2*m then by
+    have h₆ := Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₁
+    rewrite[Nat.mul_comm 2 m] at h₅
+    rewrite[←h₅] at h₆
+    contradiction
+  else by
+    simp_arith at h₄
+    exact Nat.lt_of_le_of_ne h₄ h₅
+
 theorem power_of_two_mul_two_le {n m : Nat} (h₁ : (n+1).isPowerOfTwo) (h₂ : n < 2*(m+1)) (h₃ : ¬(m+1).isPowerOfTwo) (h₄ : m > 0): n < 2*m :=
   if h₅ : n > 2*m then by
     simp_arith at h₂
@@ -253,7 +159,7 @@ def BinaryHeap.insert (elem : α) (heap : BinaryHeap α lt o) : BinaryHeap α lt
                                rewrite[s]
                                simp[r]
       have difference_decreased := Nat.le_succ_of_le $ Nat.le_succ_of_le max_height_difference
-      let result := branch a left (right.insert elem) (q) difference_decreased (by simp[(eq_power_of_two_power_of_two (n+1)), r])
+      let result := branch a left (right.insert elem) (q) difference_decreased (by simp[(Nat.power_of_two_iff_next_power_eq (n+1)), r])
       result
     else
       have q : m ≤ n+1 := by apply (Nat.le_of_succ_le)
@@ -274,7 +180,7 @@ def BinaryHeap.insert (elem : α) (heap : BinaryHeap α lt o) : BinaryHeap α lt
                          contradiction
         else by
           simp at h₁
-          rewrite[←power_of_two_iff_next_power_eq] at h₁
+          rewrite[←Nat.power_of_two_iff_next_power_eq] at h₁
           cases subtree_complete
           case inl => contradiction
           case inr => trivial
@@ -283,7 +189,7 @@ def BinaryHeap.insert (elem : α) (heap : BinaryHeap α lt o) : BinaryHeap α lt
         cases r
         case inl h₁ => rewrite[Nat.not_gt_eq n m] at h₁
                        simp_arith[Nat.le_antisymm h₁ p]
-        case inr h₁ => simp[←power_of_two_iff_next_power_eq] at h₁
+        case inr h₁ => simp[←Nat.power_of_two_iff_next_power_eq] at h₁
                        simp[h₁] at subtree_complete
                        exact power_of_two_mul_two_lt subtree_complete max_height_difference h₁
       let result := branch a (left.insert elem) right q still_in_range (Or.inr right_is_power_of_two)
@@ -342,7 +248,7 @@ def BinaryHeap.popLast {α : Type u} {lt : α → α → Bool} (heap : BinaryHea
                              simp[a]
           have rightIsFull : (m+1).isPowerOfTwo := by
             have r := And.right r
-            simp[←power_of_two_iff_next_power_eq] at r
+            simp[←Nat.power_of_two_iff_next_power_eq] at r
             assumption
           have l_lt_2_m_succ : l < 2 * (m+1) := by apply Nat.lt_of_succ_lt; assumption
           (res, q▸BinaryHeap.branch a newLeft right s l_lt_2_m_succ (Or.inr rightIsFull))
@@ -380,7 +286,7 @@ def BinaryHeap.popLast {α : Type u} {lt : α → α → Bool} (heap : BinaryHea
                            rewrite[←h₂] at subtree_complete
                            simp at subtree_complete
                            assumption
-            case inr h₁ => simp_arith[←power_of_two_iff_next_power_eq] at h₁
+            case inr h₁ => simp_arith[←Nat.power_of_two_iff_next_power_eq] at h₁
                            rewrite[h₂] at h₁
                            simp[h₁] at subtree_complete
                            assumption
@@ -393,7 +299,7 @@ def BinaryHeap.popLast {α : Type u} {lt : α → α → Bool} (heap : BinaryHea
                         have h₄ := Nat.mul_lt_mul_of_pos_right (by decide : 1 < 2) this
                         simp at h₄
                         assumption
-            | inr h₁ => simp[←power_of_two_iff_next_power_eq, h₂] at h₁
+            | inr h₁ => simp[←Nat.power_of_two_iff_next_power_eq, h₂] at h₁
                         apply power_of_two_mul_two_le <;> assumption
 
           (res, BinaryHeap.branch a left newRight s still_in_range (Or.inl leftIsFull))