fc963ffceb
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.
136 lines
5 KiB
Text
136 lines
5 KiB
Text
/-
|
||
Copyright (c) 2022 Newell Jensen. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
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
|
||
|
||
This extends the `rfl` tactic so that it works on any reflexive relation,
|
||
provided the reflexivity lemma has been marked as `@[refl]`.
|
||
-/
|
||
|
||
namespace Lean.Meta.Rfl
|
||
|
||
open Lean Meta
|
||
|
||
/-- Discrimation tree settings for the `refl` extension. -/
|
||
def reflExt.config : WhnfCoreConfig := {}
|
||
|
||
/-- Environment extensions for `refl` lemmas -/
|
||
initialize reflExt :
|
||
SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ←
|
||
registerSimpleScopedEnvExtension {
|
||
addEntry := fun dt (n, ks) => dt.insertCore ks n
|
||
initial := {}
|
||
}
|
||
|
||
initialize registerBuiltinAttribute {
|
||
name := `refl
|
||
descr := "reflexivity relation"
|
||
add := fun decl _ kind => MetaM.run' do
|
||
let declTy := (← getConstInfo decl).type
|
||
let (_, _, targetTy) ← withReducible <| forallMetaTelescopeReducing declTy
|
||
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
|
||
}
|
||
|
||
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, equality or another relation which has a reflexive lemma tagged with the
|
||
attribute [refl].
|
||
-/
|
||
def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext do
|
||
-- NB: uses whnfR, we do not want to unfold the relation itself
|
||
let t ← whnfR <|← instantiateMVars <|← goal.getType
|
||
if t.getAppNumArgs < 2 then
|
||
throwError "rfl can only be used on binary relations, not{indentExpr (← goal.getType)}"
|
||
|
||
-- Special case HEq here as it has a different argument order.
|
||
if t.isAppOfArity ``HEq 4 then
|
||
let gs ← goal.applyConst ``HEq.refl
|
||
unless gs.isEmpty do
|
||
throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
|
||
goalsToMessageData gs}"
|
||
return
|
||
|
||
let rel := t.appFn!.appFn!
|
||
let lhs := t.appFn!.appArg!
|
||
let rhs := t.appArg!
|
||
|
||
let success ← approxDefEq <| isDefEqGuarded lhs rhs
|
||
unless success do
|
||
let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
|
||
let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
|
||
return m!"The lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
|
||
throwTacticEx `apply_rfl goal explanation
|
||
|
||
if rel.isAppOfArity `Eq 1 then
|
||
-- The common case is equality: just use `Eq.refl`
|
||
let us := rel.appFn!.constLevels!
|
||
let α := rel.appArg!
|
||
goal.assign (mkApp2 (mkConst ``Eq.refl us) α lhs)
|
||
else
|
||
-- Else search through `@refl` keyed by the relation
|
||
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
|
||
throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
|
||
goalsToMessageData gs}"
|
||
catch e =>
|
||
unless ex?.isSome do
|
||
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 @[refl] lemma registered for relation{indentExpr rel}"
|
||
|
||
/-- Helper theorem for `Lean.MVarId.liftReflToEq`. -/
|
||
private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}
|
||
{x y : α} (hxy : x = y) (h : R x x) : R x y :=
|
||
hxy ▸ h
|
||
|
||
/--
|
||
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]`.
|
||
If this can't be done, returns the original `MVarId`.
|
||
-/
|
||
def _root_.Lean.MVarId.liftReflToEq (mvarId : MVarId) : MetaM MVarId := do
|
||
mvarId.checkNotAssigned `liftReflToEq
|
||
let .app (.app rel _) _ ← withReducible mvarId.getType' | return mvarId
|
||
if rel.isAppOf `Eq then
|
||
-- No need to lift Eq to Eq
|
||
return mvarId
|
||
for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
|
||
let res ← observing? do
|
||
-- First create an equality relating the LHS and RHS
|
||
-- and reduce the goal to proving that LHS is related to LHS.
|
||
let [mvarIdEq, mvarIdR] ← mvarId.apply (← mkConstWithFreshMVarLevels ``rel_of_eq_and_refl)
|
||
| failure
|
||
-- Then fill in the proof of the latter by reflexivity.
|
||
let [] ← mvarIdR.apply (← mkConstWithFreshMVarLevels lem) | failure
|
||
return mvarIdEq
|
||
if let some mvarIdEq := res then
|
||
return mvarIdEq
|
||
return mvarId
|
||
|
||
end Lean.Meta.Rfl
|