# Zulip Chat Archive

## Stream: maths

### Topic: decidability

#### Sebastien Gouezel (Nov 17 2018 at 16:00):

tldr; why do we have `linear_order`

and `decidable_linear_order`

?

I was bitten recently by the fact that some type classes are built on `linear_order`

, while some theorems require `decidable_linear_order`

(i.e., a linear order in which the relation `a ≤ b`

is decidable).

I think I understand why decidability is important from a practical point of view: you want `dec_trivial`

to be able to compute, to decide simple things, say on finite sets. What I don't get is why everything could not be said to be decidable, with the caveat that you should not use `dec_trivial`

when something is not computable. Maybe with the possibility to replace noncomputable stuff by computable ones in some types for which you really care about computability.

Could we base all mathlib on `decidable_linear_order`

, removing completely `linear_order`

or would it have dreadful consequences? Let me emphasize that I don't care at all about constructivist mathematics, or the strength of axioms used to prove theorems: my question is really about practical consequences, not philosophical ones -- although I can perfectly hear an answer of the form "there is no practical consequence, but we want to keep it separate for philosophical reasons".

NB: the following typechecks

noncomputable instance zou {α : Type u} [h : linear_order α] : decidable_linear_order α := { decidable_le := begin assume a b, apply classical.dec, end, ..h }

#### Kenny Lau (Nov 17 2018 at 16:02):

because `abs`

wants to be computable

#### Kenny Lau (Nov 17 2018 at 16:03):

(now it is not the case that `abs`

is computable implies the order is decidable, which is something I would want Lean to know, because currently we have a noncomputable `abs`

for real)

#### Sebastien Gouezel (Nov 17 2018 at 16:04):

What do you mean, it wants to be computable?

#### Kenny Lau (Nov 17 2018 at 16:05):

it means we want `abs`

to be computable

#### Kenny Lau (Nov 17 2018 at 16:06):

actually I don't know

#### Kenny Lau (Nov 17 2018 at 16:06):

I'll let other people answer this question

#### Kevin Buzzard (Nov 17 2018 at 17:34):

Here's a guess. Some arguments work fine without decidability, some need decidability. As a mathematician I used to barely notice this because the moment I needed some prop to be decidable I'd just switch on `classical.decidable_prop`

or whatever it's called and keep going. More recently I realised that there was a better way to do this -- instead of just switching this on all the time I'd just add the relevant decidability instances to the objects in the results that needed them. This seemed like a more canonical thing to do, because that way people who do care about these things can use my results anyway. Is that an answer to the question or is there more to it in this case?

#### Chris Hughes (Nov 17 2018 at 17:40):

I think sometimes you define `linear_order`

on a class of types, such that it will be decidable on some of the types but not others, so you don't just want to use classical to define the instance. For reals it's okay to use classical decidability, since you're never going to have proper decidability.

#### Sebastien Gouezel (Nov 17 2018 at 18:02):

There is more to it because of the typeclass system. Take for instance `conditionally_complete_linear_order`

, which extends `linear_order`

. In a theorem, you can not really state the assumption that your order is decidable: if you write `[conditionally_complete_linear_order α] [decidable_linear_order α]`

, then the two statements are talking about different orders, so they don't talk to each other. What you would need is a mixin to add decidability, but it is not really there. And if you add `classical.decidable_prop`

in the header or as a local instance (which I always do), the type class system is not able to use it to convert linear orders to decidable ones automagically.

What I can do for instance is change `conditionally_complete_linear_order`

to extend `decidable_linear_order`

instead of `linear_order`

. Indeed, I have done it in my library, it solves all my typeclasses problems, and the library compiles fine. I wonder if the big guys would accept a PR like that, or if there is a reason to avoid this.

#### Kevin Buzzard (Nov 17 2018 at 18:21):

Oh I see -- there really is an issue here. Yeah, typeclasses are not great for mathematics sometimes, this is why we have `distrib`

s and stuff. But why can't you just add the assumption that your order is decidable? Can't you just make it an extra hypothesis and then feed it to the type class system?

#### Chris Hughes (Nov 17 2018 at 18:22):

No because

if you write

`[conditionally_complete_linear_order α] [decidable_linear_order α]`

, then the two statements are talking about different orders, so they don't talk to each other.

#### Sebastien Gouezel (Nov 17 2018 at 18:25):

The proper solution is certainly to define yet another class `conditionally_complete_decidable_linear_order`

, defined just like `conditionally_complete_linear_order`

but replacing `linear_order`

with `decidable_linear_order`

, and prove an instance going from it to `conditionally_complete_linear_order`

. But this is getting super-heavy...

#### Kevin Buzzard (Nov 17 2018 at 18:26):

I mean why can't you just literally put `forall a b, decidable (a <= b)`

in?

#### Kenny Lau (Nov 17 2018 at 18:26):

just use old structure cmd and you'll be done in one line

#### Chris Hughes (Nov 17 2018 at 18:26):

Because `max`

is defined on `decidable_linear_order`

not `decidable_rel has_le.le`

#### Chris Hughes (Nov 17 2018 at 18:26):

As are a bunch of lemmas

#### Sebastien Gouezel (Nov 17 2018 at 18:27):

If one could remove `linear_order`

and cut the complexity in half, I certainly wouldn't mind :)

#### Kevin Buzzard (Nov 17 2018 at 18:27):

And you can't make the correct instance of `decidable_linear_order`

from the pieces you have?

#### Sebastien Gouezel (Nov 17 2018 at 18:28):

And you can't make the correct instance of

`decidable_linear_order`

from the pieces you have?

In each proof, yes you can. But not as a global instance, since there is already an arrow in the other direction and you want to avoid loops.

#### Kevin Buzzard (Nov 17 2018 at 18:29):

These issues do seem to come up sometimes. I get the feeling that the type class system is not quite right for maths sometimes. Chris had problems with diamonds coming from very innocuous issues as well, where he had two instances of a singleton (but not a Prop) which were not defeq and this really hurt him.

#### Kevin Buzzard (Nov 17 2018 at 18:30):

The issue you raise really not mathematical. It's just showing that Lean cannot cope with a situation which comes up very naturally in mathematics.

#### Kevin Buzzard (Nov 17 2018 at 18:32):

There was the whole metric space / topological space farce too -- the topological space underlying the product of two metric spaces was canonically isomorphic to but not defeq to the product of the underlying topological spaces, and because the type class system was involved Johannes had to jump through all sorts of hoops. This was presented to Patrick and me as some sort of clever trick but all the time I could see that something was wrong in the underlying system. It seemed to be the case that type class inference works great if all functors are forgetful, but the moment you want to do something where you're not in this situation you are in trouble.

#### Sebastien Gouezel (Nov 17 2018 at 18:33):

The issue you raise really not mathematical. It's just showing that Lean cannot cope with a situation which comes up very naturally in mathematics.

Let me disagree with this: in mathematics, everything is decidable, so there is just one class and the issue disappears.

#### Kevin Buzzard (Nov 17 2018 at 18:33):

right -- but you are just talking about your specific problem. I'm saying that you are a mathematician running into problems with the type class inference system, and you are by no means alone

#### Sebastien Gouezel (Nov 17 2018 at 18:34):

Yes, I can see I'm not alone!

#### Kevin Buzzard (Nov 17 2018 at 18:34):

I agree that the other issues are in some sense more non-mathematical than yours :-)

#### Kevin Buzzard (Nov 17 2018 at 18:35):

but also in Chris' issue there was just one instance, and the issue didn't disappear, because he had two copies of it and they weren't defeq even though they were trivially equal

#### Kevin Buzzard (Nov 17 2018 at 18:35):

All of us want, in some sense, to be able to insert proofs into the system. "Yes I know you now have two instances of [blah], but here's a proof that they're the same, now stop moaning"

#### Kevin Buzzard (Nov 17 2018 at 18:36):

You really want to put [decidable_linear_order] into your system and also a hypothesis that the underlying linear orders are the same one.

#### Kevin Buzzard (Nov 17 2018 at 18:36):

But that can't be done

#### Kevin Buzzard (Nov 17 2018 at 18:37):

Who knows if this will be solved in Lean 4 Kenny. I thought Sebastian said that they weren't going to change the type class system.

#### Kevin Buzzard (Nov 17 2018 at 18:37):

No doubt Mario will wake up at some point and come up with another workaround

#### Kevin Buzzard (Nov 17 2018 at 18:37):

but is workarounds what we really want?

#### Reid Barton (Nov 17 2018 at 18:51):

I get the sense that `decidable_linear_order`

should have been a mix-in, but we can't just change it because it's in core.

#### Mario Carneiro (Nov 17 2018 at 23:31):

I am okay with `conditionally_complete_linear_order`

extending `decidable_linear_order`

#### Mario Carneiro (Nov 17 2018 at 23:31):

your instance is called `classical.DLO`

by the way

#### Mario Carneiro (Nov 17 2018 at 23:33):

To quote myself from somewhere, we want to assume decidability when decidability is decidable. So when it's either definitely the case (like `rat`

) or definitely not the case (like `real`

). As chris points out there are times when you are doing a construction over generic types, and there decidability can sometimes cause problems

#### Kenny Lau (Nov 17 2018 at 23:33):

when decidability is decidable

@.@"

#### Mario Carneiro (Nov 17 2018 at 23:34):

But yes, this is in part because the typeclass exists, in core, and we have to deal with it.

#### Reid Barton (Nov 17 2018 at 23:35):

just use `classical.decidable_decidable`

#### Mario Carneiro (Nov 17 2018 at 23:35):

For `conditionally_complete_linear_order`

, this is already hopelessly non-computable (you can't define anything with the type of `Sup`

) so decidability is fine

#### Chris Hughes (Nov 17 2018 at 23:39):

Aren't integers a conditionally complete linear order?

#### Mario Carneiro (Nov 17 2018 at 23:39):

there is no computable instance of it

#### Mario Carneiro (Nov 17 2018 at 23:40):

because you can't compute a Sup

#### Mario Carneiro (Nov 17 2018 at 23:40):

even on `bool`

it's not computable

#### Bryan Gin-ge Chen (Nov 17 2018 at 23:55):

This is a somewhat-related question I had from back when I was messing with partitions. How much extra stuff would we have to write if we wanted to have a computable Sup over finsets rather than arbitrary sets?

#### Kenny Lau (Nov 17 2018 at 23:56):

zero, because it's there already

#### Bryan Gin-ge Chen (Nov 17 2018 at 23:59):

Oh, you're right! I stared at `finset.sup`

before but I didn't understand what I was looking at until now.

Last updated: May 09 2021 at 11:09 UTC