From fc963ffceb9b34d327efaece3174e034636462ff Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 20 Sep 2024 10:25:10 +0200 Subject: [PATCH] feat: apply_rfl tactic: handle Eq, HEq, better error messages (#3714) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- src/Lean/Meta/Tactic/Refl.lean | 3 + src/Lean/Meta/Tactic/Rfl.lean | 50 ++- stage0/src/stdlib_flags.h | 2 + tests/lean/run/rflApplyFoApprox.lean | 15 + tests/lean/run/rflTacticErrors.lean | 445 +++++++++++++++++++++++++++ 5 files changed, 503 insertions(+), 12 deletions(-) create mode 100644 tests/lean/run/rflApplyFoApprox.lean create mode 100644 tests/lean/run/rflTacticErrors.lean diff --git a/src/Lean/Meta/Tactic/Refl.lean b/src/Lean/Meta/Tactic/Refl.lean index 5f70029573..597735c782 100644 --- a/src/Lean/Meta/Tactic/Refl.lean +++ b/src/Lean/Meta/Tactic/Refl.lean @@ -12,6 +12,9 @@ namespace Lean.Meta /-- Close given goal using `Eq.refl`. + +See `Lean.MVarId.applyRfl` for the variant that also consults `@[refl]` lemmas, and which +backs the `rfl` tactic. -/ def _root_.Lean.MVarId.refl (mvarId : MVarId) : MetaM Unit := do mvarId.withContext do diff --git a/src/Lean/Meta/Tactic/Rfl.lean b/src/Lean/Meta/Tactic/Rfl.lean index 8cc3e9c9fa..9b683cef2c 100644 --- a/src/Lean/Meta/Tactic/Rfl.lean +++ b/src/Lean/Meta/Tactic/Rfl.lean @@ -50,33 +50,59 @@ 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 other than `=`, -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, 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 := do - let .app (.app rel _) _ ← whnfR <|← instantiateMVars <|← goal.getType - | throwError "reflexivity lemmas only apply to binary relations, not{ - indentExpr (← goal.getType)}" - if let .app (.const ``Eq [_]) _ := rel then - throwError "MVarId.applyRfl does not solve `=` goals. Use `MVarId.refl` instead." +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 - logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{ + throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{ goalsToMessageData gs}" catch e => - ex? := ex? <|> (some (← saveState, e)) -- stash the first failure of `apply` + 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 lemma with @[refl] applies" + 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} diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 0699845ba4..f636bca698 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -18,3 +18,5 @@ options get_default_options() { return opts; } } + +// please update stage0 diff --git a/tests/lean/run/rflApplyFoApprox.lean b/tests/lean/run/rflApplyFoApprox.lean new file mode 100644 index 0000000000..9a807cfa7e --- /dev/null +++ b/tests/lean/run/rflApplyFoApprox.lean @@ -0,0 +1,15 @@ + +opaque f : Nat → Nat +-- A rewrite with a free variable on the RHS + +opaque P : Nat → (Nat → Nat) → Prop +opaque Q : Nat → Prop +opaque foo (g : Nat → Nat) (x : Nat) : P x f ↔ Q (g x) := sorry + +example : P x f ↔ Q (x + 10) := by + rewrite [foo] + -- we have an mvar now + with_reducible rfl -- should should instantiate it with the lambda on the RHS and close the goal + -- same as + -- with_reducible (apply (Iff.refl _)) + -- NB: apply, not exact! Different defEq flags. diff --git a/tests/lean/run/rflTacticErrors.lean b/tests/lean/run/rflTacticErrors.lean new file mode 100644 index 0000000000..bf916b8fd0 --- /dev/null +++ b/tests/lean/run/rflTacticErrors.lean @@ -0,0 +1,445 @@ + +/-! +This file tests the `rfl` tactic: + * Extensibility + * Error messages + * Effect of `with_reducible` +-/ + +-- First, let's see what `rfl` does: + +/-- +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 reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or +`exact HEq.rfl` etc. +⊢ false = true +-/ +#guard_msgs in +example : false = true := by rfl + +-- Now to `apply_rfl`. + +-- A plain reflexive predicate +inductive P : α → α → Prop where | refl : P a a +attribute [refl] P.refl + +-- Plain error + +/-- +error: tactic 'apply_rfl' failed, The lhs + 42 +is not definitionally equal to rhs + 23 +⊢ P 42 23 +-/ +#guard_msgs in +example : P 42 23 := by apply_rfl + +-- Revealing implicit arguments + +opaque withImplicitNat {n : Nat} : Nat + +/-- +error: tactic 'apply_rfl' failed, The lhs + @withImplicitNat 42 +is not definitionally equal to rhs + @withImplicitNat 23 +⊢ P withImplicitNat withImplicitNat +-/ +#guard_msgs in +example : P (@withImplicitNat 42) (@withImplicitNat 23) := by apply_rfl + + +-- Exhaustive testing of various combinations: + +-- In addition to Eq, HEq and Iff we test four relations: + + +-- Defeq to relation `P` at reducible transparency +abbrev Q : α → α → Prop := P + +-- Defeq to relation `P` at default transparency +def Q' : α → α → Prop := P + +-- No refl attribute +inductive R : α → α → Prop where | refl : R a a + + +/- +Now we systematically test all relations with +* syntactic equal arguments +* reducibly equal arguments +* semireducibly equal arguments +* nonequal arguments + +and all using `apply_rfl` and `with_reducible apply_rfl` +-/ + + +-- Syntactic equal + +example : true = true := by apply_rfl +example : HEq true true := by apply_rfl +example : True ↔ True := by apply_rfl +example : P true true := by apply_rfl +example : Q true true := by apply_rfl +/-- +error: rfl failed, no @[refl] lemma registered for relation + Q' +-/ +#guard_msgs in example : Q' true true := by apply_rfl -- Error +/-- +error: rfl failed, no @[refl] lemma registered for relation + R +-/ +#guard_msgs in example : R true true := by apply_rfl -- Error + +example : true = true := by with_reducible apply_rfl +example : HEq true true := by with_reducible apply_rfl +example : True ↔ True := by with_reducible apply_rfl +example : P true true := by with_reducible apply_rfl +example : Q true true := by with_reducible apply_rfl +/-- +error: rfl failed, no @[refl] lemma registered for relation + Q' +-/ +#guard_msgs in +example : Q' true true := by with_reducible apply_rfl -- Error +/-- +error: rfl failed, no @[refl] lemma registered for relation + R +-/ +#guard_msgs in +example : R true true := by with_reducible apply_rfl -- Error + +-- Reducibly equal + +abbrev true' := true +abbrev True' := True + +example : true' = true := by apply_rfl +example : HEq true' true := by apply_rfl +example : True' ↔ True := by apply_rfl +example : P true' true := by apply_rfl +example : Q true' true := by apply_rfl +/-- +error: rfl failed, no @[refl] lemma registered for relation + Q' +-/ +#guard_msgs in +example : Q' true' true := by apply_rfl -- Error +/-- +error: rfl failed, no @[refl] lemma registered for relation + R +-/ +#guard_msgs in +example : R true' true := by apply_rfl -- Error + +example : true' = true := by with_reducible apply_rfl +example : HEq true' true := by with_reducible apply_rfl +example : True' ↔ True := by with_reducible apply_rfl +example : P true' true := by with_reducible apply_rfl +example : Q true' true := by with_reducible apply_rfl -- NB: No error, Q and true' reducible +/-- +error: rfl failed, no @[refl] lemma registered for relation + Q' +-/ +#guard_msgs in +example : Q' true' true := by with_reducible apply_rfl -- Error +/-- +error: rfl failed, no @[refl] lemma registered for relation + R +-/ +#guard_msgs in +example : R true' true := by with_reducible apply_rfl -- Error + +-- Equal at default transparency only + +def true'' := true +def True'' := True + +example : true'' = true := by apply_rfl +example : HEq true'' true := by apply_rfl +example : True'' ↔ True := by apply_rfl +example : P true'' true := by apply_rfl +example : Q true'' true := by apply_rfl +/-- +error: rfl failed, no @[refl] lemma registered for relation + Q' +-/ +#guard_msgs in +example : Q' true'' true := by apply_rfl -- Error +/-- +error: rfl failed, no @[refl] lemma registered for relation + R +-/ +#guard_msgs in +example : R true'' true := by apply_rfl -- Error + +/-- +error: tactic 'apply_rfl' failed, The lhs + true'' +is not definitionally equal to rhs + true +⊢ true'' = true +-/ +#guard_msgs in +example : true'' = true := by with_reducible apply_rfl -- Error +/-- +error: tactic 'apply' failed, failed to unify + @HEq ?α ?a ?α ?a +with + @HEq Bool true'' Bool true +⊢ HEq true'' true +-/ +#guard_msgs in +example : HEq true'' true := by with_reducible apply_rfl -- Error +/-- +error: tactic 'apply_rfl' failed, The lhs + True'' +is not definitionally equal to rhs + True +⊢ True'' ↔ True +-/ +#guard_msgs in +example : True'' ↔ True := by with_reducible apply_rfl -- Error +/-- +error: tactic 'apply_rfl' failed, The lhs + true'' +is not definitionally equal to rhs + true +⊢ P true'' true +-/ +#guard_msgs in +example : P true'' true := by with_reducible apply_rfl -- Error +/-- +error: tactic 'apply_rfl' failed, The lhs + true'' +is not definitionally equal to rhs + true +⊢ Q true'' true +-/ +#guard_msgs in +example : Q true'' true := by with_reducible apply_rfl -- Error +/-- +error: tactic 'apply_rfl' failed, The lhs + true'' +is not definitionally equal to rhs + true +⊢ Q' true'' true +-/ +#guard_msgs in +example : Q' true'' true := by with_reducible apply_rfl -- Error +/-- +error: tactic 'apply_rfl' failed, The lhs + true'' +is not definitionally equal to rhs + true +⊢ R true'' true +-/ +#guard_msgs in +example : R true'' true := by with_reducible apply_rfl -- Error + +-- Unequal +/-- +error: tactic 'apply_rfl' failed, The lhs + false +is not definitionally equal to rhs + true +⊢ false = true +-/ +#guard_msgs in +example : false = true := by apply_rfl -- Error +/-- +error: tactic 'apply' failed, failed to unify + HEq ?a ?a +with + HEq false true +⊢ HEq false true +-/ +#guard_msgs in +example : HEq false true := by apply_rfl -- Error +/-- +error: tactic 'apply_rfl' failed, The lhs + False +is not definitionally equal to rhs + True +⊢ False ↔ True +-/ +#guard_msgs in +example : False ↔ True := by apply_rfl -- Error +/-- +error: tactic 'apply_rfl' failed, The lhs + false +is not definitionally equal to rhs + true +⊢ P false true +-/ +#guard_msgs in +example : P false true := by apply_rfl -- Error +/-- +error: tactic 'apply_rfl' failed, The lhs + false +is not definitionally equal to rhs + true +⊢ Q false true +-/ +#guard_msgs in +example : Q false true := by apply_rfl -- Error +/-- +error: tactic 'apply_rfl' failed, The lhs + false +is not definitionally equal to rhs + true +⊢ Q' false true +-/ +#guard_msgs in +example : Q' false true := by apply_rfl -- Error +/-- +error: tactic 'apply_rfl' failed, The lhs + false +is not definitionally equal to rhs + true +⊢ R false true +-/ +#guard_msgs in +example : R false true := by apply_rfl -- Error + +/-- +error: tactic 'apply_rfl' failed, The lhs + false +is not definitionally equal to rhs + true +⊢ false = true +-/ +#guard_msgs in +example : false = true := by with_reducible apply_rfl -- Error +/-- +error: tactic 'apply' failed, failed to unify + HEq ?a ?a +with + HEq false true +⊢ HEq false true +-/ +#guard_msgs in +example : HEq false true := by with_reducible apply_rfl -- Error +/-- +error: tactic 'apply_rfl' failed, The lhs + False +is not definitionally equal to rhs + True +⊢ False ↔ True +-/ +#guard_msgs in +example : False ↔ True := by with_reducible apply_rfl -- Error +/-- +error: tactic 'apply_rfl' failed, The lhs + false +is not definitionally equal to rhs + true +⊢ P false true +-/ +#guard_msgs in +example : P false true := by with_reducible apply_rfl -- Error +/-- +error: tactic 'apply_rfl' failed, The lhs + false +is not definitionally equal to rhs + true +⊢ Q false true +-/ +#guard_msgs in +example : Q false true := by with_reducible apply_rfl -- Error +/-- +error: tactic 'apply_rfl' failed, The lhs + false +is not definitionally equal to rhs + true +⊢ Q' false true +-/ +#guard_msgs in +example : Q' false true := by with_reducible apply_rfl -- Error +/-- +error: tactic 'apply_rfl' failed, The lhs + false +is not definitionally equal to rhs + true +⊢ R false true +-/ +#guard_msgs in +example : R false true := by with_reducible apply_rfl -- Error + +-- Inheterogeneous unequal + +/-- +error: tactic 'apply' failed, failed to unify + HEq ?a ?a +with + HEq true 1 +⊢ HEq true 1 +-/ +#guard_msgs in +example : HEq true 1 := by apply_rfl -- Error +/-- +error: tactic 'apply' failed, failed to unify + HEq ?a ?a +with + HEq true 1 +⊢ HEq true 1 +-/ +#guard_msgs in +example : HEq true 1 := by with_reducible apply_rfl -- Error + +-- Rfl lemma with side condition: +-- Error message should show left-over goal + +inductive S : Bool → Bool → Prop where | refl : a = true → S a a +attribute [refl] S.refl +/-- +error: tactic 'apply_rfl' failed, The lhs + true +is not definitionally equal to rhs + false +⊢ S true false +-/ +#guard_msgs in +example : S true false := by apply_rfl -- Error +/-- +error: tactic 'apply_rfl' failed, The lhs + true +is not definitionally equal to rhs + false +⊢ S true false +-/ +#guard_msgs in +example : S true false := by with_reducible apply_rfl -- Error +/-- +error: unsolved goals +case a +⊢ true = true +-/ +#guard_msgs in +example : S true true := by apply_rfl -- Error (left-over goal) +/-- +error: unsolved goals +case a +⊢ true = true +-/ +#guard_msgs in +example : S true true := by with_reducible apply_rfl -- Error (left-over goal) +/-- +error: unsolved goals +case a +⊢ false = true +-/ +#guard_msgs in +example : S false false := by apply_rfl -- Error (left-over goal) +/-- +error: unsolved goals +case a +⊢ false = true +-/ +#guard_msgs in +example : S false false := by with_reducible apply_rfl -- Error (left-over goal)