Lean 4.21HEADmain

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