classical instance confusion

Stream: general

[Johan Commelin]

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

[Johan Commelin]

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

[Floris van Doorn]

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.

[Reid Barton]

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

[Johan Commelin]

I'd rather not have it in the first place

[Johan Commelin]

I can delta those instances, and then congr proves it

[Johan Commelin]

But that's just ugly

[Reid Barton]

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

[Reid Barton]

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

[Johan Commelin]

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.

[Johan Commelin]

It would be better if applying the lemma just worked.

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Floris van Doorn]

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

[Reid Barton]

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

[Floris van Doorn]

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

[Reid Barton]

No by making decidable_eq like the other fields

[Reid Barton]

(sorry for being cryptic, on phone)

[Floris van Doorn]

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.

[Reid Barton]

Oh I didn't look at this closely enough

[Reid Barton]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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

[Simon Hudon]

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

[Johan Commelin]

Aha, we should fix our project

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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?

[Johan Commelin]

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

[Floris van Doorn]

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.

[Floris van Doorn]

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

[Johan Commelin]

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

[Johan Commelin]

That's a bit sad.

[Chris Hughes]

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

[Reid Barton]

But that's precisely classical.decidable_linear_order right?