Skip to content

feat: add generalization hypotheses to induction tactic#7103

Merged
kmill merged 8 commits intoleanprover:masterfrom
kmill:induction_named_target
Feb 18, 2025
Merged

feat: add generalization hypotheses to induction tactic#7103
kmill merged 8 commits intoleanprover:masterfrom
kmill:induction_named_target

Conversation

@kmill
Copy link
Copy Markdown
Collaborator

@kmill kmill commented Feb 17, 2025 •
edited
Loading

This PR gives the induction tactic the ability to name hypotheses to use when generalizing targets, just like in cases. For example, induction h : xs.length leads to goals with hypotheses h : xs.length = 0 and h : xs.length = n + 1. Target handling is also slightly modified for multi-target induction principles: it used to be that if any target was not a free variable, all of the targets would be generalized (thus causing free variables to lose their connection to the local hypotheses they appear in); now only the non-free-variable targets are generalized.

This gives induction the last basic feature of the mathlib induction' tactic, which has been long-requested. Recent Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/To.20replace.20.60induction'.20h.20.3A.20f.20x.60/near/499482173

@kmill kmill added the changelog-language Language features and metaprograms label Feb 17, 2025
@kmill kmill requested review from digama0 and kim-em as code owners February 17, 2025 00:06
@kmill kmill changed the title feat: add named targets to induction tactic feat: add generalization hypotheses to induction tactic Feb 17, 2025
@kmill kmill force-pushed the induction_named_target branch from 24ac09c to 62317de Compare February 17, 2025 01:09
@kmill kmill requested a review from leodemoura as a code owner February 17, 2025 01:09
@kmill kmill changed the base branch from master to nightly-with-mathlib February 17, 2025 01:10
@kmill kmill marked this pull request as draft February 17, 2025 01:11
@kmill kmill changed the base branch from nightly-with-mathlib to master February 17, 2025 01:11
@kmill kmill mentioned this pull request Feb 17, 2025
Closed
kmill added 2 commits February 17, 2025 11:54
@kmill
feat: add named targets to induction tactic
6e078e0 
This PR gives the `induction` tactic the ability to name hypotheses to use when generalizing targets, just like `cases`. For example, `induction h : xs.length` leads to goals with hypotheses `h : xs.length = 0` and `h : xs.length = n + 1`.

This brings `induction` to feature parity with the mathlib `induction'` tactic. This has been long-requested. Recent Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/To.20replace.20.60induction'.20h.20.3A.20f.20x.60/near/499482173
@kmill
disable tests failing because of staging issues
38284bb
@kmill kmill force-pushed the induction_named_target branch from 62317de to 38284bb Compare February 17, 2025 19:54
nomeata
nomeata reviewed Feb 17, 2025
View reviewed changes
@kmill kmill marked this pull request as ready for review February 17, 2025 22:31
@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 17, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Feb 17, 2025
Update lean-toolchain for testing leanprover/lean4#7103
94033b1
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Feb 17, 2025
Update lean-toolchain for testing leanprover/lean4#7103
35c6b82
@ghost
Copy link
Copy Markdown

ghost commented Feb 17, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Feb 17, 2025
@kmill
Copy link
Copy Markdown
Collaborator Author

kmill commented Feb 18, 2025

Mathlib builds locally, merging now, and then after the stage0 update I'll make a cleanup PR.

@kmill kmill added this pull request to the merge queue Feb 18, 2025
@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 18, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Feb 18, 2025
@kmill kmill enabled auto-merge February 18, 2025 03:29
@kmill kmill added this pull request to the merge queue Feb 18, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Feb 18, 2025
Trigger CI for leanprover/lean4#7103
537aeca
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Feb 18, 2025
Trigger CI for leanprover/lean4#7103
e1939e1
Merged via the queue into leanprover:master with commit 6a59926 Feb 18, 2025
13 checks passed
@kmill kmill mentioned this pull request Feb 18, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Feb 18, 2025
@kmill
chore: cleanup after stage0 update for #7103 (#7125)
219f36f 
This PR cleans up the bootstrapping workarounds introduced in #7103
(`induction` target generalization equation names).
@nomeata nomeata mentioned this pull request Feb 18, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Feb 18, 2025
@nomeata
fix: fun_induction to generalize like induction does (#7127)
f3baff8 
This PR follows up on #7103 which changes the generaliziation behavior
of `induction`, to keep `fun_induction` in sync. Also fixes a `Syntax`
indexing off-by-one error.
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
@kmill @luisacicolini
feat: add generalization hypotheses to induction tactic (leanprover…
a5e7da2 
…#7103)

This PR gives the `induction` tactic the ability to name hypotheses to
use when generalizing targets, just like in `cases`. For example,
`induction h : xs.length` leads to goals with hypotheses `h : xs.length
= 0` and `h : xs.length = n + 1`. Target handling is also slightly
modified for multi-target induction principles: it used to be that if
any target was not a free variable, all of the targets would be
generalized (thus causing free variables to lose their connection to the
local hypotheses they appear in); now only the non-free-variable targets
are generalized.

This gives `induction` the last basic feature of the mathlib
`induction'` tactic, which has been long-requested. Recent Zulip
discussion:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/To.20replace.20.60induction'.20h.20.3A.20f.20x.60/near/499482173
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Feb 24, 2025
@kmill @luisacicolini
chore: cleanup after stage0 update for leanprover#7103 (leanprover#7125)
bfc3f7e 
This PR cleans up the bootstrapping workarounds introduced in leanprover#7103
(`induction` target generalization equation names).
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Feb 24, 2025
@nomeata @luisacicolini
fix: fun_induction to generalize like induction does (leanprover#7127)
c12bf0b 
This PR follows up on leanprover#7103 which changes the generaliziation behavior
of `induction`, to keep `fun_induction` in sync. Also fixes a `Syntax`
indexing off-by-one error.
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Feb 25, 2025
@kmill @luisacicolini
feat: add generalization hypotheses to induction tactic (leanprover…
4465f36 
…#7103)

This PR gives the `induction` tactic the ability to name hypotheses to
use when generalizing targets, just like in `cases`. For example,
`induction h : xs.length` leads to goals with hypotheses `h : xs.length
= 0` and `h : xs.length = n + 1`. Target handling is also slightly
modified for multi-target induction principles: it used to be that if
any target was not a free variable, all of the targets would be
generalized (thus causing free variables to lose their connection to the
local hypotheses they appear in); now only the non-free-variable targets
are generalized.

This gives `induction` the last basic feature of the mathlib
`induction'` tactic, which has been long-requested. Recent Zulip
discussion:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/To.20replace.20.60induction'.20h.20.3A.20f.20x.60/near/499482173
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Feb 25, 2025
@kmill @luisacicolini
chore: cleanup after stage0 update for leanprover#7103 (leanprover#7125)
5712a6f 
This PR cleans up the bootstrapping workarounds introduced in leanprover#7103
(`induction` target generalization equation names).
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Feb 25, 2025
@nomeata @luisacicolini
fix: fun_induction to generalize like induction does (leanprover#7127)
755ae57 
This PR follows up on leanprover#7103 which changes the generaliziation behavior
of `induction`, to keep `fun_induction` in sync. Also fixes a `Syntax`
indexing off-by-one error.
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>
@Seasawher Seasawher mentioned this pull request Mar 27, 2025
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@nomeata nomeata nomeata left review comments

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

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

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura 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.

2 participants

@kmill @nomeata