Merge branch 'main' into binary_rewrite

Author: linesthatinterlace

Batteries/Data/Char/AsciiCasing.lean

@@ -159,6 +159,7 @@ theorem beqCaseInsensitiveAsciiOnly.eqv : Equivalence (beqCaseInsensitiveAsciiOn
 /--
 Setoid structure on `Char` using `beqCaseInsensitiveAsciiOnly`
 -/
+@[implicit_reducible]
 def beqCaseInsensitiveAsciiOnly.isSetoid : Setoid Char:=
   ⟨(beqCaseInsensitiveAsciiOnly · ·), beqCaseInsensitiveAsciiOnly.eqv⟩
 

Batteries/Data/Char/Basic.lean

@@ -19,8 +19,6 @@ instance : Std.LawfulOrd Char :=
   .compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm
     (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt Char.le_antisymm
 
-@[simp] theorem toNat_val (c : Char) : c.val.toNat = c.toNat := rfl
-
 @[simp] theorem toNat_ofNatAux {n : Nat} (h : n.isValidChar) : toNat (ofNatAux n h) = n := by
   simp [ofNatAux, toNat]
 
@@ -29,9 +27,6 @@ theorem toNat_ofNat (n : Nat) : toNat (ofNat n) = if n.isValidChar then n else 0
   · simp [ofNat, *]
   · simp [ofNat, toNat, *]
 
-@[simp, grind =]
-theorem toNat_mk (h : UInt32.isValidChar v) : Char.toNat ⟨v, h⟩ = v.toNat := rfl
-
 @[simp]
 theorem val_ofNat (hn : Nat.isValidChar n) : (ofNat n).val = UInt32.ofNat n := by
   simp [ofNat, hn, ofNatAux, UInt32.ofNatLT_eq_ofNat]

Batteries/Data/List/Basic.lean

@@ -105,43 +105,6 @@ def splitAtD (n : Nat) (l : List α) (dflt : α) : List α × List α := go n l
   | 0, xs, acc => (acc.reverse, xs)
   | n, [], acc => (acc.reverseAux (replicate n dflt), [])
 
-/--
-Split a list at every element satisfying a predicate. The separators are not in the result.
-```
-[1, 1, 2, 3, 2, 4, 4].splitOnP (· == 2) = [[1, 1], [3], [4, 4]]
-```
--/
-def splitOnP (P : α → Bool) (l : List α) : List (List α) := go l [] where
-  /-- Auxiliary for `splitOnP`: `splitOnP.go xs acc = res'`
-  where `res'` is obtained from `splitOnP P xs` by prepending `acc.reverse` to the first element. -/
-  go : List α → List α → List (List α)
-  | [], acc => [acc.reverse]
-  | a :: t, acc => if P a then acc.reverse :: go t [] else go t (a::acc)
-
-/-- Tail recursive version of `splitOnP`. -/
-@[inline] def splitOnPTR (P : α → Bool) (l : List α) : List (List α) := go l #[] #[] where
-  /-- Auxiliary for `splitOnP`: `splitOnP.go xs acc r = r.toList ++ res'`
-  where `res'` is obtained from `splitOnP P xs` by prepending `acc.toList` to the first element. -/
-  @[specialize] go : List α → Array α → Array (List α) → List (List α)
-  | [], acc, r => r.toListAppend [acc.toList]
-  | a :: t, acc, r => bif P a then go t #[] (r.push acc.toList) else go t (acc.push a) r
-
-@[csimp] theorem splitOnP_eq_splitOnPTR : @splitOnP = @splitOnPTR := by
-  funext α P l; simp [splitOnPTR]
-  suffices ∀ xs acc r,
-    splitOnPTR.go P xs acc r = r.toList ++ splitOnP.go P xs acc.toList.reverse from
-      (this l #[] #[]).symm
-  intro xs acc r; induction xs generalizing acc r with simp [splitOnP.go, splitOnPTR.go]
-  | cons x xs IH => cases P x <;> simp [*]
-
-/--
-Split a list at every occurrence of a separator element. The separators are not in the result.
-```
-[1, 1, 2, 3, 2, 4, 4].splitOn 2 = [[1, 1], [3], [4, 4]]
-```
--/
-@[inline] def splitOn [BEq α] (a : α) (as : List α) : List (List α) := as.splitOnP (· == a)
-
 /-- Apply `f` to the last element of `l`, if it exists. -/
 @[inline] def modifyLast (f : α → α) (l : List α) : List α := go l #[] where
   /-- Auxiliary for `modifyLast`: `modifyLast.go f l acc = acc.toList ++ modifyLast f l`. -/

Batteries/Data/List/Lemmas.lean

@@ -1312,21 +1312,6 @@ theorem map_coe_finRange_eq_range : (finRange n).map (↑·) = List.range n := b
   apply List.ext_getElem <;> simp
 /-! ### sum/prod -/
 
-private theorem foldr_eq_foldl_aux (f : α → α → α) (init : α) [Std.Associative f]
-    [Std.LawfulIdentity f init] {l : List α} :
-    l.foldl f a = f a (l.foldl f init) := by
-  induction l generalizing a with
-  | nil => simp [Std.LawfulRightIdentity.right_id]
-  | cons b l ih =>
-    simp [Std.LawfulLeftIdentity.left_id, ih (a := f a b), ih (a := b), Std.Associative.assoc]
-
-theorem foldr_eq_foldl (f : α → α → α) (init : α) [Std.Associative f]
-    [Std.LawfulIdentity f init] {l : List α} :
-    l.foldr f init = l.foldl f init := by
-  induction l with
-  | nil => rfl
-  | cons a l ih => simp [ih, Std.LawfulLeftIdentity.left_id, foldr_eq_foldl_aux (a := a)]
-
 @[simp, grind =]
 theorem prod_nil [Mul α] [One α] : ([] : List α).prod = 1 := rfl
 
@@ -1367,9 +1352,6 @@ theorem prod_eq_foldl [Mul α] [One α] [Std.Associative (α := α) (· * ·)]
 theorem sum_zero_cons [Add α] [Zero α] [Std.LawfulLeftIdentity (α := α) (· + ·) 0] {l : List α} :
     (0 :: l).sum = l.sum := by simp [Std.LawfulLeftIdentity.left_id]
 
-theorem sum_singleton [Add α] [Zero α] [Std.LawfulRightIdentity (α := α) (· + ·) 0] {a : α} :
-  [a].sum = a := by simp [Std.LawfulRightIdentity.right_id]
-
 theorem sum_pair [Add α] [Zero α] [Std.LawfulRightIdentity (α := α) (· + ·) 0] {a b : α} :
   [a, b].sum = a + b := by simp [Std.LawfulRightIdentity.right_id]
 
@@ -1383,14 +1365,8 @@ theorem sum_flatten [Add α] [Zero α] [Std.LawfulIdentity (α := α) (· + ·)
     l.flatten.sum = (l.map sum).sum := by
   induction l with simp [*]
 
-theorem sum_eq_foldl [Add α] [Zero α] [Std.Associative (α := α) (· + ·)]
-    [Std.LawfulIdentity (α := α) (· + ·) 0] {l : List α} :
-    l.sum = l.foldl (· + ·) 0 := foldr_eq_foldl ..
-
 theorem take_succ_drop {l : List α} {n stop : Nat}
     (h : n < l.length - stop) :
     (l.drop stop |>.take (n + 1)) = (l.drop stop |>.take n) ++ [l[stop + n]'(by omega)] := by
   rw [← List.take_append_getElem (by simpa [← List.length_drop] using h)]
   simp [List.getElem_drop]
-
-attribute [simp] reverse_singleton

Batteries/Data/List/Pairwise.lean

@@ -69,7 +69,7 @@ theorem pwFilter_sublist [DecidableRel (α := α) R] : ∀ l : List α, pwFilter
   | [] => nil_sublist _
   | x :: l =>
     if h : ∀ y ∈ pwFilter R l, R x y then
-      pwFilter_cons_of_pos h ▸ (pwFilter_sublist l).cons₂ _
+      pwFilter_cons_of_pos h ▸ (pwFilter_sublist l).cons_cons _
     else
       pwFilter_cons_of_neg h ▸ Sublist.cons _ (pwFilter_sublist l)
 

Batteries/Data/List/Perm.lean

@@ -86,10 +86,10 @@ theorem Subperm.count_le [BEq α] {l₁ l₂ : List α} (s : l₁ <+~ l₂) (a)
     count a l₁ ≤ count a l₂ := s.countP_le _
 
 theorem subperm_cons (a : α) {l₁ l₂ : List α} : a :: l₁ <+~ a :: l₂ ↔ l₁ <+~ l₂ := by
-  refine ⟨fun ⟨l, p, s⟩ => ?_, fun ⟨l, p, s⟩ => ⟨a :: l, p.cons a, s.cons₂ _⟩⟩
+  refine ⟨fun ⟨l, p, s⟩ => ?_, fun ⟨l, p, s⟩ => ⟨a :: l, p.cons a, s.cons_cons _⟩⟩
   match s with
   | .cons _ s' => exact (p.subperm_left.2 <| (sublist_cons_self _ _).subperm).trans s'.subperm
-  | .cons₂ _ s' => exact ⟨_, p.cons_inv, s'⟩
+  | .cons_cons _ s' => exact ⟨_, p.cons_inv, s'⟩
 
 /-- Weaker version of `Subperm.cons_left` -/
 theorem cons_subperm_of_not_mem_of_mem {a : α} {l₁ l₂ : List α} (h₁ : a ∉ l₁) (h₂ : a ∈ l₂)
@@ -100,17 +100,17 @@ theorem cons_subperm_of_not_mem_of_mem {a : α} {l₁ l₂ : List α} (h₁ : a
   | @cons r₁ _ b s' ih =>
     simp at h₂
     match h₂ with
-    | .inl e => subst_vars; exact ⟨_ :: r₁, p.cons _, s'.cons₂ _⟩
+    | .inl e => subst_vars; exact ⟨_ :: r₁, p.cons _, s'.cons_cons _⟩
     | .inr m => let ⟨t, p', s'⟩ := ih h₁ m p; exact ⟨t, p', s'.cons _⟩
-  | @cons₂ _ r₂ b _ ih =>
+  | @cons_cons _ r₂ b _ ih =>
     have bm : b ∈ l₁ := p.subset mem_cons_self
     have am : a ∈ r₂ := by
       simp only [mem_cons] at h₂
       exact h₂.resolve_left fun e => h₁ <| e.symm ▸ bm
     obtain ⟨t₁, t₂, rfl⟩ := append_of_mem bm
     have st : t₁ ++ t₂ <+ t₁ ++ b :: t₂ := by simp
     obtain ⟨t, p', s'⟩ := ih (mt (st.subset ·) h₁) am (.cons_inv <| p.trans perm_middle)
-    exact ⟨b :: t, (p'.cons b).trans <| (swap ..).trans (perm_middle.symm.cons a), s'.cons₂ _⟩
+    exact ⟨b :: t, (p'.cons b).trans <| (swap ..).trans (perm_middle.symm.cons a), s'.cons_cons _⟩
 
 theorem subperm_append_left {l₁ l₂ : List α} : ∀ l, l ++ l₁ <+~ l ++ l₂ ↔ l₁ <+~ l₂
   | [] => .rfl
@@ -131,7 +131,7 @@ theorem Subperm.exists_of_length_lt {l₁ l₂ : List α} (s : l₁ <+~ l₂) (h
     match Nat.lt_or_eq_of_le (Nat.le_of_lt_succ h) with
     | .inl h => exact (IH h).imp fun a s => s.trans (sublist_cons_self _ _).subperm
     | .inr h => exact ⟨a, s.eq_of_length h ▸ .refl _⟩
-  | cons₂ b _ IH =>
+  | cons_cons b _ IH =>
     exact (IH <| Nat.lt_of_succ_lt_succ h).imp fun a s =>
       (swap ..).subperm_right.1 <| (subperm_cons _).2 s
 
@@ -155,15 +155,15 @@ theorem Nodup.perm_iff_eq_of_sublist {l₁ l₂ l : List α} (d : Nodup l)
   | cons a s₂ IH =>
     match s₁ with
     | .cons _ s₁ => exact IH d.2 s₁ h
-    | .cons₂ _ s₁ =>
+    | .cons_cons _ s₁ =>
       have := Subperm.subset ⟨_, h.symm, s₂⟩ (.head _)
       exact (d.1 this).elim
-  | cons₂ a _ IH =>
+  | cons_cons a _ IH =>
     match s₁ with
     | .cons _ s₁ =>
       have := Subperm.subset ⟨_, h, s₁⟩ (.head _)
       exact (d.1 this).elim
-    | .cons₂ _ s₁ => rw [IH d.2 s₁ h.cons_inv]
+    | .cons_cons _ s₁ => rw [IH d.2 s₁ h.cons_inv]
 
 theorem subperm_cons_erase [BEq α] [LawfulBEq α] (a : α) (l : List α) : l <+~ a :: l.erase a :=
   if h : a ∈ l then

Batteries/Data/String/Lemmas.lean

@@ -92,7 +92,7 @@ open List
 theorem utf8Len_le_of_sublist : ∀ {cs₁ cs₂}, cs₁ <+ cs₂ → utf8Len cs₁ ≤ utf8Len cs₂
   | _, _, .slnil => Nat.le_refl _
   | _, _, .cons _ h => Nat.le_trans (utf8Len_le_of_sublist h) (Nat.le_add_right ..)
-  | _, _, .cons₂ _ h => Nat.add_le_add_right (utf8Len_le_of_sublist h) _
+  | _, _, .cons_cons _ h => Nat.add_le_add_right (utf8Len_le_of_sublist h) _
 
 theorem utf8Len_le_of_infix (h : cs₁ <:+: cs₂) : utf8Len cs₁ ≤ utf8Len cs₂ :=
   utf8Len_le_of_sublist h.sublist
@@ -322,25 +322,13 @@ theorem prev_of_valid' (cs cs' : List Char) :
   | _, .inl rfl => apply Pos.Raw.prev_zero
   | _, .inr ⟨cs, c, rfl⟩ => simp [prev_of_valid, -ofList_append]
 
-theorem front_eq (s : String) : Legacy.front s = s.toList.headD default := by
-  unfold Legacy.front; simpa using get_of_valid [] s.toList
-
 theorem back_eq_get_prev_rawEndPos {s : String} : Legacy.back s = (s.rawEndPos.prev s).get s := rfl
 
-theorem back_eq (s : String) : Legacy.back s = s.toList.getLastD default := by
-  conv => lhs; rw [← s.ofList_toList]
-  match s.toList.eq_nil_or_concat with
-  | .inl h => simp [h]; rfl
-  | .inr ⟨cs, c, h⟩ =>
-    simp only [h, back_eq_get_prev_rawEndPos]
-    have : (ofList (cs ++ [c])).rawEndPos = ⟨utf8Len cs + c.utf8Size⟩ := by
-      simp [rawEndPos, utf8ByteSize_ofList]
-    simp [-ofList_append, this, prev_of_valid, get_of_valid]
-
 theorem atEnd_of_valid (cs : List Char) (cs' : List Char) :
     String.Pos.Raw.atEnd (ofList (cs ++ cs')) ⟨utf8Len cs⟩ ↔ cs' = [] := by
   rw [atEnd_iff]
-  cases cs' <;> simp [add_utf8Size_pos, rawEndPos, utf8ByteSize_ofList]
+  cases cs' <;> simp [rawEndPos, utf8ByteSize_ofList]
+  exact Nat.add_pos_left (Char.utf8Size_pos _) _
 
 unseal Legacy.posOfAux Legacy.findAux in
 theorem posOfAux_eq (s c) : Legacy.posOfAux s c = Legacy.findAux s (· == c) := (rfl)
@@ -517,24 +505,25 @@ theorem extract_of_valid (l m r : List Char) :
 
 theorem splitAux_of_valid (p l m r acc) :
     splitAux (ofList (l ++ m ++ r)) p ⟨utf8Len l⟩ ⟨utf8Len l + utf8Len m⟩ acc =
-      acc.reverse ++ (List.splitOnP.go p r m.reverse).map ofList := by
+      acc.reverse ++ (List.splitOnPPrepend p r m.reverse).map ofList := by
   unfold splitAux
   simp only [List.append_assoc, atEnd_iff, rawEndPos_ofList, utf8Len_append, Pos.Raw.mk_le_mk,
     Nat.add_le_add_iff_left, (by omega : utf8Len m + utf8Len r ≤ utf8Len m ↔ utf8Len r = 0),
     utf8Len_eq_zero, List.reverse_cons, dite_eq_ite]
   split
-  · subst r; simpa [List.splitOnP.go] using extract_of_valid l m []
+  · subst r
+    simpa using extract_of_valid l m []
   · obtain ⟨c, r, rfl⟩ := r.exists_cons_of_ne_nil ‹_›
     simp only [by
       simpa [-ofList_append] using
         (⟨get_of_valid (l ++ m) (c :: r), next_of_valid (l ++ m) c r,
             extract_of_valid l m (c :: r)⟩ :
-          _ ∧ _ ∧ _),
-      List.splitOnP.go, List.reverse_reverse]
+          _ ∧ _ ∧ _)]
     split <;> rename_i h
-    · simpa [Nat.add_assoc]
-        using splitAux_of_valid p (l++m++[c]) [] r ((ofList m)::acc)
-    · simpa [Nat.add_assoc] using splitAux_of_valid p l (m++[c]) r acc
+    · simpa [Nat.add_assoc, List.splitOnPPrepend_cons_eq_if, h] using
+        splitAux_of_valid p (l++m++[c]) [] r ((ofList m)::acc)
+    · simpa [List.splitOnPPrepend_cons_eq_if, h, Nat.add_assoc] using
+        splitAux_of_valid p l (m++[c]) r acc
 
 theorem splitToList_of_valid (s p) : splitToList s p = (List.splitOnP p s.toList).map ofList := by
   simpa [splitToList] using splitAux_of_valid p [] [] s.toList []
@@ -559,12 +548,9 @@ theorem join_eq (ss : List String) : join ss = ofList (ss.map toList).flatten :=
   | nil => simp
   | cons s ss ih => simp [ih]
 
-@[simp] theorem toList_join (ss : List String) : (join ss).toList = (ss.map toList).flatten := by
-  simp [join_eq]
-
 @[deprecated toList_join (since := "2025-10-31")]
 theorem data_join (ss : List String) : (join ss).toList = (ss.map toList).flatten :=
-  toList_join ss
+  toList_join
 
 namespace Legacy.Iterator
 
@@ -573,7 +559,7 @@ namespace Legacy.Iterator
 
 theorem hasNext_cons_addChar (c : Char) (cs : List Char) (i : Pos.Raw) :
     hasNext ⟨String.ofList (c :: cs), i + c⟩ = hasNext ⟨String.ofList cs, i⟩ := by
-  simp [hasNext, Nat.add_lt_add_iff_right]
+  simp [hasNext, utf8ByteSize_ofList]; lia
 
 /-- Validity for a string iterator. -/
 def Valid (it : Iterator) : Prop := it.pos.Valid it.s

Batteries/Data/Vector/Lemmas.lean

@@ -100,7 +100,7 @@ theorem get_tail (v : Vector α (n + 1)) (i : Fin n) :
 
 @[simp]
 theorem finIdxOf?_empty [BEq α] (v : Vector α 0) : v.finIdxOf? a = none := by
-  simp [v.eq_empty]; rfl
+  simp [v.eq_empty]
 
 @[simp]
 theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {v : Vector α n} {a : α} :

Batteries/Lean/Expr.lean

@@ -32,7 +32,7 @@ def toSyntax (e : Expr) : TermElabM Syntax.Term := withFreshMacroScope do
 /-- Like `withApp` but ignores metadata. -/
 @[inline]
 def withApp' (e : Expr) (k : Expr → Array Expr → α) : α :=
-  let dummy := mkSort levelZero
+  let dummy := mkSort .zero
   let nargs := e.getAppNumArgs'
   go e (.replicate nargs dummy) (nargs - 1)
 where

Batteries/Tactic/Alias.lean

@@ -88,9 +88,11 @@ elab (name := alias) mods:declModifiers "alias " alias:ident " := " name:ident :
     let declMods ← elabModifiers mods
     Lean.withExporting (isExporting := declMods.isInferredPublic (← getEnv)) do
     let (attrs, machineApplicable) := setDeprecatedTarget name declMods.attrs
+    let env ← getEnv
     let declMods := { declMods with
       computeKind :=
-        if isNoncomputable (← getEnv) name then .noncomputable
+        if isNoncomputable env name then .noncomputable
+        else if isMarkedMeta env name then .meta
         else declMods.computeKind
       isUnsafe := declMods.isUnsafe || cinfo.isUnsafe
       attrs
@@ -109,10 +111,11 @@ elab (name := alias) mods:declModifiers "alias " alias:ident " := " name:ident :
         safety := if declMods.isUnsafe then .unsafe else .safe
       }
     checkNotAlreadyDeclared declName
-    if declMods.isNoncomputable then
-      addDecl decl
-    else
-      addAndCompile decl
+    addDecl decl
+    if !declMods.isNoncomputable then
+      if declMods.isMeta then
+        modifyEnv (markMeta · declName)
+      compileDecl decl
     addDeclarationRangesFromSyntax declName (← getRef) alias
     Term.addTermInfo' alias (← mkConstWithLevelParams declName) (isBinder := true)
     if let some (doc, isVerso) := declMods.docString? then