From 02c5700c630dba6430bc1003f58dca0c0740d30f Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 27 Mar 2024 23:04:22 +1100 Subject: [PATCH] feat: change apply_rfl tactic so that it does not operate on = (#3784) Previously: If the `rfl` macro was going to fail, it would: 1. expand to `eq_refl`, which is implemented by `Lean.Elab.Tactic.evalRefl`, and call `Lean.MVarId.refl` which would: * either try kernel defeq (if in `.default` or `.all` transparency mode) * otherwise try `IsDefEq` * then fail. 2. Next expand to the `apply_rfl` tactic, which is implemented by `Lean.Elab.Tactic.Rfl.evalApplyRfl`, and call `Lean.MVarId.applyRefl` which would look for lemmas labelled `@[refl]`, and unfortunately in Mathlib find `Eq.refl`, so try applying that (resulting in another `IsDefEq`) 3. Because of an accidental duplication, if `Lean.Elab.Tactic.Rfl` was imported, it would *again* expand to `apply_rfl`. Now: 1. Same behaviour in `eq_refl`. 2. The `@[refl]` attribute will reject `Eq.refl`, and `MVarId.applyRefl` will fail when applied to equality goals. 3. The duplication has been removed. --- src/Init/Tactics.lean | 5 ++-- src/Lean/Elab/Tactic/Rfl.lean | 9 +------- src/Lean/Meta/Tactic/Rfl.lean | 43 ++++++++++++++++++++--------------- tests/lean/run/rewrites.lean | 2 -- 4 files changed, 29 insertions(+), 30 deletions(-) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 2e819f7133..894a15241e 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -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 diff --git a/src/Lean/Elab/Tactic/Rfl.lean b/src/Lean/Elab/Tactic/Rfl.lean index 0ade703419..bfd0f113e0 100644 --- a/src/Lean/Elab/Tactic/Rfl.lean +++ b/src/Lean/Elab/Tactic/Rfl.lean @@ -10,19 +10,12 @@ 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) diff --git a/src/Lean/Meta/Tactic/Rfl.lean b/src/Lean/Meta/Tactic/Rfl.lean index 48195183ca..8cc3e9c9fa 100644 --- a/src/Lean/Meta/Tactic/Rfl.lean +++ b/src/Lean/Meta/Tactic/Rfl.lean @@ -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 @@ -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 @@ -47,29 +50,33 @@ 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 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 + throwError "MVarId.applyRfl does not solve `=` goals. Use `MVarId.refl` instead." 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} @@ -78,7 +85,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 diff --git a/tests/lean/run/rewrites.lean b/tests/lean/run/rewrites.lean index 844bb721e8..df72bb2324 100644 --- a/tests/lean/run/rewrites.lean +++ b/tests/lean/run/rewrites.lean @@ -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: