From 9bd4dfb6960e1706151f00665b056a7fa0eb894e Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Fri, 27 Feb 2026 09:58:08 +0100 Subject: [PATCH] =?UTF-8?q?chore:=20prefer=20`cons=5Fcons`=20over=20`cons?= =?UTF-8?q?=E2=82=82`=20in=20names=20(#12710)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR deprecated the handful of names in core involving the component `cons₂` in favor of `cons_cons`. --- src/Init/Data/List/Basic.lean | 36 +++++++++++--- src/Init/Data/List/Erase.lean | 2 +- src/Init/Data/List/Find.lean | 4 +- src/Init/Data/List/Lemmas.lean | 4 +- src/Init/Data/List/Nat/BEq.lean | 2 +- src/Init/Data/List/Nat/Count.lean | 2 +- src/Init/Data/List/Nat/Pairwise.lean | 4 +- src/Init/Data/List/Nat/TakeDrop.lean | 2 +- src/Init/Data/List/Pairwise.lean | 4 +- src/Init/Data/List/Perm.lean | 10 ++-- src/Init/Data/List/Sort/Lemmas.lean | 4 +- src/Init/Data/List/Sublist.lean | 66 ++++++++++++++------------ src/Init/Data/List/ToArray.lean | 4 +- src/Init/Omega/IntList.lean | 20 +++++--- tests/elab/list_simp.lean | 2 +- tests/lean/grind/experiments/list.lean | 2 +- 16 files changed, 100 insertions(+), 68 deletions(-) diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 1ddccabbee..d4deb9493e 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -135,7 +135,11 @@ protected def beq [BEq α] : List α → List α → Bool @[simp] theorem beq_nil_nil [BEq α] : List.beq ([] : List α) ([] : List α) = true := rfl @[simp] theorem beq_cons_nil [BEq α] {a : α} {as : List α} : List.beq (a::as) [] = false := rfl @[simp] theorem beq_nil_cons [BEq α] {a : α} {as : List α} : List.beq [] (a::as) = false := rfl -theorem beq_cons₂ [BEq α] {a b : α} {as bs : List α} : List.beq (a::as) (b::bs) = (a == b && List.beq as bs) := rfl +theorem beq_cons_cons [BEq α] {a b : α} {as bs : List α} : List.beq (a::as) (b::bs) = (a == b && List.beq as bs) := rfl + +@[deprecated beq_cons_cons (since := "2026-02-26")] +theorem beq_cons₂ [BEq α] {a b : α} {as bs : List α} : + List.beq (a::as) (b::bs) = (a == b && List.beq as bs) := beq_cons_cons instance [BEq α] : BEq (List α) := ⟨List.beq⟩ @@ -175,7 +179,10 @@ Examples: @[simp, grind =] theorem isEqv_nil_nil : isEqv ([] : List α) [] eqv = true := rfl @[simp, grind =] theorem isEqv_nil_cons : isEqv ([] : List α) (a::as) eqv = false := rfl @[simp, grind =] theorem isEqv_cons_nil : isEqv (a::as : List α) [] eqv = false := rfl -@[grind =] theorem isEqv_cons₂ : isEqv (a::as) (b::bs) eqv = (eqv a b && isEqv as bs eqv) := rfl +@[grind =] theorem isEqv_cons_cons : isEqv (a::as) (b::bs) eqv = (eqv a b && isEqv as bs eqv) := rfl + +@[deprecated isEqv_cons_cons (since := "2026-02-26")] +theorem isEqv_cons₂ : isEqv (a::as) (b::bs) eqv = (eqv a b && isEqv as bs eqv) := isEqv_cons_cons /-! ## Lexicographic ordering -/ @@ -1048,9 +1055,12 @@ def dropLast {α} : List α → List α @[simp, grind =] theorem dropLast_nil : ([] : List α).dropLast = [] := rfl @[simp, grind =] theorem dropLast_singleton : [x].dropLast = [] := rfl -@[simp, grind =] theorem dropLast_cons₂ : +@[simp, grind =] theorem dropLast_cons_cons : (x::y::zs).dropLast = x :: (y::zs).dropLast := rfl +@[deprecated dropLast_cons_cons (since := "2026-02-26")] +theorem dropLast_cons₂ : (x::y::zs).dropLast = x :: (y::zs).dropLast := dropLast_cons_cons + -- Later this can be proved by `simp` via `[List.length_dropLast, List.length_cons, Nat.add_sub_cancel]`, -- but we need this while bootstrapping `Array`. @[simp] theorem length_dropLast_cons {a : α} {as : List α} : (a :: as).dropLast.length = as.length := by @@ -1085,7 +1095,11 @@ inductive Sublist {α} : List α → List α → Prop /-- If `l₁` is a subsequence of `l₂`, then it is also a subsequence of `a :: l₂`. -/ | cons a : Sublist l₁ l₂ → Sublist l₁ (a :: l₂) /-- If `l₁` is a subsequence of `l₂`, then `a :: l₁` is a subsequence of `a :: l₂`. -/ - | cons₂ a : Sublist l₁ l₂ → Sublist (a :: l₁) (a :: l₂) + | cons_cons a : Sublist l₁ l₂ → Sublist (a :: l₁) (a :: l₂) + +set_option linter.missingDocs false in +@[deprecated Sublist.cons_cons (since := "2026-02-26"), match_pattern] +abbrev Sublist.cons₂ := @Sublist.cons_cons @[inherit_doc] scoped infixl:50 " <+ " => Sublist @@ -1143,9 +1157,13 @@ def isPrefixOf [BEq α] : List α → List α → Bool @[simp, grind =] theorem isPrefixOf_nil_left [BEq α] : isPrefixOf ([] : List α) l = true := by simp [isPrefixOf] @[simp, grind =] theorem isPrefixOf_cons_nil [BEq α] : isPrefixOf (a::as) ([] : List α) = false := rfl -@[grind =] theorem isPrefixOf_cons₂ [BEq α] {a : α} : +@[grind =] theorem isPrefixOf_cons_cons [BEq α] {a : α} : isPrefixOf (a::as) (b::bs) = (a == b && isPrefixOf as bs) := rfl +@[deprecated isPrefixOf_cons_cons (since := "2026-02-26")] +theorem isPrefixOf_cons₂ [BEq α] {a : α} : + isPrefixOf (a::as) (b::bs) = (a == b && isPrefixOf as bs) := isPrefixOf_cons_cons + /-- If the first list is a prefix of the second, returns the result of dropping the prefix. @@ -2165,11 +2183,15 @@ def intersperse (sep : α) : (l : List α) → List α @[simp] theorem intersperse_nil {sep : α} : ([] : List α).intersperse sep = [] := rfl @[simp] theorem intersperse_singleton {x : α} {sep : α} : [x].intersperse sep = [x] := rfl -@[deprecated intersperse_single (since := "2026-02-26")] +@[deprecated intersperse_singleton (since := "2026-02-26")] theorem intersperse_single {x : α} {sep : α} : [x].intersperse sep = [x] := rfl -@[simp] theorem intersperse_cons₂ {x : α} {y : α} {zs : List α} {sep : α} : +@[simp] theorem intersperse_cons_cons {x : α} {y : α} {zs : List α} {sep : α} : (x::y::zs).intersperse sep = x::sep::((y::zs).intersperse sep) := rfl +@[deprecated intersperse_cons_cons (since := "2026-02-26")] +theorem intersperse_cons₂ {x : α} {y : α} {zs : List α} {sep : α} : + (x::y::zs).intersperse sep = x::sep::((y::zs).intersperse sep) := intersperse_cons_cons + /-! ### intercalate -/ set_option linter.listVariables false in diff --git a/src/Init/Data/List/Erase.lean b/src/Init/Data/List/Erase.lean index 043b4fd6a5..38681ba324 100644 --- a/src/Init/Data/List/Erase.lean +++ b/src/Init/Data/List/Erase.lean @@ -125,7 +125,7 @@ protected theorem Sublist.eraseP : l₁ <+ l₂ → l₁.eraseP p <+ l₂.eraseP by_cases h : p a · simpa [h] using s.eraseP.trans eraseP_sublist · simpa [h] using s.eraseP.cons _ - | .cons₂ a s => by + | .cons_cons a s => by by_cases h : p a · simpa [h] using s · simpa [h] using s.eraseP diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean index 3291d3ae5a..276b3adb8b 100644 --- a/src/Init/Data/List/Find.lean +++ b/src/Init/Data/List/Find.lean @@ -184,7 +184,7 @@ theorem Sublist.findSome?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) : induction h with | slnil => simp | cons a h ih - | cons₂ a h ih => + | cons_cons a h ih => simp only [findSome?] split · simp_all @@ -455,7 +455,7 @@ theorem Sublist.find?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) : (l₁.fi induction h with | slnil => simp | cons a h ih - | cons₂ a h ih => + | cons_cons a h ih => simp only [find?] split · simp diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 7a97bb47b8..aa413f1a79 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -1394,7 +1394,7 @@ theorem head_filter_of_pos {p : α → Bool} {l : List α} (w : l ≠ []) (h : p @[simp] theorem filter_sublist {p : α → Bool} : ∀ {l : List α}, filter p l <+ l | [] => .slnil - | a :: l => by rw [filter]; split <;> simp [Sublist.cons, Sublist.cons₂, filter_sublist] + | a :: l => by rw [filter]; split <;> simp [Sublist.cons, Sublist.cons_cons, filter_sublist] /-! ### filterMap -/ @@ -3154,7 +3154,7 @@ theorem dropLast_concat_getLast : ∀ {l : List α} (h : l ≠ []), dropLast l + | [], h => absurd rfl h | [_], _ => rfl | _ :: b :: l, _ => by - rw [dropLast_cons₂, cons_append, getLast_cons (cons_ne_nil _ _)] + rw [dropLast_cons_cons, cons_append, getLast_cons (cons_ne_nil _ _)] congr exact dropLast_concat_getLast (cons_ne_nil b l) diff --git a/src/Init/Data/List/Nat/BEq.lean b/src/Init/Data/List/Nat/BEq.lean index 50003973e5..6b1f9a6694 100644 --- a/src/Init/Data/List/Nat/BEq.lean +++ b/src/Init/Data/List/Nat/BEq.lean @@ -42,7 +42,7 @@ theorem beq_eq_isEqv [BEq α] {as bs : List α} : as.beq bs = isEqv as bs (· == cases bs with | nil => simp | cons b bs => - simp only [beq_cons₂, ih, isEqv_eq_decide, length_cons, Nat.add_right_cancel_iff, + simp only [beq_cons_cons, ih, isEqv_eq_decide, length_cons, Nat.add_right_cancel_iff, Nat.forall_lt_succ_left', getElem_cons_zero, getElem_cons_succ, Bool.decide_and, Bool.decide_eq_true] split <;> simp diff --git a/src/Init/Data/List/Nat/Count.lean b/src/Init/Data/List/Nat/Count.lean index d8174e3621..e5a558e4dc 100644 --- a/src/Init/Data/List/Nat/Count.lean +++ b/src/Init/Data/List/Nat/Count.lean @@ -106,7 +106,7 @@ theorem Sublist.le_countP (s : l₁ <+ l₂) (p) : countP p l₂ - (l₂.length have := s.le_countP p have := s.length_le split <;> omega - | .cons₂ a s => + | .cons_cons a s => rename_i l₁ l₂ simp only [countP_cons, length_cons] have := s.le_countP p diff --git a/src/Init/Data/List/Nat/Pairwise.lean b/src/Init/Data/List/Nat/Pairwise.lean index 511a51b3e5..2b825920b1 100644 --- a/src/Init/Data/List/Nat/Pairwise.lean +++ b/src/Init/Data/List/Nat/Pairwise.lean @@ -38,7 +38,7 @@ theorem map_getElem_sublist {l : List α} {is : List (Fin l.length)} (h : is.Pai simp only [Fin.getElem_fin, map_cons] have := IH h.of_cons (hd+1) (pairwise_cons.mp h).1 specialize his hd (.head _) - have := (drop_eq_getElem_cons ..).symm ▸ this.cons₂ (get l hd) + have := (drop_eq_getElem_cons ..).symm ▸ this.cons_cons (get l hd) have := Sublist.append (nil_sublist (take hd l |>.drop j)) this rwa [nil_append, ← (drop_append_of_le_length ?_), take_append_drop] at this simp [Nat.min_eq_left (Nat.le_of_lt hd.isLt), his] @@ -55,7 +55,7 @@ theorem sublist_eq_map_getElem {l l' : List α} (h : l' <+ l) : ∃ is : List (F refine ⟨is.map (·.succ), ?_⟩ set_option backward.isDefEq.respectTransparency false in simpa [Function.comp_def, pairwise_map] - | cons₂ _ _ IH => + | cons_cons _ _ IH => rcases IH with ⟨is,IH⟩ refine ⟨⟨0, by simp [Nat.zero_lt_succ]⟩ :: is.map (·.succ), ?_⟩ set_option backward.isDefEq.respectTransparency false in diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean index d6146cb9f6..e9b13e7f66 100644 --- a/src/Init/Data/List/Nat/TakeDrop.lean +++ b/src/Init/Data/List/Nat/TakeDrop.lean @@ -207,7 +207,7 @@ theorem take_eq_dropLast {l : List α} {i : Nat} (h : i + 1 = l.length) : · cases as with | nil => simp_all | cons b bs => - simp only [take_succ_cons, dropLast_cons₂] + simp only [take_succ_cons, dropLast_cons_cons] rw [ih] simpa using h diff --git a/src/Init/Data/List/Pairwise.lean b/src/Init/Data/List/Pairwise.lean index ab72091378..ee32dfe74a 100644 --- a/src/Init/Data/List/Pairwise.lean +++ b/src/Init/Data/List/Pairwise.lean @@ -33,7 +33,7 @@ open Nat @[grind →] theorem Pairwise.sublist : l₁ <+ l₂ → l₂.Pairwise R → l₁.Pairwise R | .slnil, h => h | .cons _ s, .cons _ h₂ => h₂.sublist s - | .cons₂ _ s, .cons h₁ h₂ => (h₂.sublist s).cons fun _ h => h₁ _ (s.subset h) + | .cons_cons _ s, .cons h₁ h₂ => (h₂.sublist s).cons fun _ h => h₁ _ (s.subset h) theorem Pairwise.imp {α R S} (H : ∀ {a b}, R a b → S a b) : ∀ {l : List α}, l.Pairwise R → l.Pairwise S @@ -226,7 +226,7 @@ theorem pairwise_iff_forall_sublist : l.Pairwise R ↔ (∀ {a b}, [a,b] <+ l constructor <;> intro h · intro | a, b, .cons _ hab => exact IH.mp h.2 hab - | _, b, .cons₂ _ hab => refine h.1 _ (hab.subset ?_); simp + | _, b, .cons_cons _ hab => refine h.1 _ (hab.subset ?_); simp · constructor · intro x hx apply h diff --git a/src/Init/Data/List/Perm.lean b/src/Init/Data/List/Perm.lean index 349301ec96..ceeef7d418 100644 --- a/src/Init/Data/List/Perm.lean +++ b/src/Init/Data/List/Perm.lean @@ -252,13 +252,13 @@ theorem exists_perm_sublist {l₁ l₂ l₂' : List α} (s : l₁ <+ l₂) (p : | cons x _ IH => match s with | .cons _ s => let ⟨l₁', p', s'⟩ := IH s; exact ⟨l₁', p', s'.cons _⟩ - | .cons₂ _ s => let ⟨l₁', p', s'⟩ := IH s; exact ⟨x :: l₁', p'.cons x, s'.cons₂ _⟩ + | .cons_cons _ s => let ⟨l₁', p', s'⟩ := IH s; exact ⟨x :: l₁', p'.cons x, s'.cons_cons _⟩ | swap x y l' => match s with | .cons _ (.cons _ s) => exact ⟨_, .rfl, (s.cons _).cons _⟩ - | .cons _ (.cons₂ _ s) => exact ⟨x :: _, .rfl, (s.cons _).cons₂ _⟩ - | .cons₂ _ (.cons _ s) => exact ⟨y :: _, .rfl, (s.cons₂ _).cons _⟩ - | .cons₂ _ (.cons₂ _ s) => exact ⟨x :: y :: _, .swap .., (s.cons₂ _).cons₂ _⟩ + | .cons _ (.cons_cons _ s) => exact ⟨x :: _, .rfl, (s.cons _).cons_cons _⟩ + | .cons_cons _ (.cons _ s) => exact ⟨y :: _, .rfl, (s.cons_cons _).cons _⟩ + | .cons_cons _ (.cons_cons _ s) => exact ⟨x :: y :: _, .swap .., (s.cons_cons _).cons_cons _⟩ | trans _ _ IH₁ IH₂ => let ⟨_, pm, sm⟩ := IH₁ s let ⟨r₁, pr, sr⟩ := IH₂ sm @@ -277,7 +277,7 @@ theorem Sublist.exists_perm_append {l₁ l₂ : List α} : l₁ <+ l₂ → ∃ | Sublist.cons a s => let ⟨l, p⟩ := Sublist.exists_perm_append s ⟨a :: l, (p.cons a).trans perm_middle.symm⟩ - | Sublist.cons₂ a s => + | Sublist.cons_cons a s => let ⟨l, p⟩ := Sublist.exists_perm_append s ⟨l, p.cons a⟩ diff --git a/src/Init/Data/List/Sort/Lemmas.lean b/src/Init/Data/List/Sort/Lemmas.lean index c1a39e81de..fc0e6de1f4 100644 --- a/src/Init/Data/List/Sort/Lemmas.lean +++ b/src/Init/Data/List/Sort/Lemmas.lean @@ -452,7 +452,7 @@ theorem sublist_mergeSort have h' := sublist_mergeSort trans total hc h rw [h₂] at h' exact h'.middle a - | _, _, @Sublist.cons₂ _ l₁ l₂ a h => by + | _, _, @Sublist.cons_cons _ l₁ l₂ a h => by rename_i hc obtain ⟨l₃, l₄, h₁, h₂, h₃⟩ := mergeSort_cons trans total a l₂ rw [h₁] @@ -460,7 +460,7 @@ theorem sublist_mergeSort rw [h₂] at h' simp only [Bool.not_eq_true', tail_cons] at h₃ h' exact - sublist_append_of_sublist_right (Sublist.cons₂ a + sublist_append_of_sublist_right (Sublist.cons_cons a ((fun w => Sublist.of_sublist_append_right w h') fun b m₁ m₃ => (Bool.eq_not_self true).mp ((rel_of_pairwise_cons hc m₁).symm.trans (h₃ b m₃)))) diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean index dfce99100e..13bfd54403 100644 --- a/src/Init/Data/List/Sublist.lean +++ b/src/Init/Data/List/Sublist.lean @@ -32,8 +32,12 @@ open Nat section isPrefixOf variable [BEq α] -@[simp, grind =] theorem isPrefixOf_cons₂_self [LawfulBEq α] {a : α} : - isPrefixOf (a::as) (a::bs) = isPrefixOf as bs := by simp [isPrefixOf_cons₂] +@[simp, grind =] theorem isPrefixOf_cons_cons_self [LawfulBEq α] {a : α} : + isPrefixOf (a::as) (a::bs) = isPrefixOf as bs := by simp [isPrefixOf_cons_cons] + +@[deprecated isPrefixOf_cons_cons_self (since := "2026-02-26")] +theorem isPrefixOf_cons₂_self [LawfulBEq α] {a : α} : + isPrefixOf (a::as) (a::bs) = isPrefixOf as bs := isPrefixOf_cons_cons_self @[simp] theorem isPrefixOf_length_pos_nil {l : List α} (h : 0 < l.length) : isPrefixOf l [] = false := by cases l <;> simp_all [isPrefixOf] @@ -45,7 +49,7 @@ variable [BEq α] | cons _ _ ih => cases n · simp - · simp [replicate_succ, isPrefixOf_cons₂, ih, Nat.succ_le_succ_iff, Bool.and_left_comm] + · simp [replicate_succ, isPrefixOf_cons_cons, ih, Nat.succ_le_succ_iff, Bool.and_left_comm] end isPrefixOf @@ -169,18 +173,18 @@ theorem subset_replicate {n : Nat} {a : α} {l : List α} (h : n ≠ 0) : l ⊆ @[simp, grind ←] theorem Sublist.refl : ∀ l : List α, l <+ l | [] => .slnil - | a :: l => (Sublist.refl l).cons₂ a + | a :: l => (Sublist.refl l).cons_cons a theorem Sublist.trans {l₁ l₂ l₃ : List α} (h₁ : l₁ <+ l₂) (h₂ : l₂ <+ l₃) : l₁ <+ l₃ := by induction h₂ generalizing l₁ with | slnil => exact h₁ | cons _ _ IH => exact (IH h₁).cons _ - | @cons₂ l₂ _ a _ IH => + | @cons_cons l₂ _ a _ IH => generalize e : a :: l₂ = l₂' at h₁ match h₁ with | .slnil => apply nil_sublist | .cons a' h₁' => cases e; apply (IH h₁').cons - | .cons₂ a' h₁' => cases e; apply (IH h₁').cons₂ + | .cons_cons a' h₁' => cases e; apply (IH h₁').cons_cons instance : Trans (@Sublist α) Sublist Sublist := ⟨Sublist.trans⟩ @@ -193,23 +197,23 @@ theorem sublist_of_cons_sublist : a :: l₁ <+ l₂ → l₁ <+ l₂ := @[simp, grind =] theorem cons_sublist_cons : a :: l₁ <+ a :: l₂ ↔ l₁ <+ l₂ := - ⟨fun | .cons _ s => sublist_of_cons_sublist s | .cons₂ _ s => s, .cons₂ _⟩ + ⟨fun | .cons _ s => sublist_of_cons_sublist s | .cons_cons _ s => s, .cons_cons _⟩ theorem sublist_or_mem_of_sublist (h : l <+ l₁ ++ a :: l₂) : l <+ l₁ ++ l₂ ∨ a ∈ l := by induction l₁ generalizing l with | nil => match h with | .cons _ h => exact .inl h - | .cons₂ _ h => exact .inr (.head ..) + | .cons_cons _ h => exact .inr (.head ..) | cons b l₁ IH => match h with | .cons _ h => exact (IH h).imp_left (Sublist.cons _) - | .cons₂ _ h => exact (IH h).imp (Sublist.cons₂ _) (.tail _) + | .cons_cons _ h => exact (IH h).imp (Sublist.cons_cons _) (.tail _) @[grind →] theorem Sublist.subset : l₁ <+ l₂ → l₁ ⊆ l₂ | .slnil, _, h => h | .cons _ s, _, h => .tail _ (s.subset h) - | .cons₂ .., _, .head .. => .head .. - | .cons₂ _ s, _, .tail _ h => .tail _ (s.subset h) + | .cons_cons .., _, .head .. => .head .. + | .cons_cons _ s, _, .tail _ h => .tail _ (s.subset h) protected theorem Sublist.mem (hx : a ∈ l₁) (hl : l₁ <+ l₂) : a ∈ l₂ := hl.subset hx @@ -245,7 +249,7 @@ theorem eq_nil_of_sublist_nil {l : List α} (s : l <+ []) : l = [] := theorem Sublist.length_le : l₁ <+ l₂ → length l₁ ≤ length l₂ | .slnil => Nat.le_refl 0 | .cons _l s => le_succ_of_le (length_le s) - | .cons₂ _ s => succ_le_succ (length_le s) + | .cons_cons _ s => succ_le_succ (length_le s) grind_pattern Sublist.length_le => l₁ <+ l₂, length l₁ grind_pattern Sublist.length_le => l₁ <+ l₂, length l₂ @@ -253,7 +257,7 @@ grind_pattern Sublist.length_le => l₁ <+ l₂, length l₂ theorem Sublist.eq_of_length : l₁ <+ l₂ → length l₁ = length l₂ → l₁ = l₂ | .slnil, _ => rfl | .cons a s, h => nomatch Nat.not_lt.2 s.length_le (h ▸ lt_succ_self _) - | .cons₂ a s, h => by rw [s.eq_of_length (succ.inj h)] + | .cons_cons a s, h => by rw [s.eq_of_length (succ.inj h)] theorem Sublist.eq_of_length_le (s : l₁ <+ l₂) (h : length l₂ ≤ length l₁) : l₁ = l₂ := s.eq_of_length <| Nat.le_antisymm s.length_le h @@ -275,7 +279,7 @@ grind_pattern tail_sublist => tail l <+ _ protected theorem Sublist.tail : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → tail l₁ <+ tail l₂ | _, _, slnil => .slnil | _, _, Sublist.cons _ h => (tail_sublist _).trans h - | _, _, Sublist.cons₂ _ h => h + | _, _, Sublist.cons_cons _ h => h @[grind →] theorem Sublist.of_cons_cons {l₁ l₂ : List α} {a b : α} (h : a :: l₁ <+ b :: l₂) : l₁ <+ l₂ := @@ -287,8 +291,8 @@ protected theorem Sublist.map (f : α → β) {l₁ l₂} (s : l₁ <+ l₂) : m | slnil => simp | cons a s ih => simpa using cons (f a) ih - | cons₂ a s ih => - simpa using cons₂ (f a) ih + | cons_cons a s ih => + simpa using cons_cons (f a) ih grind_pattern Sublist.map => l₁ <+ l₂, map f l₁ grind_pattern Sublist.map => l₁ <+ l₂, map f l₂ @@ -338,7 +342,7 @@ theorem sublist_filterMap_iff {l₁ : List β} {f : α → Option β} : cases h with | cons _ h => exact ⟨l', h, rfl⟩ - | cons₂ _ h => + | cons_cons _ h => rename_i l' exact ⟨l', h, by simp_all⟩ · constructor @@ -347,10 +351,10 @@ theorem sublist_filterMap_iff {l₁ : List β} {f : α → Option β} : | cons _ h => obtain ⟨l', s, rfl⟩ := ih.1 h exact ⟨l', Sublist.cons a s, rfl⟩ - | cons₂ _ h => + | cons_cons _ h => rename_i l' obtain ⟨l', s, rfl⟩ := ih.1 h - refine ⟨a :: l', Sublist.cons₂ a s, ?_⟩ + refine ⟨a :: l', Sublist.cons_cons a s, ?_⟩ rwa [filterMap_cons_some] · rintro ⟨l', h, rfl⟩ replace h := h.filterMap f @@ -369,7 +373,7 @@ theorem sublist_filter_iff {l₁ : List α} {p : α → Bool} : theorem sublist_append_left : ∀ l₁ l₂ : List α, l₁ <+ l₁ ++ l₂ | [], _ => nil_sublist _ - | _ :: l₁, l₂ => (sublist_append_left l₁ l₂).cons₂ _ + | _ :: l₁, l₂ => (sublist_append_left l₁ l₂).cons_cons _ grind_pattern sublist_append_left => Sublist, l₁ ++ l₂ @@ -382,7 +386,7 @@ grind_pattern sublist_append_right => Sublist, l₁ ++ l₂ @[simp, grind =] theorem singleton_sublist {a : α} {l} : [a] <+ l ↔ a ∈ l := by refine ⟨fun h => h.subset (mem_singleton_self _), fun h => ?_⟩ obtain ⟨_, _, rfl⟩ := append_of_mem h - exact ((nil_sublist _).cons₂ _).trans (sublist_append_right ..) + exact ((nil_sublist _).cons_cons _).trans (sublist_append_right ..) @[simp] theorem sublist_append_of_sublist_left (s : l <+ l₁) : l <+ l₁ ++ l₂ := s.trans <| sublist_append_left .. @@ -404,7 +408,7 @@ theorem Sublist.append_left : l₁ <+ l₂ → ∀ l, l ++ l₁ <+ l ++ l₂ := theorem Sublist.append_right : l₁ <+ l₂ → ∀ l, l₁ ++ l <+ l₂ ++ l | .slnil, _ => Sublist.refl _ | .cons _ h, _ => (h.append_right _).cons _ - | .cons₂ _ h, _ => (h.append_right _).cons₂ _ + | .cons_cons _ h, _ => (h.append_right _).cons_cons _ theorem Sublist.append (hl : l₁ <+ l₂) (hr : r₁ <+ r₂) : l₁ ++ r₁ <+ l₂ ++ r₂ := (hl.append_right _).trans ((append_sublist_append_left _).2 hr) @@ -418,10 +422,10 @@ theorem sublist_cons_iff {a : α} {l l'} : · intro h cases h with | cons _ h => exact Or.inl h - | cons₂ _ h => exact Or.inr ⟨_, rfl, h⟩ + | cons_cons _ h => exact Or.inr ⟨_, rfl, h⟩ · rintro (h | ⟨r, rfl, h⟩) · exact h.cons _ - · exact h.cons₂ _ + · exact h.cons_cons _ @[grind =] theorem cons_sublist_iff {a : α} {l l'} : @@ -435,7 +439,7 @@ theorem cons_sublist_iff {a : α} {l l'} : | cons _ w => obtain ⟨r₁, r₂, rfl, h₁, h₂⟩ := ih.1 w exact ⟨a' :: r₁, r₂, by simp, mem_cons_of_mem a' h₁, h₂⟩ - | cons₂ _ w => + | cons_cons _ w => exact ⟨[a], l', by simp, mem_singleton_self _, w⟩ · rintro ⟨r₁, r₂, w, h₁, h₂⟩ rw [w, ← singleton_append] @@ -458,7 +462,7 @@ theorem sublist_append_iff {l : List α} : | cons _ w => obtain ⟨l₁, l₂, rfl, w₁, w₂⟩ := ih.1 w exact ⟨l₁, l₂, rfl, Sublist.cons r w₁, w₂⟩ - | cons₂ _ w => + | cons_cons _ w => rename_i l obtain ⟨l₁, l₂, rfl, w₁, w₂⟩ := ih.1 w refine ⟨r :: l₁, l₂, by simp, cons_sublist_cons.mpr w₁, w₂⟩ @@ -466,9 +470,9 @@ theorem sublist_append_iff {l : List α} : cases w₁ with | cons _ w₁ => exact Sublist.cons _ (Sublist.append w₁ w₂) - | cons₂ _ w₁ => + | cons_cons _ w₁ => rename_i l - exact Sublist.cons₂ _ (Sublist.append w₁ w₂) + exact Sublist.cons_cons _ (Sublist.append w₁ w₂) theorem append_sublist_iff {l₁ l₂ : List α} : l₁ ++ l₂ <+ r ↔ ∃ r₁ r₂, r = r₁ ++ r₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂ := by @@ -516,7 +520,7 @@ theorem Sublist.middle {l : List α} (h : l <+ l₁ ++ l₂) (a : α) : l <+ l theorem Sublist.reverse : l₁ <+ l₂ → l₁.reverse <+ l₂.reverse | .slnil => Sublist.refl _ | .cons _ h => by rw [reverse_cons]; exact sublist_append_of_sublist_left h.reverse - | .cons₂ _ h => by rw [reverse_cons, reverse_cons]; exact h.reverse.append_right _ + | .cons_cons _ h => by rw [reverse_cons, reverse_cons]; exact h.reverse.append_right _ @[simp, grind =] theorem reverse_sublist : l₁.reverse <+ l₂.reverse ↔ l₁ <+ l₂ := ⟨fun h => l₁.reverse_reverse ▸ l₂.reverse_reverse ▸ h.reverse, Sublist.reverse⟩ @@ -558,7 +562,7 @@ theorem sublist_replicate_iff : l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = re obtain ⟨n, le, rfl⟩ := ih.1 (sublist_of_cons_sublist w) obtain rfl := (mem_replicate.1 (mem_of_cons_sublist w)).2 exact ⟨n+1, Nat.add_le_add_right le 1, rfl⟩ - | cons₂ _ w => + | cons_cons _ w => obtain ⟨n, le, rfl⟩ := ih.1 w refine ⟨n+1, Nat.add_le_add_right le 1, by simp [replicate_succ]⟩ · rintro ⟨n, le, w⟩ @@ -644,7 +648,7 @@ theorem flatten_sublist_iff {L : List (List α)} {l} : cases h_sub case cons h_sub => exact isSublist_iff_sublist.mpr h_sub - case cons₂ => + case cons_cons => contradiction instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+ l₂) := diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index 94d90cf152..57b1a9d47e 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean @@ -393,7 +393,7 @@ theorem isPrefixOfAux_toArray_zero [BEq α] (l₁ l₂ : List α) (hle : l₁.le | [], _ => rw [dif_neg] <;> simp | _::_, [] => simp at hle | a::l₁, b::l₂ => - simp [isPrefixOf_cons₂, isPrefixOfAux_toArray_succ', isPrefixOfAux_toArray_zero] + simp [isPrefixOf_cons_cons, isPrefixOfAux_toArray_succ', isPrefixOfAux_toArray_zero] @[simp, grind =] theorem isPrefixOf_toArray [BEq α] (l₁ l₂ : List α) : l₁.toArray.isPrefixOf l₂.toArray = l₁.isPrefixOf l₂ := by @@ -407,7 +407,7 @@ theorem isPrefixOfAux_toArray_zero [BEq α] (l₁ l₂ : List α) (hle : l₁.le cases l₂ with | nil => simp | cons b l₂ => - simp only [isPrefixOf_cons₂, Bool.and_eq_false_imp] + simp only [isPrefixOf_cons_cons, Bool.and_eq_false_imp] intro w rw [ih] simp_all diff --git a/src/Init/Omega/IntList.lean b/src/Init/Omega/IntList.lean index 868bfbc88b..437f0afaa2 100644 --- a/src/Init/Omega/IntList.lean +++ b/src/Init/Omega/IntList.lean @@ -144,7 +144,10 @@ theorem mul_def (xs ys : IntList) : xs * ys = List.zipWith (· * ·) xs ys := @[simp] theorem mul_nil_left : ([] : IntList) * ys = [] := rfl @[simp] theorem mul_nil_right : xs * ([] : IntList) = [] := List.zipWith_nil_right -@[simp] theorem mul_cons₂ : (x::xs : IntList) * (y::ys) = (x * y) :: (xs * ys) := rfl +@[simp] theorem mul_cons_cons : (x::xs : IntList) * (y::ys) = (x * y) :: (xs * ys) := rfl + +@[deprecated mul_cons_cons (since := "2026-02-26")] +theorem mul_cons₂ : (x::xs : IntList) * (y::ys) = (x * y) :: (xs * ys) := mul_cons_cons /-- Implementation of negation on `IntList`. -/ def neg (xs : IntList) : IntList := xs.map fun x => -x @@ -278,7 +281,10 @@ example : IntList.dot [a, b, c] [x, y, z] = IntList.dot [a, b, c] [x, y, z, w] : @[local simp] theorem dot_nil_left : dot ([] : IntList) ys = 0 := rfl @[simp] theorem dot_nil_right : dot xs ([] : IntList) = 0 := by simp [dot] -@[simp] theorem dot_cons₂ : dot (x::xs) (y::ys) = x * y + dot xs ys := rfl +@[simp] theorem dot_cons_cons : dot (x::xs) (y::ys) = x * y + dot xs ys := rfl + +@[deprecated dot_cons_cons (since := "2026-02-26")] +theorem dot_cons₂ : dot (x::xs) (y::ys) = x * y + dot xs ys := dot_cons_cons -- theorem dot_comm (xs ys : IntList) : dot xs ys = dot ys xs := by -- rw [dot, dot, mul_comm] @@ -296,7 +302,7 @@ example : IntList.dot [a, b, c] [x, y, z] = IntList.dot [a, b, c] [x, y, z, w] : cases ys with | nil => simp | cons y ys => - simp only [set_cons_zero, dot_cons₂, get_cons_zero, Int.sub_mul] + simp only [set_cons_zero, dot_cons_cons, get_cons_zero, Int.sub_mul] rw [Int.add_right_comm, Int.add_comm (x * y), Int.sub_add_cancel] | succ i => cases ys with @@ -319,7 +325,7 @@ theorem dot_of_left_zero (w : ∀ x, x ∈ xs → x = 0) : dot xs ys = 0 := by cases ys with | nil => simp | cons y ys => - rw [dot_cons₂, w x (by simp [List.mem_cons_self]), ih] + rw [dot_cons_cons, w x (by simp [List.mem_cons_self]), ih] · simp · intro x m apply w @@ -400,7 +406,7 @@ attribute [simp] Int.zero_dvd cases ys with | nil => simp | cons y ys => - rw [dot_cons₂, Int.add_emod, + rw [dot_cons_cons, Int.add_emod, ← Int.emod_emod_of_dvd (x * y) (gcd_cons_div_left), ← Int.emod_emod_of_dvd (dot xs ys) (Int.ofNat_dvd.mpr gcd_cons_div_right)] simp_all @@ -415,7 +421,7 @@ theorem dot_eq_zero_of_left_eq_zero {xs ys : IntList} (h : ∀ x, x ∈ xs → x cases ys with | nil => rfl | cons y ys => - rw [dot_cons₂, h x List.mem_cons_self, ih (fun x m => h x (List.mem_cons_of_mem _ m)), + rw [dot_cons_cons, h x List.mem_cons_self, ih (fun x m => h x (List.mem_cons_of_mem _ m)), Int.zero_mul, Int.add_zero] @[simp] theorem nil_dot (xs : IntList) : dot [] xs = 0 := rfl @@ -456,7 +462,7 @@ theorem dvd_bmod_dot_sub_dot_bmod (m : Nat) (xs ys : IntList) : cases ys with | nil => simp | cons y ys => - simp only [IntList.dot_cons₂, List.map_cons] + simp only [IntList.dot_cons_cons, List.map_cons] specialize ih ys rw [Int.sub_emod, Int.bmod_emod] at ih rw [Int.sub_emod, Int.bmod_emod, Int.add_emod, Int.add_emod (Int.bmod x m * y), diff --git a/tests/elab/list_simp.lean b/tests/elab/list_simp.lean index 8a2ff2a6f7..3159fe1ee0 100644 --- a/tests/elab/list_simp.lean +++ b/tests/elab/list_simp.lean @@ -229,7 +229,7 @@ variable (h : ¬ n = 0) in -- It would be nice if this also worked with `h : 0 < variable [BEq α] [LawfulBEq α] in #check_simp isPrefixOf [x, y, x] (replicate n x) ~> decide (3 ≤ n) && y == x -attribute [local simp] isPrefixOf_cons₂ in +attribute [local simp] isPrefixOf_cons_cons in variable [BEq α] [LawfulBEq α] in #check_simp isPrefixOf [x, y, x] (replicate (n+3) x) ~> y == x diff --git a/tests/lean/grind/experiments/list.lean b/tests/lean/grind/experiments/list.lean index 67605781ae..689387e516 100644 --- a/tests/lean/grind/experiments/list.lean +++ b/tests/lean/grind/experiments/list.lean @@ -864,7 +864,7 @@ theorem dropLast_concat_getLast : ∀ {l : List α} (h : l ≠ []), dropLast l + | [], h => absurd rfl h | [_], _ => rfl | _ :: b :: l, _ => by - rw [dropLast_cons₂, cons_append, getLast_cons (cons_ne_nil _ _)] + rw [dropLast_cons_cons, cons_append, getLast_cons (cons_ne_nil _ _)] congr exact dropLast_concat_getLast (cons_ne_nil b l)