From e1f64e3a14366e3733fbfd5b5de4d120bb352c11 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Mon, 18 Dec 2023 22:03:15 +0100 Subject: Even more cleanup in Heap --- Common/BinaryHeap.lean | 6 ------ Common/Nat.lean | 6 ++++++ 2 files changed, 6 insertions(+), 6 deletions(-) (limited to 'Common') diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean index 4daf7b0..eb24db6 100644 --- a/Common/BinaryHeap.lean +++ b/Common/BinaryHeap.lean @@ -41,12 +41,6 @@ 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) -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 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₂ diff --git a/Common/Nat.lean b/Common/Nat.lean index fd7337b..5725b6c 100644 --- a/Common/Nat.lean +++ b/Common/Nat.lean @@ -151,3 +151,9 @@ theorem Nat.odd_not_even_odd {n : Nat} : Nat.isOdd n ↔ ¬Nat.isEven n := 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 -- cgit v1.2.3