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_orderor 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 distribs 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_orderand 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):

Oh, you're right! I stared at finset.sup before but I didn't understand what I was looking at until now.