max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: prefer cons_cons over cons₂ in names (#12710)

Browse source 
This PR deprecated the handful of names in core involving the component
`cons₂` in favor of `cons_cons`.
This commit is contained in:
Markus Himmel 2026-02-27 09:58:08 +01:00 • committed by GitHub
parent b1db0d2798
commit 9bd4dfb696
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
16 changed files with 100 additions and 68 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
src/Init/Data/List/Basic.lean
View file

@ -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

2
src/Init/Data/List/Erase.lean
View file

@ -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

4
src/Init/Data/List/Find.lean
View file

@ -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

4
src/Init/Data/List/Lemmas.lean
View file

@ -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)

2
src/Init/Data/List/Nat/BEq.lean
View file

@ -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

2
src/Init/Data/List/Nat/Count.lean
View file

@ -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

4
src/Init/Data/List/Nat/Pairwise.lean
View file

@ -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

2
src/Init/Data/List/Nat/TakeDrop.lean
View file

@ -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

4
src/Init/Data/List/Pairwise.lean
View file

@ -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

10
src/Init/Data/List/Perm.lean
View file

@ -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⟩

4
src/Init/Data/List/Sort/Lemmas.lean
View file

@ -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₃))))

66
src/Init/Data/List/Sublist.lean
View file

@ -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₂) :=

4
src/Init/Data/List/ToArray.lean
View file

@ -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

20
src/Init/Omega/IntList.lean
View file

@ -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),

2
tests/elab/list_simp.lean
View file

@ -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

2
tests/lean/grind/experiments/list.lean
View file

@ -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)