decidable linear order

Stream: maths

[Yury G. Kudryashov]

What do you think about changing the definition of linear_order to be what's now called decidable_linear_order?

[Yury G. Kudryashov]

We always define decidable_linear_order anyway.

[Yury G. Kudryashov]

(some instances are noncomputable)

[Patrick Massot]

@Mario Carneiro ?

[Mario Carneiro]

I think this makes sense. Really, I think this will help to decrease a lot of choice usage if we just delete linear_order and replace it with DLO because there aren't any instances of linear_order that aren't DLO's, intuitionistically, because the disjunction is too hard to establish otherwise

[Mario Carneiro]

and of course in classical land they are the same thing

[Heather Macbeth]

At the moment, there are gaps in the algebraic hierarchy, because people haven't bothered exactly duplicating everything in decidable and non-decidable versions. For example I believe there is docs#decidable_linear_ordered_add_comm_group but not docs#linear_ordered_add_comm_group.

[Patrick Massot]

This is also a mess because we have too many things bundling an order relation instead of taking it as a parameter and living in Prop

[Patrick Massot]

The example you gave is an instance of this.

[Heather Macbeth]

Recently
https://github.com/leanprover-community/mathlib/blob/fee2dfaadadd9f77c8837ac6a068e4aa9002e28d/src/topology/algebra/ordered.lean#L1299
I wanted to prove something for the non-existent linear_ordered_add_comm_group, and had to instead choose between proving it for linear_ordered_ring with the unneccessary extra operation or for decidable_linear_ordered_add_comm_group with the unnecessary decidability. (I chose the former, but in retrospect that was the wrong choice.)

[Heather Macbeth]

There are many things wrong with docs#decidable_linear_ordered_add_comm_group! Another is that it should be to_additive of docs#decidable_linear_ordered_comm_group, but the latter doesn't exist.

[Patrick Massot]

My secret hope is that our refactoring machine will get tired of this mess when he'll be done with convexity.

[Yury G. Kudryashov]

There is a trick for non-existent linear_ordered_add_comm_group: you assume ordered_add_comm_group and is_total G (≤)

[Floris van Doorn]

I'm a big fan of the change!

[Floris van Doorn]

I've been looking at the file ordered_group recently too. I want to redefine docs#canonically_ordered_add_monoid so that it extends has_sub, because we currently have many instances of canonically_ordered_add_monoid with their own has_sub instance. However, to show all the lemmas about has_sub generally, I need to sometimes assume linearity of the order and sometimes cancellation for the addition (which means 3 new classes). Also, measures do not form a docs#ordered_comm_monoid, since the rule a + b < a + c → b < c does not hold. But they should still be a canonically_ordered_add_monoid, which means having 1+ more classes of canonically ordered monoids.

I'm wondering if we should make canonically_ordered_... a mixin that depends on the order via [partial_order \a] or [linear_order \a] (and maybe also on the algebra part? But what extra axioms should be in the mixin usually depends on the algebraic part).

[Gabriel Ebner]

This makes all the pi instances for orders noncomputable, right?

[Gabriel Ebner]

IMHO, we should do the same as for fields, etc., and split decidable_linear_order into linear_order and decidable_le.

[Yury G. Kudryashov]

What pi instances have linear_order?

[Mario Carneiro]

Gabriel Ebner said:

IMHO, we should do the same as for fields, etc., and split decidable_linear_order into linear_order and decidable_le.

I'm confused. Isn't this the exact opposite of the proposal? We already have linear_order and decidable_le, but I think we should do away with linear_order and replace it with DLO

[Gabriel Ebner]

We have DLO. I'm saying we should get rid of it.

[Mario Carneiro]

we have all three now

[Gabriel Ebner]

Yury G. Kudryashov said:

What pi instances have linear_order?

Of course, pi.linear_order doesn't make sense. I meant docs#pi.partial_order.

[Yury G. Kudryashov]

Why this should become noncomputable?

[Yury G. Kudryashov]

I propose to add decidable_le to linear_order, not to partial_order.

[Mario Carneiro]

but I think there isn't any reason to not put decidable assumptions in linear_order because there are zero instances of a linear_order that is not decidable

[Gabriel Ebner]

Ah, if it's only for linear orders (but not partial orders), then it should be fine.

[Mario Carneiro]

yeah, partial orders should stay as they are

[Mario Carneiro]

I do know an example of a linear order on pi, namely the ordinal exponential and similar constructions

[Mario Carneiro]

you can well order a pi if the base set is well ordered

[Mario Carneiro]

but that's a pretty choicy construction anyway so I don't think it matters too much what we do there

[Yury G. Kudryashov]

lean#484