feat(tactic/lint): add linter for simp lemmas whose lhs has a variabl…

…e as head symbol (#2038)

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

docs/commands.md

@@ -117,6 +117,7 @@ The following linters are run by default:
 10. `dangerous_instance` checks for instances that generate type-class problems with metavariables.
 11. `inhabited_nonempty` checks for `inhabited` instance arguments that should be changed to `nonempty`.
 12. `simp_nf` checks that arguments of the left-hand side of simp lemmas are in simp-normal form.
+13. `simp_var_head` checks that there are no variables as head symbol of left-hand sides of simp lemmas.
 
 Another linter, `doc_blame_thm`, checks for missing doc strings on lemmas and theorems.
 This is not run by default.

src/algebra/field.lean

@@ -276,9 +276,9 @@ section
 variables {β : Type*} [discrete_field α] [discrete_field β]
 variables (f : α → β) [is_ring_hom f] {x y : α}
 
-@[simp] lemma map_inv : f x⁻¹ = (f x)⁻¹ := (of f).map_inv
+lemma map_inv : f x⁻¹ = (f x)⁻¹ := (of f).map_inv
 
-@[simp] lemma map_div : f (x / y) = f x / f y := (of f).map_div
+lemma map_div : f (x / y) = f x / f y := (of f).map_div
 
 end
 

src/algebra/module.lean

@@ -245,16 +245,16 @@ end
 variables {f : β → γ} (lin : is_linear_map α f)
 include β γ lin
 
-@[simp] lemma map_zero : f (0 : β) = (0 : γ) :=
+lemma map_zero : f (0 : β) = (0 : γ) :=
 by rw [← zero_smul α (0 : β), lin.smul, zero_smul]
 
-@[simp] lemma map_add (x y : β) : f (x + y) = f x + f y :=
+lemma map_add (x y : β) : f (x + y) = f x + f y :=
 by rw [lin.add]
 
-@[simp] lemma map_neg (x : β) : f (- x) = - f x :=
+lemma map_neg (x : β) : f (- x) = - f x :=
 by rw [← neg_one_smul α, lin.smul, neg_one_smul]
 
-@[simp] lemma map_sub (x y : β) : f (x - y) = f x - f y :=
+lemma map_sub (x y : β) : f (x - y) = f x - f y :=
 by simp [lin.map_neg, lin.map_add]
 
 end is_linear_map
@@ -497,4 +497,3 @@ theorem exists_card_smul_ge_sum (hs : s.nonempty) :
 exists_le_of_sum_le hs $ by rw [sum_const, ← nat.smul_def, smul_sum]
 
 end finset
-

src/data/list/basic.lean

@@ -1818,7 +1818,7 @@ begin
   { rwa [find_cons_of_neg _ h, iff_true_intro h, true_and] }
 end
 
-@[simp] theorem find_some (H : find p l = some a) : p a :=
+theorem find_some (H : find p l = some a) : p a :=
 begin
   induction l with b l IH, {contradiction},
   by_cases h : p b,

src/tactic/lint.lean

@@ -26,6 +26,7 @@ The following linters are run by default:
 10. `dangerous_instance` checks for instances that generate type-class problems with metavariables.
 11. `inhabited_nonempty` checks for `inhabited` instance arguments that should be changed to `nonempty`.
 12. `simp_nf` checks that arguments of the left-hand side of simp lemmas are in simp-normal form.
+13. `simp_var_head` checks that there are no variables as head symbol of left-hand sides of simp lemmas.
 
 Another linter, `doc_blame_thm`, checks for missing doc strings on lemmas and theorems.
 This is not run by default.
@@ -511,6 +512,27 @@ some <$> do
   errors_found := "LEFT-HAND SIDE NOT IN SIMP-NF.\n" ++
     "Some simp lemmas have a left-hand side that is not in simp-normal form." }
 
+private meta def simp_var_head (d : declaration) : tactic (option string) := do
+tt ← is_simp_lemma d.to_name | pure none,
+-- Sometimes, a definition is tagged @[simp] to add the equational lemmas to the simp set.
+-- In this case, ignore the declaration if it is not a valid simp lemma by itself.
+tt ← is_valid_simp_lemma_cnst d.to_name | pure none,
+lhs ← simp_lhs d.type,
+head_sym@(expr.local_const _ _ _ _) ← pure lhs.get_app_fn | pure none,
+head_sym ← pp head_sym,
+pure $ format.to_string $ "Left-hand side has variable as head symbol: " ++ head_sym
+
+/--
+A linter for simp lemmas whose lhs has a variable as head symbol,
+and which hence never fire.
+-/
+@[linter, priority 1389] meta def linter.simp_var_head : linter :=
+{ test := simp_var_head,
+  no_errors_found :=
+    "No left-hand sides of a simp lemma has a variable as head symbol.",
+  errors_found := "LEFT-HAND SIDE HAS VARIABLE AS HEAD SYMBOL.\n" ++
+    "Some simp lemmas have a variable as head symbol of the left-hand side" }
+
 /- Implementation of the frontend. -/
 
 /-- `get_checks slow extra use_only` produces a list of linters.

test/lint_simp_var_head.lean

@@ -0,0 +1,24 @@
+import tactic.lint
+
+-- The following simp lemma has the variable `f` as head symbol of the left-hand side:
+@[simp] axiom const_zero_eq_zero (f : ℕ → ℕ) (x) : f x = 0
+
+example (f : ℕ → ℕ) : f 42 = 0 :=
+begin
+  -- Hence it doesn't work:
+  success_if_fail {simp},
+
+  -- BTW, rw doesn't work either:
+  success_if_fail {rw const_zero_eq_zero},
+
+  -- It only works if explicitly instantiate with `f`:
+  simp only [const_zero_eq_zero f]
+end
+
+
+open tactic
+#eval do
+decl ← get_decl ``const_zero_eq_zero,
+res ← linter.simp_var_head.test decl,
+-- linter complains
+guard $ res.is_some