RFC: decide! tactic variant #5629
Comments
|
There's an inconsistency here with the meaning of This need not block using |
|
Thanks, I didn’t know that! Maybe it’s generally a bad habit to just reach for |
The `decide!` tactic is like `decide`, but when it tries reducing the `Decidable` instance it uses kernel reduction rather than the elaborator's reduction. The kernel ignores transparency, so it can unfold all definitions. Furthermore, by using kernel reduction we can cache the result as an auxiliary lemma — this is more efficient than `decide`, which needs to reduce the instance once in the elaborator to check whether the tactic suceeds, and once again in the kernel during final typechecking. This implements a variant of RFC leanprover#5629, which proposes instead to skip checking altogether during elaboration. With this PR's `decide`, we can use `decide!` as more-or-less a drop-in replacement for `decide`.
The `decide!` tactic is like `decide`, but when it tries reducing the `Decidable` instance it uses kernel reduction rather than the elaborator's reduction. The kernel ignores transparency, so it can unfold all definitions. Furthermore, by using kernel reduction we can cache the result as an auxiliary lemma — this is more efficient than `decide`, which needs to reduce the instance once in the elaborator to check whether the tactic suceeds, and once again in the kernel during final typechecking. This implements a variant of RFC leanprover#5629, which proposes instead to skip checking altogether during elaboration. With this PR's `decide`, we can use `decide!` as more-or-less a drop-in replacement for `decide`.
The `decide!` tactic is like `decide`, but when it tries reducing the `Decidable` instance it uses kernel reduction rather than the elaborator's reduction. The kernel ignores transparency, so it can unfold all definitions. Furthermore, by using kernel reduction we can cache the result as an auxiliary lemma — this is more efficient than `decide`, which needs to reduce the instance once in the elaborator to check whether the tactic suceeds, and once again in the kernel during final typechecking. This implements a variant of RFC leanprover#5629, which proposes instead to skip checking altogether during elaboration. With this PR's `decide`, we can use `decide!` as more-or-less a drop-in replacement for `decide`.
The `decide!` tactic is like `decide`, but when it tries reducing the `Decidable` instance it uses kernel reduction rather than the elaborator's reduction. The kernel ignores transparency, so it can unfold all definitions (for better or for worse). Furthermore, by using kernel reduction we can cache the result as an auxiliary lemma — this is more efficient than `decide`, which needs to reduce the instance twice: once in the elaborator to check whether the tactic succeeds, and once again in the kernel during final typechecking. While RFC #5629 proposes a `decide!` that skips checking altogether during elaboration, with this PR's `decide!` we can use `decide!` as more-or-less a drop-in replacement for `decide`, since the tactic will fail if kernel reduction fails. This PR also includes two small fixes: - `blameDecideReductionFailure` now uses `withIncRecDepth`. - `Lean.Meta.zetaReduce` now instantiates metavariables while zeta reducing. Some profiling: ```lean set_option maxRecDepth 2000 set_option trace.profiler true set_option trace.profiler.threshold 0 theorem thm1 : 0 < 1 := by decide! theorem thm1' : 0 < 1 := by decide theorem thm2 : ∀ x < 400, x * x ≤ 160000 := by decide! theorem thm2' : ∀ x < 400, x * x ≤ 160000 := by decide /- [Elab.command] [0.003655] theorem thm1 : 0 < 1 := by decide! [Elab.command] [0.003164] theorem thm1' : 0 < 1 := by decide [Elab.command] [0.133223] theorem thm2 : ∀ x < 400, x * x ≤ 160000 := by decide! [Elab.command] [0.252310] theorem thm2' : ∀ x < 400, x * x ≤ 160000 := by decide -/ ``` --------- Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
|
With #5665 we now have a version of There are some ways that
|
|
Yes, please close this (and feel free to do it yourself, so that credit goes where credit is due). I thought I edited that PRs description so that it would do it, but maybe didn't save. I don't know much about the lean3 feature. Are people asking for it? Could it be the default behavior to always revert (maybe with a good explanation that this happened if no instance is found)? |
|
@nomeata There are some cases where |
|
Thats also plausible. Are there situations when reverting is not the right thing to do for |
Proposal
In the
equational_theoriesproject there are many script-generated theorems with essentiallyby decideas the proof. In theses cases, we really know that thedecidetactic will succeed (if not there is a bug somewhere), and it’s silly fordecideto first run the decision procedure at elaboration time, and then again in the kernel.Thus I propose to add a
decide!variant of the tactic that causes this check to be skipped:lean4/src/Lean/Elab/Tactic/ElabTerm.lean
Lines 404 to 405 in 01d414a
This halfs the processing time of such files.
(The equational_theories project is currently using a tactic that has this effect.)
Community Feedback
(none yet)
Impact
Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: