Skip to content

chore: attribute [induction_eliminator]#12605

Open
astrainfinita wants to merge 22 commits intomasterfrom
FR_induction
Open

chore: attribute [induction_eliminator]#12605
astrainfinita wants to merge 22 commits intomasterfrom
FR_induction

Conversation

@astrainfinita
Copy link
Copy Markdown
Collaborator

@astrainfinita astrainfinita commented May 2, 2024 •
edited by eric-wieser
Loading

Add attribute [induction_eliminator] to
AdjoinRoot.induction_on
ENat.recTopCoe
ENNReal.recTopCoe
Finset.induction
Magma.AssocQuotient.induction_on
ManyOneDegree.ind_on
Module.Ray.ind (and add Orientation.ind for Orientation, an abbrev of it. I wish that we do not need to add it in the future.)
Multiset.induction
MvPolynomial.induction_on
OnePoint.rec
Opposite.rec'
Ordinal.limitRecOn
PartENat.casesOn
Polynomial.induction_on'
QuotientAddGroup.induction_on' (and add AddCircle.induction_on for AddCircle, an abbrev of it. I wish that we do not need to add it in the future.)
QuotientGroup.induction_on' (doesn't actually work)
Real.Angle.induction_on
SimplexCategory.rec
Trunc.induction_on

Open in Gitpod

@astrainfinita astrainfinita added the WIP Work in progress label May 2, 2024
astrainfinita
astrainfinita commented May 2, 2024
View reviewed changes
Mathlib/Algebra/Group/WithOne/Basic.lean
theorem map_id : map (MulHom.id α) = MonoidHom.id (WithOne α) := by
ext x
induction x using WithOne.cases_on <;> rfl
induction x <;> rfl
Copy link
Copy Markdown
Collaborator Author

@astrainfinita astrainfinita May 2, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We have WithOne.recOneCoe and WithZero.recZeroCoe. Can we just remove WithOne.cases_on and WithZero.cases_on?

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 3, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 15, 2024
@astrainfinita astrainfinita added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed WIP Work in progress labels May 16, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 16, 2024
@urkud
Copy link
Copy Markdown
Member

urkud commented May 19, 2024

Does it make induction use these theorems by default? Should Finset default to cons_induction?

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 20, 2024
This was referenced May 21, 2024
Closed
Closed
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented May 21, 2024

193 files is pretty large to review; can this be split? I've made #13096 for the really basic WithX cases.

@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented May 21, 2024

Another good split would be all the Free constructions.

@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 21, 2024
mathlib-bors bot pushed a commit that referenced this pull request May 22, 2024
@eric-wieser
chore: add induction_eliminator to With{Top,Bot,Zero,One} (#13096)
cdceebb 
This is a smaller version of #12605.

This allows `using` to be dropped from `induction`.
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 22, 2024
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 26, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 26, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 26, 2024
@eric-wieser
chore: register {OreLocalization, Localization, `ModuleLocalizati…
ae2d027 
…on`} with `induction` and `cases` (#14132)

Spit from #12605, which picked up some conflicts here.

Co-authored-by: negiizhao [zhao.yu-yang@foxmail.com](mailto:zhao.yu-yang@foxmail.com)
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@eric-wieser @kbuzzard
chore: register MulOpposite.rec with induction and cases (#14136)
c15f60a 
Split from #12605.

Co-authored-by: negiizhao zhao.yu-yang@foxmail.com
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@eric-wieser @kbuzzard
chore: add induction_eliminator and cases_eliminator for free obj…
2ae28da 
…ects (#14135)

Namely, for

* `FreeMagma` / `FreeAddMagma`
* `FreeSemigroup` / `FreeAddSemigroup`
* `FreeMonoid` / `FreeAddMonoid`
* `FreeCommRing`
* `FreeAlgebra`

Split from #12605


Co-authored-by: negiizhao <zhao.yu-yang@foxmail.com>
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@eric-wieser @kbuzzard
chore: register {OreLocalization, Localization, `ModuleLocalizati…
51d69bf 
…on`} with `induction` and `cases` (#14132)

Spit from #12605, which picked up some conflicts here.

Co-authored-by: negiizhao [zhao.yu-yang@foxmail.com](mailto:zhao.yu-yang@foxmail.com)
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Jun 27, 2024

QuotientGroup.induction_on' (doesn't actually work)

leanprover/lean4#4577

This was referenced Jun 27, 2024
Closed
Closed
mathlib-bors bot pushed a commit that referenced this pull request Jun 30, 2024
@eric-wieser
chore: add cases_eliminator and induction_eliminator to some simp…
d465284 
…le types (#14205)

Namely:

* `AList`
* `Cycle`
* `ConjAct`
* `Projectivization`
* `Lex`
* `NatOrdinal`
* `WithLawson`
* `WithLower`
* `WithUpper`
* `WithScott`
* `WithUpperSet`
* `WithLowerSet`
* `Speicalization` (which had an incorrectly-stated induction principle)

These are just for the cases which have docstrings of the form "Use as `induction .* using .*`".

Inspired by #12605.
mathlib-bors bot pushed a commit that referenced this pull request Jun 30, 2024
@eric-wieser
chore: register TensorProduct with induction_eliminator (#14204)
69ed7ba 
Split from #12605
@eric-wieser eric-wieser mentioned this pull request Jun 30, 2024
Closed
mathlib-bors bot pushed a commit that referenced this pull request Jun 30, 2024
@eric-wieser
chore: register Sym2 with induction (#14288)
4e1da24 
Split from #12605

Also cleans up some proofs that used `revert` instead of `induction`.
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 30, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 30, 2024
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Jun 30, 2024

193 files is pretty large to review

Now down to 140 files!

I think the Finset ones are possibly controversial; I'd much prefer cons_induction to be the default, but I suspect that stance is also controversial.

dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@eric-wieser @dagurtomas
chore: register MulOpposite.rec with induction and cases (#14136)
1cdaa0a 
Split from #12605.

Co-authored-by: negiizhao zhao.yu-yang@foxmail.com
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@eric-wieser @dagurtomas
chore: add induction_eliminator and cases_eliminator for free obj…
0a7bea1 
…ects (#14135)

Namely, for

* `FreeMagma` / `FreeAddMagma`
* `FreeSemigroup` / `FreeAddSemigroup`
* `FreeMonoid` / `FreeAddMonoid`
* `FreeCommRing`
* `FreeAlgebra`

Split from #12605


Co-authored-by: negiizhao <zhao.yu-yang@foxmail.com>
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@eric-wieser @dagurtomas
chore: register {OreLocalization, Localization, `ModuleLocalizati…
27cfaaa 
…on`} with `induction` and `cases` (#14132)

Spit from #12605, which picked up some conflicts here.

Co-authored-by: negiizhao [zhao.yu-yang@foxmail.com](mailto:zhao.yu-yang@foxmail.com)
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@eric-wieser @dagurtomas
chore: add cases_eliminator and induction_eliminator to some simp…
083a7ab 
…le types (#14205)

Namely:

* `AList`
* `Cycle`
* `ConjAct`
* `Projectivization`
* `Lex`
* `NatOrdinal`
* `WithLawson`
* `WithLower`
* `WithUpper`
* `WithScott`
* `WithUpperSet`
* `WithLowerSet`
* `Speicalization` (which had an incorrectly-stated induction principle)

These are just for the cases which have docstrings of the form "Use as `induction .* using .*`".

Inspired by #12605.
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@eric-wieser @dagurtomas
chore: register TensorProduct with induction_eliminator (#14204)
fc2eed6 
Split from #12605
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@eric-wieser @dagurtomas
chore: register Sym2 with induction (#14288)
daa4f13 
Split from #12605

Also cleans up some proofs that used `revert` instead of `induction`.
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 7, 2024
@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Jan 23, 2025

What's the status here? I think this is a useful PR

@urkud
Copy link
Copy Markdown
Member

urkud commented Apr 19, 2025

@FR-vdash-bot What parts of this is not in master yet? Do you need help with merging master?

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

awaiting-author A reviewer has asked the author a question or requested changes. merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@astrainfinita @urkud @eric-wieser @YaelDillies