merge

Batteries/Data/Array/Basic.lean

@@ -137,29 +137,12 @@ This will perform the update destructively provided that `a` has a reference cou
 abbrev setN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) : Array α :=
   a.set i x
 
-/--
-`swapN a i j hi hj` swaps two `Nat` indexed entries in an `Array α`.
-Uses `get_elem_tactic` to supply a proof that the indices are in range.
-`hi` and `hj` are both given a default argument `by get_elem_tactic`.
-This will perform the update destructively provided that `a` has a reference count of 1 when called.
--/
-abbrev swapN (a : Array α) (i j : Nat)
-    (hi : i < a.size := by get_elem_tactic) (hj : j < a.size := by get_elem_tactic) : Array α :=
-  Array.swap a ⟨i,hi⟩ ⟨j, hj⟩
+@[deprecated (since := "2024-11-24")] alias swapN := swap
 
-/--
-`swapAtN a i h x` swaps the entry with index `i : Nat` in the vector for a new entry `x`.
-The old entry is returned alongwith the modified vector.
-Automatically generates proof of `i < a.size` with `get_elem_tactic` where feasible.
--/
-abbrev swapAtN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) :
-    α × Array α := swapAt a ⟨i,h⟩ x
+@[deprecated (since := "2024-11-24")] alias swapAtN := swapAt
 
 @[deprecated (since := "2024-11-20")] alias eraseIdxN := eraseIdx
 
-/-- `finRange n` is the array of all elements of `Fin n` in order. -/
-protected def finRange (n : Nat) : Array (Fin n) := ofFn fun i => i
-
 end Array
 
 

Batteries/Data/Array/Lemmas.lean

@@ -26,14 +26,6 @@ theorem forIn_eq_forIn_toList [Monad m]
 @[deprecated (since := "2024-09-09")] alias data_zipWith := toList_zipWith
 @[deprecated (since := "2024-08-13")] alias zipWith_eq_zipWith_data := data_zipWith
 
-@[simp] theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
-    (as.zipWith bs f).size = min as.size bs.size := by
-  rw [size_eq_length_toList, toList_zipWith, List.length_zipWith]
-
-@[simp] theorem size_zip (as : Array α) (bs : Array β) :
-    (as.zip bs).size = min as.size bs.size :=
-  as.size_zipWith bs Prod.mk
-
 /-! ### filter -/
 
 theorem size_filter_le (p : α → Bool) (l : Array α) :
@@ -82,11 +74,6 @@ theorem size_set! (a : Array α) (i v) : (a.set! i v).size = a.size := by simp
 
 /-! ### map -/
 
-theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
-  rw [mapM, mapM.map]; rfl
-
-theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty f
-
 /-! ### mem -/
 
 theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp
@@ -151,13 +138,11 @@ theorem getElem_insertIdx_loop_gt {as : Array α} {i : Nat} {j : Nat} {hj : j <
     have : j - 1 < j := by omega
     rw [getElem_insertIdx_loop_gt w]
     rw [getElem_swap]
-    simp only [Fin.getElem_fin]
     split <;> rename_i h₂
     · rw [if_neg (by omega), if_neg (by omega)]
       have t : k ≤ j := by omega
       simp [t]
     · rw [getElem_swap]
-      simp only [Fin.getElem_fin]
       rw [if_neg (by omega)]
       split <;> rename_i h₃
       · simp [h₃]
@@ -229,15 +214,3 @@ theorem getElem_insertIdx_gt (as : Array α) (i : Nat) (h : i ≤ as.size) (v :
 
 @[deprecated getElem_insertIdx_gt (since := "2024-11-20")] alias getElem_insertAt_gt :=
 getElem_insertIdx_gt
-
-/-! ### finRange -/
-
-@[simp] theorem size_finRange (n) : (Array.finRange n).size = n := by
-  simp [Array.finRange]
-
-@[simp] theorem getElem_finRange (n i) (h : i < (Array.finRange n).size) :
-    (Array.finRange n)[i] = ⟨i, size_finRange n ▸ h⟩ := by
-  simp [Array.finRange]
-
-@[simp] theorem toList_finRange (n) : (Array.finRange n).toList = List.finRange n := by
-  simp [Array.finRange, List.finRange]

Batteries/Data/BinaryHeap.lean

@@ -67,9 +67,9 @@ def heapifyUp (lt : α → α → Bool) (a : Vector α sz) (i : Fin sz) :
   match i with
   | ⟨0, _⟩ => a
   | ⟨i'+1, hi⟩ =>
-    let j := ⟨i'/2, by get_elem_tactic⟩
+    let j := i'/2
     if lt a[j] a[i] then
-      heapifyUp lt (a.swap i j) j
+      heapifyUp lt (a.swap i j) ⟨j, by get_elem_tactic⟩
     else a
 
 /-- `O(1)`. Build a new empty heap. -/
@@ -107,7 +107,7 @@ def popMax (self : BinaryHeap α lt) : BinaryHeap α lt :=
   if h0 : self.size = 0 then self else
     have hs : self.size - 1 < self.size := Nat.pred_lt h0
     have h0 : 0 < self.size := Nat.zero_lt_of_ne_zero h0
-    let v := self.vector.swap ⟨_, h0⟩ ⟨_, hs⟩ |>.pop
+    let v := self.vector.swap _ _ h0 hs |>.pop
     if h : 0 < self.size - 1 then
       ⟨heapifyDown lt v ⟨0, h⟩ |>.toArray⟩
     else
@@ -136,7 +136,7 @@ def insertExtractMax (self : BinaryHeap α lt) (x : α) : α × BinaryHeap α lt
   | none => (x, self)
   | some m =>
     if lt x m then
-      let v := self.vector.set ⟨0, size_pos_of_max e⟩ x
+      let v := self.vector.set 0 x (size_pos_of_max e)
       (m, ⟨heapifyDown lt v ⟨0, size_pos_of_max e⟩ |>.toArray⟩)
     else (x, self)
 
@@ -145,7 +145,7 @@ def replaceMax (self : BinaryHeap α lt) (x : α) : Option α × BinaryHeap α l
   match e : self.max with
   | none => (none, ⟨self.vector.push x |>.toArray⟩)
   | some m =>
-    let v := self.vector.set ⟨0, size_pos_of_max e⟩ x
+    let v := self.vector.set 0 x (size_pos_of_max e)
     (some m, ⟨heapifyDown lt v ⟨0, size_pos_of_max e⟩ |>.toArray⟩)
 
 /-- `O(log n)`. Replace the value at index `i` by `x`. Assumes that `x ≤ self.get i`. -/

Batteries/Data/List/Basic.lean

@@ -1064,6 +1064,3 @@ where
   | a :: as, acc => match (a :: as).dropPrefix? i with
     | none => go as (a :: acc)
     | some s => (acc.reverse, s)
-
-/-- `finRange n` lists all elements of `Fin n` in order -/
-def finRange (n : Nat) : List (Fin n) := ofFn fun i => i

Batteries/Data/List/FinRange.lean

@@ -7,54 +7,20 @@ import Batteries.Data.List.OfFn
 
 namespace List
 
-@[simp] theorem length_finRange (n) : (List.finRange n).length = n := by
-  simp [List.finRange]
-
 @[deprecated (since := "2024-11-19")]
 alias length_list := length_finRange
 
-@[simp] theorem getElem_finRange (i : Nat) (h : i < (List.finRange n).length) :
-    (finRange n)[i] = Fin.cast (length_finRange n) ⟨i, h⟩ := by
-  simp [List.finRange]
-
 @[deprecated (since := "2024-11-19")]
 alias getElem_list := getElem_finRange
 
-@[simp] theorem finRange_zero : finRange 0 = [] := by simp [finRange, ofFn]
-
 @[deprecated (since := "2024-11-19")]
 alias list_zero := finRange_zero
 
-theorem finRange_succ (n) : finRange (n+1) = 0 :: (finRange n).map Fin.succ := by
-  apply List.ext_getElem; simp; intro i; cases i <;> simp
-
 @[deprecated (since := "2024-11-19")]
 alias list_succ := finRange_succ
 
-theorem finRange_succ_last (n) :
-    finRange (n+1) = (finRange n).map Fin.castSucc ++ [Fin.last n] := by
-  apply List.ext_getElem
-  · simp
-  · intros
-    simp only [List.finRange, List.getElem_ofFn, getElem_append, length_map, length_ofFn,
-      getElem_map, Fin.castSucc_mk, getElem_singleton]
-    split
-    · rfl
-    · next h => exact Fin.eq_last_of_not_lt h
-
 @[deprecated (since := "2024-11-19")]
 alias list_succ_last := finRange_succ_last
 
-theorem finRange_reverse (n) : (finRange n).reverse = (finRange n).map Fin.rev := by
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    conv => lhs; rw [finRange_succ_last]
-    conv => rhs; rw [finRange_succ]
-    rw [reverse_append, reverse_cons, reverse_nil, nil_append, singleton_append, ← map_reverse,
-      map_cons, ih, map_map, map_map]
-    congr; funext
-    simp [Fin.rev_succ]
-
 @[deprecated (since := "2024-11-19")]
 alias list_reverse := finRange_reverse

Batteries/Data/List/Lemmas.lean

@@ -15,26 +15,6 @@ namespace List
 @[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) :
     (Array.mk xs)[i] = xs[i] := rfl
 
-/-! ### == -/
-
-@[simp] theorem beq_nil_iff [BEq α] {l : List α} : (l == []) = l.isEmpty := by
-  cases l <;> rfl
-
-@[simp] theorem nil_beq_iff [BEq α] {l : List α} : ([] == l) = l.isEmpty := by
-  cases l <;> rfl
-
-@[simp] theorem cons_beq_cons [BEq α] {a b : α} {l₁ l₂ : List α} :
-    (a :: l₁ == b :: l₂) = (a == b && l₁ == l₂) := rfl
-
-theorem length_eq_of_beq [BEq α] {l₁ l₂ : List α} (h : l₁ == l₂) : l₁.length = l₂.length :=
-  match l₁, l₂ with
-  | [], [] => rfl
-  | [], _ :: _ => by simp [beq_nil_iff] at h
-  | _ :: _, [] => by simp [nil_beq_iff] at h
-  | a :: l₁, b :: l₂ => by
-    simp at h
-    simpa using length_eq_of_beq h.2
-
 /-! ### next? -/
 
 @[simp] theorem next?_nil : @next? α [] = none := rfl

Batteries/Data/UInt.lean

@@ -10,11 +10,6 @@ import Batteries.Classes.Order
 @[ext] theorem UInt8.ext : {x y : UInt8} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-@[simp] theorem UInt8.val_val_eq_toNat (x : UInt8) : x.val.val = x.toNat := rfl
-
-@[simp] theorem UInt8.toNat_ofNat (n) :
-    (no_index (OfNat.ofNat n) : UInt8).toNat = n % UInt8.size := rfl
-
 theorem UInt8.toNat_lt (x : UInt8) : x.toNat < 2 ^ 8 := x.val.isLt
 
 @[simp] theorem UInt8.toUInt16_toNat (x : UInt8) : x.toUInt16.toNat = x.toNat := rfl
@@ -23,19 +18,6 @@ theorem UInt8.toNat_lt (x : UInt8) : x.toNat < 2 ^ 8 := x.val.isLt
 
 @[simp] theorem UInt8.toUInt64_toNat (x : UInt8) : x.toUInt64.toNat = x.toNat := rfl
 
-theorem UInt8.toNat_add (x y : UInt8) : (x + y).toNat = (x.toNat + y.toNat) % UInt8.size := rfl
-
-theorem UInt8.toNat_sub (x y : UInt8) :
-    (x - y).toNat = (UInt8.size - y.toNat + x.toNat) % UInt8.size := rfl
-
-theorem UInt8.toNat_mul (x y : UInt8) : (x * y).toNat = (x.toNat * y.toNat) % UInt8.size := rfl
-
-theorem UInt8.le_antisymm_iff {x y : UInt8} : x = y ↔ x ≤ y ∧ y ≤ x :=
-  UInt8.ext_iff.trans Nat.le_antisymm_iff
-
-theorem UInt8.le_antisymm {x y : UInt8} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
-  UInt8.le_antisymm_iff.2 ⟨h1, h2⟩
-
 instance : Batteries.LawfulOrd UInt8 := .compareOfLessAndEq
   (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt8.le_antisymm
 
@@ -44,11 +26,6 @@ instance : Batteries.LawfulOrd UInt8 := .compareOfLessAndEq
 @[ext] theorem UInt16.ext : {x y : UInt16} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-@[simp] theorem UInt16.val_val_eq_toNat (x : UInt16) : x.val.val = x.toNat := rfl
-
-@[simp] theorem UInt16.toNat_ofNat (n) :
-    (no_index (OfNat.ofNat n) : UInt16).toNat = n % UInt16.size := rfl
-
 theorem UInt16.toNat_lt (x : UInt16) : x.toNat < 2 ^ 16 := x.val.isLt
 
 @[simp] theorem UInt16.toUInt8_toNat (x : UInt16) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
@@ -57,19 +34,6 @@ theorem UInt16.toNat_lt (x : UInt16) : x.toNat < 2 ^ 16 := x.val.isLt
 
 @[simp] theorem UInt16.toUInt64_toNat (x : UInt16) : x.toUInt64.toNat = x.toNat := rfl
 
-theorem UInt16.toNat_add (x y : UInt16) : (x + y).toNat = (x.toNat + y.toNat) % UInt16.size := rfl
-
-theorem UInt16.toNat_sub (x y : UInt16) :
-    (x - y).toNat = (UInt16.size - y.toNat + x.toNat) % UInt16.size := rfl
-
-theorem UInt16.toNat_mul (x y : UInt16) : (x * y).toNat = (x.toNat * y.toNat) % UInt16.size := rfl
-
-theorem UInt16.le_antisymm_iff {x y : UInt16} : x = y ↔ x ≤ y ∧ y ≤ x :=
-  UInt16.ext_iff.trans Nat.le_antisymm_iff
-
-theorem UInt16.le_antisymm {x y : UInt16} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
-  UInt16.le_antisymm_iff.2 ⟨h1, h2⟩
-
 instance : Batteries.LawfulOrd UInt16 := .compareOfLessAndEq
   (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt16.le_antisymm
 
@@ -78,11 +42,6 @@ instance : Batteries.LawfulOrd UInt16 := .compareOfLessAndEq
 @[ext] theorem UInt32.ext : {x y : UInt32} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-@[simp] theorem UInt32.val_val_eq_toNat (x : UInt32) : x.val.val = x.toNat := rfl
-
-@[simp] theorem UInt32.toNat_ofNat (n) :
-    (no_index (OfNat.ofNat n) : UInt32).toNat = n % UInt32.size := rfl
-
 theorem UInt32.toNat_lt (x : UInt32) : x.toNat < 2 ^ 32 := x.val.isLt
 
 @[simp] theorem UInt32.toUInt8_toNat (x : UInt32) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
@@ -91,19 +50,6 @@ theorem UInt32.toNat_lt (x : UInt32) : x.toNat < 2 ^ 32 := x.val.isLt
 
 @[simp] theorem UInt32.toUInt64_toNat (x : UInt32) : x.toUInt64.toNat = x.toNat := rfl
 
-theorem UInt32.toNat_add (x y : UInt32) : (x + y).toNat = (x.toNat + y.toNat) % UInt32.size := rfl
-
-theorem UInt32.toNat_sub (x y : UInt32) :
-    (x - y).toNat = (UInt32.size - y.toNat + x.toNat) % UInt32.size := rfl
-
-theorem UInt32.toNat_mul (x y : UInt32) : (x * y).toNat = (x.toNat * y.toNat) % UInt32.size := rfl
-
-theorem UInt32.le_antisymm_iff {x y : UInt32} : x = y ↔ x ≤ y ∧ y ≤ x :=
-  UInt32.ext_iff.trans Nat.le_antisymm_iff
-
-theorem UInt32.le_antisymm {x y : UInt32} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
-  UInt32.le_antisymm_iff.2 ⟨h1, h2⟩
-
 instance : Batteries.LawfulOrd UInt32 := .compareOfLessAndEq
   (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt32.le_antisymm
 
@@ -112,11 +58,6 @@ instance : Batteries.LawfulOrd UInt32 := .compareOfLessAndEq
 @[ext] theorem UInt64.ext : {x y : UInt64} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-@[simp] theorem UInt64.val_val_eq_toNat (x : UInt64) : x.val.val = x.toNat := rfl
-
-@[simp] theorem UInt64.toNat_ofNat (n) :
-    (no_index (OfNat.ofNat n) : UInt64).toNat = n % UInt64.size := rfl
-
 theorem UInt64.toNat_lt (x : UInt64) : x.toNat < 2 ^ 64 := x.val.isLt
 
 @[simp] theorem UInt64.toUInt8_toNat (x : UInt64) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
@@ -125,19 +66,6 @@ theorem UInt64.toNat_lt (x : UInt64) : x.toNat < 2 ^ 64 := x.val.isLt
 
 @[simp] theorem UInt64.toUInt32_toNat (x : UInt64) : x.toUInt32.toNat = x.toNat % 2 ^ 32 := rfl
 
-theorem UInt64.toNat_add (x y : UInt64) : (x + y).toNat = (x.toNat + y.toNat) % UInt64.size := rfl
-
-theorem UInt64.toNat_sub (x y : UInt64) :
-    (x - y).toNat = (UInt64.size - y.toNat + x.toNat) % UInt64.size := rfl
-
-theorem UInt64.toNat_mul (x y : UInt64) : (x * y).toNat = (x.toNat * y.toNat) % UInt64.size := rfl
-
-theorem UInt64.le_antisymm_iff {x y : UInt64} : x = y ↔ x ≤ y ∧ y ≤ x :=
-  UInt64.ext_iff.trans Nat.le_antisymm_iff
-
-theorem UInt64.le_antisymm {x y : UInt64} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
-  UInt64.le_antisymm_iff.2 ⟨h1, h2⟩
-
 instance : Batteries.LawfulOrd UInt64 := .compareOfLessAndEq
   (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt64.le_antisymm
 
@@ -146,11 +74,6 @@ instance : Batteries.LawfulOrd UInt64 := .compareOfLessAndEq
 @[ext] theorem USize.ext : {x y : USize} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-@[simp] theorem USize.val_val_eq_toNat (x : USize) : x.val.val = x.toNat := rfl
-
-@[simp] theorem USize.toNat_ofNat (n) :
-    (no_index (OfNat.ofNat n) : USize).toNat = n % USize.size := rfl
-
 theorem USize.size_eq : USize.size = 2 ^ System.Platform.numBits := by
   rw [USize.size]
 
@@ -172,18 +95,5 @@ theorem USize.toNat_lt (x : USize) : x.toNat < 2 ^ System.Platform.numBits := by
 
 @[simp] theorem UInt32.toUSize_toNat (x : UInt32) : x.toUSize.toNat = x.toNat := rfl
 
-theorem USize.toNat_add (x y : USize) : (x + y).toNat = (x.toNat + y.toNat) % USize.size := rfl
-
-theorem USize.toNat_sub (x y : USize) :
-    (x - y).toNat = (USize.size - y.toNat + x.toNat) % USize.size := rfl
-
-theorem USize.toNat_mul (x y : USize) : (x * y).toNat = (x.toNat * y.toNat) % USize.size := rfl
-
-theorem USize.le_antisymm_iff {x y : USize} : x = y ↔ x ≤ y ∧ y ≤ x :=
-  USize.ext_iff.trans Nat.le_antisymm_iff
-
-theorem USize.le_antisymm {x y : USize} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
-  USize.le_antisymm_iff.2 ⟨h1, h2⟩
-
 instance : Batteries.LawfulOrd USize := .compareOfLessAndEq
   (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt USize.le_antisymm