simproc in ComposableArrow

Stream: mathlib4

[Patrick Massot]

I just wasted one hour because I missed those lines in ComposableArrows.lean

/-!
New `simprocs` that run even in `dsimp` have caused breakages in this file.

(e.g. `dsimp` can now simplify `2 + 3` to `5`)

For now, we just turn off simprocs in this file.
We'll soon provide finer grained options here, e.g. to turn off simprocs only in `dsimp`, etc.

*However*, hopefully it is possible to refactor the material here so that no backwards compatibility
`set_option`s are required at all
-/
set_option simprocs false

Do we have any gadget that could output a warning if the type ComposableArrows appears in a file that does not turn off simprocs? Is there any plan about the refactor mentioned in the above file? @Kim Morrison @Joël Riou @yannis monbru

[Joël Riou]

I am afraid I cannot help very much here, because when I originally wrote the code, I took care that dsimp did the best we may expect, but I do not understand exactly what are the changes in the internals of Lean which broke this and led to this set_option fix.

[Patrick Massot]

You can see what happens in:

import Mathlib.CategoryTheory.ComposableArrows

open CategoryTheory ComposableArrows

variable {C : Type*} [Category C] {X₀ X₁ X₂ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂)


example : map' (mk₂ f g) 1 2 = g := by
  dsimp -- fails

example : map' (mk₂ f g) 1 2 = g := by
  dsimp [-Nat.reduceAdd, -Int.reduceNeg, -Int.reduceAdd, -Int.reduceSub, -Fin.reduceFinMk]

set_option simprocs false

example : map' (mk₂ f g) 1 2 = g := by dsimp

[Patrick Massot]

Note this is three times the same statement.k

[Damiano Testa]

Something like

open Lean Meta.Simp in
elab "warn_me" : command => do
  let composableArrows? := (← getEnv).find? `CategoryTheory.ComposableArrows
  let opt := simprocs.get (← getOptions)
  if opt && composableArrows?.isSome then
    logWarning "Consider turning off `simprocs` using `set_option simprocs false`"

could be easily turned into a linter.

[Eric Wieser]

This works as a slightly finer-grained fix than disabling all simprocs:

attribute [- simprocAttr] Fin.reduceFinMk
example : map' (mk₂ f g) 1 2 = g := by
  dsimp

(docs#Fin.reduceFinMk)

[Patrick Massot]

Damiano, this is a bit too much since importing the file (transitively) would be enough to trigger the warning.

[Patrick Massot]

Eric: nice, there are less issues than I thought (I simply looked at all simp lemmas in the failing dsimp).

[Eric Wieser]

It would be helpful if these simprocs had docstrings

[Eric Wieser]

Especially since unlike theorems, you have no idea what they do from the hover in vscode

[Joël Riou]

Eric Wieser said:

Especially since unlike theorems, you have no idea what they do from the hover in vscode

Thanks for looking at this. After looking at the code, I still have no idea what they do!

What could be changed in lemmas like Precomp.map_succ_succ (or any other which may not be in the suitable form) so that it may still be applied automatically by dsimp without any change in options/attributes?

[Eric Wieser]

I think you run into a mess around OfNat.ofNat here

[Eric Wieser]

I think the only way to counter this dsimproc is with another dsimproc