Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

refactor: WF: create unfold theorems eagerly #6898

Draft
wants to merge 19 commits into
base: master
Choose a base branch
from
Draft

refactor: WF: create unfold theorems eagerly #6898

wants to merge 19 commits into from
+209 −116

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Feb 1, 2025

This PR changes how the unfold theorems for well-founded recursion are created. They are created eagerly (anticipating that the behaivor may be affected by simp sets soon), and without the detour of going through equational theorems.

@nomeata
refactor: WF: create unfold theorems eagerly
a6af2c2 
This PR changes how the unfold theorems for well-founded recursion are created.
They are created eagerly (anticipating that the behaivor may be affected by simp
sets soon), and without the detour of going through equational theorems.
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 1, 2025 11:28 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 1, 2025 11:36 Inactive
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 1, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6898
473bf75
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6898
04ea401
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Feb 1, 2025 •
edited
Loading

Mathlib CI status (docs):

  • 💥 Mathlib branch lean-pr-testing-6898 build failed against this PR. (2025-02-01 12:28:01) View Log
  • 💥 Mathlib branch lean-pr-testing-6898 build failed against this PR. (2025-02-01 17:02:39) View Log
  • 🟡 Mathlib branch lean-pr-testing-6898 build against this PR was cancelled. (2025-02-01 17:31:37) View Log
  • ✅ Mathlib branch lean-pr-testing-6898 has successfully built against this PR. (2025-02-01 18:57:19) View Log
  • ✅ Mathlib branch lean-pr-testing-6898 has successfully built against this PR. (2025-02-01 20:12:53) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase deb3299263b8d43324d60b82df262f7ca4a97b7c --onto 66471ba6e248a9dffe869880c88f8b3f098afc1a. (2025-02-01 20:35:26)
  • ❗ 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-02 11:55:54)

@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Feb 1, 2025
@nomeata
avoid eta-expansion in simpMatch
ba05bf7
@nomeata
refactor: simpMatch to not etaStruct
32caf9a 
This PR changes the `simpMatch` function, used inside the equation generator for
WF-rec functions, to not do eta-expansion.

This makes the process a bit more robust and disciplined, and avoids removing
match-statements (and introduce projections and dependencies) that we'd rather
split instead.
@nomeata
Merge branch 'joachim/simpMatch-no-etaStruct' into joachim/wf-eager-u…
7b77dbf 
…nfold
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 1, 2025 16:18 Inactive
@nomeata nomeata mentioned this pull request Feb 1, 2025
Merged
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6898
1a18a42
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6898
1b3e991
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 1, 2025 16:44 Inactive
@nomeata
Use the generic mkEqns also for WF-rec functions
7e0fda0 
but thread the tryRefl flag through, as well as the declNames.
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 1, 2025 16:52 Inactive
@github-actions github-actions bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Feb 1, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6898
dac7a2b
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6898
d744d4d
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 1, 2025 17:19 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6898
b5b1ce6
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6898
2c29e59
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 1, 2025 17:57 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6898
d3aa539
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6898
a39dbb5
@leanprover-community-bot 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 Feb 1, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 1, 2025 19:10 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6898
e32f88e
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6898
ca37b47
github-merge-queue bot pushed a commit that referenced this pull request Feb 1, 2025
@nomeata
refactor: simpMatch to not etaStruct (#6901)
deb3299 
This PR changes the `simpMatch` function, used inside the equation
generator for WF-rec functions, to not do eta-expansion.

This makes the process a bit more robust and disciplined, and avoids
removing match-statements (and introduce projections and dependencies)
that we'd rather split instead.

Also adds more tracing to the equational theorem generator.

Extracted from #6898.
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 1, 2025 20:29 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 2, 2025 11:29 Inactive
@github-actions github-actions bot removed the changes-stage0 Contains stage0 changes, merge manually using rebase label Feb 2, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 2, 2025 11:49 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 2, 2025 16:34 Inactive
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@nomeata @leanprover-community-bot