[Merged by Bors] - feat: port GroupTheory.Subgroup.Basic #1797
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Collaborator
Ruben-VandeVelde
commented
Jan 23, 2023
Ruben-VandeVelde
commented
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
Ruben-VandeVelde
added
help-wanted
LukasMias
added
mathlib-port
|
It's somewhat surprising that this seems to have more problems than |
|
I think I see the issue: |
…classes should not repeat the parents' `outParam`
…er-community/mathlib4 into port/GroupTheory.Subgroup.Basic
Vierkantor
added a commit
that referenced
this pull request
Jan 25, 2023
… parents' `outParam` This PR fixes a large amount of issues encountered in the port of `GroupTheory.Subgroup.Basic`, #1797. Subobject classes such as `MulMemClass` and `SubmonoidClass` take a `SetLike` parameter, and we were used to just copy over the `M : outParam Type` declaration from `SetLike`. Since Lean 3 synthesized from left to right, we'd fill in the `outParam` from `SetLike`, then the `Mul M` instance would be available for synthesis and we'd be in business. In Lean 4 however, we often go from right to left, so that `MulMemClass ?M S [?inst : Mul ?M]` is handled first, which can't be solved before finding a `Mul ?M` instance on the metavariable `?M`, causing search through all `Mul` instances. The solution is: whenever a class is declared that takes another class as parameter (i.e. unbundled inheritance), the `outParam`s of the parent class should be unmarked and become in-params in the child class. Then Lean will try to find the parent class instance first, fill in the `outParam`s and we'll be able to synthesize the child class instance without problems.
|
I spun out the |
bors bot
pushed a commit
that referenced
this pull request
Jan 25, 2023
… parents' `outParam` (#1832) This PR fixes a large amount of issues encountered in the port of `GroupTheory.Subgroup.Basic`, #1797. Subobject classes such as `MulMemClass` and `SubmonoidClass` take a `SetLike` parameter, and we were used to just copy over the `M : outParam Type` declaration from `SetLike`. Since Lean 3 synthesized from left to right, we'd fill in the `outParam` from `SetLike`, then the `Mul M` instance would be available for synthesis and we'd be in business. In Lean 4 however, we often go from right to left, so that `MulMemClass ?M S [?inst : Mul ?M]` is handled first, which can't be solved before finding a `Mul ?M` instance on the metavariable `?M`, causing search through all `Mul` instances. The solution is: whenever a class is declared that takes another class as parameter (i.e. unbundled inheritance), the `outParam`s of the parent class should be unmarked and become in-params in the child class. Then Lean will try to find the parent class instance first, fill in the `outParam`s and we'll be able to synthesize the child class instance without problems. Pair: leanprover-community/mathlib#18291
… into port/GroupTheory.Subgroup.Basic
Ruben-VandeVelde
added
awaiting-review
| #align add_subgroup.add_subgroup_of AddSubgroup.addSubgroupOf | ||
|
|
||
| /-- If `H ≤ K`, then `H` as a subgroup of `K` is isomorphic to `H`. -/ | ||
| @[to_additive "If `H ≤ K`, then `H` as a subgroup of `K` is isomorphic to `H`.", simps] |
There was a problem hiding this comment.
Does this transfer the simps as well, or does it not need to?
There was a problem hiding this comment.
no, this needs fixing with to_additive (attr := simps)
|
|
||
| /-- A non-computable version of `MonoidHom.liftOfRightInverse` for when no computable right | ||
| inverse is available, that uses `Function.surjInv`. -/ | ||
| @[simp, |
There was a problem hiding this comment.
Does this need to_additive-izing?
There was a problem hiding this comment.
this should raise a linter error... Yes, it does.
|
bors merge |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Jan 26, 2023
Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Lukas Miaskiwskyi <lukas.mias@gmail.com> Co-authored-by: qawbecrdtey <qawbecrdtey@naver.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
|
Pull request successfully merged into master. Build succeeded:
|
bors
bot
changed the title
bors bot
pushed a commit
to leanprover-community/mathlib
that referenced
this pull request
Jan 27, 2023
…d not repeat the parents' `out_param` (#18291) This PR is a backport for a mathlib4 fix for a large amount of issues encountered in the port of `group_theory.subgroup.basic`, leanprover-community/mathlib4#1797. Subobject classes such as `mul_mem_class` and `submonoid_class` take a `set_like` parameter, and we were used to just copy over the `M : out_param Type` declaration from `set_like`. Since Lean 3 synthesizes from left to right, we'd fill in the `out_param` from `set_like`, then the `has_mul M` instance would be available for synthesis and we'd be in business. In Lean 4 however, we will often go from right to left, so that `MulMemClass ?M S [?inst : Mul ?M]` is handled first, which can't be solved before finding a `Mul ?M` instance on the metavariable `?M`, causing search through all `Mul` instances. The solution is: whenever a class is declared that takes another class as parameter (i.e. unbundled inheritance), the `out_param`s of the parent class should be unmarked and become in-params in the child class. Then Lean will try to find the parent class instance first, fill in the `out_param`s and we'll be able to synthesize the child class instance without problems. One consequence is that sometimes we have to give slightly more type ascription when talking about membership and the types don't quite align: if `M` and `M'` are semireducibly defeq, then before `zero_mem_class S M` would work to prove `(0 : M') ∈ (s : S)`, since the `out_param` became a metavariable, was filled in, and then checked (up to semireducibility apparently) for equality. Now `M` is checked to equal `M'` before applying the instance, with instance-reducible transparency. I don't think this is a huge issue since it feels Lean 4 is stricter about these kinds of equalities anyway. Mathlib4 pair: leanprover-community/mathlib4#1832
bors bot
pushed a commit
to leanprover-community/mathlib
that referenced
this pull request
Jan 27, 2023
…d not repeat the parents' `out_param` (#18291) This PR is a backport for a mathlib4 fix for a large amount of issues encountered in the port of `group_theory.subgroup.basic`, leanprover-community/mathlib4#1797. Subobject classes such as `mul_mem_class` and `submonoid_class` take a `set_like` parameter, and we were used to just copy over the `M : out_param Type` declaration from `set_like`. Since Lean 3 synthesizes from left to right, we'd fill in the `out_param` from `set_like`, then the `has_mul M` instance would be available for synthesis and we'd be in business. In Lean 4 however, we will often go from right to left, so that `MulMemClass ?M S [?inst : Mul ?M]` is handled first, which can't be solved before finding a `Mul ?M` instance on the metavariable `?M`, causing search through all `Mul` instances. The solution is: whenever a class is declared that takes another class as parameter (i.e. unbundled inheritance), the `out_param`s of the parent class should be unmarked and become in-params in the child class. Then Lean will try to find the parent class instance first, fill in the `out_param`s and we'll be able to synthesize the child class instance without problems. One consequence is that sometimes we have to give slightly more type ascription when talking about membership and the types don't quite align: if `M` and `M'` are semireducibly defeq, then before `zero_mem_class S M` would work to prove `(0 : M') ∈ (s : S)`, since the `out_param` became a metavariable, was filled in, and then checked (up to semireducibility apparently) for equality. Now `M` is checked to equal `M'` before applying the instance, with instance-reducible transparency. I don't think this is a huge issue since it feels Lean 4 is stricter about these kinds of equalities anyway. Mathlib4 pair: leanprover-community/mathlib4#1832
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.