Union of finsets

Stream: new members

[Guilherme Espada]

How do I talk about the result of a union of finite sets? The expected, \union operator doesn't seem to work

def consts : term -> finset term
| t_true := singleton t_true
| t_false := singleton t_false
| (t_if t1 t2 t3) := (consts t1) ∪  (consts t2) ∪  (consts t3)

gives me the error:

failed to synthesize type class instance for
consts : term → finset term,
t1 t2 t3 : term
⊢ has_union (finset term)

[Johan Commelin]

@Guilherme Espada For various reasons, we don't use \union but \sup

[Johan Commelin]

So that gives you a square union symbol

[Guilherme Espada]

I did try sup too after scrolling a bit thru the source of finset, but I get a similar error:

Failed to synthesize type class instance for
consts : term → finset term,
t1 t2 t3 : term
⊢ has_sup (finset term)

[Ruben Van de Velde]

Do you need decidable equality?

[Ruben Van de Velde]

 def finset.has_union {α : Type u_1} [decidable_eq α] :
has_union (finset α)

[Yakov Pechersky]

Probably easiest to get by writing "@[derive decidable_eq]" wherever you define "term"

[Guilherme Espada]

This does work! it also allows me to use the set syntax which didn't work before. What exactly does this do? mark this type as something which can be "equaled"?

[Yakov Pechersky]

Exactly. You might want to say "@[derive [decidable_eq, fintype]]"

[Yakov Pechersky]

It marks that you can decidably check it two terms are equal or not equal. Examples of types where that isn't true for terms are the reals, or infinite streams, etc

[Kevin Buzzard]

finset keeps explicit track of the terms in the set, so it can offer a computable finset.card. This is problematic if you're dealing with sets like the real numbers, because $\{\pi^2/6,\sum_{n\geq1}n^{-2}\}$ is a set of size one but checking this needs as input a theorem of Euler. This is fixed in Lean by demanding that there's an algorithm which can tell whether two terms of your type are equal, because then you don't run into these problems when trying to compute the size of your set. Whether or not finset is the appropriate thing to use depends on your use case.

[Guilherme Espada]

Cool, thanks for the info. Where is the fintype deriveable located? I can't seem to import it

[Yakov Pechersky]

If you don't need it, then you don't need it. Otherwise, tactic.derive_fintype like Bryan said below

[Bryan Gin-ge Chen]

I think the derive handler is in tactic.derive_fintype.

[Bryan Gin-ge Chen]

This imports data.fintype.basic, so presumably you can't get it by importing data.fintype.basic.