[Merged by Bors] - feat: add simp linter

.github/workflows/build.yml

@@ -33,5 +33,8 @@ jobs:
       - name: test mathlib
         run: make test
 
+      - name: lint mathlib
+        run: env LEAN_PATH=build/lib lean scripts/runLinter.lean
+
       - name: check that all files are imported
         run: git diff --exit-code

Mathlib.lean

@@ -42,6 +42,10 @@ import Mathlib.Tactic.Core
 import Mathlib.Tactic.Ext
 import Mathlib.Tactic.Find
 import Mathlib.Tactic.LibrarySearch
+import Mathlib.Tactic.Lint
+import Mathlib.Tactic.Lint.Basic
+import Mathlib.Tactic.Lint.Frontend
+import Mathlib.Tactic.Lint.Simp
 import Mathlib.Tactic.NoMatch
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.OpenPrivate

Mathlib/Algebra/Group/Defs.lean

@@ -222,7 +222,7 @@ theorem neg_add_self (a : A) : -a + a = 0 := add_left_neg a
 @[simp] theorem neg_add_cancel_left (a b : A) : -a + (a + b) = b :=
 by rw [← add_assoc, add_left_neg, zero_add]
 
-@[simp] theorem neg_eq_of_add_eq_zero (h : a + b = 0) : -a = b :=
+theorem neg_eq_of_add_eq_zero (h : a + b = 0) : -a = b :=
 left_neg_eq_right_neg (neg_add_self a) h
 
 @[simp] theorem neg_neg (a : A) : -(-a) = a :=

Mathlib/Data/Equiv/Basic.lean

@@ -36,7 +36,9 @@ namespace equiv
 instance : CoeFun (α ≃ β) (λ _ => α → β):=
 ⟨to_fun⟩
 
-@[simp] theorem coe_fn_mk (f : α → β) (g l r) : (equiv.mk f g l r : α → β) = f :=
+-- Does not need to be simp, since the coercion is the projection,
+-- which simp has built-in support for.
+theorem coe_fn_mk (f : α → β) (g l r) : (equiv.mk f g l r : α → β) = f :=
 rfl
 
 def refl (α) : α ≃ α := ⟨id, id, λ _ => rfl, λ _ => rfl⟩

Mathlib/Data/List/Basic.lean

@@ -139,15 +139,15 @@ def mem (a : α) : List α → Prop
 
 instance : Mem α (List α) := ⟨mem⟩
 
-@[simp] lemma mem_nil (a : α) : a ∈ [] ↔ False := Iff.rfl
+lemma mem_nil (a : α) : a ∈ [] ↔ False := Iff.rfl
 
-@[simp] lemma mem_cons {a b : α} {l : List α} :
+lemma mem_cons {a b : α} {l : List α} :
   a ∈ (b :: l) ↔ a = b ∨ a ∈ l := Iff.rfl
 
-lemma mem_nil_iff (a : α) : a ∈ ([] : List α) ↔ False :=
+@[simp] lemma mem_nil_iff (a : α) : a ∈ ([] : List α) ↔ False :=
 Iff.rfl
 
-@[simp] lemma not_mem_nil (a : α) : a ∉ ([] : List α) :=
+lemma not_mem_nil (a : α) : a ∉ ([] : List α) :=
 not_false
 
 lemma mem_cons_self (a : α) (l : List α) : a ∈ a :: l :=
@@ -220,7 +220,7 @@ fun this : a ∈ [b] => Or.elim
   (fun this : a = b => this)
   (fun this : a ∈ [] => absurd this (not_mem_nil a))
 
-@[simp] theorem mem_singleton {a b : α} : a ∈ [b] ↔ a = b :=
+@[simp 900] theorem mem_singleton {a b : α} : a ∈ [b] ↔ a = b :=
 ⟨eq_of_mem_singleton, Or.inl⟩
 
 theorem mem_of_mem_cons_of_mem {a b : α} {l : List α} : a ∈ b::l → b ∈ l → a ∈ l :=
@@ -400,7 +400,7 @@ theorem ne_nil_of_length_eq_succ {l : List α} : ∀ {n : Nat}, length l = Nat.s
 theorem length_eq_zero {l : List α} : length l = 0 ↔ l = [] :=
 ⟨eq_nil_of_length_eq_zero, fun h => by rw [h]; rfl⟩
 
-@[simp] lemma length_singleton (a : α) : length [a] = 1 := rfl
+@[simp 900] lemma length_singleton (a : α) : length [a] = 1 := rfl
 
 theorem length_pos_of_mem {a : α} : ∀ {l : List α}, a ∈ l → 0 < length l
 | nil,  h => by cases h
@@ -644,31 +644,20 @@ theorem mem_filter (as : List α) (p : α → Bool) (x : α) :
 
 lemma append_eq_has_append {L₁ L₂ : List α} : List.append L₁ L₂ = L₁ ++ L₂ := rfl
 
-@[simp] lemma singleton_append {x : α} {l : List α} : [x] ++ l = x :: l := rfl
+@[simp 900] lemma singleton_append {x : α} {l : List α} : [x] ++ l = x :: l := rfl
 
-theorem append_ne_nil_of_ne_nil_left (s t : List α) : s ≠ [] → s ++ t ≠ [] := by
-  induction s with
-  | nil => intros; contradiction
-  | cons a s ih => rw [cons_append]; intros _ h; contradiction
+@[simp] lemma append_eq_nil {p q : List α} : (p ++ q) = [] ↔ p = [] ∧ q = [] := by
+  cases p <;> simp
 
-theorem append_ne_nil_of_ne_nil_right (s t : List α) : t ≠ [] → s ++ t ≠ [] := by
-  induction s with
-  | nil => intros; rw [nil_append]; assumption
-  | cons a s ih => rw [cons_append]; intros _ h; contradiction
+theorem append_ne_nil_of_ne_nil_left (s t : List α) : s ≠ [] → s ++ t ≠ [] := by simp_all
 
-@[simp] lemma append_eq_nil {p q : List α} : (p ++ q) = [] ↔ p = [] ∧ q = [] := by
-  cases p with
-  | nil => simp
-  | cons a p => simp
+theorem append_ne_nil_of_ne_nil_right (s t : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all
 
 @[simp] lemma nil_eq_append_iff {a b : List α} : [] = a ++ b ↔ a = [] ∧ b = [] :=
 by rw [eq_comm, append_eq_nil]
 
 
-@[simp] lemma append_ne_nil_of_left_ne_nil {A : Type u} (a b : List A) (h0 : a ≠ []) : a ++ b ≠ [] := by
-cases a with
-| nil => exact absurd rfl h0
-| cons h t => simp
+lemma append_ne_nil_of_left_ne_nil (a b : List α) (h0 : a ≠ []) : a ++ b ≠ [] := by simp [*]
 
 -- lemma append_eq_cons_iff {a b c : List α} {x : α} :
 --   a ++ b = x :: c ↔ (a = [] ∧ b = x :: c) ∨ (∃a', a = x :: a' ∧ c = a' ++ b) := by
@@ -779,7 +768,7 @@ cases a with
 | 0 => []
 | Nat.succ n => a :: repeat a n
 
-@[simp] def repeatSucc (a: α) (n: ℕ): repeat a (n + 1) = a :: repeat a n := rfl
+theorem repeatSucc (a: α) (n: ℕ) : repeat a (n + 1) = a :: repeat a n := rfl
 theorem exists_of_mem_bind {b : β} {l : List α} {f : α → List β} :
   b ∈ List.bind l f → ∃ a, a ∈ l ∧ b ∈ f a :=
 mem_bind.1
@@ -813,7 +802,7 @@ def insert (a : α) (l : List α) := if a ∈ l then l else a :: l
   focus
     rw [insert_of_not_mem h]; rfl
 
-@[simp] theorem mem_insert_self (a : α) (l : List α) : a ∈ insert a l :=
+@[simp 900] theorem mem_insert_self (a : α) (l : List α) : a ∈ insert a l :=
 mem_insert_iff.2 (Or.inl rfl)
 
 theorem mem_insert_of_mem {a b : α} {l : List α} (h : a ∈ l) : a ∈ insert b l :=
@@ -999,7 +988,6 @@ theorem erase_eq_erasep (a : α) (l : List α) : l.erase a = l.erasep (Eq a) :=
         simp [h]
       simp [h, Ne.symm h, ih]
 
-@[simp]
 theorem erase_of_not_mem {a : α} {l : List α} (h : a ∉ l) : l.erase a = l := by
   induction l with
     | nil => rfl

Mathlib/Data/Nat/Basic.lean

@@ -28,10 +28,10 @@ protected lemma le_or_le (a b : ℕ) : a ≤ b ∨ b ≤ a := (Nat.lt_or_ge _ _)
 
 protected lemma le_of_not_le {a b : ℕ} : ¬ a ≤ b → b ≤ a := (Nat.le_or_le _ _).resolve_left
 
-@[simp] protected lemma not_lt {n m : ℕ} : ¬ n < m ↔ m ≤ n :=
+protected lemma not_lt {n m : ℕ} : ¬ n < m ↔ m ≤ n :=
 ⟨Nat.le_of_not_lt, Nat.not_lt_of_le⟩
 
-@[simp] protected lemma not_le {n m : ℕ} : ¬ n ≤ m ↔ m < n :=
+protected lemma not_le {n m : ℕ} : ¬ n ≤ m ↔ m < n :=
 ⟨Nat.lt_of_not_le, Nat.not_le_of_lt⟩
 
 protected lemma lt_or_eq_of_le {n m : ℕ} (h : n ≤ m) : n < m ∨ n = m :=

Mathlib/Data/Prod.lean

@@ -17,10 +17,8 @@ This file defines `Prod.swap : α × β → β × α` and proves various simple
 
 variable {α : Type _} {β : Type _} {γ : Type _} {δ : Type _}
 
-@[simp] lemma prod_map (f : α → γ) (g : β → δ) (p : α × β) : Prod.map f g p = (f p.1, g p.2) :=
-by have : p = ⟨p.1, p.2⟩ := (Prod.ext _).symm
-   rw [this]
-   exact rfl
+@[simp] lemma prod_map (f : α → γ) (g : β → δ) (p : α × β) : Prod.map f g p = (f p.1, g p.2) := by
+  cases p; rfl
 
 namespace Prod
 
@@ -36,12 +34,10 @@ Prod.forall
 theorem exists' {p : α → β → Prop} : (∃ x : α × β, p x.1 x.2) ↔ ∃ a b, p a b :=
 Prod.exists
 
-@[simp] lemma map_mk (f : α → γ) (g : β → δ) (a : α) (b : β) : map f g (a, b) = (f a, g b) := rfl
+lemma map_mk (f : α → γ) (g : β → δ) (a : α) (b : β) : map f g (a, b) = (f a, g b) := rfl
 
-@[simp]
 lemma map_fst (f : α → γ) (g : β → δ) (p : α × β) : (map f g p).1 = f (p.1) := by simp
 
-@[simp]
 lemma map_snd (f : α → γ) (g : β → δ) (p : α × β) : (map f g p).2 = g (p.2) := by simp
 
 lemma map_fst' (f : α → γ) (g : β → δ) : (Prod.fst ∘ map f g) = f ∘ Prod.fst :=
@@ -67,7 +63,7 @@ lemma map_map {ε ζ : Type _}
   (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ → ζ) (x : α × γ) :
   Prod.map g g' (Prod.map f f' x) = Prod.map (g ∘ f) (g' ∘ f') x := by simp
 
-@[simp] theorem mk.inj_iff {a₁ a₂ : α} {b₁ b₂ : β} : (a₁, b₁) = (a₂, b₂) ↔ (a₁ = a₂ ∧ b₁ = b₂) :=
+theorem mk.inj_iff {a₁ a₂ : α} {b₁ b₂ : β} : (a₁, b₁) = (a₂, b₂) ↔ (a₁ = a₂ ∧ b₁ = b₂) :=
 ⟨Prod.mk.inj,
  by intro hab; rw [hab.left, hab.right]⟩
 
@@ -125,10 +121,10 @@ def swap : α × β → β × α := λp => (p.2, p.1)
 @[simp] lemma swap_swap_eq : swap ∘ swap = @id (α × β) :=
 funext swap_swap
 
-@[simp] lemma swap_left_inverse : Function.left_inverse (@swap α β) swap :=
+lemma swap_left_inverse : Function.left_inverse (@swap α β) swap :=
 swap_swap
 
-@[simp] lemma swap_right_inverse : Function.right_inverse (@swap α β) swap :=
+lemma swap_right_inverse : Function.right_inverse (@swap α β) swap :=
 swap_swap
 
 lemma swap_injective : Function.injective (@swap α β) :=

Mathlib/Data/String/Lemmas.lean

@@ -3,8 +3,8 @@ import Mathlib.Data.String.Defs
 
 namespace String
 
-@[simp] lemma congr_append : ∀ (a b : String), a ++ b = String.mk (a.data ++ b.data)
-| ⟨a⟩, ⟨b⟩ => by simp only [HAppend.hAppend, Append.append, String.append]
+lemma congr_append : ∀ (a b : String), a ++ b = String.mk (a.data ++ b.data)
+| ⟨a⟩, ⟨b⟩ => rfl
 
 @[simp] lemma length_append : ∀ (as bs : String), (as ++ bs).length = as.length + bs.length
 | ⟨as⟩, ⟨bs⟩ => by

Mathlib/Data/Subtype.lean

@@ -62,9 +62,8 @@ ext_iff
 
 @[simp] theorem coe_eta (a : {a // p a}) (h : p (a : α)) : mk (a : α) h = a := Subtype.ext rfl
 
-@[simp] theorem coe_mk (a h) : (@mk α p a h : α) = a := rfl
+theorem coe_mk (a h) : (@mk α p a h : α) = a := rfl
 
-@[simp]
 theorem mk_eq_mk {a h a' h'} : @mk α p a h = @mk α p a' h' ↔ a = a' :=
 ext_iff
 
@@ -171,6 +170,7 @@ namespace Subtype
 /-! Some facts about sets, which require that `α` is a type. -/
 variable {α : Type _} {β : Type _} {γ : Type _} {p : α → Prop}
 
-@[simp] lemma val_prop {S : Set α} (a : {a // a ∈ S}) : a.val ∈ S := a.property
+-- ∈-notation is reducible in Lean 4, so this won't trigger as a simp-lemma
+lemma val_prop {S : Set α} (a : {a // a ∈ S}) : a.val ∈ S := a.property
 
 end Subtype

Mathlib/Init/Data/Nat/Basic.lean

@@ -14,7 +14,4 @@ namespace Nat
 instance : Dvd ℕ where
   dvd a b := ∃ c, b = a * c
 
-@[simp] lemma nat_zero_eq_zero : Nat.zero = 0 :=
-rfl
-
 end Nat

Mathlib/Init/Logic.lean

@@ -14,7 +14,7 @@ import Mathlib.Tactic.Ext
 @[ext] protected lemma Unit.ext (x y : Unit) : x = y := Subsingleton.allEq _ _
 @[ext] protected lemma PUnit.ext (x y : Unit) : x = y := Subsingleton.allEq _ _
 
-@[simp] theorem opt_param_eq (α : Sort u) (default : α) : optParam α default = α := optParam_eq α default
+theorem opt_param_eq (α : Sort u) (default : α) : optParam α default = α := optParam_eq α default
 
 theorem Not.intro {a : Prop} (h : a → False) : ¬ a := h
 
@@ -45,7 +45,7 @@ lemma cast_proof_irrel (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂
 
 /- ne -/
 
-@[simp] lemma Ne.def {α : Sort u} (a b : α) : (a ≠ b) = ¬ (a = b) := rfl
+lemma Ne.def {α : Sort u} (a b : α) : (a ≠ b) = ¬ (a = b) := rfl
 
 def eq_rec_heq := @eqRec_heq
 
@@ -132,17 +132,19 @@ lemma imp_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a → b) ↔ (c → d) := i
 lemma not_of_not_not_not (h : ¬¬¬a) : ¬a :=
 λ ha => absurd (not_not_intro ha) h
 
-@[simp] lemma not_true : (¬ True) ↔ False :=
+-- @[simp] -- Lean 4 has this built-in because it simplifies using decidable instances
+lemma not_true : (¬ True) ↔ False :=
 iff_false_intro (not_not_intro trivial)
 
-@[simp] lemma not_false_iff : (¬ False) ↔ True :=
+-- @[simp] -- Lean 4 has this built-in because it simplifies using decidable instances
+lemma not_false_iff : (¬ False) ↔ True :=
 iff_true_intro not_false
 
 lemma not_congr (h : a ↔ b) : ¬a ↔ ¬b := ⟨mt h.2, mt h.1⟩
 
 lemma ne_self_iff_false (a : α) : a ≠ a ↔ False := not_iff_false_intro rfl
 
-@[simp] lemma eq_self_iff_true (a : α) : a = a ↔ True := iff_true_intro rfl
+lemma eq_self_iff_true (a : α) : a = a ↔ True := iff_true_intro rfl
 
 lemma heq_self_iff_true (a : α) : HEq a a ↔ True := iff_true_intro HEq.rfl
 

Mathlib/Logic/Basic.lean

@@ -400,7 +400,6 @@ theorem iff_false_left (ha : ¬a) : (a ↔ b) ↔ ¬b :=
 theorem iff_false_right (ha : ¬a) : (b ↔ a) ↔ ¬b :=
 Iff.comm.trans (iff_false_left ha)
 
-@[simp]
 lemma iff_mpr_iff_true_intro {P : Prop} (h : P) : Iff.mpr (iff_true_intro h) True.intro = h := rfl
 
 -- See Note [decidable namespace]

Mathlib/Logic/Function/Basic.lean

@@ -7,6 +7,7 @@ import Mathlib.Logic.Basic
 import Mathlib.Init.Function
 import Mathlib.Init.Set
 import Mathlib.Init.SetNotation
+import Mathlib.Tactic.Lint.Basic
 
 universe u v w
 
@@ -26,7 +27,7 @@ lemma comp_apply {α : Sort u} {β : Sort v} {φ : Sort w} (f : β → φ) (g :
 
 lemma const_def {y : β} : (λ x : α => y) = const α y := rfl
 
-@[simp] lemma const_apply {y : β} {x : α} : const α y x = y := rfl
+@[simp, nolint simpNF] lemma const_apply {y : β} {x : α} : const α y x = y := rfl
 
 @[simp] lemma const_comp {f : α → β} {c : γ} : const β c ∘ f = const α c := rfl
 

Mathlib/Mathport/Attributes.lean

@@ -12,8 +12,5 @@ initialize symmAttr : TagAttribute ← registerTagAttribute `symm "symmetric rel
 initialize transAttr : TagAttribute ← registerTagAttribute `trans "transitive relation"
 initialize substAttr : TagAttribute ← registerTagAttribute `subst "substitution"
 
-initialize linterAttr : TagAttribute ←
-  registerTagAttribute `linter "Use this declaration as a linting test in #lint"
-
 initialize hintTacticAttr : TagAttribute ←
   registerTagAttribute `hintTactic "A tactic that should be tried by `hint`."

Mathlib/Mathport/Syntax.lean

@@ -641,8 +641,6 @@ namespace Attr
 syntax (name := intro) "intro" : attr
 syntax (name := intro!) "intro!" : attr
 
-syntax (name := nolint) "nolint" (ppSpace ident)* : attr
-
 syntax (name := ext) "ext" (ppSpace ident)? : attr
 
 syntax (name := higherOrder) "higherOrder" (ppSpace ident)? : attr
@@ -686,11 +684,6 @@ syntax args := opts " only"? ident*
 
 end Lint
 
-syntax (name := lint) "#lint" Lint.args : command
-syntax (name := lintMathlib) "#lint_mathlib" Lint.args : command
-syntax (name := lintAll) "#lint_all" Lint.args : command
-syntax (name := listLinters) "#list_linters" : command
-
 syntax (name := copyDocString) "copy_doc_string " ident " → " ident* : command
 syntax (name := libraryNote) docComment "library_note " str : command
 syntax (name := addTacticDoc) (docComment)? "add_tactic_doc " term : command

Mathlib/Tactic/Lint.lean

@@ -0,0 +1,2 @@
+import Mathlib.Tactic.Lint.Simp
+import Mathlib.Tactic.Lint.Frontend