feat(tactic/lint): linter for commutativity lemmas that are marked si…

…mp (#2045)

* feat(tactic/lint): linter for commutativity lemmas that are marked simp

* chore(*): remove simp from commutativity lemmas

* doc(*): document simp_comm linter

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

docs/commands.md

@@ -118,6 +118,7 @@ The following linters are run by default:
 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.
+14. `simp_comm` checks that no commutativity lemmas (such as `add_comm`) are marked simp.
 
 Another linter, `doc_blame_thm`, checks for missing doc strings on lemmas and theorems.
 This is not run by default.

src/data/finmap.lean

@@ -231,8 +231,8 @@ induction_on s $ lookup_erase a
   lookup a (erase a' s) = lookup a s :=
 induction_on s $ λ s, lookup_erase_ne h
 
-@[simp] theorem erase_erase {a a' : α} {s : finmap β} : erase a (erase a' s) = erase a' (erase a s) :=
-induction_on s $ λ s, ext (by simp)
+theorem erase_erase {a a' : α} {s : finmap β} : erase a (erase a' s) = erase a' (erase a s) :=
+induction_on s $ λ s, ext (by simp [alist.erase_erase])
 
 lemma mem_iff {a : α} {s : finmap β} : a ∈ s ↔ ∃ b, s.lookup a = some b :=
 induction_on s $ λ s,

src/data/finset.lean

@@ -325,7 +325,7 @@ theorem subset_union_left (s₁ s₂ : finset α) : s₁ ⊆ s₁ ∪ s₂ := λ
 
 theorem subset_union_right (s₁ s₂ : finset α) : s₂ ⊆ s₁ ∪ s₂ := λ x, mem_union_right _
 
-@[simp] theorem union_comm (s₁ s₂ : finset α) : s₁ ∪ s₂ = s₂ ∪ s₁ :=
+theorem union_comm (s₁ s₂ : finset α) : s₁ ∪ s₂ = s₂ ∪ s₁ :=
 ext.2 $ λ x, by simp only [mem_union, or_comm]
 
 instance : is_commutative (finset α) (∪) := ⟨union_comm⟩
@@ -400,16 +400,16 @@ by rw [← coe_inj, coe_inter, coe_union, set.union_inter_cancel_left]
 @[simp] theorem union_inter_cancel_right {s t : finset α} : (s ∪ t) ∩ t = t :=
 by rw [← coe_inj, coe_inter, coe_union, set.union_inter_cancel_right]
 
-@[simp] theorem inter_comm (s₁ s₂ : finset α) : s₁ ∩ s₂ = s₂ ∩ s₁ :=
+theorem inter_comm (s₁ s₂ : finset α) : s₁ ∩ s₂ = s₂ ∩ s₁ :=
 ext.2 $ λ _, by simp only [mem_inter, and_comm]
 
 @[simp] theorem inter_assoc (s₁ s₂ s₃ : finset α) : (s₁ ∩ s₂) ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) :=
 ext.2 $ λ _, by simp only [mem_inter, and_assoc]
 
-@[simp] theorem inter_left_comm (s₁ s₂ s₃ : finset α) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) :=
+theorem inter_left_comm (s₁ s₂ s₃ : finset α) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) :=
 ext.2 $ λ _, by simp only [mem_inter, and.left_comm]
 
-@[simp] theorem inter_right_comm (s₁ s₂ s₃ : finset α) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ :=
+theorem inter_right_comm (s₁ s₂ s₃ : finset α) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ :=
 ext.2 $ λ _, by simp only [mem_inter, and.right_comm]
 
 @[simp] theorem inter_self (s : finset α) : s ∩ s = s :=
@@ -1379,11 +1379,15 @@ show (insert a ∅ : finset α).bind t = t a, from bind_insert.trans $ union_emp
 
 theorem bind_inter (s : finset α) (f : α → finset β) (t : finset β) :
   s.bind f ∩ t = s.bind (λ x, f x ∩ t) :=
-by { ext x, simp, exact ⟨λ ⟨xt, y, ys, xf⟩, ⟨y, ys, xt, xf⟩, λ ⟨y, ys, xt, xf⟩, ⟨xt, y, ys, xf⟩⟩ }
+begin
+  ext x,
+  simp only [mem_bind, mem_inter],
+  tauto
+end
 
 theorem inter_bind (t : finset β) (s : finset α) (f : α → finset β) :
   t ∩ s.bind f = s.bind (λ x, t ∩ f x) :=
-by rw [inter_comm, bind_inter]; simp
+by rw [inter_comm, bind_inter]; simp [inter_comm]
 
 theorem image_bind [decidable_eq γ] {f : α → β} {s : finset α} {t : β → finset γ} :
   (s.image f).bind t = s.bind (λa, t (f a)) :=

src/data/hash_map.lean

@@ -308,7 +308,7 @@ begin
   rcases hash_map.valid.erase_aux a (array.read bkts (mk_idx n (hash_fn a)))
     ((contains_aux_iff nd).1 Hc) with ⟨u, w, b, hl, hfl⟩,
   refine (v.modify hash_fn u [⟨a, b⟩] [] w hl hfl list.nodup_nil _ _ _).2;
-  { intros, simp at *; contradiction }
+  simp
 end
 
 end

src/data/list/alist.lean

@@ -147,7 +147,7 @@ lookup_kerase a s.nodupkeys
   lookup a (erase a' s) = lookup a s :=
 lookup_kerase_ne h
 
-@[simp] theorem erase_erase (a a' : α) (s : alist β) :
+theorem erase_erase (a a' : α) (s : alist β) :
   (s.erase a).erase a' = (s.erase a').erase a :=
 ext $ kerase_kerase
 

src/data/list/basic.lean

@@ -3401,7 +3401,7 @@ section disjoint
 theorem disjoint.symm {l₁ l₂ : list α} (d : disjoint l₁ l₂) : disjoint l₂ l₁
 | a i₂ i₁ := d i₁ i₂
 
-@[simp] theorem disjoint_comm {l₁ l₂ : list α} : disjoint l₁ l₂ ↔ disjoint l₂ l₁ :=
+theorem disjoint_comm {l₁ l₂ : list α} : disjoint l₁ l₂ ↔ disjoint l₂ l₁ :=
 ⟨disjoint.symm, disjoint.symm⟩
 
 theorem disjoint_left {l₁ l₂ : list α} : disjoint l₁ l₂ ↔ ∀ {a}, a ∈ l₁ → a ∉ l₂ := iff.rfl
@@ -3427,6 +3427,9 @@ disjoint_of_subset_right (list.subset_cons _ _)
 @[simp] theorem disjoint_nil_left (l : list α) : disjoint [] l
 | a := (not_mem_nil a).elim
 
+@[simp] theorem disjoint_nil_right (l : list α) : disjoint l [] :=
+by rw disjoint_comm; exact disjoint_nil_left _
+
 @[simp] theorem singleton_disjoint {l : list α} {a : α} : disjoint [a] l ↔ a ∉ l :=
 by simp only [disjoint, mem_singleton, forall_eq]; refl
 

src/data/multiset.lean

@@ -2142,7 +2142,7 @@ def disjoint (s t : multiset α) : Prop := ∀ ⦃a⦄, a ∈ s → a ∈ t →
 theorem disjoint.symm {s t : multiset α} (d : disjoint s t) : disjoint t s
 | a i₂ i₁ := d i₁ i₂
 
-@[simp] theorem disjoint_comm {s t : multiset α} : disjoint s t ↔ disjoint t s :=
+theorem disjoint_comm {s t : multiset α} : disjoint s t ↔ disjoint t s :=
 ⟨disjoint.symm, disjoint.symm⟩
 
 theorem disjoint_left {s t : multiset α} : disjoint s t ↔ ∀ {a}, a ∈ s → a ∉ t := iff.rfl
@@ -2180,15 +2180,15 @@ by simp [disjoint, or_imp_distrib, forall_and_distrib]
 
 @[simp] theorem disjoint_add_right {s t u : multiset α} :
   disjoint s (t + u) ↔ disjoint s t ∧ disjoint s u :=
-disjoint_comm.trans $ by simp [disjoint_append_left]
+by rw [disjoint_comm, disjoint_add_left]; tauto
 
 @[simp] theorem disjoint_cons_left {a : α} {s t : multiset α} :
   disjoint (a::s) t ↔ a ∉ t ∧ disjoint s t :=
 (@disjoint_add_left _ (a::0) s t).trans $ by simp
 
 @[simp] theorem disjoint_cons_right {a : α} {s t : multiset α} :
   disjoint s (a::t) ↔ a ∉ s ∧ disjoint s t :=
-disjoint_comm.trans $ by simp [disjoint_cons_left]
+by rw [disjoint_comm, disjoint_cons_left]; tauto
 
 theorem inter_eq_zero_iff_disjoint [decidable_eq α] {s t : multiset α} : s ∩ t = 0 ↔ disjoint s t :=
 by rw ← subset_zero; simp [subset_iff, disjoint]
@@ -2543,7 +2543,7 @@ iff.trans (by simp [disjoint]) disjoint_cons_left
 
 @[simp] theorem disjoint_ndinsert_right {a : α} {s t : multiset α} :
   disjoint s (ndinsert a t) ↔ a ∉ s ∧ disjoint s t :=
-disjoint_comm.trans $ by simp
+by rw [disjoint_comm, disjoint_ndinsert_left]; tauto
 
 /- finset union -/
 

src/data/nat/dist.lean

@@ -16,7 +16,7 @@ def dist (n m : ℕ) := (n - m) + (m - n)
 
 theorem dist.def (n m : ℕ) : dist n m = (n - m) + (m - n) := rfl
 
-@[simp] theorem dist_comm (n m : ℕ) : dist n m = dist m n :=
+theorem dist_comm (n m : ℕ) : dist n m = dist m n :=
 by simp [dist.def]
 
 @[simp] theorem dist_self (n : ℕ) : dist n n = 0 :=

src/linear_algebra/basis.lean

@@ -1085,7 +1085,7 @@ assume t, finset.induction_on t
           by rw [span_insert_eq_span hb₁] at hb₃; simpa using hb₃,
         let ⟨u, hust, hsu, eq⟩ := ih _ (by simp [insert_subset, hb₂s, hs']) hst this in
         ⟨u, subset.trans hust $ union_subset_union (subset.refl _) (by simp [subset_insert]),
-          hsu, by rw [finset.union_comm] at hb₂t'; simp [eq, hb₂t', hb₁t, hb₁s']⟩)),
+          hsu, by simp [eq, hb₂t', hb₁t, hb₁s']⟩)),
 begin
   letI := classical.dec_pred (λx, x ∈ s),
   have eq : t.filter (λx, x ∈ s) ∪ t.filter (λx, x ∉ s) = t,

src/tactic/lint.lean

@@ -27,6 +27,7 @@ The following linters are run by default:
 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.
+14. `simp_comm` checks that no commutativity lemmas (such as `add_comm`) are marked simp.
 
 Another linter, `doc_blame_thm`, checks for missing doc strings on lemmas and theorems.
 This is not run by default.
@@ -447,22 +448,26 @@ do tt ← is_prop d.type | return none,
   no_errors_found := "No uses of `inhabited` arguments should be replaced with `nonempty`",
   errors_found := "USES OF `inhabited` SHOULD BE REPLACED WITH `nonempty`." }
 
-/-- `simp_lhs ty` returns the left-hand side of a simp lemma with type `ty`. -/
-private meta def simp_lhs : expr → tactic expr | ty := do
+/-- `simp_lhs_rhs ty` returns the left-hand and right-hand sides of a simp lemma with type `ty`. -/
+private meta def simp_lhs_rhs : expr → tactic (expr × expr) | ty := do
 ty ← whnf ty transparency.reducible,
 -- We only detect a fixed set of simp relations here.
 -- This is somewhat justified since for a custom simp relation R,
 -- the simp lemma `R a b` is implicitly converted to `R a b ↔ true` as well.
 match ty with
-| `(¬ %%lhs) := pure lhs
-| `(%%lhs = _) := pure lhs
-| `(%%lhs ↔ _) := pure lhs
+| `(¬ %%lhs) := pure (lhs, `(false))
+| `(%%lhs = %%rhs) := pure (lhs, rhs)
+| `(%%lhs ↔ %%rhs) := pure (lhs, rhs)
 | (expr.pi n bi a b) := do
   l ← mk_local' n bi a,
-  simp_lhs (b.instantiate_var l)
-| ty := pure ty
+  simp_lhs_rhs (b.instantiate_var l)
+| ty := pure (ty, `(true))
 end
 
+/-- `simp_lhs ty` returns the left-hand side of a simp lemma with type `ty`. -/
+private meta def simp_lhs (ty : expr) : tactic expr :=
+prod.fst <$> simp_lhs_rhs ty
+
 private meta def heuristic_simp_lemma_extraction (prf : expr) : tactic (list name) :=
 prf.list_constant.to_list.mfilter is_simp_lemma
 
@@ -533,6 +538,27 @@ and which hence never fire.
   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" }
 
+private meta def simp_comm (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, rhs) ← simp_lhs_rhs d.type,
+if lhs.get_app_fn.const_name ≠ rhs.get_app_fn.const_name then pure none else do
+(lhs', rhs') ← (prod.snd <$> mk_meta_pis d.type) >>= simp_lhs_rhs,
+tt ← succeeds $ unify rhs' lhs transparency.reducible | pure none,
+tt ← succeeds $ is_def_eq rhs lhs' transparency.reducible | pure none,
+-- ensure that the second application makes progress:
+ff ← succeeds $ is_def_eq lhs' rhs' transparency.reducible | pure none,
+pure $ "should not be marked simp"
+
+/-- A linter for commutativity lemmas that are marked simp. -/
+@[linter, priority 1385] meta def linter.simp_comm : linter :=
+{ test := simp_comm,
+  no_errors_found := "No commutativity lemma is marked simp.",
+  errors_found := "COMMUTATIVITY LEMMA IS SIMP.\n" ++
+    "Some commutativity lemmas are simp lemmas" }
+
 /- Implementation of the frontend. -/
 
 /-- `get_checks slow extra use_only` produces a list of linters.

src/topology/algebra/infinite_sum.lean

@@ -168,7 +168,7 @@ mem_at_top_sets.mpr $ exists.intro fsts $ assume bs (hbs : fsts ⊆ bs),
       from hu _ $ finset.subset.trans u_subset $ sigma_mono hbs $
         assume b, @finset.subset_union_right (γ b) _ _ _,
     exists.intro cs' $
-    by simp [sum_eq, this]; { intros b hb, simp [cs', hb, finset.subset_union_right] },
+    by simp [sum_eq, this]; { intros b hb, simp [cs', hb, finset.subset_union_left] },
   have tendsto (λp:(Πb:β, finset (γ b)), bs.sum (λb, (p b).sum (λc, f ⟨b, c⟩)))
       (⨅b (h : b ∈ bs), at_top.comap (λp, p b)) (𝓝 (bs.sum g)),
     from tendsto_finset_sum bs $

test/lint_simp_comm.lean

@@ -0,0 +1,43 @@
+import tactic.lint
+
+/-! ## Commutativity lemmas should be rejected  -/
+
+attribute [simp] add_comm add_left_comm
+
+open tactic
+#eval do
+decl ← get_decl ``add_comm,
+res ← linter.simp_comm.test decl,
+-- linter complains
+guard res.is_some
+
+open tactic
+#eval do
+decl ← get_decl ``add_left_comm,
+res ← linter.simp_comm.test decl,
+-- linter complains
+guard res.is_some
+
+/-! ## Floris' trick should be accepted -/
+
+@[simp] lemma list.filter_congr_decidable {α} (s : list α) (p : α → Prop) (h : decidable_pred p)
+  [decidable_pred p] : @list.filter α p h s = s.filter p :=
+by congr
+
+-- lemma is unproblematic
+example : @list.filter _ (λ x, x > 0) (λ _, classical.prop_decidable _) [1,2,3] = [1,2,3] :=
+begin
+  -- can rewrite once
+  simp only [list.filter_congr_decidable],
+  -- but not twice
+  success_if_fail { simp only [list.filter_congr_decidable] },
+  refl
+end
+
+open tactic
+set_option pp.all true
+#eval do
+decl ← get_decl ``list.filter_congr_decidable,
+res ← linter.simp_comm.test decl,
+-- linter does not complain
+guard res.is_none