decidable_eq diamond

Stream: general

[Yaël Dillies]

I think I've just uncovered a diamond between nat.decidable_eq and decidable_eq_of_decidable_le.

import data.nat.basic

example :
  nat.decidable_eq = @decidable_eq_of_decidable_le ℕ (by apply_instance) (by apply_instance) :=
by refl --fails

[Johan Commelin]

oof, I can't imagine this has been around for years and nobody got bitten by this before.

[Reid Barton]

Is it ever really sensible to use decidable_eq_of_decidable_le? What would happen if we just deleted it?

[Reid Barton]

By which I mean make it a non-instance

[Yaël Dillies]

Well, I would need to give decidable_eq α in many lemmas, I assume.

[Reid Barton]

Right, I thought that was currently understood to be good practice anyways

[Eric Wieser]

I started writing a linter to require explicit decidable arguments everywhere, but it ran into lots of gray areas where it wasn't clear what the right thing to do was. There's a PR open somewhere.

[Yaël Dillies]

Why is decidable_eq not a subsingleton, by the way?

[Eric Wieser]

It is

[Eric Wieser]

But that's not relevant to typeclass search

[Yaël Dillies]

Ah, so refl doesn't eliminate subsingletons?

[Reid Barton]

refl is about definitional equality.

[Reid Barton]

This is why the information about how to compute a thing should not be contained in the definition of the thing.

[Yaël Dillies]

I agree this is THE annoying thing about finset.

[Yaël Dillies]

This diamond is actually pretty annoying for me... It prevents my lemmas newly generalized from ℕ to any locally finite order to apply.

[Yaël Dillies]

Can I make decidable_eq_of_decidable_le locally not an instance?

[Johan Commelin]

Yeah, I think you can local attribute [-instance] it

[Yaël Dillies]

I guess the motivation is that the decidable_eq instance should be able to match any decidable_eq instance typeclass inference comes up with?

[Yaël Dillies]

There's a similar diamond between decidable_lt_of_decidable_le and linear_order.decidable_lt. :fear:

[Yury G. Kudryashov]

How do you get terms with decidable_*_of_decidable_le?

[Yury G. Kudryashov]

Possibly you should reformulate some of the lemmas you add and/or use.

[Yury G. Kudryashov]

E.g., if you have if h : a = b then ... else ... in the statement of a lemma, then you should assume [decidable (a = b)], not [decidable (≤)].

[Yaël Dillies]

It happens because I need to assume [decidable_rel (≤)] to filter out the greatest/least element of Icc, like so (finset_Icc a b).filter (λ x, ¬b ≤ x).

[Yury G. Kudryashov]

Can you provide an #mwe?

[Yury G. Kudryashov]

For this filter I recommend to assume ∀ x, decidable (¬b ≤ x).

[Yury G. Kudryashov]

Or use filter (λ x, x < b) and assume [decidable_rel (<)].

[Yaël Dillies]

Actually, everything works fine now that I've done local attribute [-instance] decidable_eq_of_decidable_le decidable_lt_of_decidable_le

[Yaël Dillies]

If you want to have a look, this is in data.finset.intervals on the branch#localfinorder

[Yaël Dillies]

and the corresponding PR is #7987

[Yaël Dillies]

I assume one thing that could bite us is that it will have derived ∀ a b, decidable (¬a ≤ b) from decidable_rel (≤) and this will be repercuted in the kind of decidable instance you can plug in the lemmas.

[Yury G. Kudryashov]

I'm going to fix this.

[Yury G. Kudryashov]

(refactoring order/locally_finite to deal with diamonds now)

[Yaël Dillies]

This is great! Thank you!

[Yaël Dillies]

If you have time, branch#antitone is to my eyes even more useful to fix because the PR is ready apart from that.

[Yury G. Kudryashov]

I suggest that we drop all default/tactic-default stuff from locally_finite_order, and add a custom constructor of_finset_Icc instead. If someone wants to override only some finset_Ixx's, they can use { finset_Ioc := _, mem_finset_Ioc := _, .. of_finset_Icc}.

[Yury G. Kudryashov]

This will simplify the design a lot. And we mention the of_finset_Icc constructor in the class docstring.

[Yury G. Kudryashov]

Done. I fixed locally_finite_order, but you may get new failures later.

[Yury G. Kudryashov]

And now you don't need to assume any decidability to speak about locally_finite_orders.

[Yury G. Kudryashov]

BTW, have a look at docs#set.ord_connected You can assume it as a typeclass instead of a custom hp at the end of locally_finite_order.lean.

[Yaël Dillies]

Yury G. Kudryashov said:

I suggest that we drop all default/tactic-default stuff from locally_finite_order, and add a custom constructor of_finset_Icc instead. If someone wants to override only some finset_Ixx's, they can use { finset_Ioc := _, mem_finset_Ioc := _, .. of_finset_Icc}.

I quite liked my fancy default constructors :cry: but I guess you're right as no decidability is needed anymore.

[Yaël Dillies]

Yury G. Kudryashov said:

BTW, have a look at docs#set.ord_connected You can assume it as a typeclass instead of a custom hp at the end of locally_finite_order.lean.

Oh yes I know about that but it's still deeprooted in my brain that set.ord_connected = predicate.

[Yaël Dillies]

Thanks a lot again!