Zulip Chat Archive

Stream: general

Topic: classical instance confusion


view this post on Zulip Johan Commelin (Oct 08 2019 at 13:27):

For some reason Lean is inferring two different orders on nnreal in some code that I'm working on.

 classical.decidable_linear_order = nnreal.decidable_linear_order

I have open_locale classical at the top of my file... I would hope that makes everything classical...

view this post on Zulip Johan Commelin (Oct 08 2019 at 13:28):

Also... the order on nnreal must be defined using classical, so really Lean is just being pretty silly right now.

view this post on Zulip Floris van Doorn (Oct 08 2019 at 13:41):

Do you have a MWE? I'm surprised that classical.decidable_linear_order appears in your goal. It's not even an instance, and doesn't seem to be used often in the library.

view this post on Zulip Reid Barton (Oct 08 2019 at 15:05):

Are you stuck proving this goal or would you just prefer that it not arise in the first place?

view this post on Zulip Johan Commelin (Oct 08 2019 at 15:15):

I'd rather not have it in the first place

view this post on Zulip Johan Commelin (Oct 08 2019 at 15:15):

I can delta those instances, and then congr proves it

view this post on Zulip Johan Commelin (Oct 08 2019 at 15:15):

But that's just ugly

view this post on Zulip Reid Barton (Oct 08 2019 at 15:19):

I was going to say you should prove/apply a lemma of the form "two DLOs are equal if their orderings are equal" and then use refl

view this post on Zulip Reid Barton (Oct 08 2019 at 15:19):

At least, I assume that's what's going on here since I can't see how it could be otherwise

view this post on Zulip Johan Commelin (Oct 08 2019 at 15:21):

I was trying to apply a lemma, but it failed. So I used convert, and it worked, but gave me the goal to prove that these orders were equal.

view this post on Zulip Johan Commelin (Oct 08 2019 at 15:22):

It would be better if applying the lemma just worked.

view this post on Zulip Johan Commelin (Oct 08 2019 at 15:22):

But I don't know how to make sure that the right order gets inferred

view this post on Zulip Johan Commelin (Oct 08 2019 at 15:23):

I tried giving classical.decidable_eq priority 1 or 1001 but the problem remained.

view this post on Zulip Reid Barton (Oct 08 2019 at 15:38):

One of them probably uses classical.prop_decidable where the other uses @decidable_eq_of_decidable_le _ _ classical.prop_decidable

view this post on Zulip Reid Barton (Oct 08 2019 at 15:39):

decidable_linear_order.lift's definition of decidable_eq might also be implicated

view this post on Zulip Reid Barton (Oct 08 2019 at 15:40):

(why is there both classical.decidable_linear_order and classical.DLO?)

view this post on Zulip Floris van Doorn (Oct 08 2019 at 15:42):

Do you know what declaration caused classical.decidable_linear_order to appear in your goal? That is likely the declaration we want to change.

view this post on Zulip Reid Barton (Oct 08 2019 at 15:56):

I think in any case we should also fix decidable_linear_order.lift and this may or may not avoid your issue

view this post on Zulip Floris van Doorn (Oct 08 2019 at 15:58):

You want to fix it by using classical.prop_decidable? That doesn't seem objectively better...

view this post on Zulip Reid Barton (Oct 08 2019 at 16:00):

No by making decidable_eq like the other fields

view this post on Zulip Reid Barton (Oct 08 2019 at 16:00):

(sorry for being cryptic, on phone)

view this post on Zulip Floris van Doorn (Oct 08 2019 at 16:08):

I'm not sure if you can have much improvement: decidable_le and decidable_lt reduces definitionally to f x ? f y, but decidable_eq doesn't, and you have to use injectivity of f.

view this post on Zulip Reid Barton (Oct 08 2019 at 16:20):

Oh I didn't look at this closely enough

view this post on Zulip Reid Barton (Oct 08 2019 at 16:39):

Right, so I guess there is no way to make decidable_linear_order.lift of classical.decidable_linear_order (or anything similar defined using classical.prop_decidable) agree definitionally with using classical.decidable_linear_order directly.

view this post on Zulip Johan Commelin (Oct 08 2019 at 16:47):

The problematic code is here https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/valuation/perfection.lean#L96

view this post on Zulip Johan Commelin (Oct 08 2019 at 16:47):

I'm not very good at debugging this sort of thing.

view this post on Zulip Reid Barton (Oct 08 2019 at 16:48):

Well, probably it has to do with one of the several places where you have local attribute [instance, priority 0] classical.decidable_linear_order

view this post on Zulip Simon Hudon (Oct 08 2019 at 16:49):

@Floris van Doorn argues that priority 10 is better for inclusion in mathlib

view this post on Zulip Johan Commelin (Oct 08 2019 at 16:49):

Aha, we should fix our project

view this post on Zulip Reid Barton (Oct 08 2019 at 16:50):

Well I don't think the priority is the relevant bit

view this post on Zulip Reid Barton (Oct 08 2019 at 16:54):

Using classical.decidable_linear_order less might help, but I'm not sure you should really try very hard to avoid this situation

view this post on Zulip Reid Barton (Oct 08 2019 at 17:03):

what happens if you just delete all those local instances? Do you really use decidable_linear_order in a way other than to give you decidable (x < y), which follows from classical.prop_decidable anyways?

view this post on Zulip Johan Commelin (Oct 08 2019 at 17:11):

Probably not, we should just replace all of them with open_locale classical

view this post on Zulip Floris van Doorn (Oct 08 2019 at 18:33):

The fact that valuation/localization has local attribute [instance] classical.decidable_linear_order without a lower priority is likely the culprit: now the instance that nnreal is a DLO is synthesized using that.

view this post on Zulip Floris van Doorn (Oct 08 2019 at 18:38):

Oh wait, I don't think your file imports that. In that case I agree with Reid.

view this post on Zulip Johan Commelin (Oct 09 2019 at 11:14):

Hmm, even with open_locale classical in place, Lean still complains that it can find decidable_linear_order Γ₀.

view this post on Zulip Johan Commelin (Oct 09 2019 at 11:15):

That's a bit sad.

view this post on Zulip Chris Hughes (Oct 09 2019 at 11:15):

There's no instance for that. There is a def somewhere though.

view this post on Zulip Reid Barton (Oct 09 2019 at 13:23):

But that's precisely classical.decidable_linear_order right?


Last updated: May 13 2021 at 20:13 UTC