diff options
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/Get.lean | 2 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean | 22 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapOperations.lean | 2 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/NatLemmas.lean | 11 | ||||
| -rw-r--r-- | lean-toolchain | 2 |
5 files changed, 16 insertions, 23 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean index 7379638..aad82c5 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean @@ -9,7 +9,7 @@ theorem get_zero_eq_root {α : Type u} {n : Nat} (tree : CompleteTree α n) (h | nn+1, ⟨j+1,h₄⟩, _ => by subst h₂ simp only [Nat.succ_eq_add_one, Fin.zero_eta, heq_eq_eq, Fin.ext_iff, Fin.val_zero, - Nat.self_eq_add_left, Nat.add_one_ne_zero] at h₃ + Nat.right_eq_add, Nat.add_one_ne_zero] at h₃ theorem get_right {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin n) (h₂ : index > tree.leftLen (Nat.zero_lt_of_lt index.isLt)) : have h₁ : n > 0 := Nat.zero_lt_of_lt index.isLt diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean b/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean index e913a59..5e11d8e 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean @@ -21,13 +21,13 @@ private theorem Option.bind_some_eq_map {α β : Type u} (f : α → β) (a : Op private theorem Option.is_some_map {α : Type u} {β : Type v} {f : α → β} {a : Option α} : (Option.map f a).isSome ↔ a.isSome := by cases a - case none => simp only [Option.map_none', Option.isSome_none] - case some => simp only [Option.map_some', Option.isSome_some] + case none => simp only [Option.map_none, Option.isSome_none] + case some => simp only [Option.map_some, Option.isSome_some] -private theorem Option.orElse_is_some {α : Type u} (a b : Option α) : (HOrElse.hOrElse a λ_ ↦ b).isSome = (a.isSome || b.isSome) := by +private theorem Option.orElse_is_some {α : Type u} (a b : Option α) : (Option.orElse a (λ_↦b)).isSome = true ↔ a.isSome || b.isSome := by cases a - case none => simp only [Option.none_orElse, Option.isSome_none, Bool.false_or] - case some _ => simp only [Option.some_orElse, Option.isSome_some, Bool.true_or] + case none => simp only [Option.none_orElse, Option.isSome_none, Bool.false_or, imp_self] + case some _ => simp only [Option.some_orElse, Option.isSome_some, Bool.true_or, imp_self] private theorem Option.isSome_of_eq_some {α : Type u} {a : α} {o : Option α} : o = some a → o.isSome := by intro h₁ @@ -55,7 +55,7 @@ private theorem indexOfNoneImpPredFalseAux {α : Type u} {n : Nat} (tree : Compl simp only [Nat.add_zero, Nat.reduceAdd, Option.pure_def, Option.bind_eq_bind] at h₂ have h₂₂ := Option.orElse_result_none_both_none h₂ repeat rw[Option.bind_some_eq_map] at h₂₂ - simp only [Option.map_eq_none'] at h₂₂ + simp only [Option.map_eq_none_iff] at h₂₂ if h₃ : index = ⟨0,h₁⟩ then subst index rw[←get_zero_eq_root, root_unfold] @@ -99,7 +99,7 @@ private theorem indexOfSomeImpPredTrueAux2 {α : Type u} {p : Nat} {r : Complete simp only [Option.isSome_some, imp_self] case isFalse => unfold Function.comp - simp only [Option.map_some'] + simp only [Option.map_some] repeat rw[Option.bind_some_eq_map] simp only [Option.orElse_is_some, Bool.or_eq_true, Option.is_some_map] intro h₁ @@ -142,7 +142,7 @@ private theorem indexOfAuxAddsCurrentIndex {α : Type u} {n : Nat} (tree : Compl have hx₂ := Option.isSome_of_eq_some hx₂ have hx₂ : (Internal.indexOfAux l pred _).isSome := Option.is_some_map.mp hx₂ have hx₂ := indexOfSomeImpPredTrueAux2 _ off hx₂ - have hx₁ := Option.map_eq_none.mp hx₁ + have hx₁ := Option.map_eq_none_iff.mp hx₁ have hx₁ := Option.not_isSome_iff_eq_none.mpr hx₁ contradiction all_goals @@ -227,11 +227,11 @@ theorem indexOfSomeImpPredTrue {α : Type u} {n : Nat} (tree : CompleteTree α n case false => --unfold HOrElse.hOrElse instHOrElseOfOrElse at he₁ unfold Function.comp at he₁ - simp only [h₃, Bool.false_eq_true, ↓reduceIte, Option.map_some', Option.bind_some_eq_map] at he₁ + simp only [h₃, Bool.false_eq_true, ↓reduceIte, Option.map_some, Option.bind_some_eq_map] at he₁ cases h₄ : (Option.map (fun a => Fin.ofNat' (o+p+1) a.val) (Internal.indexOfAux l pred 1)) case none => rw[h₄, Option.none_orElse] at he₁ - simp only [Option.map_map, Option.map_eq_some', Function.comp_apply] at he₁ + simp only [Option.map_map, Option.map_eq_some_iff, Function.comp_apply] at he₁ rw[Nat.zero_add] at he₁ have h₅ : (Internal.indexOfAux r pred (o + 1)).isSome := Option.isSome_iff_exists.mpr (Exists.imp (λx ↦ And.left) he₁) have h₆ := indexOfSomeImpPredTrueAux2 _ 0 h₅ @@ -246,7 +246,7 @@ theorem indexOfSomeImpPredTrue {α : Type u} {n : Nat} (tree : CompleteTree α n exact h₉ case some lindex => rw[h₄, Option.some_orElse, Option.some_inj] at he₁ - simp only [Option.map_map, Option.map_eq_some', Function.comp_apply] at h₄ + simp only [Option.map_map, Option.map_eq_some_iff, Function.comp_apply] at h₄ subst lindex have h₅ : (Internal.indexOfAux l pred 1).isSome := Option.isSome_iff_exists.mpr (Exists.imp (λx ↦ And.left) h₄) have h₆ := indexOfSomeImpPredTrueAux2 _ 0 h₅ diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean index 28115b0..2901b61 100644 --- a/BinaryHeap/CompleteTree/HeapOperations.lean +++ b/BinaryHeap/CompleteTree/HeapOperations.lean @@ -11,7 +11,7 @@ private theorem power_of_two_mul_two_lt {n m : Nat} (h₁ : m.isPowerOfTwo) (h if h₄ : n+1 > 2*m then absurd h₄ ((Nat.not_lt_eq (2*m) (n+1)).substr $ Nat.succ_le_of_lt h₂) else if h₅ : n+1 = 2*m then - have h₆ : (2*m).isPowerOfTwo := (Nat.mul_comm 2 m).substr $ Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₁ + have h₆ : (2*m).isPowerOfTwo := (Nat.mul_comm 2 m).substr $ Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo h₁ have h₇ : (n+1).isPowerOfTwo := h₅.substr h₆ absurd h₇ h₃ else diff --git a/BinaryHeap/CompleteTree/NatLemmas.lean b/BinaryHeap/CompleteTree/NatLemmas.lean index 1050c17..b8b067a 100644 --- a/BinaryHeap/CompleteTree/NatLemmas.lean +++ b/BinaryHeap/CompleteTree/NatLemmas.lean @@ -27,7 +27,7 @@ private theorem mul2_isPowerOfTwo_smaller_smaller_equal (n : Nat) (power : Nat) 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 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 @@ -57,7 +57,7 @@ theorem power_of_two_iff_next_power_eq (n : Nat) : n.isPowerOfTwo ↔ (n.nextPow 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.mul2_isPowerOfTwo_of_isPowerOfTwo + 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₂] @@ -152,13 +152,6 @@ theorem sub_lt_of_lt_add {a b c : Nat} (h₁ : a < c + b) (h₂ : b ≤ a) : a - 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 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 at *; assumption - -- Yes, this is trivial. Still, I needed it so often, that it deserves its own lemma. theorem add_comm_right (a b c : Nat) : a + b + c = a + c + b := (rfl : a + b + c = a + b + c) diff --git a/lean-toolchain b/lean-toolchain index a0922e9..6c721df 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.19.0 +leanprover/lean4:4.20.1 |