From 4eea57841d1012d6c2edab0f270e433d43f92520 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 3 Sep 2024 21:51:14 +0200 Subject: [PATCH] refactor: rfl tactic: do not use Kernel.isDefEq (#3772) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Sebastian mentioned that the use of the kernel defeq was to work around a performance issue that was fixed since. Let's see if we can do without. This is also a semantic change: Ground terms (no free vars, no mvars) are reduced at “all” transparency even if the the transparency setting is default. This was the case even before 03f6b87647ae79cdca92c5de87a84603eba78b06 switched to the kernel defeq checking for performance. It seems that this is rather surprising behavior from the user point of view. The fallout on batteries and mathlib is rather limited, only a few `rfl` proofs seem to have (inadvertently or not) have relied on this. The speedcenter reports no significant regressions on core or mathlib. --- src/Lean/Meta/Tactic/Refl.lean | 11 +---------- tests/lean/run/4644.lean | 14 +++++++++++--- tests/lean/run/ack.lean | 14 -------------- tests/lean/run/treeNode.lean | 2 +- tests/lean/run/wfirred.lean | 10 +++++++++- 5 files changed, 22 insertions(+), 29 deletions(-) diff --git a/src/Lean/Meta/Tactic/Refl.lean b/src/Lean/Meta/Tactic/Refl.lean index 15ed85289f..5f70029573 100644 --- a/src/Lean/Meta/Tactic/Refl.lean +++ b/src/Lean/Meta/Tactic/Refl.lean @@ -10,12 +10,6 @@ import Lean.Meta.Tactic.Apply namespace Lean.Meta -private def useKernel (lhs rhs : Expr) : MetaM Bool := do - if lhs.hasFVar || lhs.hasMVar || rhs.hasFVar || rhs.hasMVar then - return false - else - return (← getTransparency) matches TransparencyMode.default | TransparencyMode.all - /-- Close given goal using `Eq.refl`. -/ @@ -27,10 +21,7 @@ def _root_.Lean.MVarId.refl (mvarId : MVarId) : MetaM Unit := do throwTacticEx `rfl mvarId m!"equality expected{indentExpr targetType}" let lhs ← instantiateMVars targetType.appFn!.appArg! let rhs ← instantiateMVars targetType.appArg! - let success ← if (← useKernel lhs rhs) then - ofExceptKernelException (Kernel.isDefEq (← getEnv) {} lhs rhs) - else - isDefEq lhs rhs + let success ← isDefEq lhs rhs unless success do throwTacticEx `rfl mvarId m!"equality lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}" let us := targetType.getAppFn.constLevels! diff --git a/tests/lean/run/4644.lean b/tests/lean/run/4644.lean index fd1dc490db..c4c5612a4c 100644 --- a/tests/lean/run/4644.lean +++ b/tests/lean/run/4644.lean @@ -10,9 +10,17 @@ termination_by a.size - i def check_sorted [x: LE α] [DecidableRel x.le] (a: Array α): Bool := sorted_from_var a 0 --- works (because `rfl` of closed terms resorts to kernel defeq, see #3772) -example: check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] := by - rfl +/-- +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. +⊢ check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] = true +-/ +#guard_msgs in +example: check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] = true := by + rfl -- fails because `rfl` uses `.default` transparency, and `sorted_from_var` is marked as irreducible /-- error: tactic 'decide' failed for proposition diff --git a/tests/lean/run/ack.lean b/tests/lean/run/ack.lean index ed2f68c22b..974c4d1e28 100644 --- a/tests/lean/run/ack.lean +++ b/tests/lean/run/ack.lean @@ -25,17 +25,3 @@ set_option diagnostics.threshold 500 in set_option diagnostics true in theorem ex : ack 3 2 = 29 := rfl - - -/-- -info: [kernel] unfolded declarations (max: 1193, num: 4): - [kernel] Nat.casesOn ↦ 1193 - [kernel] Nat.rec ↦ 1065 - [kernel] Eq.ndrec ↦ 973 - [kernel] Eq.rec ↦ 973use `set_option diagnostics.threshold ` to control threshold for reporting counters --/ -#guard_msgs in -set_option diagnostics true in -set_option diagnostics.threshold 800 in -theorem ack_3_2_eq_29 : ack 3 2 = 29 := by - rfl -- uses kernel defeq checker, so only kernel diags shown diff --git a/tests/lean/run/treeNode.lean b/tests/lean/run/treeNode.lean index 77c9bb0090..40f7a318fc 100644 --- a/tests/lean/run/treeNode.lean +++ b/tests/lean/run/treeNode.lean @@ -37,5 +37,5 @@ theorem length_treeToList_eq_numNames (t : TreeNode) : (treeToList t).length = n where helper (cs : List TreeNode) : (cs.map treeToList).join.length = numNamesLst cs := by match cs with - | [] => rfl + | [] => simp [List.join, numNamesLst] | c::cs' => simp [List.join, List.map, numNamesLst, length_treeToList_eq_numNames c, helper cs'] diff --git a/tests/lean/run/wfirred.lean b/tests/lean/run/wfirred.lean index ee96ba698a..89fbfcbc9f 100644 --- a/tests/lean/run/wfirred.lean +++ b/tests/lean/run/wfirred.lean @@ -29,7 +29,15 @@ but is expected to have type #guard_msgs in example : foo (n+1) = foo n := rfl --- This succeeding is a bug or misfeature in the rfl tactic, using the kernel defeq check +-- also for closed terms +/-- +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. +⊢ foo 0 = 0 +-/ #guard_msgs in example : foo 0 = 0 := by rfl