DecidableLE for Finset

Stream: mathlib4

[Lukas Miaskiwskyi]

This is related to PR mathlib4#1600. In mathlib3, the theorem uv.card_compress is able to infer that finset has a [decidable_rel has_le.le] (this is needed for uv.compress). However, nowhere in mathlib3 is an instance decidable_le for finsets explicitly declared, as far as I can tell. There is one for multisets, which I'm guessing this infers, since finsets essentially are multisets. Is that correct?

Anyway, in mathlib4, this does not work anymore, and when porting uv.card_compress, lean bemoans the lack of a DecidableRel fun x x_1 => x ≤ x_1 instance for the Finset.Le, as seen in the above PR. Should we add such an instance to Data.Finset.Basic, or how can we make lean infer it better?

[Yaël Dillies]

It definitely is not using the one from multiset. Try looking at the corresponding statements in mathlib and inspect them with the infoview to see what instance is inferred.

[Eric Wieser]

I would guess it finds the instance for subset

[Lukas Miaskiwskyi]

@Yaël Dillies Thanks, I spent so much time in lean 4 that I forgot that the lean 3 infoview is actually powerful enough to tell me that very easily. docs#finset.decidable_dforall_finset is what it finds, which is also ported, so I still don't quite get the problem, but that brings me closer to understanding it (tomorrow after some sleep)

[Yaël Dillies]

Hmm, did the definition of subset change?

[Yaël Dillies]

There was a similar change with the definition on set

[Eric Wieser]

I would guess that Lean3 just unfolded in places where Lean4 doesn't

[Xavier Roblot]

I found a similar problem in !4#4762 were the following is failing

instance : DecidableRel fun x y : ℕ × ℕ  ↦ x ≤ y := by infer_instance -- fails

It was synthesizedautomatically in Lean 3.
It is of course straightforward to prove but it is strange that Lean 4 cannot do it by itself

instance : DecidableRel fun x y : ℕ × ℕ  ↦ x ≤ y := fun _ _ => And.decidable

[Eric Wieser]

I don't think this is that strange; typeclass search isn't allowed to unfold definitions

[Xavier Roblot]

So why did it work in Lean3?

[Eric Wieser]

Because in Lean 3 random things did random amounts of unfolding

[Xavier Roblot]

So I should just add the instance where it is needed? Or somewhere globally?

[Eric Wieser]

There should be a global instance as close to where prod.has_le is defined as possible

[Eric Wieser]

The instance should assume Decidable (the implementation of le) and produce Decidable (x ≤ y)

[Xavier Roblot]

!4#5083