Merge remote-tracking branch 'origin/bump/v4.16.0' into bump_to_v4.16…

….0-rc1

Batteries.lean

@@ -94,7 +94,6 @@ import Batteries.Tactic.ShowUnused
 import Batteries.Tactic.SqueezeScope
 import Batteries.Tactic.Trans
 import Batteries.Tactic.Unreachable
-import Batteries.Tactic.Where
 import Batteries.Util.Cache
 import Batteries.Util.ExtendedBinder
 import Batteries.Util.LibraryNote

Batteries/Data/Array/Lemmas.lean

@@ -49,7 +49,7 @@ where
        ((l.toList.drop i).indexOf? a).map (·+i) = (indexOfAux l a i).map Fin.val := by
     rw [indexOfAux]
     if h : i < l.size then
-      rw [List.drop_eq_getElem_cons h, ←getElem_eq_getElem_toList, List.indexOf?_cons]
+      rw [List.drop_eq_getElem_cons h, getElem_toList, List.indexOf?_cons]
       if h' : l[i] == a then
         simp [h, h']
       else
@@ -76,8 +76,6 @@ theorem size_set! (a : Array α) (i v) : (a.set! i v).size = a.size := by simp
 
 /-! ### mem -/
 
-theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp
-
 /-! ### insertAt -/
 
 @[simp] private theorem size_insertIdx_loop (as : Array α) (i : Nat) (j : Fin as.size) :

Batteries/Data/Char.lean

@@ -9,9 +9,6 @@ import Batteries.Tactic.Alias
 theorem Char.le_antisymm_iff {x y : Char} : x = y ↔ x ≤ y ∧ y ≤ x :=
   Char.ext_iff.trans UInt32.le_antisymm_iff
 
-theorem Char.le_antisymm {x y : Char} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
-  Char.le_antisymm_iff.2 ⟨h1, h2⟩
-
 instance : Batteries.LawfulOrd Char := .compareOfLessAndEq
   (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt Char.le_antisymm
 

Batteries/Data/HashMap/WF.lean

@@ -26,7 +26,7 @@ theorem toList_update (self : Buckets α β) (i d h) :
 theorem exists_of_update (self : Buckets α β) (i d h) :
     ∃ l₁ l₂, self.1.toList = l₁ ++ self.1[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
       (self.update i d h).1.toList = l₁ ++ d :: l₂ := by
-  simp only [Array.length_toList, Array.ugetElem_eq_getElem, Array.getElem_eq_getElem_toList]
+  simp only [Array.length_toList, Array.ugetElem_eq_getElem, Array.getElem_toList]
   exact List.exists_of_set h
 
 theorem update_update (self : Buckets α β) (i d d' h h') :
@@ -46,7 +46,7 @@ theorem WF.mk' [BEq α] [Hashable α] (h) : (Buckets.mk n h : Buckets α β).WF
   refine ⟨fun _ h => ?_, fun i h => ?_⟩
   · simp only [Buckets.mk, mkArray, List.mem_replicate, ne_eq] at h
     simp [h, List.Pairwise.nil]
-  · simp [Buckets.mk, empty', mkArray, Array.getElem_eq_getElem_toList, AssocList.All]
+  · simp [Buckets.mk, empty', Array.getElem_toList, AssocList.All]
 
 theorem WF.update [BEq α] [Hashable α] {buckets : Buckets α β} {i d h} (H : buckets.WF)
     (h₁ : ∀ [PartialEquivBEq α] [LawfulHashable α],
@@ -60,7 +60,7 @@ theorem WF.update [BEq α] [Hashable α] {buckets : Buckets α β} {i d h} (H :
     | .inl hl => H.1 _ hl
     | .inr rfl => h₁ (H.1 _ (Array.getElem_mem_toList ..))
   · revert hp
-    simp only [Array.getElem_eq_getElem_toList, toList_update, List.getElem_set,
+    simp only [← Array.getElem_toList, toList_update, List.getElem_set,
       Array.length_toList, update_size]
     split <;> intro hp
     · next eq => exact eq ▸ h₂ (H.2 _ _) _ hp
@@ -110,7 +110,7 @@ where
           List.length_nil, Nat.sum_append, List.sum_cons, Nat.zero_add, Array.length_toList]
         rw [Nat.add_assoc, Nat.add_assoc, Nat.add_assoc]; congr 1
         (conv => rhs; rw [Nat.add_left_comm]); congr 1
-        rw [← Array.getElem_eq_getElem_toList]
+        rw [Array.getElem_toList]
         have := @reinsertAux_size α β _; simp [Buckets.size] at this
         induction source[i].toList generalizing target <;> simp [*, Nat.succ_add]; rfl
     · next H =>
@@ -173,7 +173,7 @@ where
       · match List.mem_or_eq_of_mem_set hl with
         | .inl hl => exact hs₁ _ hl
         | .inr e => exact e ▸ .nil
-      · simp only [Array.length_toList, Array.size_set, Array.getElem_eq_getElem_toList,
+      · simp only [Array.length_toList, Array.size_set, ← Array.getElem_toList,
           Array.toList_set, List.getElem_set]
         split
         · nofun
@@ -371,7 +371,7 @@ theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable
     have := H.out.2.1 _ h
     rw [← List.pairwise_map (R := (¬ · == ·))] at this ⊢
     exact this.sublist (H3 l.toList)
-  · simp only [Array.size_mk, List.length_map, Array.length_toList, Array.getElem_eq_getElem_toList,
+  · simp only [Array.size_toArray, List.length_map, Array.length_toList, ← Array.getElem_toList,
       List.getElem_map] at h ⊢
     have := H.out.2.2 _ h
     simp only [AssocList.All, List.toList_toAssocList, List.mem_reverse, List.mem_filterMap,

Batteries/Data/PairingHeap.lean

@@ -123,7 +123,7 @@ theorem Heap.size_merge_node (le) (a₁ : α) (c₁ s₁ : Heap α) (a₂ : α)
 theorem Heap.size_merge (le) {s₁ s₂ : Heap α} (h₁ : s₁.NoSibling) (h₂ : s₂.NoSibling) :
     (merge le s₁ s₂).size = s₁.size + s₂.size := by
   match h₁, h₂ with
-  | .nil, .nil | .nil, .node _ _ | .node _ _, .nil => simp [size]
+  | .nil, .nil | .nil, .node _ _ | .node _ _, .nil => simp [merge, size]
   | .node _ _, .node _ _ => unfold merge; dsimp; split <;> simp_arith [size]
 
 theorem Heap.size_combine (le) (s : Heap α) :

Batteries/Data/Range/Lemmas.lean

@@ -8,100 +8,24 @@ import Batteries.Data.List.Lemmas
 
 namespace Std.Range
 
-/-- The number of elements contained in a `Std.Range`. -/
-def numElems (r : Range) : Nat :=
-  if r.step = 0 then
-    -- This is a very weird choice, but it is chosen to coincide with the `forIn` impl
-    if r.stop ≤ r.start then 0 else r.stop
-  else
-    (r.stop - r.start + r.step - 1) / r.step
+@[deprecated size (since := "2024-12-19")] alias numElems := size
 
-theorem numElems_stop_le_start : ∀ r : Range, r.stop ≤ r.start → r.numElems = 0
-  | ⟨start, stop, step⟩, h => by
-    simp [numElems]; split <;> simp_all
-    apply Nat.div_eq_of_lt; simp [Nat.sub_eq_zero_of_le h]
-    exact Nat.pred_lt ‹_›
+theorem size_stop_le_start : ∀ r : Range, r.stop ≤ r.start → r.size = 0
+  | ⟨start, stop, step, _⟩, h => by
+    simp_all [size, Nat.div_eq_zero_iff_lt]
+    omega
 
-theorem numElems_step_1 (start stop) : numElems ⟨start, stop, 1⟩ = stop - start := by
-  simp [numElems]
+@[deprecated size_stop_le_start (since := "2024-12-19")]
+alias numElems_stop_le_start := size_stop_le_start
 
-private theorem numElems_le_iff {start stop step i} (hstep : 0 < step) :
-    (stop - start + step - 1) / step ≤ i ↔ stop ≤ start + step * i :=
-  calc (stop - start + step - 1) / step ≤ i
-    _ ↔ stop - start + step - 1 < step * i + step := by
-      rw [← Nat.lt_succ (n := i), Nat.div_lt_iff_lt_mul hstep, Nat.mul_comm, ← Nat.mul_succ]
-    _ ↔ stop - start + step - 1 < step * i + 1 + (step - 1) := by
-      rw [Nat.add_right_comm, Nat.add_assoc, Nat.sub_add_cancel hstep]
-    _ ↔ stop ≤ start + step * i := by
-      rw [Nat.add_sub_assoc hstep, Nat.add_lt_add_iff_right, Nat.lt_succ,
-        Nat.sub_le_iff_le_add']
+theorem size_step_1 (start stop) : size ⟨start, stop, 1, by decide⟩ = stop - start := by
+  simp [size]
 
-theorem mem_range'_elems (r : Range) (h : x ∈ List.range' r.start r.numElems r.step) : x ∈ r := by
-  obtain ⟨i, h', rfl⟩ := List.mem_range'.1 h
-  refine ⟨Nat.le_add_right .., ?_⟩
-  unfold numElems at h'; split at h'
-  · split at h' <;> [cases h'; simp_all]
-  · next step0 =>
-    refine Nat.not_le.1 fun h =>
-      Nat.not_le.2 h' <| (numElems_le_iff (Nat.pos_of_ne_zero step0)).2 h
+@[deprecated size_step_1 (since := "2024-12-19")]
+alias numElems_step_1 := size_step_1
 
-theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
-    (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
-    forIn' r init f =
-    forIn
-      ((List.range' r.start r.numElems r.step).pmap Subtype.mk fun _ => mem_range'_elems r)
-      init (fun ⟨a, h⟩ => f a h) := by
-  let ⟨start, stop, step⟩ := r
-  let L := List.range' start (numElems ⟨start, stop, step⟩) step
-  let f' : { a // start ≤ a ∧ a < stop } → _ := fun ⟨a, h⟩ => f a h
-  suffices ∀ H, forIn' [start:stop:step] init f = forIn (L.pmap Subtype.mk H) init f' from this _
-  intro H; dsimp only [forIn', Range.forIn']
-  if h : start < stop then
-    simp only [numElems, Nat.not_le.2 h, ↓reduceIte, L]; split
-    · subst step
-      suffices ∀ n H init,
-          forIn'.loop start stop 0 f n start (Nat.le_refl _) init =
-          forIn ((List.range' start n 0).pmap Subtype.mk H) init f' from this _ ..
-      intro n; induction n with
-        (intro H init
-         unfold forIn'.loop
-         simp only [↓reduceDIte, Nat.add_zero, List.pmap, List.forIn_cons, List.forIn_nil, h])
-      | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl
-    · next step0 =>
-      have hstep := Nat.pos_of_ne_zero step0
-      suffices ∀ fuel l i hle H, l ≤ fuel →
-          (∀ j, stop ≤ i + step * j ↔ l ≤ j) → ∀ init,
-          forIn'.loop start stop step f fuel i hle init =
-          forIn ((List.range' i l step).pmap Subtype.mk H) init f' by
-        refine this _ _ _ _ _
-          ((numElems_le_iff hstep).2 (Nat.le_trans ?_ (Nat.le_add_left ..)))
-          (fun _ => (numElems_le_iff hstep).symm) _
-        conv => lhs; rw [← Nat.one_mul stop]
-        exact Nat.mul_le_mul_right stop hstep
-      intro fuel; induction fuel with intro l i hle H h1 h2 init
-      | zero => simp [forIn'.loop, Nat.le_zero.1 h1]
-      | succ fuel ih =>
-        cases l with
-        | zero => rw [forIn'.loop]; simp [Nat.not_lt.2 <| by simpa using (h2 0).2 (Nat.le_refl _)]
-        | succ l =>
-          have ih := ih _ _ (Nat.le_trans hle (Nat.le_add_right ..))
-            (List.forall_mem_cons.1 H).2 (Nat.le_of_succ_le_succ h1) fun i => by
-              rw [Nat.add_right_comm, Nat.add_assoc, ← Nat.mul_succ, h2, Nat.succ_le_succ_iff]
-          have := h2 0
-          simp only [Nat.mul_zero, Nat.add_zero, Nat.le_zero_eq, Nat.add_one_ne_zero, iff_false,
-            Nat.not_le] at this
-          rw [forIn'.loop]
-          simp only [this, ↓reduceDIte, ih, List.pmap, List.forIn_cons]
-          rfl
-  else
-    simp only [numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), List.range'_zero,
-      List.pmap, List.forIn_nil, L]
-    cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h]
+@[deprecated mem_of_mem_range' (since := "2024-12-19")]
+alias mem_range'_elems := mem_of_mem_range'
 
-theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
-    (init : β) (f : Nat → β → m (ForInStep β)) :
-    forIn r init f = forIn (List.range' r.start r.numElems r.step) init f := by
-  refine Eq.trans ?_ <| (forIn'_eq_forIn_range' r init (fun x _ => f x)).trans ?_
-  · simp [forIn, forIn']
-  · suffices ∀ L H, forIn (List.pmap Subtype.mk L H) init (f ·.1) = forIn L init f from this _ ..
-    intro L; induction L generalizing init <;> intro H <;> simp [*]
+@[deprecated forIn'_eq_forIn'_range' (since := "2024-12-19")]
+alias forIn'_eq_forIn_range' := forIn'_eq_forIn'_range'

Batteries/Data/String/Lemmas.lean

@@ -14,13 +14,9 @@ namespace String
 -- TODO(kmill): add `@[ext]` attribute to `String.ext` in core.
 attribute [ext (iff := false)] ext
 
-theorem lt_trans {s₁ s₂ s₃ : String} : s₁ < s₂ → s₂ < s₃ → s₁ < s₃ :=
-  List.lt_trans (α := Char) Nat.lt_trans
-    (fun h1 h2 => Nat.not_lt.2 <| Nat.le_trans (Nat.not_lt.1 h2) (Nat.not_lt.1 h1))
-
-theorem lt_antisymm {s₁ s₂ : String} (h₁ : ¬s₁ < s₂) (h₂ : ¬s₂ < s₁) : s₁ = s₂ :=
-  ext <| List.lt_antisymm (α := Char)
-    (fun h1 h2 => Char.le_antisymm (Nat.not_lt.1 h2) (Nat.not_lt.1 h1)) h₁ h₂
+theorem lt_antisymm {s₁ s₂ : String} (h₁ : ¬s₁ < s₂) (h₂ : ¬s₂ < s₁) : s₁ = s₂ := by
+  simp at h₁ h₂
+  exact String.le_antisymm h₂ h₁
 
 instance : Batteries.TransOrd String := .compareOfLessAndEq
   String.lt_irrefl String.lt_trans String.lt_antisymm
@@ -153,7 +149,7 @@ theorem utf8GetAux_of_valid (cs cs' : List Char) {i p : Nat} (hp : i + utf8Len c
   | [], [] => rfl
   | [], c::cs' => simp [← hp, utf8GetAux]
   | c::cs, cs' =>
-    simp only [utf8GetAux, List.append_eq, Char.reduceDefault, ↓Char.isValue]
+    simp only [List.cons_append, utf8GetAux, Char.reduceDefault]
     rw [if_neg]
     case hnc => simp only [← hp, utf8Len_cons, Pos.ext_iff]; exact ne_self_add_add_utf8Size
     refine utf8GetAux_of_valid cs cs' ?_
@@ -172,7 +168,7 @@ theorem utf8GetAux?_of_valid (cs cs' : List Char) {i p : Nat} (hp : i + utf8Len
   | [], [] => rfl
   | [], c::cs' => simp [← hp, utf8GetAux?]
   | c::cs, cs' =>
-    simp only [utf8GetAux?, List.append_eq]
+    simp only [List.cons_append, utf8GetAux?]
     rw [if_neg]
     case hnc => simp only [← hp, Pos.ext_iff]; exact ne_self_add_add_utf8Size
     refine utf8GetAux?_of_valid cs cs' ?_
@@ -224,7 +220,7 @@ theorem utf8PrevAux_of_valid {cs cs' : List Char} {c : Char} {i p : Nat}
   match cs with
   | [] => simp [utf8PrevAux, ← hp, Pos.addChar_eq]
   | c'::cs =>
-    simp only [utf8PrevAux, Pos.addChar_eq, ← hp, utf8Len_cons, List.append_eq]
+    simp only [utf8PrevAux, List.cons_append, utf8Len_cons, ← hp]
     rw [if_neg]
     case hnc =>
       simp only [Pos.ext_iff]
@@ -361,7 +357,7 @@ theorem extract.go₂_append_left : ∀ (s t : List Char) (i e : Nat),
     e = utf8Len s + i → go₂ (s ++ t) ⟨i⟩ ⟨e⟩ = s
 | [], t, i, _, rfl => by cases t <;> simp [go₂]
 | c :: cs, t, i, _, rfl => by
-  simp only [go₂, utf8Len_cons, Pos.ext_iff, ne_add_utf8Size_add_self, ↓reduceIte, List.append_eq,
+  simp only [List.cons_append, utf8Len_cons, go₂, Pos.ext_iff, ne_add_utf8Size_add_self, ↓reduceIte,
     Pos.addChar_eq, List.cons.injEq, true_and]
   apply go₂_append_left; rw [Nat.add_right_comm, Nat.add_assoc]
 
@@ -388,7 +384,7 @@ theorem extract.go₁_append_right : ∀ (s t : List Char) (i b : Nat) (e : Pos)
     b = utf8Len s + i → go₁ (s ++ t) ⟨i⟩ ⟨b⟩ e = go₂ t ⟨b⟩ e
 | [], t, i, _, e, rfl => by cases t <;> simp [go₁, go₂]
 | c :: cs, t, i, _, e, rfl => by
-  simp only [go₁, utf8Len_cons, Pos.ext_iff, ne_add_utf8Size_add_self, ↓reduceIte, List.append_eq,
+  simp only [go₁, utf8Len_cons, Pos.ext_iff, ne_add_utf8Size_add_self, ↓reduceIte, List.cons_append,
     Pos.addChar_eq]
   apply go₁_append_right; rw [Nat.add_right_comm, Nat.add_assoc]
 

Batteries/Data/UnionFind/Basic.lean

@@ -296,7 +296,6 @@ theorem findAux_s {self : UnionFind} {x : Fin self.size} :
     apply dif_pos
     exact parent'_lt ..
 
-set_option linter.deprecated false in
 theorem rankD_findAux {self : UnionFind} {x : Fin self.size} :
     rankD (findAux self x).s i = self.rank i := by
   if h : i < self.size then
@@ -307,11 +306,10 @@ theorem rankD_findAux {self : UnionFind} {x : Fin self.size} :
     split <;>
       simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt _ x.2⟩), -Array.get_eq_getElem]
   else
-    simp only [rankD, Array.data_length, Array.get_eq_getElem, rank]
+    simp only [rankD, Array.length_toList, Array.get_eq_getElem, rank]
     rw [dif_neg (by rwa [FindAux.size_eq]), dif_neg h]
 termination_by self.rankMax - self.rank x
 
-set_option linter.deprecated false in
 theorem parentD_findAux {self : UnionFind} {x : Fin self.size} :
     parentD (findAux self x).s i =
     if i = x then self.rootD x else parentD (self.findAux ⟨_, self.parent'_lt _ x.2⟩).s i := by
@@ -321,7 +319,7 @@ theorem parentD_findAux {self : UnionFind} {x : Fin self.size} :
   · next h =>
     rw [parentD]; split <;> rename_i h'
     · rw [Array.getElem_modify (by simpa using h')]
-      simp only [Array.data_length, @eq_comm _ i]
+      simp only [Array.length_toList, @eq_comm _ i]
       split <;> simp [← parentD_eq, -Array.get_eq_getElem]
     · rw [if_neg (mt (by rintro rfl; simp [FindAux.size_eq]) h')]
       rw [parentD, dif_neg]; simpa using h'