From ff5c64836ede27d87dbc56b3869021ad8b0d255b Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Sun, 2 Nov 2025 16:23:04 +0100 Subject: Lean 4.21 --- BinaryHeap/CompleteTree/AdditionalOperations.lean | 6 ++-- .../AdditionalProofs/HeapUpdateAt.lean | 8 ++--- .../CompleteTree/AdditionalProofs/IndexOf.lean | 41 +++++++++++----------- .../CompleteTree/HeapProofs/HeapUpdateAt.lean | 4 +-- lean-toolchain | 2 +- 5 files changed, 31 insertions(+), 30 deletions(-) diff --git a/BinaryHeap/CompleteTree/AdditionalOperations.lean b/BinaryHeap/CompleteTree/AdditionalOperations.lean index 82dfbe9..5fcfbea 100644 --- a/BinaryHeap/CompleteTree/AdditionalOperations.lean +++ b/BinaryHeap/CompleteTree/AdditionalOperations.lean @@ -13,15 +13,15 @@ protected def Internal.indexOfAux {α : Type u} (heap : CompleteTree α o) (pred | (n+m+1), .branch a left right _ _ _ => have : NeZero (n + m + 1 + currentIndex) := ⟨Nat.pos_iff_ne_zero.mp $ Nat.add_pos_left (Nat.add_pos_right n (Nat.succ_pos m)) currentIndex⟩ if pred a then - let result := Fin.ofNat' _ currentIndex + let result := Fin.ofNat _ currentIndex some result else let found_left := CompleteTree.Internal.indexOfAux left pred (currentIndex + 1) - let found_left : Option (Fin (n+m+1+currentIndex)) := found_left.map λ a ↦ Fin.ofNat' _ a + let found_left : Option (Fin (n+m+1+currentIndex)) := found_left.map λ a ↦ Fin.ofNat _ a let found_right := found_left <|> - (CompleteTree.Internal.indexOfAux right pred (currentIndex + n + 1)).map ((λ a ↦ Fin.ofNat' _ a) : _ → Fin (n+m+1+currentIndex)) + (CompleteTree.Internal.indexOfAux right pred (currentIndex + n + 1)).map ((λ a ↦ Fin.ofNat _ a) : _ → Fin (n+m+1+currentIndex)) found_right /--Finds the first occurance of a given element in the heap and returns its index. Indices are depth first.-/ diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean index 8b5c5e3..ce4c894 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean @@ -97,14 +97,14 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo rename_i d1 d2 d3 d4 d5 o p v l r _ _ _ updateIndex _ _ clear d1 d2 d3 d4 d5 cases le v val <;> dsimp - case isFalse.true => + case h_1.true => -- v ≤ val -> current root smaller or equal, keep current root, move val down. split <;> simp only [gt_iff_lt, Nat.zero_lt_succ, contains_as_root_left_right] <;> left <;> rewrite[root_unfold] <;> rw[root_unfold] - case isFalse.false => + case h_1.false => -- v > val -> repace current root by val, move current root down. split <;> simp only [gt_iff_lt, Nat.zero_lt_succ, contains_as_root_left_right] @@ -137,7 +137,7 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo have h₄₂ : otherIndex > 0 := Fin.pos_iff_ne_zero.mpr h₄ rw[contains_as_root_left_right _ _ (Nat.succ_pos _)] right - case false.isTrue h₅ | true.isTrue h₅ => + case h_1.false.isTrue h₅ | h_1.true.isTrue h₅ => if h₆ : otherIndex ≤ o then have : otherIndex ≤ (branch v l r olep mhd stc).leftLen (Nat.succ_pos _) := by simp only [leftLen_unfold, h₆] rw[get_left _ _ h₄₂ this] @@ -157,7 +157,7 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo rw[contains_iff_index_exists] generalize (⟨↑otherIndex - o - 1, _⟩ : Fin _) = solution -- Allows to skip the annoying proof that Lean already has... exists solution - case false.isFalse h₅ | true.isFalse h₅ => + case h_1.false.isFalse h₅ | h_1.true.isFalse h₅ => if h₆ : otherIndex ≤ o then have : otherIndex ≤ (branch v l r olep mhd stc).leftLen (Nat.succ_pos _) := by simp only [leftLen_unfold, h₆] rw[get_left _ _ h₄₂ this] diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean b/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean index 5e11d8e..5cbfbf5 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean @@ -26,8 +26,8 @@ private theorem Option.is_some_map {α : Type u} {β : Type v} {f : α → β} { 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, imp_self] - case some _ => simp only [Option.some_orElse, Option.isSome_some, Bool.true_or, imp_self] + case none => simp only [Option.orElse_eq_or, Option.none_or, Option.isSome_none, Bool.false_or] + case some _ => simp only [Option.orElse_eq_or, Option.some_or, Option.isSome_some, Bool.true_or] private theorem Option.isSome_of_eq_some {α : Type u} {a : α} {o : Option α} : o = some a → o.isSome := by intro h₁ @@ -101,7 +101,7 @@ private theorem indexOfSomeImpPredTrueAux2 {α : Type u} {p : Nat} {r : Complete unfold Function.comp 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] + simp only [Option.isSome_or, Option.isSome_map, Bool.or_eq_true] intro h₁ cases h₁ case inl h₁ => @@ -119,8 +119,8 @@ private theorem indexOfAuxAddsCurrentIndex {α : Type u} {n : Nat} (tree : Compl split case isTrue => have : currentIndex < o + p + 1 + currentIndex := by simp +arith - simp only [Nat.add_eq, Nat.succ_eq_add_one, Option.get_some, Fin.val_ofNat', this, - Nat.mod_eq_of_lt, Nat.add_zero, Nat.zero_lt_succ, Nat.zero_add] + simp only [Nat.add_eq, Nat.succ_eq_add_one, Option.get_some, Fin.val_ofNat, this, + Nat.mod_eq_of_lt, Nat.add_zero, Fin.ofNat_zero, Fin.val_zero, Nat.zero_add] case isFalse => simp only [Nat.add_eq, Nat.succ_eq_add_one, Option.pure_def, Option.bind_eq_bind, Option.bind_some_eq_map, Option.map_map, Nat.add_zero, Nat.reduceAdd] @@ -136,9 +136,10 @@ private theorem indexOfAuxAddsCurrentIndex {α : Type u} {n : Nat} (tree : Compl clear d1 d2 -- In Lean, you know you are in for a world of pain if you split <;> split. split at hsplit₁ <;> split at hsplit₂ - case' h_1.h_2 => let off := 1 - case' h_2.h_1 => let off := currentIndex + 1 - case h_1.h_2 hx₂ _ _ hx₁ | h_2.h_1 hx₁ _ _ _ hx₂ => + rotate_left --case labels are now messed up in Lean 4.21... Soo, less readable... + case' h_2 => let off := 1 + case' h_1 => let off := currentIndex + 1 + case h_2 hx₂ _ _ hx₁ | h_1 hx₁ _ _ _ hx₂ => 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₂ @@ -147,20 +148,20 @@ private theorem indexOfAuxAddsCurrentIndex {α : Type u} {n : Nat} (tree : Compl contradiction all_goals simp only [Option.some.injEq] at hsplit₂ hsplit₁ - case' h_1.h_1 => + case' h_1 => have hsplit₂ := hsplit₂.symm have hsplit₁ := hsplit₁.symm subst hsplit₂ hsplit₁ let o1 := currentIndex + 1 let o2 := 1 let t := l - case' h_2.h_2 => + case' h_2 => let o1 := currentIndex + o + 1 let o2 := 0 + o + 1 let he₁ := hsplit₁ let he₂ := hsplit₂ let t := r - case h_1.h_1 he₂ he₁ | h_2.h_2 => + case h_1 he₂ he₁ | h_2 => have h₃ : (Internal.indexOfAux t pred o1).isSome := match Option.eq_some_iff_get_eq.mp he₁ with | Exists.intro he₁ _ => Option.is_some_map.mp he₁ @@ -178,11 +179,11 @@ private theorem indexOfAuxAddsCurrentIndex {α : Type u} {n : Nat} (tree : Compl simp +arith[o1, o2] -private theorem indexOfSomeImpPredTrueAuxR {α : Type u} {p : Nat} (r : CompleteTree α p) (pred : α → Bool) {o : Nat} (index : Fin ((o+p)+1)) (h₂ : (Internal.indexOfAux r pred 0).isSome) : ∀(a : Fin (p + (o + 1))), (Internal.indexOfAux r pred (o + 1) = some a ∧ Fin.ofNat' (o+p+1) ↑a = index) → (Internal.indexOfAux r pred 0).get h₂ + o + 1 = index.val := by +private theorem indexOfSomeImpPredTrueAuxR {α : Type u} {p : Nat} (r : CompleteTree α p) (pred : α → Bool) {o : Nat} (index : Fin ((o+p)+1)) (h₂ : (Internal.indexOfAux r pred 0).isSome) : ∀(a : Fin (p + (o + 1))), (Internal.indexOfAux r pred (o + 1) = some a ∧ Fin.ofNat (o+p+1) ↑a = index) → (Internal.indexOfAux r pred 0).get h₂ + o + 1 = index.val := by simp only [Nat.add_zero, and_imp] intros index₂ h₃ h₄ have : index₂.val = index.val := by - rw[Fin.ext_iff, Fin.val_ofNat'] at h₄ + rw[Fin.ext_iff, Fin.val_ofNat] at h₄ have : index₂.val % (o + p + 1) = index₂.val := Nat.mod_eq_of_lt $ (Nat.add_comm o p).substr $ (Nat.add_assoc o p 1).substr index₂.isLt exact this.subst (motive := λx↦x=index.val) h₄ rw[←this] @@ -191,11 +192,11 @@ private theorem indexOfSomeImpPredTrueAuxR {α : Type u} {p : Nat} (r : Complete rw[←this] simp only [h₃, Option.get_some] -private theorem indexOfSomeImpPredTrueAuxL {α : Type u} {o : Nat} (l : CompleteTree α o) (pred : α → Bool) {p : Nat} (index : Fin ((o+p)+1)) (h₂ : (Internal.indexOfAux l pred 0).isSome) : ∀(a : Fin ((o + 1))), (Internal.indexOfAux l pred 1 = some a ∧ Fin.ofNat' (o+p+1) ↑a = index) → (Internal.indexOfAux l pred 0).get h₂ + 1 = index.val := by +private theorem indexOfSomeImpPredTrueAuxL {α : Type u} {o : Nat} (l : CompleteTree α o) (pred : α → Bool) {p : Nat} (index : Fin ((o+p)+1)) (h₂ : (Internal.indexOfAux l pred 0).isSome) : ∀(a : Fin ((o + 1))), (Internal.indexOfAux l pred 1 = some a ∧ Fin.ofNat (o+p+1) ↑a = index) → (Internal.indexOfAux l pred 0).get h₂ + 1 = index.val := by simp only [Nat.add_zero, and_imp] intros index₂ h₃ h₄ have : index₂.val = index.val := by - rw[Fin.ext_iff, Fin.val_ofNat'] at h₄ + rw[Fin.ext_iff, Fin.val_ofNat] at h₄ have : o + 1 ≤ o+p+1 := Nat.succ_le_succ $ Nat.le_add_right o p have : index₂.val % (o + p + 1) = index₂.val := Nat.mod_eq_of_lt $ Nat.lt_of_lt_of_le index₂.isLt this exact this.subst (motive := λx↦x=index.val) h₄ @@ -220,7 +221,7 @@ theorem indexOfSomeImpPredTrue {α : Type u} {n : Nat} (tree : CompleteTree α n case true => simp only [h₃, ↓reduceIte, Option.some.injEq] at he₁ subst index - simp[Fin.ofNat'] at h₂ + simp[Fin.ofNat] at h₂ rw[←Fin.zero_eta, ←get_zero_eq_root, root_unfold] at h₂ subst v assumption @@ -228,10 +229,10 @@ theorem indexOfSomeImpPredTrue {α : Type u} {n : Nat} (tree : CompleteTree α n --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₁ - cases h₄ : (Option.map (fun a => Fin.ofNat' (o+p+1) a.val) (Internal.indexOfAux l pred 1)) + 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_iff, Function.comp_apply] at he₁ + rw[h₄, Option.none_or] at he₁ + simp only [Option.map_eq_some_iff] 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₅ @@ -245,7 +246,7 @@ theorem indexOfSomeImpPredTrue {α : Type u} {n : Nat} (tree : CompleteTree α n simp[this] exact h₉ case some lindex => - rw[h₄, Option.some_orElse, Option.some_inj] at he₁ + rw[h₄, Option.some_or, Option.some_inj] at he₁ 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₄) diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean index 17a40e9..685a726 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean @@ -84,7 +84,7 @@ where exact h₁₀ case false.isTrue => have h₁₀ := not_le_imp_le h₄ v value (Bool.eq_false_iff.mp h₁₀) - have h₁₄ : o > 0 := by cases o; simp at h₅ h; exact absurd (Fin.val_inj.mp h : index = 0) h₅; exact Nat.zero_lt_succ _ + have h₁₄ : o > 0 := by cases o; simp at h₅ h; exact absurd h h₅; exact Nat.zero_lt_succ _ apply And.intro <;> try apply And.intro case left => exact heapUpdateAtIsHeap le ⟨index.val - 1, _⟩ v l h₂.left h₃ h₄ case right.right => exact HeapPredicate.leOrLeaf_transitive h₃ h₁₀ h₂.right.right.right @@ -119,7 +119,7 @@ where apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃ exact h₁₀ case true.isTrue => - have h₁₄ : o > 0 := by cases o; simp at h₅ h; exact absurd (Fin.val_inj.mp h : index = 0) h₅; exact Nat.zero_lt_succ _ + have h₁₄ : o > 0 := by cases o; simp at h₅ h; exact absurd h h₅; exact Nat.zero_lt_succ _ apply And.intro case left => exact heapUpdateAtIsHeap le ⟨index.val - 1, _⟩ value l h₂.left h₃ h₄ case right => diff --git a/lean-toolchain b/lean-toolchain index 6c721df..893a7f3 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.20.1 +leanprover/lean4:4.21.0 -- cgit v1.2.3