move init.algebra.order from core to mathlib?

Stream: general

[Scott Morrison]

In core lean, library/init/algebra/order.lean is not actually imported by anything else. Would anyone object if we moved it to mathlib?

[Gabriel Ebner]

Are you sure? At least init.algebra.functions imports it, and I find it hard to believe that max and min are unused.

[Gabriel Ebner]

But if it is unused (or we can easily make it unused), then I'm all for moving it to mathlib. Core Lean 4 doesn't have orders either.

[Yaël Dillies]

I'm all for it too. Just be wary that it is transitively imported by init.data.nat.lemmas which is imported by a bunch of other stuff too.

[Yaël Dillies]

I'll be happy to carry out the extraction this weekend.

[Yaël Dillies]

What's our general core extraction policy? In my opinion, we could empty core one file at a time, starting from the leaves of the import tree, but maybe swe don't want some of it in mathlib?

[Johan Commelin]

@Yaël Dillies Core extraction to mathlib usually happens in a big bump. Because you need to release a new version of Lean, and then bump mathlib to that new version.

[Johan Commelin]

Doing that 1 file at a time would get very tiresome quickly.

[Yaël Dillies]

Ah yeah. So what do we want to extract from core this time?

[Scott Morrison]

Err, yes I was totally wrong about being able to remove it. However I'm trying to remove all decidable instances embedded inside linear_order. So far it is going well, but I'm not sure how much remains.

[Mario Carneiro]

wait, why are you doing that?

[Mario Carneiro]

That's reversing a patch that was done a year or so ago

[Scott Morrison]

Really? :-) Oops. I better go read up on that. Why did we do that?

[Mario Carneiro]

to get rid of decidable_linear_order

[Scott Morrison]

But why not just have decidability of le completely separate?

[Mario Carneiro]

it turned out that linear_order without decidability was just annoying and useless

[Mario Carneiro]

so you had lots of undesirable decidable arguments to lemmas

[Scott Morrison]

I guess I was imagining that by the time we got to mathlib we would just turn on classical.

[Mario Carneiro]

sure, but in this case that means that you don't need to do anything to fill in the extra fields on linear_order

[Scott Morrison]

That's true. It was just upsetting me that the definition had this weird computational cruft in it. :-)

[Scott Morrison]

I'm not particularly attached!

[Scott Morrison]

The change seems pretty straightforward on the core side: https://github.com/leanprover-community/lean/pull/628.

But I'm happy to drop it.

[Mario Carneiro]

Also, there are a few choice-free proofs in mathlib, and one of the primary reasons for classical use in those cases was due to lemmas about linear orders that used classical instead of a decidable argument, even though literally every (constructively provable) linear_order instance in mathlib is a decidable_linear_order instance

[Mario Carneiro]

so it makes sense to bundle them together

[Mario Carneiro]

We had talks about a linter that would watch specific choice-free theorems to ensure they stay choice-free. I never got around to writing it, but I'm fairly sure your PR would fail the linter. :)

[Scott Morrison]

I guess the reason I started looking at this was continuing experiments with removing old_structure_cmd. I had a case where I wanted to make linear_order the "non-primary" parent, so (until we reach Lean4), I would have to copy and paste in all the fields of linear_order.

[Scott Morrison]

With this change, that would just be le_total. But as is I'd have to copy and paste a lot of cruft! :-)

[Scott Morrison]

Could that linter be as simple as a test that prints axioms, and a script that checks the output?

[Mario Carneiro]

Yes, although it is also possible to make it a bit nicer by using the axiom checker tactic that exists somewhere on zulip (search for @[intuit])

[Scott Morrison]

What do you think about this argument via old_structure_cmd in favour of stripping down linear_order?

[Mario Carneiro]

I'm not sure I have the whole context. What's the class diamond in question?

[Mario Carneiro]

I notice that linear_order has grown a max and min field since last I checked. I think this stuff just builds up over time

[Mario Carneiro]

One way to reduce the duplication is with a mixin that collects all the fields being added. Mathcomp does that systematically

[Scott Morrison]

(conditionally_)complete_linear_order has linear_order and (conditionally_)complete_lattice as parents.

[Yaël Dillies]

One thing that I would like to see off core is init.data.list.basic so that I can document it, but again it seems a bit hard as of now.

[Scott Morrison]

Here's a hand-drawn picture of the lattice hierarchy

[Scott Morrison]

@Yaël Dillies, you can send documentation PRs to core!

[Yaël Dillies]

I guess!

[Yaël Dillies]

Okay, one thing we can strip off core is all the ℤ stuff.

[Scott Morrison]

@Mario Carneiro, do you know why linear_order ended up with three separate decidable fields, when only the le is needed?

[Mario Carneiro]

As far as I know, it's always been like that. But I think the reasoning is the same as for why we have max and min or any number of other "redundant" fields: deriving one field from another can lead to diamond problems

[Yaël Dillies]

Scott Morrison said:

Here's a hand-drawn picture of the lattice hierarchy

Why isn't complete_linear_order extending conditionally_complete_linear_order?

[Mario Carneiro]

I think the sup function has a different type in those two cases

[Yaël Dillies]

Yeah, I did a similar thing recently with locally_finite_order. Only finset.Icc is needed but I also put Ico, Ioc and Ioo as fields.

[Mario Carneiro]

I can't think of any examples where you would want to use a conditionally_complete_linear_order lemma on a complete_linear_order. The extra assumptions are basically always unwanted

[Gabriel Ebner]

deriving one field from another can lead to diamond problems

It's not just diamonds, but also performance issues. A single equality check is typically faster than two less-than checks.

[Yaël Dillies]

Yaël Dillies said:

Okay, one thing we can strip off core is all the ℤ stuff.

How do I do that? For now, should I just open a PR to core that deletes the files?

[Scott Morrison]

Generally the thing to do is create a PR that modifies core, then build a local copy of Lean3, create a elan toolchain link pointing to that, then make a branch of mathlib in which you use elan override set to ask lean to use your local copy, and then make sure that you can fix mathlib. :-)

[Scott Morrison]

If so, then you ask for the PR to core to be merged.

[Yaël Dillies]

Uh uh, how do I do any of those steps?

[Yaël Dillies]

By "local copy of mathlib", do you mean a branch?

[Yaël Dillies]

And what should I do with the tests that are in core? Simply delete them and maybe restore them on the other side?

[Johan Commelin]

If the tests are testing stuff that you are removing, yes. If the tests are using stuff you remove as an example, but they are testing something else, then the test needs to be rewritten.

[Yaël Dillies]

Okay, how do I create a copy of Lean3?

[Yaël Dillies]

My current copy seems to not be set up properly.

[Scott Morrison]

The basic version is

git clone git@github.com:leanprover-community/lean.git
cd lean
mkdir -p build/release
cd build/release
cmake ../../src
make

[Scott Morrison]

and see https://github.com/leanprover-community/lean/blob/master/doc/make/index.md when things go wrong.

[Scott Morrison]

I didn't say a local copy of mathlib, I said a local copy of Lean3. (Although if you're using elan override, I prefer to make a new copy of mathlib to do that in, so that when I forget to remove the override life isn't too confusing...)

[Scott Morrison]

I better go to sleep, hopefully others can help. Good luck!

[Yaël Dillies]

Thanks!

[Yaël Dillies]

I'm stuck at cmake ../../src.

[Eric Rodriguez]

What do you mean stuck? Do you have cmake and make?

[Yaël Dillies]

I just installed cmake. Not sure I have make

[Yaël Dillies]

I am very bad at software stuff, I'm sorry.

[Yaël Dillies]

I've opened lean#629

[Yaël Dillies]

test.lean.extra.print_info fails, but it seems it was already doing so before?

[Eric Rodriguez]

I'm not sure what OS you're on, but this is a major PITA in Windows I remmeber

[Yaël Dillies]

I'm on Windows indeed :sob:

[Eric Rodriguez]

I wrote some install guide in the Lean repo if you want, also alternatively clion is pretty OK at dealing with it but that's a big install and you're not gonna mess with the c++ stuff I guess

[Yaël Dillies]

Seems like I got tricked by docgen not showing the default imports + the multi-imports lines.

[Yaël Dillies]

Could we get an import graph of core Lean?

[Floris van Doorn]

I noticed a problem that is related to this: docs#subtype.linear_order gives a different proof of decidable equality than docs#subtype.decidable_eq. I'm fixing this in #9701