Move BinaryHeap to its own Github project.

1 files changed, 0 insertions, 172 deletions

diff --git a/Common/Nat.lean b/Common/Nat.lean
deleted file mode 100644
index e921f2b..0000000
--- a/Common/Nat.lean
+++ /dev/null
@@ -1,172 +0,0 @@
-
-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 isTrue 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 isFalse h₄ => rewrite[Nat.not_lt_eq power n] at h₄
-                     exact Nat.le_antisymm h₃ h₄
-termination_by n - power
-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₄
-        | 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
-  -- intentionally not decidable. This is a logical model, not meant for runtime!
-  def Nat.isEven : Nat → Prop
-  | .zero => True
-  | .succ n => Nat.isOdd n
-  -- intentionally not decidable. This is a logical model, not meant for runtime!
-  def Nat.isOdd : Nat → Prop
-  | .zero => False
-  | .succ n => Nat.isEven n
-end
-
-theorem Nat.mul_2_is_even {n m : Nat} (h₁ : n = 2 * m) : Nat.isEven n := by
-  cases m with
-  | zero => simp[Nat.isEven, h₁]
-  | succ o => simp_arith at h₁
-              simp[Nat.isEven, Nat.isOdd, h₁]
-              exact Nat.mul_2_is_even (rfl)
-
-theorem Nat.isPowerOfTwo_even_or_one {n : Nat} (h₁ : n.isPowerOfTwo) : (n = 1 ∨ (Nat.isEven n)) := by
-  simp[Nat.isPowerOfTwo] at h₁
-  let ⟨k,h₂⟩ := h₁
-  cases k with
-  | zero => simp_arith[h₂]
-  | succ l => rewrite[Nat.pow_succ] at h₂
-              rewrite[Nat.mul_comm (2^l) 2] at h₂
-              exact Or.inr $ Nat.mul_2_is_even h₂
-
-mutual
-  private theorem Nat.not_even_odd {n : Nat} (h₁ : ¬Nat.isEven n) : (Nat.isOdd n) := by
-    cases n with
-    | zero => unfold Nat.isEven at h₁; contradiction
-    | succ o => simp[Nat.isEven, Nat.isOdd] at *
-                exact (Nat.not_odd_even (by simp[h₁]))
-  private theorem Nat.not_odd_even {n : Nat} (h₁ : ¬Nat.isOdd n) : (Nat.isEven n) := by
-    cases n with
-    | zero => simp[isEven]
-    | succ o => simp[Nat.isEven, Nat.isOdd] at *
-                exact (Nat.not_even_odd (by simp[h₁]))
-end
-
-mutual
-  private theorem Nat.even_not_odd {n : Nat} (h₁ : Nat.isEven n) : ¬(Nat.isOdd n ):= by
-    cases n with
-    | zero => unfold Nat.isOdd; trivial
-    | succ o => simp[Nat.isEven, Nat.isOdd] at *
-                simp[Nat.odd_not_even h₁]
-  private theorem Nat.odd_not_even {n : Nat} (h₁ : Nat.isOdd n) : ¬(Nat.isEven n ):= by
-    cases n with
-    | zero => unfold isOdd at h₁; contradiction
-    | succ o => simp[Nat.isEven, Nat.isOdd] at *
-                simp[Nat.even_not_odd h₁]
-end
-
-theorem Nat.odd_not_even_odd {n : Nat} : Nat.isOdd n ↔ ¬Nat.isEven n :=
-  Iff.intro Nat.odd_not_even Nat.not_even_odd
-
-theorem Nat.even_not_odd_even {n : Nat} : Nat.isEven n ↔ ¬Nat.isOdd n :=
-  Iff.intro Nat.even_not_odd Nat.not_odd_even
-
-theorem Nat.pred_even_odd {n : Nat} (h₁ : Nat.isEven n) (h₂ : n > 0) : Nat.isOdd n.pred := by
-  cases n with
-  | zero => contradiction
-  | succ o => simp[Nat.isEven] at h₁
-              assumption
-
-theorem Nat.sub_lt_of_lt_add {a b c : Nat} (h₁ : a < c + b) (h₂ : b ≤ a) : a - b < c :=
-  have h₃ : a + 1 ≤ c + b := Nat.succ_le_of_lt h₁
-  have h₄ := Nat.sub_le_of_le_add h₃
-  have h₅ : 1 + a - b ≤ c := (Nat.add_comm a 1).subst (motive := λx ↦ x - b ≤ c) h₄
-  have h₆ := Nat.add_sub_assoc h₂ 1
-  have h₇ : 1 + (a-b) ≤ c := h₆.subst (motive := λx ↦ x ≤ c) h₅
-  have h₈ : (a-b) + 1 ≤ c := (Nat.add_comm 1 (a-b)).subst (motive := λx ↦ x ≤ c) h₇
-  Nat.lt_of_succ_le h₈
-
-theorem Nat.sub_lt_sub_right {a b c : Nat} (h₁ : b ≤ a) (h₂ : a < c) : (a - b < c - b) := by
-  apply Nat.sub_lt_of_lt_add
-  case h₂ => assumption
-  case h₁ =>
-    have h₃ : b ≤ c := Nat.le_of_lt $ Nat.lt_of_le_of_lt h₁ h₂
-    rw[Nat.sub_add_cancel h₃]
-    assumption
-
-theorem Nat.add_eq_zero {a b : Nat} :  a + b = 0 ↔ a = 0 ∧ b = 0 := by
-  constructor <;> intro h₁
-  case mpr =>
-    simp[h₁]
-  case mp =>
-    cases a <;> simp_arith at *; assumption