feat: elementwise linting checks, and putting into simp normal form (#…

…2956)

Some `elementwise` lemmas are completely trivial even without any simp lemmas, likely because coercions are being unfolded. We add some linting checks to let the user know they can omit the `elementwise` attribute.

Also, `elementwise` doesn't necessarily put lemmas into simp normal form, which means `@[elementwise (attr := simp)]` can lead to failing the simpNF linter. Now by default `elementwise` will apply `simp` to the left-hand and right-hand sides of the lemma. Use `@[elementwise nosimp]` to override this.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/CategoryTheory/Elementwise.lean

@@ -25,9 +25,8 @@ so we need to add the attribute after the fact.
 
 open CategoryTheory
 
--- Porting note: We remove the simp attribute to re-add it with `elementwise (attr := simp)`
--- attribute [-simp] Iso.hom_inv_id Iso.inv_hom_id IsIso.hom_inv_id IsIso.inv_hom_id
+-- Porting note: Iso.hom_inv_id and Iso.inv_hom_id produce trivial elementwise lemmas now.
 
 -- This list is incomplete, and it would probably be useful to add more.
 set_option linter.existingAttributeWarning false in
-attribute [elementwise] Iso.hom_inv_id Iso.inv_hom_id IsIso.hom_inv_id IsIso.inv_hom_id
+attribute [elementwise (attr := simp)] IsIso.hom_inv_id IsIso.inv_hom_id

Mathlib/Lean/Meta/Simp.lean

@@ -179,9 +179,11 @@ def simpTheoremsOfNames (lemmas : List Name) : MetaM SimpTheorems := do
 -- TODO We need to write a `mkSimpContext` in `MetaM`
 -- that supports all the bells and whistles in `simp`.
 -- It should generalize this, and another partial implementation in `Tactic.Simps.Basic`.
-def simpOnlyNames (lemmas : List Name) (e : Expr) : MetaM Simp.Result := do
+def simpOnlyNames (lemmas : List Name) (e : Expr) (config : Simp.Config := {}) :
+    MetaM Simp.Result := do
   (·.1) <$> simp e
-    { simpTheorems := #[← simpTheoremsOfNames lemmas], congrTheorems := ← getSimpCongrTheorems }
+    { simpTheorems := #[← simpTheoremsOfNames lemmas], congrTheorems := ← getSimpCongrTheorems,
+      config := config }
 
 /--
 Given a simplifier `S : Expr → MetaM Simp.Result`,
@@ -194,6 +196,22 @@ def simpType (S : Expr → MetaM Simp.Result) (e : Expr) : MetaM Expr := do
   -- We use `mkExpectedTypeHint` in this branch as well, in order to preserve the binder types.
   | ⟨ty', some prf, _⟩ => mkExpectedTypeHint (← mkEqMP prf e) ty'
 
+/-- Independently simplify both the left-hand side and the right-hand side
+of an equality. The equality is allowed to be under binders.
+Returns the simplified equality and a proof of it. -/
+def simpEq (S : Expr → MetaM Simp.Result) (type pf : Expr) : MetaM (Expr × Expr) := do
+  forallTelescope type fun fvars type => do
+    let .app (.app (.app (.const `Eq [u]) α) lhs) rhs := type | throwError "simpEq expecting Eq"
+    let ⟨lhs', lhspf?, _⟩ ← S lhs
+    let ⟨rhs', rhspf?, _⟩ ← S rhs
+    let mut pf' := mkAppN pf fvars
+    if let some lhspf := lhspf? then
+      pf' ← mkEqTrans (← mkEqSymm lhspf) pf'
+    if let some rhspf := rhspf? then
+      pf' ← mkEqTrans pf' rhspf
+    let type' := mkApp3 (mkConst ``Eq [u]) α lhs' rhs'
+    return (← mkForallFVars fvars type', ← mkLambdaFVars fvars pf')
+
 /-- Checks whether `declName` is in `SimpTheorems` as either a lemma or definition to unfold. -/
 def SimpTheorems.contains (d : SimpTheorems) (declName : Name) :=
   d.isLemma (.decl declName) || d.isDeclToUnfold declName

Mathlib/Tactic/Elementwise.lean

@@ -6,6 +6,7 @@ Authors: Scott Morrison, Kyle Miller
 
 import Mathlib.CategoryTheory.ConcreteCategory.Basic
 import Mathlib.Util.AddRelatedDecl
+import Std.Tactic.Lint
 
 /-!
 # Tools to reformulate category-theoretic lemmas in concrete categories
@@ -56,7 +57,10 @@ def elementwiseThms : List Name :=
   [``CategoryTheory.coe_id, ``CategoryTheory.coe_comp, ``CategoryTheory.comp_apply,
     ``CategoryTheory.id_apply,
     -- further simplifications if the category is `Type`
-    ``forget_hom_Type, ``forall_congr_forget_Type]
+    ``forget_hom_Type, ``forall_congr_forget_Type,
+    -- simp can itself simplify trivial equalities into `true`. Adding this lemma makes it
+    -- easier to detect when this has occurred.
+    ``implies_true]
 
 /--
 Given an equation `f = g` between morphisms `X ⟶ Y` in a category `C`
@@ -66,12 +70,32 @@ with compositions fully right associated and identities removed.
 
 Returns the proof of the new theorem along with (optionally) a new level metavariable
 for the first universe parameter to `ConcreteCategory`.
+
+The `simpSides` option controles whether to simplify both sides of the equality, for simpNF
+purposes.
 -/
-def elementwiseExpr (type pf : Expr) : MetaM (Expr × Option Level) := do
+def elementwiseExpr (src : Name) (type pf : Expr) (simpSides := true) :
+    MetaM (Expr × Option Level) := do
   let type := (← instantiateMVars type).cleanupAnnotations
   forallTelescope type fun fvars type' => do
     mkHomElementwise type' (mkAppN pf fvars) fun eqPf instConcr? => do
-      let eqPf' ← simpType (simpOnlyNames elementwiseThms) eqPf
+      -- First simplify using elementwise-specific lemmas
+      let mut eqPf' ← simpType (simpOnlyNames elementwiseThms (config := { decide := false })) eqPf
+      if (← inferType eqPf') == .const ``True [] then
+        throwError "elementwise lemma for {src} is trivial after applying ConcreteCategory {""
+          }lemmas, which can be caused by how applications are unfolded. {""
+          }Using elementwise is unnecessary."
+      if simpSides then
+        let ctx := { ← Simp.Context.mkDefault with config.decide := false }
+        let (ty', eqPf'') ← simpEq (fun e => return (← simp e ctx).1) (← inferType eqPf') eqPf'
+        -- check that it's not a simp-trivial equality:
+        forallTelescope ty' fun _ ty' => do
+          if let some (_, lhs, rhs) := ty'.eq? then
+            if ← Std.Tactic.Lint.isSimpEq lhs rhs then
+              throwError "applying simp to both sides reduces elementwise lemma for {src} {""
+                }to the trivial equality {ty'}. {""
+                }Either add `nosimp` or remove the `elementwise` attribute."
+        eqPf' ← mkExpectedTypeHint eqPf'' ty'
       if let some (w, instConcr) := instConcr? then
         return (← Meta.mkLambdaFVars (fvars.push instConcr) eqPf', w)
       else
@@ -89,11 +113,10 @@ where
       MetaM α := do
     let (C, instC) ← try extractCatInstance eqTy catch _ =>
       throwError "elementwise expects equality of morphisms in a category"
-    try
-      -- First try being optimistic that there is already a ConcreteCategory instance.
-      let eqPf' ← mkAppM ``hom_elementwise #[eqPf]
+    -- First try being optimistic that there is already a ConcreteCategory instance.
+    if let some eqPf' ← observing? (mkAppM ``hom_elementwise #[eqPf]) then
       k eqPf' none
-    catch _ =>
+    else
       -- That failed, so we need to introduce the instance, which takes creating
       -- a fresh universe level for `ConcreteCategory`'s forgetful functor.
       let .app (.const ``Category [v, u]) _ ← inferType instC
@@ -121,7 +144,13 @@ private partial def mkUnusedName (names : List Name) (baseName : Name) : Name :=
 creates a new lemma for a `ConcreteCategory` giving an equation with those morphisms applied
 to some value.
 
-For example:
+Syntax examples:
+- `@[elementwise]`
+- `@[elementwise nosimp]` to not use `simp` on both sides of the generated lemma
+- `@[elementwise (attr := simp)]` to apply the `simp` attribute to both the generated lemma and
+  the original lemma.
+
+Example application of `elementwise`:
 
 ```lean
 @[elementwise]
@@ -148,18 +177,19 @@ The `[ConcreteCategory C]` argument will be omitted if it is possible to synthes
 The name of the produced lemma can be specified with `@[elementwise other_lemma_name]`.
 If `simp` is added first, the generated lemma will also have the `simp` attribute.
  -/
-syntax (name := elementwise) "elementwise" ("(" &"attr" ":=" Parser.Term.attrInstance,* ")")? : attr
+syntax (name := elementwise) "elementwise"
+  "nosimp"? ("(" &"attr" ":=" Parser.Term.attrInstance,* ")")? : attr
 
 initialize registerBuiltinAttribute {
   name := `elementwise
   descr := ""
   applicationTime := .afterCompilation
   add := fun src ref kind => match ref with
-  | `(attr| elementwise $[(attr := $stx?,*)]?) => MetaM.run' do
+  | `(attr| elementwise $[nosimp%$nosimp?]? $[(attr := $stx?,*)]?) => MetaM.run' do
     if (kind != AttributeKind.global) then
       throwError "`elementwise` can only be used as a global attribute"
     addRelatedDecl src "_apply" ref `elementwise stx? fun type value levels => do
-      let (newValue, level?) ← elementwiseExpr type value
+      let (newValue, level?) ← elementwiseExpr src type value (simpSides := nosimp?.isNone)
       let newLevels ← if let some level := level? then do
         let w := mkUnusedName levels `w
         unless ← isLevelDefEq level (mkLevelParam w) do
@@ -187,10 +217,14 @@ Like the `@[elementwise]` attribute, `elementwise_of%` inserts a `ConcreteCatego
 instance argument if it can't synthesize a relevant `ConcreteCategory` instance.
 (Technical note: The forgetful functor's universe variable is instantiated with a
 fresh level metavariable in this case.)
+
+One difference between `elementwise_of%` and `@[elementwise]` is that `@[elementwise]` by
+default applies `simp` to both sides of the generated lemma to get something that is in simp
+normal form. `elementwise_of%` does not do this.
 -/
 elab "elementwise_of% " t:term : term => do
   let e ← Term.elabTerm t none
-  let (pf, _) ← elementwiseExpr (← inferType e) e
+  let (pf, _) ← elementwiseExpr .anonymous (← inferType e) e (simpSides := false)
   return pf
 
 end Tactic.Elementwise

Mathlib/Tactic/Reassoc.lean

@@ -37,6 +37,7 @@ theorem eq_whisker' {X Y : C} {f g : X ⟶ Y} (w : f = g) {Z : C} (h : Y ⟶ Z)
 /-- Simplify an expression using only the axioms of a category. -/
 def categorySimp (e : Expr) : MetaM Simp.Result :=
   simpOnlyNames [``Category.comp_id, ``Category.id_comp, ``Category.assoc] e
+    (config := { decide := false })
 
 /--
 Given an equation `f = g` between morphisms `X ⟶ Y` in a category (possibly after a `∀` binder),

test/elementwise.lean

@@ -26,7 +26,8 @@ theorem ex2 [Category C] (X : C) (f g h : X ⟶ X) (h' : g ≫ h = h ≫ g) :
 example : ∀ C [Category C] (X : C) (f g h : X ⟶ X) (_ : g ≫ h = h ≫ g) [ConcreteCategory C]
     (x : X), h (g (f x)) = g (h (f x)) := @ex2_apply
 
-@[elementwise]
+-- Need nosimp on the following `elementwise` since the lemma can be proved by simp anyway.
+@[elementwise nosimp]
 theorem ex3 [Category C] {X Y : C} (f : X ≅ Y) : f.hom ≫ f.inv = 𝟙 X :=
   Iso.hom_inv_id _