RFC: A single rfl tactic implementation #3302

nomeata · 2024-02-11T21:35:59Z

I noticed (while #3299 passed by) that rfl produces a rather unhelpful error message:

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

gives

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

This is not a good UX for a tactic that early users will be exposed to early (and also not great later on).

Looking at what happens I found that there are four different implementations registered (using macro/macro_rules) for rfl:

Wrapping Lean.MVarId.refl, for Eq.
exact HEq.rfl
exact Iff.rfl
https://leanprover-community.github.io/mathlib4_docs/Std/Tactic/Relation/Rfl.html#Lean.MVarId.applyRfl, which supports any relation with a suitable @[refl] lemma.

Unfortunately, it seems that using macro_rules to extend tactics doesn’t give great control over which error message is shown if all fail.

Assuming we want @[refl] in core, I propose that, after upstreaming Std.Tactic.Relation.Rfl, we back the rlf tactic by a single function that combines Lean.MVarId.refl and Lean.MVarId.applyRfl, possibly still with a special path for Eq (should that be needed, TBD), and with good error messages for the various failure modes.

With a suitable @[refl] attribute, this should allow us to remove the extra exact ….rfl macro rules.

Community Feedback

This was escalated from a discussion on zulip.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

The text was updated successfully, but these errors were encountered:

nomeata · 2024-03-18T15:44:47Z

Having a closer look. One issue is that the order of parameters in HEq makes it ineligible to the @[refl] machinery:

HEq.refl.{u} {α : Sort u} (a : α) : @HEq α a α a

(it would have to be @HEq α α a a).

If one still wants to persue the goal of a macro_rules-free implementation to get good control over the error messages, I see these plausible options:

Hard-coding HEq.refl in the tactic implementation
~~Changing the order of parameters on HEq~~

~~I personally would have expected~~
```
inductive HEq : {α : Sort u} → {β : Sort u} → α → β → Prop where
```
but there may be a good reason for the other order that I don’t know (if there is
we should put a comment on the code).

~~Even if there is no such good reason, not wanting to break existing code may be a reason.~~

(See explanation below)
Drop HEq support from the rfl tactic, and expect people to write exact HEq.rfl. Maybe that’s the best option, given that HEq is a rather special case anyways and it doesn’t hurt to be explicit here.

digama0 · 2024-03-18T15:57:29Z

Changing the order of parameters on HEq
I personally would have expected
inductive HEq : {α : Sort u} → {β : Sort u} → α → β → Prop where
but there may be a good reason for the other order that I don’t know (if there is
we should put a comment on the code).

There is: In Eq and HEq, the left argument is a parameter and the right one is an index of the inductive type. Lean strictly enforces that parameters come before indices in the inductive type, so interchanging the arguments would make (a : α) argument an index as well, which changes the type of HEq.rec considerably (try it and see), in a less than helpful direction.

digama0 · 2024-03-18T16:03:28Z

There is another option you did not list:

Make the @[rfl] attribute support relations that have dependencies on both sides.

This would be desirable for other reasons as well; I recall something similar coming up with being able to use calc for arrows in a category or something like that, where the type signature of Trans wasn't general enough to handle the implicit arguments. (I forget whether this concerns the current or a previous version of Trans though, I'd have to look up the details.)

In short, the issue here is not unique to HEq, so I would advise against something that special cases it.

nomeata · 2024-03-18T16:06:29Z

Ah, yes, parameter vs. index makes sense, thanks.

True, extending rfl is an option. I disregarded it as too complex initially, but if we find more examples then that might eventually be the best course of action. I also vaguely remember the Trans issues.

digama0 · 2024-03-18T16:09:47Z

I think keeping apply HEq.refl as a special extra case in the meantime (but in an elab rather than using macro_rules alternation so that you can control the error message better) would be a way to not regress rfl while figuring out how to handle the general case.

Another reason you probably want rfl to work on HEq goals even though they are discouraged: HEq goals / hypotheses are generated by congr and cases in order to reason about telescope equalities, and rfl is used to close those goals when they are trivial. It's possible that there is some eq_of_heq inserted that will save you but I wouldn't be surprised if either some tactic is skipping that step or if there is some weird metavariable condition under which eq_of_heq won't apply because the types are not yet known to be equal and as a result rfl is given a HEq goal anyway.

nomeata · 2024-03-18T17:00:10Z

(Just for my own record: I attempted this refactoring, but got stuck in what’s either a boostrapping maze or a misunderstanding of how things works, and ran out of time today. Putting this back on the stack of things to look at when I have some extra time to spare. If someone else does tackles before I do then of course I don’t mind.)

(Update: #3714 has the tactic as I think it could be, it doesn’t swap it out for rfl yet.)

this implements the first half of #3302: It improves the extensible `rfl` tactic (the one that looks at `refl` attributes) to * Check itself that the lhs and rhs are defEq, and give a nice consistent error message when they don't (instead of just passing on the less helpful error message from `apply Foo.refl`) * Also handle `Eq` and `HEq` (built in) and `Iff` (using the attribute) Care ist taken that, as before, the transparency setting affects comparing the lhs and rhs, but not the reduction of the relation A test file checks the various failure modes and error messages. I believe this `apply_rfl` can serve as the only implementation of `rfl`, which would then complete #3302, but that seems to require a non-trivial bootstrapping dance, so maybe better done separately.

fixes #3770 Also start `rfl` with a `fail` message that is hopefully more helpful than what we get now (see updated test output). This would be a cheaper way to address #3302 without changing the implementation of rfl (as tried in #3714).

leodemoura · 2024-06-06T00:38:07Z

The new message is

error: The rfl tactic failed. Possible reasons:
- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
- The arguments of the relation are not equal.
Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
P : Prop
⊢ P

Marking it as closing soon

nomeata · 2024-06-06T06:05:22Z

#3714 and #3718 contain further improvements, including even better error messages, by having a single implementation, but I got stalled there because of the different transparency levels the current tactics work at. Might revisit that later, but I have the draft PRs to recall, so happy to close this issue.

This implements the first half of #3302: It improves the extensible `apply_rfl` tactic (the one that looks at `refl` attributes, part of the `rfl` macro) to * Check itself and ahead of time that the lhs and rhs are defEq, and give a nice consistent error message when they don't (instead of just passing on the less helpful error message from `apply Foo.refl`), and using the machinery that `apply` uses to elaborate expressions to highlight diffs in implicit arguments. * Also handle `Eq` and `HEq` (built in) and `Iff` (using the attribute) Care is taken that, as before, the current transparency setting affects comparing the lhs and rhs, but not the reduction of the relation So before we had ```lean opaque P : Nat → Nat → Prop @[refl] axiom P.refl (n : Nat) : P n n /-- error: tactic 'apply' failed, failed to unify P ?n ?n with P 42 23 ⊢ P 42 23 -/ #guard_msgs in example : P 42 23 := by apply_rfl opaque withImplicitNat {n : Nat} : Nat /-- error: tactic 'apply' failed, failed to unify P ?n ?n with P withImplicitNat withImplicitNat ⊢ P withImplicitNat withImplicitNat -/ #guard_msgs in example : P (@withImplicitNat 42) (@withImplicitNat 23) := by apply_rfl ``` and with this PR the messages we get are ``` error: tactic 'apply_rfl' failed, The lhs 42 is not definitionally equal to rhs 23 ⊢ P 42 23 ``` resp. ``` error: tactic 'apply_rfl' failed, The lhs @withImplicitNat 42 is not definitionally equal to rhs @withImplicitNat 23 ⊢ P withImplicitNat withImplicitNat ``` A test file checks the various failure modes and error messages. I believe this `apply_rfl` can serve as the only implementation of `rfl`, which would then complete #3302, and actually expose these improved error messages to the user. But as that seems to require a non-trivial bootstrapping dance, it’ll be separate.

nomeata · 2024-09-25T09:28:24Z

I actually picked up the work on these PRs. So reopening this, so that merging them can close it properly :-D

building upon #3714, this (almost) implements the second half of #3302. The main effect is that we now get a better error message when `rfl` fails. For ```lean example : n+1+m = n + (1+m) := by rfl ``` instead of the wall of text ``` The rfl tactic failed. Possible reasons: - The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma). - The arguments of the relation are not equal. Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or `exact HEq.rfl` etc. n m : Nat ⊢ n + 1 + m = n + (1 + m) ``` we now get ``` error: tactic 'rfl' failed, the left-hand side n + 1 + m is not definitionally equal to the right-hand side n + (1 + m) n m : Nat ⊢ n + 1 + m = n + (1 + m) ``` Unfortunately, because of very subtle differences in semantics (which transparency setting is used when reducing the goal and whether the “implicit lambda” feature applies) I could not make this simply the only `rfl` implementation. So `rfl` remains a macro and is still expanded to `eq_refl` (difference transparency setting) and `exact Iff.rfl` and `exact HEq.rfl` (implicit lambda) to not break existing code. This can be revised later, so this still closes: #3302. A user might still be puzzled *why* to terms are not defeq. Explaining that better (“reduced to… and reduces to… etc.”) would also be great, but that’s not specific to `rfl`, so better left for some other time.

nomeata mentioned this issue Mar 14, 2024

feat: upstream Std's rfl tactic #3671

Merged

This was referenced Mar 19, 2024

feat: apply_rfl tactic: handle Eq, HEq, better error messages #3714

Merged

refactor: back rfl tactic primarily via apply_rfl #3718

Merged

RFC: macros should show last error, not first #3770

Closed

nomeata mentioned this issue Mar 26, 2024

feat: failing macros to show error from first registered rule #3771

Merged

leodemoura added the closing soon This issue will be closed soon (<1 month) as it is missing essential features. label Jun 6, 2024

nomeata closed this as completed Jun 6, 2024

nomeata reopened this Sep 25, 2024

nomeata removed the closing soon This issue will be closed soon (<1 month) as it is missing essential features. label Sep 25, 2024

nomeata closed this as completed in #3718 Sep 25, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

RFC: A single rfl tactic implementation #3302

RFC: A single rfl tactic implementation #3302

nomeata commented Feb 11, 2024

nomeata commented Mar 18, 2024 •

edited

Loading

digama0 commented Mar 18, 2024 •

edited

Loading

digama0 commented Mar 18, 2024 •

edited

Loading

nomeata commented Mar 18, 2024

digama0 commented Mar 18, 2024 •

edited

Loading

nomeata commented Mar 18, 2024 •

edited

Loading

leodemoura commented Jun 6, 2024

nomeata commented Jun 6, 2024

nomeata commented Sep 25, 2024 •

edited

Loading

RFC: A single rfl tactic implementation #3302

RFC: A single rfl tactic implementation #3302

Comments

nomeata commented Feb 11, 2024

Community Feedback

Impact

nomeata commented Mar 18, 2024 • edited Loading

digama0 commented Mar 18, 2024 • edited Loading

digama0 commented Mar 18, 2024 • edited Loading

nomeata commented Mar 18, 2024

digama0 commented Mar 18, 2024 • edited Loading

nomeata commented Mar 18, 2024 • edited Loading

leodemoura commented Jun 6, 2024

nomeata commented Jun 6, 2024

nomeata commented Sep 25, 2024 • edited Loading

nomeata commented Mar 18, 2024 •

edited

Loading

digama0 commented Mar 18, 2024 •

edited

Loading

digama0 commented Mar 18, 2024 •

edited

Loading

digama0 commented Mar 18, 2024 •

edited

Loading

nomeata commented Mar 18, 2024 •

edited

Loading

nomeata commented Sep 25, 2024 •

edited

Loading