Feature request: attribute dsimp-nf

Stream: mathlib4

[Joël Riou]

In category theory (and probably other areas of mathlib such as algebraic geometry), general purpose lemmas are not necessarily in dsimp normal form, but still it has been possible to use them with rw and simp until https://github.com/leanprover/lean4/pull/12179
The temporary fix is using set_option backward.isDefEq.respectTransparency false but it is considered as a technical debt #mathlib4 > Technical Debt Counters @ 💬

[Joël Riou]

Feature-request: add an attribute dsimp-nf which would replace a lemma by its dsimped-version, e.g. in the example below, the statement of naturality would be transformed into naturality'. (It would be nice to have a setup which would allow to automatically apply this attribute to all the simp-lemmas that are declared in a given file/section.)

[Joël Riou]

module

public import Mathlib.CategoryTheory.Functor.Category

open CategoryTheory

variable {C D : Type*} [Category* C] [Category* D] {F : C ⥤ D} {G : D ⥤ C}
  (τ : F ⋙ G ⟶ 𝟭 C) {X Y : C} (f : X ⟶ Y)

set_option backward.isDefEq.respectTransparency true

lemma naturality : G.map (F.map f) ≫ τ.app Y = τ.app X ≫ f := by
  -- Note that we can do `dsimp only [Functor.id_obj, Functor.comp_obj]` here
  -- which means that the statement is not in "dsimp" normal form
  exact NatTrans.naturality τ f

lemma test : G.map (F.map f) ≫ τ.app Y = τ.app X ≫ f := by
  dsimp
  rw [naturality] -- fails since https://github.com/leanprover/lean4/pull/12179
  -- unless we do `set_option backward.isDefEq.respectTransparency false`

lemma naturality' :
    letI a : G.obj (F.obj X) ⟶ G.obj (F.obj Y) := G.map (F.map f)
    letI b : G.obj (F.obj Y) ⟶ Y := τ.app Y
    letI c : G.obj (F.obj X) ⟶ X := τ.app X
    a ≫ b = c ≫ f :=
  NatTrans.naturality τ f

lemma test' : G.map (F.map f) ≫ τ.app Y = τ.app X ≫ f := by
  dsimp
  rw [naturality']

[Christian Merten]

Alternatively or additionally, I am wondering if we should use unification hints for some of the standard identities that we want to treat as reducible equalities. For example, with this

unif_hint where ⊢ (Functor.id C).obj X ≟ X

the example works.

[Christian Merten]

Everywhere where we have (non-reducible) bundled objects with projections involving terms that (often) appear in types (i.e. everywhere in category theory / algebraic geometry), it has always been difficult to write reducibly type-correct lemmas. Aggressively running dsimp on all statements is maybe one fix, but it seems more like a hack than a long-term solution to me.

[Joël Riou]

In principle, the simpNF linter should complain on these lemmas...
What I am basically saying is that set_option backward.isDefEq.respectTransparency true completely breaks the experience of writing category theory Lean code unless one or more reasonable solutions are found!

[Robin Carlier]

Christian Merten said:

Alternatively or additionally, I am wondering if we should use unification hints for some of the standard identities that we want to treat as reducible equalities. For example, with this

unif_hint where ⊢ (Functor.id C).obj X ≟ X

the example works.

Where do I start learning more about unification hints? What do they do exactly that makes this example work? The command unif_hint has no hover info, and is not mentionned in the reference manual.

[Christian Merten]

Robin Carlier said:

Where do I start learning more about unification hints?

Unfortunately, I think this is an open question. If you find the answer, I am happy to hear it. Maybe the best documentation is following the source code. This is the only invocation of tryUnificationHints and it happens as one of the last steps in the def-eq algorithm (which is why I don't get why they are called unification hints, the name suggests to me they should be checked much earlier).

The one thing I learnt, purely from observation, is that

unif_hint foo where ⊢ A ≟ B

makes A and B reducibly def-eq if A and B are def-eq.

[Christian Merten]

And unif_hint can be conditional, i.e. you can write things like

unif_hint foo where A ≟ B ⊢ F A ≟ F B

[Robin Arnez]

When normal definition equality fails (as part of onFailure), then it tries unification hints. In a call of isDefEq t s trying a unification hint unif_hint name? binders... where $[clhs ≟ crhs]* ⊢ lhs ≟ rhs does the following: it first tries unifying t with lhs as well as s with rhs under reducible transparency and then checks definitional equality of all constraints, i.e. it checks isDefEq clhs crhs for every constraint. If this fails, it tries again with t and s swapped.
So roughly speaking, it tells definitional equality what to do in a situation that looks like lhs =?= rhs, namely, that it should try unifying all clhs =?= crhs in that case. Also notable is that unification hints are indexed using their left-hand side, so that should be the more specific side.
However, the current implementation of unification hints is not safe, consider:

unif_hint {α : Sort u} (x y : α) where ⊢ x =?= y -- totally fine
example : (1, 2) = (3, 4) := rfl -- kernel error

c.f. lean4#8982 and lean4#8988

[Robin Carlier]

Thanks to you both for taking the time to explain!

[Christian Merten]

This is maybe similar to what you are imagining (as a command, because attributes need two files which is not compatible with the live editor). I unfortunately don't know how to replace the original declaration by the dsimped one.

import Mathlib.CategoryTheory.Functor.Category

section
open Lean Meta Elab Term

def dsimpExpr (e : Expr) : TermElabM Expr := do
  (flip simpType) e fun e => do
    let ctxt ← Simp.Context.ofNames
    let (res, _) ← dsimp e ctxt
    return { expr := res }

elab "dsimp_decl" name:ident : command => do
  let src := name.getId
  let info ← withoutExporting <| getConstInfo src
  let value := Expr.const src (info.levelParams.map mkLevelParam)
  let newName : Name := src.appendAfter "_dsimped"
  Command.liftTermElabM <| do
    let newValue ← dsimpExpr value
    let newType ← instantiateMVars (← inferType newValue)
    addDecl <| ← mkThmOrUnsafeDef
      { levelParams := info.levelParams, type := newType, name := newName, value := newValue }

end

open CategoryTheory

variable {C D : Type*} [Category* C] [Category* D] {F : C ⥤ D} {G : D ⥤ C}
  (τ : F ⋙ G ⟶ 𝟭 C) {X Y : C} (f : X ⟶ Y)

set_option backward.isDefEq.respectTransparency true

lemma naturality : G.map (F.map f) ≫ τ.app Y = τ.app X ≫ f := by
  -- Note that we can do `dsimp only [Functor.id_obj, Functor.comp_obj]` here
  -- which means that the statement is not in "dsimp" normal form
  exact NatTrans.naturality τ f

dsimp_decl naturality

lemma test : G.map (F.map f) ≫ τ.app Y = τ.app X ≫ f := by
  dsimp
  -- fails
  fail_if_success
    rw [naturality]
  -- succeeds
  rw [naturality_dsimped]