Zulip Chat Archive

Stream: maths

Topic: decidable linear order


view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 19:39):

We always define decidable_linear_order anyway.

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 19:39):

(some instances are noncomputable)

view this post on Zulip Patrick Massot (Oct 18 2020 at 19:43):

@Mario Carneiro ?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 18 2020 at 19:47):

and of course in classical land they are the same thing

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Oct 18 2020 at 19:56):

The example you gave is an instance of this.

view this post on Zulip Heather Macbeth (Oct 18 2020 at 19:56):

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.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 (≤)

view this post on Zulip Floris van Doorn (Oct 18 2020 at 23:17):

I'm a big fan of the change!

view this post on Zulip 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).

view this post on Zulip Gabriel Ebner (Oct 19 2020 at 07:42):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 19 2020 at 12:39):

What pi instances have linear_order?

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Oct 19 2020 at 12:43):

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

view this post on Zulip Mario Carneiro (Oct 19 2020 at 12:43):

we have all three now

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 19 2020 at 12:44):

Why this should become noncomputable?

view this post on Zulip Yury G. Kudryashov (Oct 19 2020 at 12:44):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 19 2020 at 12:45):

yeah, partial orders should stay as they are

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 19 2020 at 12:46):

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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Oct 20 2020 at 03:48):

lean#484


Last updated: May 14 2021 at 19:21 UTC