Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 5 commits into from
Mar 27, 2024
Merged

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

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
2d67075
feat: change apply_rfl tactic so that it does not operate on =
kim-em Mar 27, 2024
de0b388
fix test
kim-em Mar 27, 2024
2d41692
just don't do equality
kim-em Mar 27, 2024
aba38d1
fix
kim-em Mar 27, 2024
d7140a0
Merge remote-tracking branch 'origin/master' into refl_duplication
kim-em Mar 27, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions src/Init/Tactics.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -377,8 +377,9 @@ macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)

/--
This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
This tactic applies to a goal whose target has the form `x ~ x`,
where `~` is a reflexive relation other than `=`,
that is, a relation which has a reflexive lemma tagged with the attribute @[refl].
-/
syntax (name := applyRfl) "apply_rfl" : tactic

Expand Down
13 changes: 4 additions & 9 deletions src/Lean/Elab/Tactic/Rfl.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,22 +10,17 @@ import Lean.Elab.Tactic.Basic
/-!
# `rfl` tactic extension for reflexive relations

This extends the `rfl` tactic so that it works on any reflexive relation,
This extends the `rfl` tactic so that it works on reflexive relations other than `=`,
provided the reflexivity lemma has been marked as `@[refl]`.
-/

namespace Lean.Elab.Tactic.Rfl

/--
This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
-/
elab_rules : tactic
| `(tactic| rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)

@[builtin_tactic Lean.Parser.Tactic.applyRfl] def evalApplyRfl : Tactic := fun stx =>
match stx with
| `(tactic| apply_rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)
-- We call `applyRfl` with `failOnEq := true`,
-- so that this does not do duplicative work when called on an `=` goal from `rfl`.
| `(tactic| apply_rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl true)
| _ => throwUnsupportedSyntax

end Lean.Elab.Tactic.Rfl
48 changes: 29 additions & 19 deletions src/Lean/Meta/Tactic/Rfl.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ Authors: Newell Jensen, Thomas Murrills
prelude
import Lean.Meta.Tactic.Apply
import Lean.Elab.Tactic.Basic
import Lean.Meta.Tactic.Refl

/-!
# `rfl` tactic extension for reflexive relations
Expand Down Expand Up @@ -38,6 +39,8 @@ initialize registerBuiltinAttribute {
let fail := throwError
"@[refl] attribute only applies to lemmas proving x ∼ x, got {declTy}"
let .app (.app rel lhs) rhs := targetTy | fail
if let .app (.const ``Eq [_]) _ := rel then
throwError "@[refl] attribute may not be used on `Eq.refl`."
unless ← withNewMCtxDepth <| isDefEq lhs rhs do fail
let key ← DiscrTree.mkPath rel reflExt.config
reflExt.add (decl, key) kind
Expand All @@ -47,29 +50,36 @@ open Elab Tactic

/-- `MetaM` version of the `rfl` tactic.

This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
This tactic applies to a goal whose target has the form `x ~ x`,
where `~` is a reflexive relation other than `=`,
that is, a relation which has a reflexive lemma tagged with the attribute @[refl].
-/
def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := do
def _root_.Lean.MVarId.applyRfl (goal : MVarId) (failOnEq : Bool := false) : MetaM Unit := do
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we have a use case for failOnEq := false?

It seems we have

  • End users calling rfl. They don’t need it.
  • Tactics or Meta use that wants to work on Eq only. They can use eq_refl or with_reducible eq_refl resp. MVarId.refl or withReducible MVarId.refl as suitable.

Who wants to use MVarId.applyRfl, wants to handle more than Eq, but also wants to handle Eq, and can’t go via the rfl tactic?

(Also note that .applyRfl still behaves different than the rfl tactic. All very confusing.)

Preventing users from registering Eq.refl is fine.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess I can grep mathlib myself…

There is

def rflTac : TacticM Unit :=
  withMainContext do liftMetaFinishingTactic (·.applyRfl)

which is corresponds to

src/Lean/Elab/Tactic/Rfl.lean:  | `(tactic| apply_rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)

in core.

It is used in

attribute [aesop safe tactic (rule_sets := [CategoryTheory])] Mathlib.Tactic.rflTac

Then there is

/-- See if the term is `a = b` and the goal is `a ∼ b` or `b ∼ a`, with `∼` reflexive. -/
@[gcongr_forward] def exactRefl : ForwardExt where
  eval h goal := do
    let m ← mkFreshExprMVar none
    goal.assignIfDefeq (← mkAppOptM ``Eq.subst #[h, m])
    goal.applyRfl

in Mathlib/Tactic/GCongr/Core.lean. I’m not entirely sure, but it seems that here you don’t want to handle also Eq.

There is also

withReducible (← mkFreshExprMVar r.result.eNew).mvarId!.applyRfl

in Mathlib/Tactic/Rewrites.lean. Upstreamed and fixed with #3783.

And finally in rw_search we have

/-- Check whether a goal can be solved by `rfl`, and fill in the `SearchNode.rfl?` field. -/
def compute_rfl? (n : SearchNode) : MetaM SearchNode := withMCtx n.mctx do
  if (← try? n.goal.applyRfl).isSome then

and I wonder if that really wants to use applyRfl, and not .refl instead.

Hyrum’s law is strong again :-)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this last one does want to use applyRfl, or at least there are test cases that expect it, so they can discharge Iff goals...

So when this PR lands, it will again break rw_search, and I'll patch it up to try .refl and then .applyRfl....

let .app (.app rel _) _ ← whnfR <|← instantiateMVars <|← goal.getType
| throwError "reflexivity lemmas only apply to binary relations, not{
indentExpr (← goal.getType)}"
let s ← saveState
let mut ex? := none
for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
try
let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
if gs.isEmpty then return () else
logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
goalsToMessageData gs}"
catch e =>
ex? := ex? <|> (some (← saveState, e)) -- stash the first failure of `apply`
s.restore
if let some (sErr, e) := ex? then
sErr.restore
throw e
if let .app (.const ``Eq [_]) _ := rel then
if failOnEq then
throwError "MVarId.applyRfl fails on equality goals when `failOnEq` is true"
else
goal.refl
else
throwError "rfl failed, no lemma with @[refl] applies"
let s ← saveState
let mut ex? := none
for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
try
let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
if gs.isEmpty then return () else
logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
goalsToMessageData gs}"
catch e =>
ex? := ex? <|> (some (← saveState, e)) -- stash the first failure of `apply`
s.restore
if let some (sErr, e) := ex? then
sErr.restore
throw e
else
throwError "rfl failed, no lemma with @[refl] applies"

/-- Helper theorem for `Lean.MVarId.liftReflToEq`. -/
private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}
Expand All @@ -78,7 +88,7 @@ private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}

/--
Convert a goal of the form `x ~ y` into the form `x = y`, where `~` is a reflexive
relation, that is, a relation which has a reflexive lemma tagged with the attribute `[refl]`.
relation, that is, a relation which has a reflexive lemma tagged with the attribute `@[refl]`.
If this can't be done, returns the original `MVarId`.
-/
def _root_.Lean.MVarId.liftReflToEq (mvarId : MVarId) : MetaM MVarId := do
Expand Down
2 changes: 0 additions & 2 deletions tests/lean/run/rewrites.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@
attribute [refl] Eq.refl

private axiom test_sorry : ∀ {α}, α

-- To see the (sorted) list of lemmas that `rw?` will try rewriting by, use:
Expand Down