[Merged by Bors] - refactor(library): decouple algebraic hierarchy from core lib #229

jcommelin · 2020-05-11T17:42:08Z

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.

gebner · 2020-05-11T17:49:20Z

Can you merge master? The diff is full with changes from your norm_num PR.

gebner · 2020-05-11T17:50:50Z

Also: PR title!

urkud · 2020-05-11T18:04:53Z

What's the point of commenting out the code instead of deleting it?

jcommelin · 2020-05-11T18:08:40Z

Because it's still somewhat WIPpy. I didn't know if it had to be resurrected or not.

jcommelin · 2020-05-12T05:18:16Z

I've now also removed a whole bunch of commented code.

jcommelin · 2020-05-12T06:32:49Z

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.

gebner · 2020-05-12T09:19:15Z

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:

Some tests fail because you've removed lemmas that the C++ code relies on (and that are listed in constants.txt). Check the errors in the check_constants.lean and put the lemmas back.
(by cc : a + b = b + a) requires instances for is_associative (+) and is_commutative (+). Add them back (locally?). Same goes for ac_refl.
Often add_comm can be replaced by nat.add_comm.
Try to keep the spirit of the test.
Many tests are named after the issue number, check the old Lean bug tracker to figure out what the test is supposed to be testing. That is, for 1898.lean go to segfault with broken code (accessing H.0 if H : comm_ring R) leanprover/lean3#1898

This reverts commit ee2c42f.

This reverts commit 55ddbbc.

gebner

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/algebra/functions.lean

library/init/data/int/basic.lean

library/init/data/int/order.lean

library/init/data/nat/bitwise.lean

gebner · 2020-05-15T08:15:14Z

library/init/data/nat/gcd.lean

@@ -9,7 +9,7 @@ prelude
 import init.data.nat.lemmas init.meta.well_founded_tactics



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 : ℕ → ℕ → ℕ := ...

@digama0 I thought you said it could go. I'll let you two decide, and then fix accordingly.

Ok, I'm putting the defs back

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.

@digama0 I don't follow. Is there something that should be changed? The CI seems happy.

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.

@digama0 Aah, that was on a different branch. I decided not to pursue that here.
Anyways, that settles this discussion, I think.

What happened to removing default_dec_tac? Isn't that needed for the decoupling project?

No, it turns out that it isn't needed.

It might still be a good idea. But it can be a different PR.

library/init/data/nat/lemmas.lean

This reverts commit 7682053.

gebner · 2020-05-15T17:07:24Z

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>

bors · 2020-05-15T17:19:19Z

Build failed:

Build linux Release

bryangingechen · 2020-05-15T17:42:57Z

A test from #237 needs to be updated: https://github.com/leanprover-community/lean/runs/678900032#step:8:1241

gebner · 2020-05-15T17:47:30Z

bors d+

bors · 2020-05-15T17:47:31Z

✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

jcommelin · 2020-05-15T17:48:22Z

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>

bors · 2020-05-15T18:28:12Z

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/mathlib@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

jcommelin added 7 commits May 11, 2020 07:35

Remove norm_num

e55c7e1

Remove a bunch of tests

a349f31

And remove another test

b1c6ca1

Merge remote-tracking branch 'origin/master' into remove-norm-num

93ac6c4

Regenerate constants

864a425

Make import lines start with 'import'

7774d40

Decouple algebraic hierarchy from core lib

83a50a5

jcommelin added WIP Work in progress rfc labels May 11, 2020

gebner added the enhancement New feature or request label May 11, 2020

Merge branch 'master' into strip-algebra

5c41ca3

jcommelin changed the title ~~Strip algebra -- decouple algebraic hierarchy from core lib~~ refactor(library): decouple algebraic hierarchy from core lib May 11, 2020

jcommelin added 3 commits May 11, 2020 21:10

Remove unshackled files

55ddbbc

Remove commented code

ee2c42f

Remove a test

b7f8b57

jcommelin and others added 8 commits May 13, 2020 06:33

Revert "Remove commented code"

8a9d32d

This reverts commit ee2c42f.

Revert "Remove unshackled files"

97a0088

This reverts commit 55ddbbc.

wip

23f9ca8

Merge branch 'master' into strip-algebra

b249cba

Hooray, we're compiling again

0449851

Remove unshackled files

83cf72d

Fix constants

1a190f3

Remove unused code.

245b721

jcommelin added 7 commits May 14, 2020 09:18

Fix run test smt_ematch_alg_issue

7076b9e

Fix run test simp_lemma_issue

4ff4ece

Fix run test ematch2

5ee4e4f

Remove example in run test using_smt2

1a3031c

Remove 4 failing tests

9ff741d

Fix test 123-2

82d875d

Merge branch 'master' into strip-algebra

6260f1b

gebner removed the WIP Work in progress label May 14, 2020

gebner reviewed May 15, 2020

View reviewed changes

jcommelin added 3 commits May 15, 2020 13:00

Remove a lot of dead code, put gcd back in core

2b5d4bf

Revert "Fix run test exhaustive_vm_impl_test"

02b8bcd

This reverts commit 7682053.

Remove more commented code

aec23b2

Merge remote-tracking branch 'origin/master' into strip-algebra

3a09238

Fix run test 236c

c2787f2

bors bot changed the title ~~refactor(library): decouple algebraic hierarchy from core lib~~ [Merged by Bors] - refactor(library): decouple algebraic hierarchy from core lib May 15, 2020

bors bot closed this May 15, 2020

bors bot deleted the strip-algebra branch May 15, 2020 18:28

jcommelin mentioned this pull request May 16, 2020

[Merged by Bors] - chore(*): release 3.13.0 #243

Closed

bryangingechen mentioned this pull request May 17, 2020

[Merged by Bors] - fix(library/init/data/int/order): remove double namespaces, protect nat and int lemmas #245

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(library): decouple algebraic hierarchy from core lib #229

[Merged by Bors] - refactor(library): decouple algebraic hierarchy from core lib #229

jcommelin commented May 11, 2020 •

edited

Loading

gebner commented May 11, 2020

gebner commented May 11, 2020

urkud commented May 11, 2020

jcommelin commented May 11, 2020

jcommelin commented May 12, 2020

jcommelin commented May 12, 2020

gebner commented May 12, 2020

gebner left a comment

gebner May 15, 2020

jcommelin May 15, 2020 •

edited

Loading

jcommelin May 15, 2020

digama0 May 15, 2020

jcommelin May 15, 2020

digama0 May 15, 2020

jcommelin May 15, 2020

digama0 May 15, 2020 •

edited

Loading

jcommelin May 15, 2020

jcommelin May 15, 2020

gebner commented May 15, 2020

bors bot commented May 15, 2020

bryangingechen commented May 15, 2020

gebner commented May 15, 2020

bors bot commented May 15, 2020

jcommelin commented May 15, 2020

bors bot commented May 15, 2020

		@@ -9,7 +9,7 @@ prelude
		import init.data.nat.lemmas init.meta.well_founded_tactics

[Merged by Bors] - refactor(library): decouple algebraic hierarchy from core lib #229

[Merged by Bors] - refactor(library): decouple algebraic hierarchy from core lib #229

Conversation

jcommelin commented May 11, 2020 • edited Loading

gebner commented May 11, 2020

gebner commented May 11, 2020

urkud commented May 11, 2020

jcommelin commented May 11, 2020

jcommelin commented May 12, 2020

jcommelin commented May 12, 2020

gebner commented May 12, 2020

gebner left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jcommelin May 15, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

digama0 May 15, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gebner commented May 15, 2020

bors bot commented May 15, 2020

bryangingechen commented May 15, 2020

gebner commented May 15, 2020

bors bot commented May 15, 2020

jcommelin commented May 15, 2020

bors bot commented May 15, 2020

jcommelin commented May 11, 2020 •

edited

Loading

jcommelin May 15, 2020 •

edited

Loading

digama0 May 15, 2020 •

edited

Loading