feat: nested well-founded recursion via automatic preprocessing #6744

nomeata · 2025-01-22T17:25:09Z

This PR extend the preprocessing of well-founded recursive definitions to bring assumptions like h✝ : x ∈ xs into scope automatically.

This fixes #5471, and follows (roughly) the design written there.
See the module docs at src/Lean/Elab/PreDefinition/WF/AutoAttach.lean for details on the implementation.

This only works for higher-order functions that have a suitable setup. See for example section “Well-founded recursion preprocessing setup” in src/Init/Data/List/Attach.lean.

This does not change the decreasing_tactic, so in some cases there is still the need for a manual termination proof some cases. We expect a better termination tactic in the near future.

leanprover-community-bot · 2025-01-22T18:49:28Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-6744 build failed against this PR. (2025-01-22 18:49:27) View Log
💥 Mathlib branch lean-pr-testing-6744 build failed against this PR. (2025-01-23 11:35:04) View Log
✅ Mathlib branch lean-pr-testing-6744 has successfully built against this PR. (2025-01-23 14:20:24) View Log
✅ Mathlib branch lean-pr-testing-6744 has successfully built against this PR. (2025-01-23 15:23:15) View Log
❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-01-27 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2025-01-27 10:18:50)
✅ Mathlib branch lean-pr-testing-6744 has successfully built against this PR. (2025-01-28 20:05:19) View Log
💥 Mathlib branch lean-pr-testing-6744 build failed against this PR. (2025-01-29 23:09:00) View Log
💥 Mathlib branch lean-pr-testing-6744 build failed against this PR. (2025-01-30 11:53:34) View Log
💥 Mathlib branch lean-pr-testing-6744 build failed against this PR. (2025-01-30 16:45:45) View Log
✅ Mathlib branch lean-pr-testing-6744 has successfully built against this PR. (2025-01-30 19:19:11) View Log
✅ Mathlib branch lean-pr-testing-6744 has successfully built against this PR. (2025-01-30 22:30:49) View Log
❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-02-02 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2025-02-03 10:23:47)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase eab91e68c5762b3ca1f4ea4fc34cdbbb12da9877 --onto 832d7c500d709deb5e7f0a5a6fd0f01865d1a303. (2025-02-03 11:10:16)
❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-02-04 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2025-02-04 10:23:10)
✅ Mathlib branch lean-pr-testing-6744 has successfully built against this PR. (2025-02-04 12:45:54) View Log
✅ Mathlib branch lean-pr-testing-6744 has successfully built against this PR. (2025-02-04 15:03:06) View Log
🟡 Mathlib branch lean-pr-testing-6744 build against this PR was cancelled. (2025-02-04 15:48:12) View Log
✅ Mathlib branch lean-pr-testing-6744 has successfully built against this PR. (2025-02-04 16:43:41) View Log
❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-02-05 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2025-02-05 11:38:23)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 60aeb79a75974c3197a8606f90dea18985307f8a --onto 412389f71f8a24307e3adba69b38b4b685b04f72. (2025-02-05 17:04:23)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 60aeb79a75974c3197a8606f90dea18985307f8a --onto 1f956ad1af1cf423ad68f3ddc294fd2b7e5117df. (2025-02-06 08:00:54)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 60aeb79a75974c3197a8606f90dea18985307f8a --onto b01ca8ee237a1b3c299384e73ad79d424e216a84. (2025-02-06 10:50:36)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 07c880f7ff1b3490e4de60e561dbe21fa7a833dc --onto b01ca8ee237a1b3c299384e73ad79d424e216a84. (2025-02-06 15:03:56)
✅ Mathlib branch lean-pr-testing-6744 has successfully built against this PR. (2025-02-10 13:00:37) View Log
✅ Mathlib branch lean-pr-testing-6744 has successfully built against this PR. (2025-02-10 17:55:53) View Log

This PR avoids a `let` in the elaboration of `forIn`. It was introduced in f51328ff112 but nothing seems to break when I simplify the code. This produces cleaner termination proof goals which would otherwise have an unexpected ``` let col✝ := ``` in the context.

This reverts commit 5627e54.

…lean4 into joachim/forIn-let

This documents the changes from leanprover/lean4#6744. --------- Co-authored-by: David Thrane Christiansen <[email protected]>

) this PR helps with bootstrapping leanprover#6744.

…prover#6744) This PR extend the preprocessing of well-founded recursive definitions to bring assumptions like `h✝ : x ∈ xs` into scope automatically. This fixes leanprover#5471, and follows (roughly) the design written there. See the module docs at `src/Lean/Elab/PreDefinition/WF/AutoAttach.lean` for details on the implementation. This only works for higher-order functions that have a suitable setup. See for example section “Well-founded recursion preprocessing setup” in `src/Init/Data/List/Attach.lean`. This does not change the `decreasing_tactic`, so in some cases there is still the need for a manual termination proof some cases. We expect a better termination tactic in the near future.

) this PR helps with bootstrapping leanprover#6744.

…prover#6744) This PR extend the preprocessing of well-founded recursive definitions to bring assumptions like `h✝ : x ∈ xs` into scope automatically. This fixes leanprover#5471, and follows (roughly) the design written there. See the module docs at `src/Lean/Elab/PreDefinition/WF/AutoAttach.lean` for details on the implementation. This only works for higher-order functions that have a suitable setup. See for example section “Well-founded recursion preprocessing setup” in `src/Init/Data/List/Attach.lean`. This does not change the `decreasing_tactic`, so in some cases there is still the need for a manual termination proof some cases. We expect a better termination tactic in the near future.

nomeata added 8 commits January 22, 2025 14:47

Simple test cases

4b3f34e

Switch from transform to simp

021f1f2

Do not use explicit binders in dite_eq_ite

f17a96c

Try macro to get daggered h

8858af1

More tracing

2f355fa

feat: simp to remove unused let_fun only when zeta := true

c68ff1a

Update test

767a1b9

defeq checking: heed cfg.zeta in consumeLetIfZeta

acea290

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

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 22, 2025

Update lean-toolchain for testing leanprover/lean4#6744

9030431

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 22, 2025

Update lean-toolchain for testing leanprover/lean4#6744

1dec0bf

leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jan 22, 2025

nomeata added 4 commits January 23, 2025 10:41

Try to add zetaUnused

a048b51

feat: zetaUnused option (without functionality)

97491f0

chore: update stage0

dc220c5

Merge branch 'joachim/zeta-unused' into joachim/auto-attach

4c6dd4e

nomeata changed the base branch from master to nightly-with-mathlib January 23, 2025 10:32

Nudge CI

a44675c

github-actions bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Jan 23, 2025

github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 23, 2025 10:49 Inactive

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 23, 2025

Trigger CI for leanprover/lean4#6744

05276df

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 23, 2025

Trigger CI for leanprover/lean4#6744

9704951

nomeata added 3 commits January 23, 2025 14:58

tests

d5aca05

Test case

3081ca5

More tests

63ad38b

leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Jan 23, 2025

github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 23, 2025 14:22 Inactive

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 23, 2025

Trigger CI for leanprover/lean4#6744

9013470

nomeata changed the title ~~feat: nested recursion preprocessing for well-founded recursion~~ feat: nested well-founded recursion via automatic preprocessing Feb 6, 2025

nomeata added 2 commits February 6, 2025 17:05

Also preprocess forIn to forIn'

7f45bba

forIn elaboration: Avoid extra let

e231bf4

github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 6, 2025 16:18 Inactive

nomeata added 7 commits February 6, 2025 17:19

add test case

7569cfb

Use registerCustomErrorIfMVar

5627e54

Revert "Use registerCustomErrorIfMVar"

9968520

This reverts commit 5627e54.

Merge branch 'joachim/forIn-let' into joachim/auto-attach

7fbf7d5

Merge branch 'nightly-with-mathlib' of https://github.com/leanprover/…

500c723

…lean4 into joachim/forIn-let

Merge branch 'joachim/forIn-let' into joachim/auto-attach

3e13025

nomeata added the will-merge-soon …unless someone speaks up label Feb 10, 2025

github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 10, 2025 11:19 Inactive

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

Trigger CI for leanprover/lean4#6744

a2dd8a6

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

Trigger CI for leanprover/lean4#6744

fa33bf0

nomeata mentioned this pull request Feb 10, 2025

Missing equality between arguments in termination proof goal #7020

Closed

3 tasks

Spurious file

56196d0

nomeata enabled auto-merge February 10, 2025 16:24

github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 10, 2025 16:31 Inactive

nomeata added this pull request to the merge queue Feb 10, 2025

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

Trigger CI for leanprover/lean4#6744

8dd50ca

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

Trigger CI for leanprover/lean4#6744

1f0631c

Merged via the queue into master with commit 4016a80 Feb 10, 2025
16 checks passed

nomeata mentioned this pull request Feb 11, 2025

feat: well-founded function definition preprocessing leanprover/reference-manual#296

Merged

tobiasgrosser pushed a commit to opencompl/lean4 that referenced this pull request Feb 16, 2025

feat: add auto_attach simp set (no functionality yet) (leanprover#6956

973a745

) this PR helps with bootstrapping leanprover#6744.

luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Feb 24, 2025

feat: add auto_attach simp set (no functionality yet) (leanprover#6956

6963d28

) this PR helps with bootstrapping leanprover#6744.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: nested well-founded recursion via automatic preprocessing #6744

feat: nested well-founded recursion via automatic preprocessing #6744

nomeata commented Jan 22, 2025 •

edited

Loading

leanprover-community-bot commented Jan 22, 2025 •

edited

Loading

feat: nested well-founded recursion via automatic preprocessing #6744

feat: nested well-founded recursion via automatic preprocessing #6744

Conversation

nomeata commented Jan 22, 2025 • edited Loading

leanprover-community-bot commented Jan 22, 2025 • edited Loading

nomeata commented Jan 22, 2025 •

edited

Loading

leanprover-community-bot commented Jan 22, 2025 •

edited

Loading