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

feat: functional cases theorem for non-recursive functions #6261

Merged
merged 9 commits into from
Jan 21, 2025
Merged

feat: functional cases theorem for non-recursive functions #6261

merged 9 commits into from
Jan 21, 2025

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Nov 29, 2024 •
edited
Loading

This PR adds foo.fun_cases, an automatically generated theorem that splits the goal according to the branching structure of foo, much like the Functional Induction Principle, but for all functions (not just recursive ones), and without providing inductive hypotheses.

The design isn't quite final yet as to which function parameters should become targets of the motive, and which parameters of the theorem, but the current version is already proven to be useful, so start with this and iterate later.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc November 29, 2024 14:59 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 Nov 29, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 29, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6261
09ec190
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 29, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6261
2318eb2
@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 Nov 29, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 29, 2024 •
edited
Loading

Mathlib CI status (docs):

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc November 29, 2024 16:05 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 29, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6261
1ab92f1
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 29, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6261
6ad3bd2
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc December 2, 2024 09:04 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 2, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6261
a62d37e
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 2, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6261
d1aad53
@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 Dec 2, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc December 3, 2024 11:44 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 3, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6261
802b4af
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 3, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6261
d720155
@nomeata nomeata changed the title experiment: induction principles for non-recursive functions feat: functional cases theorem for non-recursive functions Jan 21, 2025
@nomeata nomeata added the changelog-language Language features, tactics, and metaprograms label Jan 21, 2025
@nomeata nomeata marked this pull request as ready for review January 21, 2025 09:56
@nomeata nomeata requested a review from leodemoura as a code owner January 21, 2025 09:56
@nomeata nomeata enabled auto-merge January 21, 2025 10:01
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 21, 2025 10:07 Inactive
@nomeata nomeata added this pull request to the merge queue Jan 21, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 21, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6261
ca1e7b1
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 21, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6261
2eb4f10
Merged via the queue into master with commit 3569797 Jan 21, 2025
23 of 24 checks passed
@leanprover-community-bot leanprover-community-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Jan 21, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

Assignees
No one assigned
Labels
breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-language Language features, tactics, and metaprograms 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