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: fun_induction and fun_cases tactics #7069

Merged
merged 11 commits into from
Feb 16, 2025
Merged

feat: fun_induction and fun_cases tactics #7069

merged 11 commits into from
Feb 16, 2025

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Feb 13, 2025 •
edited
Loading

This PR adds the fun_induction and fun_cases tactics, which add convenience around using functional induction and functional cases principles.

fun_induction foo  x y z

elaborates foo x y z, then looks up foo.induct, and then essentially does

induction z using foo.induct y

including and in particular figuring out which arguments are parameters, targets or dropped. This only works for non-mutual functions so far.

Likewise there is the fun_cases tactic using foo.fun_cases.

@nomeata nomeata added the changelog-language Language features, tactics, and metaprograms label Feb 13, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 13, 2025 15:06 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 13, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 13, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#7069
9bb47b0
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 13, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#7069
822c780
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Feb 13, 2025
@leanprover-community-bot
Copy link
Collaborator

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

Mathlib CI status (docs):

@nomeata nomeata force-pushed the joachim/funind-tactic branch from 7ac5386 to 06930b8 Compare February 13, 2025 16:41
@nomeata nomeata force-pushed the joachim/funind-tactic branch from 06930b8 to d5f4405 Compare February 13, 2025 16:45
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 13, 2025 16:54 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 13, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7069
8a26768
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 13, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7069
91278c2
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 14, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7069
a2cae03
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 14, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7069
988e80d
@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 Feb 14, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 14, 2025 10:37 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 14, 2025 10:55 Inactive
@nomeata nomeata mentioned this pull request Feb 14, 2025
Merged
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 14, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7069
f1a673c
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 14, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7069
633b575
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 14, 2025 12:57 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 14, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7069
ccf676f
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 14, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7069
f3b0b63
@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 14, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 15, 2025 20:55 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 15, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7069
8e995d0
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 15, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7069
de04449
@nomeata nomeata marked this pull request as ready for review February 16, 2025 10:36
@nomeata nomeata enabled auto-merge February 16, 2025 10:42
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 16, 2025 10:47 Inactive
@nomeata nomeata added this pull request to the merge queue Feb 16, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 16, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7069
bc9fa76
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 16, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7069
cee801b
Merged via the queue into master with commit 96c6f9d Feb 16, 2025
16 checks passed
kmill pushed a commit to kmill/lean4 that referenced this pull request Feb 17, 2025
@nomeata @kmill
feat: fun_induction and fun_cases tactics (leanprover#7069)
234afb6 
This PR adds the `fun_induction` and `fun_cases` tactics, which add
convenience around using functional induction and functional cases
principles.

```
fun_induction foo  x y z
```
elaborates `foo x y z`, then looks up `foo.induct`, and then essentially
does
```
induction z using foo.induct y
```
including and in particular figuring out which arguments are parameters,
targets or dropped. This only works for non-mutual functions so far.

Likewise there is the `fun_cases` tactic using `foo.fun_cases`.
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

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR 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