diff options
Diffstat (limited to 'Common')
| -rw-r--r-- | Common/BinaryHeap.lean | 56 | ||||
| -rw-r--r-- | Common/Nat.lean | 60 |
2 files changed, 61 insertions, 55 deletions
diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean index 741318b..4daf7b0 100644 --- a/Common/BinaryHeap.lean +++ b/Common/BinaryHeap.lean @@ -41,60 +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) -mutual - def Nat.isEven : Nat → Prop - | .zero => True - | .succ n => Nat.isOdd n - 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 - theorem Nat.not_even_odd {n : Nat} (h₁ : ¬Nat.isEven n) : (Nat.isOdd n) := by - simp[Nat.isEven] at h₁ - cases n with - | zero => contradiction - | succ o => simp[Nat.isEven, Nat.isOdd] at * - exact (Nat.not_odd_even (by simp[h₁])) - theorem Nat.not_odd_even {n : Nat} (h₁ : ¬Nat.isOdd n) : (Nat.isEven n) := by - simp[Nat.isOdd] at h₁ - cases n with - | zero => trivial - | succ o => simp[Nat.isEven, Nat.isOdd] at * - exact (Nat.not_even_odd (by simp[h₁])) -end - -mutual - theorem Nat.even_not_odd {n : Nat} (h₁ : Nat.isEven n) : ¬(Nat.isOdd n ):= by - cases n with - | zero => simp - | succ o => simp[Nat.isEven, Nat.isOdd] at * - simp[Nat.odd_not_even h₁] - theorem Nat.odd_not_even {n : Nat} (h₁ : Nat.isOdd n) : ¬(Nat.isEven n ):= by - cases n with - | zero => contradiction - | succ o => simp[Nat.isEven, Nat.isOdd] at * - simp[Nat.even_not_odd h₁] -end - - theorem Nat.pred_even_odd {n : Nat} (h₁ : Nat.isEven n) (h₂ : n > 0) : Nat.isOdd n.pred := by cases n with | zero => contradiction @@ -135,7 +81,7 @@ theorem power_of_two_mul_two_le {n m : Nat} (h₁ : (n+1).isPowerOfTwo) (h₂ : have h₉ := Nat.pred_even_odd h₉ (by simp_arith[h₇]) simp at h₉ have h₁₀ := Nat.mul_2_is_even h₆ - have h₁₀ := Nat.even_not_odd h₁₀ + have h₁₀ := Nat.even_not_odd_even.mp h₁₀ contradiction else by simp[Nat.not_gt_eq] at h₅ diff --git a/Common/Nat.lean b/Common/Nat.lean index 71420ed..fd7337b 100644 --- a/Common/Nat.lean +++ b/Common/Nat.lean @@ -91,3 +91,63 @@ theorem Nat.mul2_ispowerOfTwo_iff_isPowerOfTwo (n : Nat) : n.isPowerOfTwo ↔ (2 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 => trivial + | 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 => 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 |