-
Notifications
You must be signed in to change notification settings - Fork 80
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.
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
[Merged by Bors] - refactor(library): decouple algebraic hierarchy from core lib #229
Conversation
Can you merge master? The diff is full with changes from your |
Also: PR title! |
What's the point of commenting out the code instead of deleting it? |
Because it's still somewhat WIPpy. I didn't know if it had to be resurrected or not. |
I've now also removed a whole bunch of commented code. |
There's a whole bunch of tests failing. What do we want to do with them? I've removed one that I think clearly could be removed, but I'm not sure what to do with most of them. |
I've quickly looked over the failing tests:
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The tests look good. The commented-out stuff should be removed.
As I've said, I'm not sure we should remove nat.gcd
and int.gcd
.
library/init/data/nat/gcd.lean
Outdated
@@ -9,7 +9,7 @@ prelude | |||
import init.data.nat.lemmas init.meta.well_founded_tactics | |||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure if you should remove the gcd. nat.gcd
and int.gcd
have an efficient VM implementations using GMP.
One option is to keep the gcd implementation as meta constants, and then use vm_override
in mathlib to hook up to fast implementation:
meta constant nat.gcd_gmp : ℕ → ℕ → ℕ
-- in mathlib:
@[vm_override nat.gcd_gmp]
def nat.gcd : ℕ → ℕ → ℕ := ...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@digama0 I thought you said it could go. I'll let you two decide, and then fix accordingly.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ok, I'm putting the defs back
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh, I didn't know that these were vm overridden. If so, then they should stay. But AFAIR they don't require much automation, although the def has to be stated a bit differently for the decreasing proof to work.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@digama0 I don't follow. Is there something that should be changed? The CI seems happy.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure what the latest version of this is, but you've probably fixed it. You asked about it earlier and I said to shift the | (succ x) y := ...
cases to | (succ x) := \lam y, ...
so that lean gets the recursion domain right.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@digama0 Aah, that was on a different branch. I decided not to pursue that here.
Anyways, that settles this discussion, I think.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What happened to removing default_dec_tac
? Isn't that needed for the decoupling project?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, it turns out that it isn't needed.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It might still be a good idea. But it can be a different PR.
LGTM. bors merge |
This PR allows moving `ordered_monoid`, `semiring`, and all the other algebraic classes into mathlib. Classes that are only about orders, such as `decidable_linear_order` remain in core. Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Build failed: |
A test from #237 needs to be updated: https://github.com/leanprover-community/lean/runs/678900032#step:8:1241 |
bors d+ |
✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge pleeeease..... |
This PR allows moving `ordered_monoid`, `semiring`, and all the other algebraic classes into mathlib. Classes that are only about orders, such as `decidable_linear_order` remain in core. Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Pull request successfully merged into master. Build succeeded: |
Features: - use persistent data structures, to improve performance of (module) docstrings (#241) - cache constructed `simp_lemma` objects (#234) - support `local attribute [-instance]` (#240) - show goal after `;` (#239) - `==`: compare id (#238) - mark deps of fixed as fixed (#237) Changes: - Most of `library/init/algebra/*` has been deleted, as part of moving the algebraic hierarchy to mathlib (#229)
…at and int lemmas (#245) This PR protects the lemmas listed in leanprover-community/mathlib3@85ce04a since they are superseded in mathlib. They were all added in #229. Also, this PR removes: - `int.mul_sub_left_distrib` in favor of the shorter `int.mul_sub`, - `int.mul_sub_right_distrib` in favor of the shorter `int.sub_mul`. Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/preparing.20for.20lean-3.2E13.2E0/near/197817609
This PR allows moving
ordered_monoid
,semiring
, and all the other algebraic classes into mathlib.Classes that are only about orders, such as
decidable_linear_order
remain in core.