diff options
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean | 22 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapOperations.lean | 25 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean | 4 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean | 10 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/NatLemmas.lean | 145 |
5 files changed, 91 insertions, 115 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index 8222879..c3b77ad 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -31,7 +31,7 @@ protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : N case isFalse goRight => dsimp only [Nat.pred_eq_sub_one, Nat.succ_eq_add_one, Fin.isValue] cases r -- to work around cast - case leaf => simp +ground at goRight; exact absurd goRight.symm n_m_not_zero + case leaf => exact absurd ⟨Nat.pos_of_ne_zero (Ne.symm n_m_not_zero),Nat.isPowerOfTwo_one⟩ goRight case branch rv rl rr rm_le_n rmax_height_difference rsubtree_full => rw[get_right, right_unfold] case h₂ => simp +arith[leftLen_unfold] @@ -76,9 +76,7 @@ protected theorem heapRemoveLastWithIndexHeapRemoveLastSameTree {α : Type u} {n simp only cases p case zero => - simp +ground only [Nat.zero_add, decide_true, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂ - simp only [Nat.add_zero] at h₁ - exact absurd h₂.symm h₁ + exact absurd ⟨Nat.pos_of_ne_zero (Ne.symm h₁),Nat.isPowerOfTwo_one⟩ h₂ case succ pp => simp only have h₃ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameTree r @@ -111,9 +109,7 @@ protected theorem heapRemoveLastWithIndexHeapRemoveLastSameElement {α : Type u} simp only cases p case zero => - simp +ground only [Nat.zero_add, decide_true, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂ - simp only [Nat.add_zero] at h₁ - exact absurd h₂.symm h₁ + exact absurd ⟨Nat.pos_of_ne_zero (Ne.symm h₁),Nat.isPowerOfTwo_one⟩ h₂ case succ pp => simp only have h₃ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameElement r @@ -205,7 +201,7 @@ rename_i o p v l r _ _ _ simp only [Nat.add_eq, ne_eq] at h₂ simp only [Nat.add_eq, h₂, ↓reduceDIte, decide_eq_true_eq, Fin.zero_eta, Fin.isValue, Nat.succ_eq_add_one, Fin.castLE_succ, Nat.pred_eq_sub_one, gt_iff_lt] at h₁ ⊢ -if h₃ : p < o ∧ (p + 1).nextPowerOfTwo = p + 1 then +if h₃ : p < o ∧ (p + 1).isPowerOfTwo then --removed left simp only [h₃, and_self, ↓reduceDIte, Fin.isValue] at h₁ ⊢ cases o @@ -258,9 +254,7 @@ else simp only [h₃, ↓reduceDIte, Fin.isValue] at h₁ ⊢ cases p <;> simp only [Nat.add_zero, Nat.reduceSub, Nat.reduceAdd, Fin.isValue] at h₁ ⊢ case zero => - simp +ground only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₃ - subst o - contradiction + exact absurd ⟨Nat.pos_of_ne_zero (Ne.symm h₂),Nat.isPowerOfTwo_one⟩ h₃ case succ pp _ _ _ _ => generalize hold : get index (branch v l r _ _ _) = oldValue have h₄ : index ≠ 0 := Fin.ne_zero_of_gt h₁ @@ -316,7 +310,7 @@ protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (hea simp only [Nat.add_eq, ne_eq] at h₃ simp only [h₃, Nat.add_eq, Fin.zero_eta, Fin.isValue, decide_eq_true_eq, Nat.succ_eq_add_one, Fin.castLE_succ, Nat.pred_eq_sub_one, reduceDIte] at h₁ ⊢ - if h₄ : p < o ∧ (p + 1).nextPowerOfTwo = p + 1 then + if h₄ : p < o ∧ (p + 1).isPowerOfTwo then --removed left --get has to go into the square hole - erm, left branch too cases o @@ -348,9 +342,7 @@ protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (hea simp only [h₄, ↓reduceDIte, Fin.isValue] at h₁ ⊢ cases p case zero => - simp +ground only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₄ - subst o - contradiction + exact absurd ⟨Nat.pos_of_ne_zero (Ne.symm h₃),Nat.isPowerOfTwo_one⟩ h₄ case succ pp _ _ _ _ => if h₄ : index > o then --get goes into right branch -> recursion diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean index 2901b61..5ebc335 100644 --- a/BinaryHeap/CompleteTree/HeapOperations.lean +++ b/BinaryHeap/CompleteTree/HeapOperations.lean @@ -25,7 +25,7 @@ def heapPush (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) : let (elem, a) := if le elem a then (a, elem) else (elem, a) -- okay, based on n and m we know if we want to add left or right. -- the left tree is full, if (n+1) is a power of two AND n != m - let leftIsFull := (n+1).nextPowerOfTwo = n+1 + let leftIsFull := (n+1).isPowerOfTwo if r : m < n ∧ leftIsFull then ( branch @@ -34,7 +34,7 @@ def heapPush (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) : (right.heapPush le elem) r.left (Nat.le_succ_of_le ∘ Nat.le_succ_of_le $ max_height_difference) - (Or.inl $ (Nat.power_of_two_iff_next_power_eq (n+1)).mpr r.right) + (Or.inl r.right) : CompleteTree α (n+(m+1)+1) ) else @@ -49,7 +49,6 @@ def heapPush (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) : have h₃ : ¬m≤n := Nat.not_le_of_gt $ Nat.lt_of_le_of_ne h₂ s absurd p h₃ else - have h₁ : ¬(n+1).isPowerOfTwo := h₁ ∘ (Nat.power_of_two_iff_next_power_eq (n+1)).mp match subtree_complete with | .inl h₂ => absurd h₂ h₁ | .inr h₂ => h₂ @@ -61,7 +60,6 @@ def heapPush (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) : have : ∀ (a : Nat), a > 0 → a < 2 * a := λa ha ↦ (Nat.one_mul _).subst (motive := λx ↦ x < 2*a) $ (Nat.mul_lt_mul_right ha).mpr (Nat.lt.base 1) h₁.subst (motive := λx↦(n+1) < 2*(x+1)) $ this (n+1) (Nat.succ_pos _) | .inr h₁ => - have h₁ : ¬(n+1).isPowerOfTwo := h₁ ∘ (Nat.power_of_two_iff_next_power_eq (n+1)).mp match subtree_complete with | .inl h₂ => absurd h₂ h₁ | .inr h₂ => power_of_two_mul_two_lt h₂ max_height_difference h₁ @@ -86,7 +84,7 @@ private theorem power_of_two_mul_two_le {n m : Nat} (h₁ : (n+1).isPowerOfTwo) if h₅ : n > 2*m then have h₆ : n + 1 = 2*(m+1) := congrArg Nat.succ $ Nat.eq_of_le_of_lt_succ h₅ h₂ have h₇ : (2*(m+1)).isPowerOfTwo := h₆.subst h₁ - have h₈ : (m+1).isPowerOfTwo := (Nat.mul2_ispowerOfTwo_iff_isPowerOfTwo (m+1)).mpr h₇ + have h₈ : (m+1).isPowerOfTwo := by exact (Nat.mul2_ispowerOfTwo_iff_isPowerOfTwo (m+1)).mpr h₇ absurd h₈ h₃ else if h₆ : n = 2*m then -- since (n+1) is a power of 2, n cannot be an even number, but n = 2*m means it's even @@ -104,25 +102,23 @@ private theorem power_of_two_mul_two_le {n m : Nat} (h₁ : (n+1).isPowerOfTwo) h₅.resolve_left h₆ /-- Helper for heapRemoveLastAux -/ -private theorem removeRightLeftIsFull {n m : Nat} (r : ¬(m < n ∧ ((m+1).nextPowerOfTwo = m+1 : Bool))) (m_le_n : m ≤ n) (subtree_complete : (n + 1).isPowerOfTwo ∨ (m + 1).isPowerOfTwo) : (n+1).isPowerOfTwo := by +private theorem removeRightLeftIsFull {n m : Nat} (r : ¬(m < n ∧ (m+1).isPowerOfTwo)) (m_le_n : m ≤ n) (subtree_complete : (n + 1).isPowerOfTwo ∨ (m + 1).isPowerOfTwo) : (n+1).isPowerOfTwo := by rewrite[Decidable.not_and_iff_or_not] at r cases r case inl h₁ => rewrite[Nat.not_lt_eq] at h₁ have h₂ := Nat.le_antisymm h₁ m_le_n rewrite[←h₂, or_self] at subtree_complete assumption - case inr h₁ => simp[←Nat.power_of_two_iff_next_power_eq] at h₁ - exact Or.resolve_right subtree_complete h₁ + case inr h₁ => exact Or.resolve_right subtree_complete h₁ /-- Helper for heapRemoveLastAux -/ -private theorem stillInRange {n m : Nat} (r : ¬(m < n ∧ ((m+1).nextPowerOfTwo = m+1 : Bool))) (m_le_n : m ≤ n) (m_gt_0 : m > 0) (leftIsFull : (n+1).isPowerOfTwo) (max_height_difference: n < 2 * (m + 1)) : n < 2*m := by +private theorem stillInRange {n m : Nat} (r : ¬(m < n ∧ (m+1).isPowerOfTwo)) (m_le_n : m ≤ n) (m_gt_0 : m > 0) (leftIsFull : (n+1).isPowerOfTwo) (max_height_difference: n < 2 * (m + 1)) : n < 2*m := by rewrite[Decidable.not_and_iff_or_not] at r cases r with | inl h₁ => have m_eq_n : m = n := Nat.le_antisymm m_le_n (Nat.not_lt.mp h₁) have m_lt_2_m : m < 2 * m := (Nat.one_mul m).subst (motive := λ x ↦ x < 2 * m) $ Nat.mul_lt_mul_of_pos_right Nat.one_lt_two m_gt_0 exact m_eq_n.subst (motive := λx ↦ x < 2 * m) m_lt_2_m - | inr h₁ => simp +zetaDelta only [← Nat.power_of_two_iff_next_power_eq, decide_eq_true_eq] at h₁ - apply power_of_two_mul_two_le <;> assumption + | inr h₁ => apply power_of_two_mul_two_le <;> assumption /-- Removes the last element, and computes additional values via the supplied lambdas. @@ -145,7 +141,7 @@ protected def Internal.heapRemoveLastAux if p : 0 = (n+m) then (p▸CompleteTree.leaf, p▸aux0 a) else - let rightIsFull : Bool := (m+1).nextPowerOfTwo = m+1 + let rightIsFull := (m+1).isPowerOfTwo if r : m < n ∧ rightIsFull then --remove left match n, left with @@ -153,17 +149,16 @@ protected def Internal.heapRemoveLastAux let ((newLeft : CompleteTree α l), res) := Internal.heapRemoveLastAux left aux0 auxl auxr have q : l + m + 1 = l + 1 + m := Nat.add_right_comm l m 1 have s : m ≤ l := Nat.le_of_lt_succ r.left - have rightIsFull : (m+1).isPowerOfTwo := (Nat.power_of_two_iff_next_power_eq (m+1)).mpr $ decide_eq_true_eq.mp r.right have l_lt_2_m_succ : l < 2 * (m+1) := Nat.lt_of_succ_lt max_height_difference let res := auxl res (Nat.lt_of_le_of_lt (Nat.le_add_right (l+1) m) (Nat.lt_succ_self (l+1+m))) - (q▸CompleteTree.branch a newLeft right s l_lt_2_m_succ (Or.inr rightIsFull), res) + (q▸CompleteTree.branch a newLeft right s l_lt_2_m_succ (Or.inr r.right), res) else --remove right have m_gt_0 : m > 0 := match hm : m with | 0 => have hn : 0 < n := Nat.pos_of_ne_zero $ Ne.symm p - have hr : rightIsFull = true := decide_eq_true $ hm▸(Nat.nextPowerOfTwo.go.eq_def 1 1 _).substr (p := λx↦x = 0+1) rfl + have hr : (m+1).isPowerOfTwo := hm.substr $ (Nat.zero_add 1).subst Nat.isPowerOfTwo_one absurd ⟨hn, hr⟩ r | mm+1 => Nat.succ_pos mm let l := m.pred diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean index 52cba4c..4320473 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean @@ -46,7 +46,7 @@ theorem heapPushRootSameOrElem (elem : α) (heap : CompleteTree α o) (lt : α contradiction simp rename_i n m v l r _ _ _ - split -- if h : m < n ∧ Nat.nextPowerOfTwo (n + 1) = n + 1 then + split -- if h : m < n ∧ (n + 1).isPowerOfTwo then case h_2.isTrue h => cases (lt elem v) <;> simp[instDecidableEqBool, Bool.decEq, root] case h_2.isFalse h => @@ -109,7 +109,7 @@ theorem heapPushIsHeap {α : Type u} {elem : α} {heap : CompleteTree α o} {le trivial case h_2 n m v l r m_le_n _ _ => simp - split -- if h₅ : m < n ∧ Nat.nextPowerOfTwo (n + 1) = n + 1 then + split -- if h₅ : m < n ∧ (n + 1).isPowerOfTwo then case' isTrue => have h := heapPushIsHeapAux le n m v elem l r h₁ h₂ h₃ case' isFalse => diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean index 8eec6df..3d8f65a 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean @@ -85,7 +85,7 @@ protected theorem heapRemoveLastAuxLeavesRoot have h₃ : (0 ≠ o + p) := Ne.symm $ Nat.ne_zero_of_lt h₁ simp[h₃] exact - if h₄ : p < o ∧ Nat.nextPowerOfTwo (p + 1) = p + 1 then by + if h₄ : p < o ∧ (p + 1).isPowerOfTwo then by simp[h₄] cases o case zero => exact absurd h₄.left $ Nat.not_lt_zero p @@ -97,8 +97,7 @@ protected theorem heapRemoveLastAuxLeavesRoot simp[h₄] cases p case zero => - have h₁ : 0 < o := (Nat.add_zero o).subst h₁ - simp +ground[h₁] at h₄ -- the second term in h₄ is decidable and True. What remains is ¬(0 < o), or o = 0 + exact absurd ⟨h₁,Nat.isPowerOfTwo_one⟩ h₄ case succ pp hp => simp +arith apply root_unfold @@ -121,7 +120,7 @@ private theorem heapRemoveLastAuxIsHeap else by simp[h₄] exact - if h₅ : (m<n ∧ Nat.nextPowerOfTwo (m+1) = m+1) then by + if h₅ : (m<n ∧ (m+1).isPowerOfTwo) then by simp only [h₅, and_self, ↓reduceDIte] cases n case zero => @@ -148,8 +147,7 @@ private theorem heapRemoveLastAuxIsHeap simp[h₅] cases m case zero => - simp only [Nat.add_zero] at h₄ -- n ≠ 0 - simp +ground only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq, Ne.symm h₄] at h₅ -- the second term in h₅ is decidable and True. What remains is ¬(0 < n), or n = 0 + exact absurd ⟨Nat.pos_of_ne_zero (Ne.symm h₄), Nat.isPowerOfTwo_one⟩ h₅ case succ mm h₆ h₇ h₈ => unfold HeapPredicate at * simp only [h₁, heapRemoveLastAuxIsHeap aux0 auxl auxr h₁.right.left h₂ h₃, true_and] diff --git a/BinaryHeap/CompleteTree/NatLemmas.lean b/BinaryHeap/CompleteTree/NatLemmas.lean index b8b067a..5c01b13 100644 --- a/BinaryHeap/CompleteTree/NatLemmas.lean +++ b/BinaryHeap/CompleteTree/NatLemmas.lean @@ -1,5 +1,16 @@ namespace Nat +instance {n : Nat} : Decidable (isPowerOfTwo n) := + have h₀ : ∀(x:Nat), 1<<<x = 2^x := λx ↦ (Nat.one_mul _).subst $ Nat.shiftLeft_eq 1 x + if h₁ : 1<<<n.log2 = n then + Decidable.isTrue ⟨n.log2, (h₀ n.log2).subst h₁.symm⟩ + else + Decidable.isFalse λ⟨k,h₂⟩ ↦ + have : 2^(log2 (2^k)) ≠ 2 ^ k := h₂.subst (motive := λx ↦ 2^(log2 x) ≠ x) ((h₀ n.log2).subst (Ne.symm h₁)).symm + have := Nat.log2_two_pow.subst (motive := λx ↦ 2^x ≠ 2^k) this + this.elim rfl + +@[deprecated Nat.pow_lt_pow_iff_right (since := "2025-11-10")] theorem 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_right (q) h₁ @@ -9,85 +20,78 @@ theorem smaller_smaller_exp {n m o : Nat} (p : o ^ n < o ^ m) (q : o > 0) : n < 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_right h₆) - rewrite [h₅] at h₃ - rewrite [h₄] at h₃ - have h₃ := smaller_smaller_exp h₃ - simp 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.isPowerOfTwo_mul_two_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 - 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.isPowerOfTwo_one - 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 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 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.isPowerOfTwo_mul_two_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 + have h₂ : (2*n).isPowerOfTwo → n.isPowerOfTwo := by + unfold isPowerOfTwo + intro h₂ + have ⟨k, h₂⟩ := h₂ + have : n = 2 ^ k.pred := by + rw[←Nat.pow_pred_mul, Nat.mul_comm, Nat.mul_left_inj (by decide)] at h₂ + assumption + cases n + case zero => + have := Nat.ne_of_lt (Nat.pow_pos (n := k) (Nat.two_pos)) + exact absurd ((Nat.mul_zero 2).subst (motive := λx↦x = 2^k) h₂) this + case succ m h₁ => + have h₃ : 2^0 = 1 := rfl + cases k + case zero => + rw[h₃] at h₂ + have : 2* (m+1) > 1 := (Nat.mul_succ 2 m).substr $ Nat.lt_add_left (2 * m) Nat.one_lt_two + exact absurd h₂ $ Nat.ne_of_gt this + case succ kk => exact Nat.zero_lt_succ kk + exact ⟨k.pred, this⟩ Iff.intro h₁ h₂ mutual - -- intentionally not decidable. This is a logical model, not meant for runtime! def isEven : Nat → Prop | .zero => True | .succ n => Nat.isOdd n - -- intentionally not decidable. This is a logical model, not meant for runtime! def isOdd : Nat → Prop | .zero => False | .succ n => Nat.isEven n end +mutual +private theorem mod2_eq_zero_even {n : Nat} (h₀ : n % 2 = 0) : n.isEven := match n with +| .zero => True.intro +| .succ m => + have : m % 2 ≠ 0 := Nat.mod_two_ne_zero.mpr (Nat.succ_mod_succ_eq_zero_iff.mp h₀) + mod2_ne_zero_odd this + +private theorem mod2_ne_zero_odd {n : Nat} (h₀ : n % 2 ≠ 0) : n.isOdd := match n with +| .zero => h₀.elim rfl +| .succ m => + have : m % 2 = 0 := by + have : m.succ % 2 = 1 := Nat.mod_two_ne_zero.mp h₀ + rw[←Nat.succ_mod_succ_eq_zero_iff, (Nat.add_assoc m 1 1), Nat.mod_eq] at this + simp at this + assumption + mod2_eq_zero_even this +end + +mutual + private theorem 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 odd_not_even {n : Nat} (h₁ : Nat.isOdd n) : ¬(Nat.isEven n ):= by + cases n with + | zero => exact h₁.elim + | succ o => simp[Nat.isEven, Nat.isOdd] at * + simp[Nat.even_not_odd h₁] +end + +instance {n : Nat} : Decidable (isEven n) := + if h₀ : n % 2 = 0 then + Decidable.isTrue $ mod2_eq_zero_even h₀ + else + Decidable.isFalse $ odd_not_even $ mod2_ne_zero_odd h₀ + theorem mul_2_is_even {n m : Nat} (h₁ : n = 2 * m) : Nat.isEven n := by cases m with | zero => simp[Nat.isEven, h₁] @@ -118,19 +122,6 @@ mutual exact (Nat.not_even_odd (by simp[h₁])) end -mutual - private theorem 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 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 odd_not_even_odd {n : Nat} : Nat.isOdd n ↔ ¬Nat.isEven n := Iff.intro Nat.odd_not_even Nat.not_even_odd |