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

nomeata · 2024-03-19T09:25:09Z

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

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.

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.

leanprover-community-mathlib4-bot · 2024-03-19T09:43:25Z

Mathlib CI status (docs):

❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-03-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-03-19 09:43:25)
❌ Mathlib branch lean-pr-testing-3714 built against this PR, but linting failed. (2024-03-19 13:33:57) View Log
❌ Mathlib branch lean-pr-testing-3714 built against this PR, but linting failed. (2024-03-19 13:52:24) View Log
💥 Mathlib branch lean-pr-testing-3714 build failed against this PR. (2024-09-10 07:58:17) View Log
💥 Mathlib branch lean-pr-testing-3714 build failed against this PR. (2024-09-10 09:17:09) View Log
❌ Mathlib branch lean-pr-testing-3714 built against this PR, but the archive failed. (2024-09-10 11:10:48) View Log
✅ Mathlib branch lean-pr-testing-3714 has successfully built against this PR. (2024-09-10 14:27:39) View Log
✅ Mathlib branch lean-pr-testing-3714 has successfully built against this PR. (2024-09-11 09:49:40) View Log
✅ Mathlib branch lean-pr-testing-3714 has successfully built against this PR. (2024-09-13 10:57:06) View Log
✅ Mathlib branch lean-pr-testing-3714 has successfully built against this PR. (2024-09-14 10:38:21) View Log
💥 Mathlib branch lean-pr-testing-3714 build failed against this PR. (2024-09-15 22:12:07) View Log
❌ Mathlib branch lean-pr-testing-3714 built against this PR, but the archive failed. (2024-09-16 09:17:29) View Log
✅ Mathlib branch lean-pr-testing-3714 has successfully built against this PR. (2024-09-16 10:42:54) View Log
✅ Mathlib branch lean-pr-testing-3714 has successfully built against this PR. (2024-09-16 11:51:14) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e417ad8a704fcc1b5b4e6fb316fbe0ae739fb586 --onto 77cd700fa877033316046f463f4c1b455b4498d2. (2024-09-18 20:04:22)
❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-09-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-09-19 14:29:29)
💥 Mathlib branch lean-pr-testing-3714 build failed against this PR. (2024-09-19 15:23:45) View Log
✅ Mathlib branch lean-pr-testing-3714 has successfully built against this PR. (2024-09-19 17:48:38) View Log

digama0 · 2024-03-19T12:16:32Z

src/Lean/Meta/Tactic/Rfl.lean

+      throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
+        goalsToMessageData gs}"


this seems like it should be a function somewhere

src/Lean/Meta/Tactic/Rfl.lean

builds upon #3714

nomeata · 2024-03-19T21:39:47Z

Ah, interesting: The eq_refl tactic reduces the goal with the current transparency (whnf) before it checks if it is an Eq, while the extensible apply_rfl tactic reduces the goal only with reducible transparency (whnfR) before consulting the the @[refl] lemmas. This PR currently tries to do the whnfR same in both cases, but of course that breaks existing proofs.

So I should adjust this code to do these things as well (reduce with whnf, check if it is Eq, IfforHEq, handle that, else re-reduce with whnfR`, and handle that) to not have to chance down breakages.

nomeata · 2024-03-20T09:36:00Z

This is a bit unfortunate: since a given goal can look quite different under whnf and whnfR, in general there are also two different lhs/rhs pairs that need to be compared. And thus in the failure case, a comprehensive error message would have to somehow explain thas, requiring an annoying amount of code.

Given prominence of rfl, it's probably still with it…

(The alternative of using either whnf or whnfR exclusively is likely too disruptive…)

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).

the `rfl` was a bit of a defeq abuse: The goal was `StateEqRs a b` for definitely different terms `a` and `b`, but it was still using `StateEqRs.refl a`, because then after unfolding `StateEqRs` and doing a bit of computation the proof held. This would break once leanprover/lean4#3714 lands, and is a bit fishy in any case so let's just let `simp` handle it.

…l-errors

…-errors

This reverts commit c972bcb.

…l-errors

…acro

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 requested a review from leodemoura as a code owner March 19, 2024 09:25

nomeata added the awaiting-review Waiting for someone to review the PR label Mar 19, 2024

nomeata mentioned this pull request Mar 19, 2024

RFC: A single rfl tactic implementation #3302

Closed

nomeata requested a review from digama0 March 19, 2024 09:30

github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 19, 2024 09:38 Inactive

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 19, 2024

nomeata changed the title ~~feat: apply_rfl tactic: Handle Eq~~ feat: apply_rfl tactic: handle Eq, HEq, better error messages Mar 19, 2024

digama0 reviewed Mar 19, 2024

View reviewed changes

src/Lean/Meta/Tactic/Rfl.lean Outdated Show resolved Hide resolved

nomeata added 2 commits March 19, 2024 13:22

Update src/Lean/Meta/Tactic/Rfl.lean

0dd354f

Update Rfl.lean

3cbfc42

github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 19, 2024 12:35 Inactive

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 19, 2024

Update lean-toolchain for testing leanprover/lean4#3714

d4d4d6b

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 19, 2024

Update lean-toolchain for testing leanprover/lean4#3714

d55bafb

nomeata added a commit that referenced this pull request Mar 19, 2024

refactor: let rfl tactic deal with Iff via @[refl]

09a7c21

builds upon #3714

nomeata mentioned this pull request Mar 19, 2024

refactor: back rfl tactic primarily via apply_rfl #3718

Merged

nomeata removed the awaiting-review Waiting for someone to review the PR label Mar 19, 2024

leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 19, 2024

github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 19, 2024 13:36 Inactive

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 19, 2024

Trigger CI for leanprover/lean4#3714

729f632

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 19, 2024

Trigger CI for leanprover/lean4#3714

2f0e4e1

This was referenced Mar 26, 2024

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

Merged

chore: add refl attribute to Eq.refl #3773

Closed

kim-em mentioned this pull request Mar 27, 2024

feat: change apply_rfl tactic so that it does not operate on = #3784

Merged

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 16, 2024

Update lean-toolchain for testing leanprover/lean4#3714

a949d3d

Trigger stage0 update after merge

52cdde3

nomeata mentioned this pull request Sep 16, 2024

chore: ensure that the rfl tactic tries Iff.rfl #5359

Merged

leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Sep 16, 2024

github-actions bot temporarily deployed to lean-lang.org/lean4/doc September 16, 2024 10:45 Inactive

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 16, 2024

Trigger CI for leanprover/lean4#3714

8dfddc4

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 16, 2024

Trigger CI for leanprover/lean4#3714

321f629

nomeata added 8 commits September 18, 2024 14:41

Merge branch 'nightly' of github.com:leanprover/lean4 into joachim/rf…

449506b

…l-errors

Merge branch 'master' of github.com:leanprover/lean4 into joachim/rfl…

9f0636c

…-errors

Do not use isDefEqGuarded

c972bcb

Remove exact Iff.rfl macro

802fa76

Revert "Do not use isDefEqGuarded"

85f50e8

This reverts commit c972bcb.

Update test

fa5b6e2

Merge branch 'nightly' of github.com:leanprover/lean4 into joachim/rf…

e351221

…l-errors

Actually, let's not get this PR entangled with removing the Iff.rfl m…

bb5b28d

…acro

github-actions bot temporarily deployed to lean-lang.org/lean4/doc September 19, 2024 14:13 Inactive

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 19, 2024

Trigger CI for leanprover/lean4#3714

a0a5efc

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 19, 2024

Trigger CI for leanprover/lean4#3714

e3e8e9b

leanprover-community-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Sep 19, 2024

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 19, 2024

Trigger CI for leanprover/lean4#3714

c2cf542

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 19, 2024

Update lean-toolchain for testing leanprover/lean4#3714

fbfd4df

leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Sep 19, 2024

nomeata added this pull request to the merge queue Sep 20, 2024

Merged via the queue into master with commit fc963ff Sep 20, 2024
21 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

nomeata commented Mar 19, 2024 •

edited

Loading

leanprover-community-mathlib4-bot commented Mar 19, 2024 •

edited by leanprover-community-bot

Loading

digama0 Mar 19, 2024

nomeata commented Mar 19, 2024

nomeata commented Mar 20, 2024

		throwError MessageData.tagged `Tactic.unsolvedGoals <\| m!"unsolved goals\n{
		goalsToMessageData gs}"

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

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

Conversation

nomeata commented Mar 19, 2024 • edited Loading

leanprover-community-mathlib4-bot commented Mar 19, 2024 • edited by leanprover-community-bot Loading

digama0 Mar 19, 2024

Choose a reason for hiding this comment

nomeata commented Mar 19, 2024

nomeata commented Mar 20, 2024

nomeata commented Mar 19, 2024 •

edited

Loading

leanprover-community-mathlib4-bot commented Mar 19, 2024 •

edited by leanprover-community-bot

Loading