## Stream: maths

### Topic: decidable linear order

#### Yury G. Kudryashov (Oct 18 2020 at 19:38):

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

#### Yury G. Kudryashov (Oct 18 2020 at 19:39):

We always define decidable_linear_order anyway.

#### Yury G. Kudryashov (Oct 18 2020 at 19:39):

(some instances are noncomputable)

#### Patrick Massot (Oct 18 2020 at 19:43):

@Mario Carneiro ?

#### Mario Carneiro (Oct 18 2020 at 19:46):

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 (Oct 18 2020 at 19:47):

and of course in classical land they are the same thing

#### Heather Macbeth (Oct 18 2020 at 19:54):

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 (Oct 18 2020 at 19:55):

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 (Oct 18 2020 at 19:56):

The example you gave is an instance of this.

#### Heather Macbeth (Oct 18 2020 at 19:56):

Recently
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 (Oct 18 2020 at 19:57):

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 (Oct 18 2020 at 20:00):

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

#### Yury G. Kudryashov (Oct 18 2020 at 20:39):

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 (Oct 18 2020 at 23:17):

I'm a big fan of the change!

#### Floris van Doorn (Oct 18 2020 at 23:23):

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 (Oct 19 2020 at 07:42):

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

#### Gabriel Ebner (Oct 19 2020 at 07:44):

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

#### Yury G. Kudryashov (Oct 19 2020 at 12:39):

What pi instances have linear_order?

#### Mario Carneiro (Oct 19 2020 at 12:42):

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 (Oct 19 2020 at 12:43):

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

#### Mario Carneiro (Oct 19 2020 at 12:43):

we have all three now

#### Gabriel Ebner (Oct 19 2020 at 12:44):

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 (Oct 19 2020 at 12:44):

Why this should become noncomputable?

#### Yury G. Kudryashov (Oct 19 2020 at 12:44):

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

#### Mario Carneiro (Oct 19 2020 at 12:44):

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 (Oct 19 2020 at 12:45):

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

#### Mario Carneiro (Oct 19 2020 at 12:45):

yeah, partial orders should stay as they are

#### Mario Carneiro (Oct 19 2020 at 12:46):

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

#### Mario Carneiro (Oct 19 2020 at 12:46):

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

#### Mario Carneiro (Oct 19 2020 at 12:47):

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

#### Yury G. Kudryashov (Oct 20 2020 at 03:48):

lean#484

Last updated: May 14 2021 at 19:21 UTC