Zulip Chat Archive

Stream: general

Topic: decidable_eq diamond


Yaël Dillies (Sep 15 2021 at 18:17):

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 (Sep 15 2021 at 18:21):

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

Reid Barton (Sep 15 2021 at 18:30):

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

Reid Barton (Sep 15 2021 at 18:31):

By which I mean make it a non-instance

Yaël Dillies (Sep 15 2021 at 18:31):

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

Reid Barton (Sep 15 2021 at 18:32):

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

Eric Wieser (Sep 15 2021 at 18:38):

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 (Sep 15 2021 at 18:38):

Why is decidable_eq not a subsingleton, by the way?

Eric Wieser (Sep 15 2021 at 18:38):

It is

Eric Wieser (Sep 15 2021 at 18:38):

But that's not relevant to typeclass search

Yaël Dillies (Sep 15 2021 at 18:39):

Ah, so refl doesn't eliminate subsingletons?

Reid Barton (Sep 15 2021 at 18:40):

refl is about definitional equality.

Reid Barton (Sep 15 2021 at 18:40):

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

Yaël Dillies (Sep 15 2021 at 18:41):

I agree this is THE annoying thing about finset.

Yaël Dillies (Sep 15 2021 at 20:08):

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 (Sep 15 2021 at 20:09):

Can I make decidable_eq_of_decidable_le locally not an instance?

Johan Commelin (Sep 15 2021 at 20:18):

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

Yaël Dillies (Sep 15 2021 at 20:25):

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 (Sep 16 2021 at 06:52):

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

Yury G. Kudryashov (Sep 16 2021 at 22:02):

How do you get terms with decidable_*_of_decidable_le?

Yury G. Kudryashov (Sep 16 2021 at 22:02):

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

Yury G. Kudryashov (Sep 16 2021 at 22:03):

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 (Sep 17 2021 at 06:25):

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 (Sep 17 2021 at 10:55):

Can you provide an #mwe?

Yury G. Kudryashov (Sep 17 2021 at 10:56):

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

Yury G. Kudryashov (Sep 17 2021 at 10:57):

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

Yaël Dillies (Sep 17 2021 at 12:49):

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 (Sep 17 2021 at 12:50):

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

Yaël Dillies (Sep 17 2021 at 12:51):

and the corresponding PR is #7987

Yaël Dillies (Sep 17 2021 at 13:00):

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 (Sep 17 2021 at 13:25):

I'm going to fix this.

Yury G. Kudryashov (Sep 17 2021 at 13:26):

(refactoring order/locally_finite to deal with diamonds now)

Yaël Dillies (Sep 17 2021 at 13:31):

This is great! Thank you!

Yaël Dillies (Sep 17 2021 at 13:33):

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 (Sep 17 2021 at 14:13):

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 (Sep 17 2021 at 14:13):

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

Yury G. Kudryashov (Sep 17 2021 at 14:41):

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

Yury G. Kudryashov (Sep 17 2021 at 14:42):

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

Yury G. Kudryashov (Sep 17 2021 at 14:42):

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 (Sep 17 2021 at 15:17):

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 (Sep 17 2021 at 15:17):

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 (Sep 17 2021 at 15:23):

Thanks a lot again!


Last updated: Dec 20 2023 at 11:08 UTC