dsimp conv

Stream: mathlib4

[Moritz Doll]

So I've looked a bit into the conv-version of dsimp and I have run into two issues: First I don't know what
the syntax argument of mkSimpContext is supposed to do (so in the code I first set it to Lean.Syntax.missing).
Also I messed up the elaboration, so that it changes the usual dsimp and not the conv dsimp and I have no idea how to fix that.

The code

import Mathlib.Tactic.Basic
import Mathlib.Tactic.Core

namespace Lean.Parser.Tactic.Conv
open Elab.Tactic Elab.Tactic.Conv

/- N -/ syntax (name := dsimp) "dsimp" (&" only")? (dsimpArgs)? : conv

def evalDSimp : Tactic := fun stx => withMainContext do
  let { ctx, .. } ← mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
  let lhs ← getLhs
  let result ← Lean.Meta.dsimp lhs ctx
  changeLhs result

elab "dsimp" : tactic => evalDSimp Lean.Syntax.missing

example : (1 + 0) = 1 := by
  dsimp

example : (1 + 0) = 1 := by
  conv =>
    lhs
    dsimp

[Moritz Doll]

If I change it to elab "dsimp" : conv => .., then the error becomes "unsupported syntax category 'conv'" and I have no idea what that refers to

[Gabriel Ebner]

So there's quite a few things going on here.

[Gabriel Ebner]

Let me start at the end.

[Gabriel Ebner]

elab "dsimp" : conv => ..

Yes, it would be nice if we had this.. But it is not implemented in core. (As you've noticed we only have it for tactic but not for conv.)

[Gabriel Ebner]

The error message means just that: the elab command does not support conv.

[Gabriel Ebner]

Even if elab ... : conv worked it does something different than what you think it does. The elab command declares a new syntax parser (in this case dsimp) and then immediately defines an elaborator for this syntax. It would conflict with the syntax defined at the beginning of the file (and produce ambiguous parse trees with choice nodes).

[Gabriel Ebner]

If you looked at how the simp conv tactic is implemented in core, it looks like this:

@[builtinTactic Lean.Parser.Tactic.Conv.simp] def evalSimp : Tactic := fun stx => withMainContext do

The builtinTactic attribute is what registers the evalSimp attribute as an elaborator for the simp conv-tactic in core. The reason that this is called builtinTactic is because it uses builtin_initialize to add the tactic elaborator when loading the C++ code.

[Gabriel Ebner]

In mathlib, we need to use @[tactic Lean.Parser.Tactic.Conv.simp] instead.

[Gabriel Ebner]

mkSimpContext

The mkSimpContext function is super evil. Basically it assumes that the syntax argument is defined in exactly the same way as the builtin simp tactic, just with a different name. If you want to use it, you need to define dsimp as:

syntax (name := dsimp) "dsimp " (config)? (discharger)? (&"only ")? ("[" dsimpArg,* "]")? : conv

Basically it looks at stx[1] and hopes that it is a (config)?. If you leave out the (config)? in the syntax definition, mkSimpContext will fail in exciting ways.

[Gabriel Ebner]

(For consistency, I would suggest to use the syntax definition above ^^ and use mkSimpContext.)

[Moritz Doll]

Thank you so much Gabriel, it now works :octopus:
I saw the builtinTactic attribute, but I did not know that there is a version for non-builtin tactics. Is this documented anywhere and if not where should it be? maybe in @Arthur Paulino's book?
The reason I changed the syntax was only that I had funny import errors in the beginning and I thought leaving out some arguments might make it easier to get going.

[Moritz Doll]

do we have any useful tests for dsimp in mathlib3? I could not find anything in the test/conv folder and the one above does not really test more than that the command does not fail, because conv can finish the goal on its own

[Moritz Doll]

nevertheless the info view shows that it works as it should

[Gabriel Ebner]

Feel free to invent some tests. I would probably set up a goal like a * 1 + 0 and then two separate tests dsimp and dsimp only [Nat.add_zero].

[Moritz Doll]

I've managed to find one test that actually fails if the dsimp is omitted.