feat: `decide!` tactic for using kernel reduction #5665

kmill · 2024-10-09T23:37:36Z

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:

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
-/

leanprover-community-bot · 2024-10-10T01:13:33Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-5665 has successfully built against this PR. (2024-10-10 01:13:31) View Log
✅ Mathlib branch lean-pr-testing-5665 has successfully built against this PR. (2024-10-10 17:06:40) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8e88e8061a8b497d74f95e2232314c73b335b8a9 --onto d10d41bc07942ca6d8f3081a637045321db15c5a. (2024-10-11 06:44:23)
✅ Mathlib branch lean-pr-testing-5665 has successfully built against this PR. (2024-10-11 06:58:46) View Log

nomeata · 2024-10-10T07:30:50Z

src/Lean/Elab/Tactic/ElabTerm.lean

+    if kernelOnly then
+      -- Reduce the decidable instance to (hopefully!) `isTrue` by passing `pf` to the kernel.
+      -- The `mkAuxLemma` function caches the result in two ways:
+      -- 1. First, the function makes use of a `type`-indexed cache per module.


I wonder if this will still work with parallelism. Also is it not a bit strange to have a per module cache, and penalize users for splitting modules?

How is the matcher caching auxiliary definitions?

I'm not sure whether cross-decide! caching will still be supported with parallelism. I just know that mkAuxLemma is used by simp when processing simp lemmas.

The matcher uses its own cache, and the key function is Lean.Meta.Match.mkMatcherAuxDefinition

Ah, right, you are basically getting this for free by using mkAuxLemma? So whatever will happen to that feature of simp will also happen to decide!. That’s fine.

nomeata · 2024-10-10T15:39:54Z

src/Lean/Parser/Tactic.lean

+- Since it uses kernel reduction instead of elaboratior reduction, it ignores transparancy and can unfold everything.
+- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,
+  and once during kernel type checking), the `decide!` tactic reduces it exactly once.
+- When `decide!` is successful, the result is cached for the current module.


Maybe remove that from the docstring. We don’t want people to relying on that behavior if we don't know if and how that will work post-parallelism.

Suggested change

- When `decide!` is successful, the result is cached for the current module.

Sure. How does leaving the caching test sound, so we know when this finally has broken?

Absolutely!

src/Lean/Parser/Tactic.lean

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`.

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

kmill requested a review from Kha as a code owner October 9, 2024 23:37

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Oct 10, 2024

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 10, 2024

Update lean-toolchain for testing leanprover/lean4#5665

f33ef47

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 10, 2024

Update lean-toolchain for testing leanprover/lean4#5665

5b01a33

leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Oct 10, 2024

nomeata reviewed Oct 10, 2024

View reviewed changes

nomeata approved these changes Oct 10, 2024

View reviewed changes

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 10, 2024

Trigger CI for leanprover/lean4#5665

32c7b0a

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 10, 2024

Trigger CI for leanprover/lean4#5665

1860ed0

kmill commented Oct 11, 2024

View reviewed changes

src/Lean/Parser/Tactic.lean Outdated Show resolved Hide resolved

kmill enabled auto-merge October 11, 2024 05:40

kmill added this pull request to the merge queue Oct 11, 2024

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 11, 2024

Trigger CI for leanprover/lean4#5665

a48482c

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 11, 2024

Trigger CI for leanprover/lean4#5665

ae58e87

kmill removed this pull request from the merge queue due to a manual request Oct 11, 2024

kmill requested review from hargoniX and mhuisi as code owners October 11, 2024 06:19

kmill and others added 5 commits October 10, 2024 23:26

fix test

8683246

remove caching claims from docstring

1af5f4a

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

docstring typos

f0e33d7

fix completionTactics test

b2e3ad9

kmill force-pushed the decidebang branch from 0a32276 to b2e3ad9 Compare October 11, 2024 06:28

kmill enabled auto-merge October 11, 2024 06:29

kmill added this pull request to the merge queue Oct 11, 2024

Merged via the queue into leanprover:master with commit fe0fbc6 Oct 11, 2024
13 checks passed

kmill mentioned this pull request Oct 13, 2024

RFC: decide! tactic variant #5629

Closed

nomeata mentioned this pull request Oct 15, 2024

feat: decide! #5631

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: `decide!` tactic for using kernel reduction #5665

feat: `decide!` tactic for using kernel reduction #5665

kmill commented Oct 9, 2024 •

edited

Loading

leanprover-community-bot commented Oct 10, 2024 •

edited

Loading

nomeata Oct 10, 2024

kmill Oct 10, 2024

nomeata Oct 10, 2024

nomeata Oct 10, 2024

kmill Oct 10, 2024

nomeata Oct 10, 2024

feat: decide! tactic for using kernel reduction #5665

feat: decide! tactic for using kernel reduction #5665

Conversation

kmill commented Oct 9, 2024 • edited Loading

leanprover-community-bot commented Oct 10, 2024 • edited Loading

nomeata Oct 10, 2024

Choose a reason for hiding this comment

kmill Oct 10, 2024

Choose a reason for hiding this comment

nomeata Oct 10, 2024

Choose a reason for hiding this comment

nomeata Oct 10, 2024

Choose a reason for hiding this comment

kmill Oct 10, 2024

Choose a reason for hiding this comment

nomeata Oct 10, 2024

Choose a reason for hiding this comment

feat: `decide!` tactic for using kernel reduction #5665

feat: `decide!` tactic for using kernel reduction #5665

kmill commented Oct 9, 2024 •

edited

Loading

leanprover-community-bot commented Oct 10, 2024 •

edited

Loading