Partial cleanup of Heap

1 files changed, 93 insertions, 0 deletions

diff --git a/Common/Nat.lean b/Common/Nat.lean
new file mode 100644
index 0000000..71420ed
--- /dev/null
+++ b/Common/Nat.lean
@@ -0,0 +1,93 @@
+
+theorem Nat.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
+
+theorem Nat.smaller_smaller_exp {n m o : Nat} (p : o ^ n < o ^ m) (q : o > 0) : n < m :=
+  if h₁ : m ≤ n  then
+    by have h₂ := Nat.pow_le_pow_of_le_right (q) 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₃ := Nat.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₁)
+
+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
+
+theorem Nat.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 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₂