From 539545228c4d78cc3fdbf369c3934ad27fd17b32 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Sun, 1 Sep 2024 00:03:28 +0200 Subject: Move BinaryHeap to its own Github project. --- Common/Nat.lean | 172 -------------------------------------------------------- 1 file changed, 172 deletions(-) delete mode 100644 Common/Nat.lean (limited to 'Common/Nat.lean') 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 -- cgit v1.2.3