Skip to content

feat: fun_induction and fun_cases tactics#7069

Merged
nomeata merged 11 commits intomasterfrom
joachim/funind-tactic
Feb 16, 2025
Merged

feat: fun_induction and fun_cases tactics#7069
nomeata merged 11 commits intomasterfrom
joachim/funind-tactic

Conversation

@nomeata
Copy link
Copy Markdown
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 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
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Feb 13, 2025
Update lean-toolchain for testing leanprover/lean4#7069
9bb47b0
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Feb 13, 2025
Update lean-toolchain for testing leanprover/lean4#7069
822c780
@ghost ghost added the builds-mathlib CI has verified that Mathlib builds against this PR label Feb 13, 2025
@ghost
Copy link
Copy Markdown

ghost commented Feb 13, 2025 •
edited by ghost
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
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Feb 13, 2025
Trigger CI for leanprover/lean4#7069
8a26768
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Feb 13, 2025
Trigger CI for leanprover/lean4#7069
91278c2
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Feb 14, 2025
Trigger CI for leanprover/lean4#7069
a2cae03
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Feb 14, 2025
Trigger CI for leanprover/lean4#7069
988e80d
@ghost ghost 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
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Feb 14, 2025
Trigger CI for leanprover/lean4#7069
f1a673c
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Feb 14, 2025
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
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Feb 14, 2025
Trigger CI for leanprover/lean4#7069
ccf676f
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Feb 14, 2025
Trigger CI for leanprover/lean4#7069
f3b0b63
@ghost ghost 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
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Feb 15, 2025
Trigger CI for leanprover/lean4#7069
8e995d0
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Feb 15, 2025
Trigger CI for leanprover/lean4#7069
de04449
@nomeata nomeata marked this pull request as ready for review February 16, 2025 10:36
nomeata
nomeata commented Feb 16, 2025
View reviewed changes
nomeata
nomeata commented Feb 16, 2025
View reviewed changes
@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
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Feb 16, 2025
Trigger CI for leanprover/lean4#7069
bc9fa76
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Feb 16, 2025
Trigger CI for leanprover/lean4#7069
cee801b
Merged via the queue into master with commit 96c6f9d Feb 16, 2025
13 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`.
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 21, 2025
@kim-em @jcommelin
@TwoFX @nomeata @kmill @tydeu
chore: adaptations for nightly-2025-02-20 (#22144)
91028e3 
* lake update

* fixes

* fix namespace

* fix test

* Merge master into nightly-testing

* chore: bump to nightly-2025-02-06

* copy test from master

* Merge master into nightly-testing

* chore: bump to nightly-2025-02-07

* chore: bump to nightly-2025-02-08

* update

* chore: bump to nightly-2025-02-09

* didn't commit

* fix

* fix test

* Update lean-toolchain for testing leanprover/lean4#7013

* chore: bump to nightly-2025-02-10

* fixes for leanprover/lean4#7013

* fixes for leanprover/lean4#7013

* Trigger CI for leanprover/lean4#7013

* chore: bump to nightly-2025-02-11

* update

* Update lean-toolchain for testing leanprover/lean4#7046

* Trigger CI for leanprover/lean4#7046

* Switch from mk to ofBitVec

* chore: bump to nightly-2025-02-12

* Update lean-toolchain for testing leanprover/lean4#7050

* lake update

* lake update

* fixes

* another maxheartbeats

* fix tests

* Update lean-toolchain for testing leanprover/lean4#7059

* fix

* chore: bump to nightly-2025-02-13

* lake update

* fixes

* lake exe shake --fix

* Update lean-toolchain for testing leanprover/lean4#7069

* Trigger CI for leanprover/lean4#7069

* chore: adaptations for nightly-2025-02-13

* remove upstreamed

* Trigger CI for leanprover/lean4#7059

* Trigger CI for leanprover/lean4#7059

* chore: bump to nightly-2025-02-14

* Trigger CI for leanprover/lean4#7069

* Trigger CI for leanprover/lean4#7069

* Update lean-toolchain for testing leanprover/lean4#7082

* quite a bit more to go

* lake update

* fix merge

* fix

* adapt

* adapt

* Trigger CI for leanprover/lean4#7082

* Trigger CI for leanprover/lean4#7069

* lake update

* lake update

* fixes

* fixes

* chore: bump to nightly-2025-02-15

* Trigger CI for leanprover/lean4#7069

* Update lean-toolchain for testing leanprover/lean4#7100

* chore: bump to nightly-2025-02-16

* fixes

* fixes 2

* fixes 3

* built mathlib

* Trigger CI for leanprover/lean4#7069

* fix simps test

* fixes for leanprover/lean4#7059

* fix: cache lib dir (adaption for lean4#7001) (#21967)

* fixes

* fixes for leanprover/lean4#7059

* restore broken files

* chore: bump to nightly-2025-02-17

* lake update

* lake update

* oops

* comment out broken files

* longFile

* oops, one more

* .

* searchPath

* .

* Update lean-toolchain for testing leanprover/lean4#7103

* fixes

* update manifest

* fix

* fix

* Trigger CI for leanprover/lean4#7103

* chore: bump to nightly-2025-02-18

* lake update

* deprecations

* restore computability files broken by defeq yesterday

* fixes

* chore: adaptations for nightly-2025-02-18

* chore: bump to nightly-2025-02-19

* lake update

* fixes

* fix merge

* chore: adaptations for nightly-2025-02-19

* Merge master into nightly-testing

* chore: bump to nightly-2025-02-20

* fix merge

* chore: adaptations for nightly-2025-02-20

* minor reverts

* more

* deprecation

* another

* more

* restore check-yaml

* .

* .

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Feb 24, 2025
@nomeata @luisacicolini
feat: fun_induction and fun_cases tactics (leanprover#7069)
2ddbc54 
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`.
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Feb 25, 2025
@nomeata @luisacicolini
feat: fun_induction and fun_cases tactics (leanprover#7069)
ccfcf4d 
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`.
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 10, 2025
@jcommelin @kim-em
@TwoFX @nomeata @kmill @tydeu @jrr6 @kbuzzard @Kha @mattrobball @JovanGerb
chore: adaptations for nightly-2025-03-09 (#22758)
ec93745 
* chore: adaptations for nightly-2025-02-20

* Merge master into nightly-testing

* minor reverts

* more

* deprecation

* another

* more

* restore check-yaml

* .

* .

* chore: adaptations for nightly-2025-02-20 (#22144)

* lake update

* fixes

* fix namespace

* fix test

* Merge master into nightly-testing

* chore: bump to nightly-2025-02-06

* copy test from master

* Merge master into nightly-testing

* chore: bump to nightly-2025-02-07

* chore: bump to nightly-2025-02-08

* update

* chore: bump to nightly-2025-02-09

* didn't commit

* fix

* fix test

* Update lean-toolchain for testing leanprover/lean4#7013

* chore: bump to nightly-2025-02-10

* fixes for leanprover/lean4#7013

* fixes for leanprover/lean4#7013

* Trigger CI for leanprover/lean4#7013

* chore: bump to nightly-2025-02-11

* update

* Update lean-toolchain for testing leanprover/lean4#7046

* Trigger CI for leanprover/lean4#7046

* Switch from mk to ofBitVec

* chore: bump to nightly-2025-02-12

* Update lean-toolchain for testing leanprover/lean4#7050

* lake update

* lake update

* fixes

* another maxheartbeats

* fix tests

* Update lean-toolchain for testing leanprover/lean4#7059

* fix

* chore: bump to nightly-2025-02-13

* lake update

* fixes

* lake exe shake --fix

* Update lean-toolchain for testing leanprover/lean4#7069

* Trigger CI for leanprover/lean4#7069

* chore: adaptations for nightly-2025-02-13

* remove upstreamed

* Trigger CI for leanprover/lean4#7059

* Trigger CI for leanprover/lean4#7059

* chore: bump to nightly-2025-02-14

* Trigger CI for leanprover/lean4#7069

* Trigger CI for leanprover/lean4#7069

* Update lean-toolchain for testing leanprover/lean4#7082

* quite a bit more to go

* lake update

* fix merge

* fix

* adapt

* adapt

* Trigger CI for leanprover/lean4#7082

* Trigger CI for leanprover/lean4#7069

* lake update

* lake update

* fixes

* fixes

* chore: bump to nightly-2025-02-15

* Trigger CI for leanprover/lean4#7069

* Update lean-toolchain for testing leanprover/lean4#7100

* chore: bump to nightly-2025-02-16

* fixes

* fixes 2

* fixes 3

* built mathlib

* Trigger CI for leanprover/lean4#7069

* fix simps test

* fixes for leanprover/lean4#7059

* fix: cache lib dir (adaption for lean4#7001) (#21967)

* fixes

* fixes for leanprover/lean4#7059

* restore broken files

* chore: bump to nightly-2025-02-17

* lake update

* lake update

* oops

* comment out broken files

* longFile

* oops, one more

* .

* searchPath

* .

* Update lean-toolchain for testing leanprover/lean4#7103

* fixes

* update manifest

* fix

* fix

* Trigger CI for leanprover/lean4#7103

* chore: bump to nightly-2025-02-18

* lake update

* deprecations

* restore computability files broken by defeq yesterday

* fixes

* chore: adaptations for nightly-2025-02-18

* chore: bump to nightly-2025-02-19

* lake update

* fixes

* fix merge

* chore: adaptations for nightly-2025-02-19

* Merge master into nightly-testing

* chore: bump to nightly-2025-02-20

* fix merge

* chore: adaptations for nightly-2025-02-20

* minor reverts

* more

* deprecation

* another

* more

* restore check-yaml

* .

* .

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>

* chore: bump to nightly-2025-02-21

* chore: bump to nightly-2025-02-22

* chore(Tactic/DeriveTraversable): adapt to `auxDeclToFullName` relocation

* Update lean-toolchain for testing leanprover/lean4#7196

* fixes

* update batteries

* update proofwidgets

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* chore: bump to nightly-2025-02-24

* lake update

* fixes

* deprecations

* .

* archive

* fix tests

* fix tests

* chore: adaptations for nightly-2025-02-24 (#22266)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>

* chore: bump to nightly-2025-02-25

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* Adapt

* Trigger CI for leanprover/lean4#7166

* revert Mathlib/Data/Multiset/Basic, and refix

* Merge master into nightly-testing

* chore: bump to nightly-2025-02-26

* remove upstreamed

* fix

* fix tests

* Apply suggestions from code review

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

* chore: adaptations for nightly-2025-02-26 (#22347)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>

* chore: bump to nightly-2025-02-27

* Trigger CI for leanprover/lean4#7166

* Update lean-toolchain for testing leanprover/lean4#7259

* fix

* I would not have guessed that this lemma already exists!

* chore: bump to nightly-2025-02-28

* fix

* chore: bump to nightly-2025-03-01

* chore: bump to nightly-2025-03-02

* Merge master into nightly-testing

* deprecation

* Trigger CI for leanprover/lean4#7166

* deprecation

* chore: adaptations for nightly-2025-03-02 (#22460)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>

* chore: adaptations for nightly-2025-03-02

* chore: bump to nightly-2025-03-03

* remove upstreamed

* chore: adaptations for nightly-2025-03-03

* Trigger CI for leanprover/lean4#7166

* chore: adaptations for nightly-2025-03-03 (#22493)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

* bump toolchain and dependencies

* Trigger CI for leanprover/lean4#7166

* chore: bump to nightly-2025-03-04

* lake update

* Trigger CI for leanprover/lean4#7166

* chore: bump to nightly-2025-03-05

* fix?

* add adaptation notes to revert _root_

* Update lean-toolchain for testing leanprover/lean4#7358

* chore: bump to nightly-2025-03-06

* chore: adaptations for nightly-2025-03-06

* chore: adaptations for nightly-2025-03-06

* Merge master into nightly-testing

* chore: bump to nightly-2025-03-06

* Update lean-toolchain for testing leanprover/lean4#7261

* fixes for leanprover/lean4#7358

* fixes for leanprover/lean4#7358

* fixes for leanprover/lean4#7358

* Trigger CI for leanprover/lean4#7358

* Trigger CI for leanprover/lean4#7261

* fix Mathlib.Linter.getNamesFrom

* chore: adaptations for nightly-2025-03-06

* chore: bump to nightly-2025-03-07

* lake update

* add_div is protected

* Update lean-toolchain for testing leanprover/lean4#7378

* More like that

* adapt

* Trigger CI for leanprover/lean4#7378

* Fix

* fix

* chore: bump to nightly-2025-03-08

* lake update

* chore: bump to nightly-2025-03-09

* chore(RingTheory/LocalRing/ResidueField/Ideal): increase `simp` prio, analogous to #22215

* process adaptation notes

---------

Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
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 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.

1 participant

@nomeata