## Stream: general

### Topic: classical instance confusion

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

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

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

#### 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?

#### Johan Commelin (Oct 08 2019 at 15:15):

I'd rather not have it in the first place

#### Johan Commelin (Oct 08 2019 at 15:15):

I can delta those instances, and then congr proves it

#### Johan Commelin (Oct 08 2019 at 15:15):

But that's just ugly

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

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

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

#### Johan Commelin (Oct 08 2019 at 15:22):

It would be better if applying the lemma just worked.

#### Johan Commelin (Oct 08 2019 at 15:22):

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

#### Johan Commelin (Oct 08 2019 at 15:23):

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

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

#### Reid Barton (Oct 08 2019 at 15:39):

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

#### Reid Barton (Oct 08 2019 at 15:40):

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

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

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

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

#### Reid Barton (Oct 08 2019 at 16:00):

No by making decidable_eq like the other fields

#### Reid Barton (Oct 08 2019 at 16:00):

(sorry for being cryptic, on phone)

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

#### Reid Barton (Oct 08 2019 at 16:20):

Oh I didn't look at this closely enough

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

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

#### Johan Commelin (Oct 08 2019 at 16:47):

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

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

#### Simon Hudon (Oct 08 2019 at 16:49):

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

#### Johan Commelin (Oct 08 2019 at 16:49):

Aha, we should fix our project

#### Reid Barton (Oct 08 2019 at 16:50):

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

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

#### 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?

#### Johan Commelin (Oct 08 2019 at 17:11):

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

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

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

#### 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 Γ₀.

#### Johan Commelin (Oct 09 2019 at 11:15):

But that's precisely classical.decidable_linear_order right?