rfl tactic without a macro

Stream: lean4

[Joachim Breitner]

Right now, the rfl tactic is a macro that tries (once you load std4) exact HEq.rfl, exact Iff.rfl and then docs#Lean.MVarId.refl. A consequence of this implementation is that the the error message isn’t beginner friendly (talks about Iff.rfl or HEq.rfl), and maybe it is a tad slower than it needs to be when using the general macro/exact machinery.

Since Iff and HEq are both in Core, I wonder whether it would make sense to simply teach docs#Lean.MVarId.refl (or a variant thereof) to support all these three relations directly. This might make it (a bit) faster (not sure how important that is, maybe rfl is used within other tactics a lot?) and have a better error message when it fails.

[Mario Carneiro]

This might be fixed in the near future since lots of std tactics are getting upstreamed to core

[Joachim Breitner]

Indeed, seeing the upstreaming PR of Iff.rfl and the error message regression is what made me ponder this question.

[Joachim Breitner]

So assuming all functionality is in core, is the macro_rule based implementation or the single-MetaM-function implementation preferrable?

[Mario Carneiro]

I would say single MetaM function

[Mario Carneiro]

certainly it makes it easier to fix the error messages

[Mario Carneiro]

plus the relation rfl tactic (using @[refl] theorems) already subsumes all of the others

[Joachim Breitner]

Is that a separate tactic? (I thought something like this would exist, but didn't find it right away)

[Joachim Breitner]

Ah, found it. The macro_rules line isn’t on the same line as rfl and escaped my grepping :-).
Looks like the macro and attribute is defined in std4, but almost most attribute assignments are in Mathlib, including those duplicating that macro_rules with exact Heq.rfl and Iff.rfl. Hmm. Maybe I’ll wait for the upstreaming storm to settle before barging into this area :-)

[Joachim Breitner]

BTW, the error message for

import Std
example P := by rfl

is

don't know how to synthesize implicit argument
  @HEq.rfl (?m.16 P) (?m.17 P)
context:
P: ?m.2
⊢ ?m.16 P

:man_facepalming:

[Joachim Breitner]

A bit better with

import Std
example (P : Prop) : P := by rfl

but not much:

type mismatch
  HEq.rfl
has type
  HEq ?m.10 ?m.10 : Prop
but is expected to have type
  P : Prop

[Mario Carneiro]

The first one looks like a mistake, presumably you wanted a colon before P

[Mario Carneiro]

I think this is one reason not to allow unparenthesized binders, they are much more likely to be typos of either the result type or the theorem name

[Joachim Breitner]

Fair enough.

BTW, is there a way to query the registered macro rules? I.e. list all rules that apply to a given syntax term?

[Mario Carneiro]

#help tactic is similar but doesn't cover individual macro rules

[Mario Carneiro]

Oh, this is already implemented as

import Mathlib.Tactic.HelpCmd

#help tactic+ trivial

syntax "trivial"... [Lean.Parser.Tactic.tacticTrivial]
  `trivial` tries different simple tactics (e.g., `rfl`, `contradiction`, ...)
  to close the current goal.
  You can use the command `macro_rules` to extend the set of tactics used. Example:
  ```
  macro_rules | `(tactic| trivial) => `(tactic| simp)
  ```
+ macro Lean.Parser.Tactic._aux_Init_Tactics___macroRules_Lean_Parser_Tactic_tacticTrivial_6
+ macro Lean.Parser.Tactic._aux_Init_Tactics___macroRules_Lean_Parser_Tactic_tacticTrivial_5
+ macro Lean.Parser.Tactic._aux_Init_Tactics___macroRules_Lean_Parser_Tactic_tacticTrivial_4
+ macro Lean.Parser.Tactic._aux_Init_Tactics___macroRules_Lean_Parser_Tactic_tacticTrivial_3
+ macro Lean.Parser.Tactic._aux_Init_Tactics___macroRules_Lean_Parser_Tactic_tacticTrivial_2
+ macro Lean.Parser.Tactic._aux_Init_Tactics___macroRules_Lean_Parser_Tactic_tacticTrivial_1

The constant names are go-to-def-able (unfortunately I couldn't find a less noisy way to do that in the current infoview)

[Joachim Breitner]

Mario Carneiro said:

I would say single MetaM function

JFTR: escalated this to an RFC at https://github.com/leanprover/lean4/issues/3302