has_union problem

Stream: new members

[Tung Tran]

Hi everyone! I'm new to lean, and I was testing around when I had the following silly question:

import data.finset

section example_block

universes u_1
example : ∀ {α : Type u_1} [_inst_1 : decidable_eq α] (s₁ s₂ : finset α), s₁ ∪ s₂ = s₂ ∪ s₁ :=
begin
refl
end

end example_block

This code throws the following error:

test_2.lean:7:77
failed to synthesize type class instance for
α : Type u_1,
_inst_1 : decidable_eq α,
s₁ s₂ : finset α
⊢ has_union (finset α)

test_2.lean:7:87
failed to synthesize type class instance for
α : Type u_1,
_inst_1 : decidable_eq α,
s₁ s₂ : finset α
⊢ has_union (finset α)

I'm not sure where the problem is. I thought import finset is enough, but apparently not. Thank you in advance!

[Yaël Dillies]

That's because [_inst_1 : decidable_eq α] is right to the colon.

import data.finset

example {α : Type*} [_inst_1 : decidable_eq α] (s₁ s₂ : finset α) : s₁ ∪ s₂ = s₂ ∪ s₁ :=
begin
  refl
end

[Arthur Paulino]

I think this should work too:

import data.finset

example {α : Type*} [decidable_eq α] (s₁ s₂ : finset α) : s₁ ∪ s₂ = s₂ ∪ s₁ :=
begin
  refl
end

(untested)

[Kyle Miller]

@Yaël Dillies "column" -> "colon" probably?

@Tung Tran Lean doesn't add typeclasses in quantifiers to the cache by default. Typeclass arguments before the colon get added to the cache.

[Kyle Miller]

Just to show you how you can coax Lean into using the typeclass inside a quantifier:

import data.finset

section example_block

universes u_1
example : ∀ {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α), by exactI s₁ ∪ s₂ = s₂ ∪ s₁ :=
begin
  sorry
end

end example_block

[Tung Tran]

Thank you so much for all the help!
@Kyle Miller Also this is exactly what I need, thank you!

[Kevin Buzzard]

I was looking at this thread thinking "?? this is refl??" and it's only now I'm at a computer and I've checked, I find that you've all been winding me up.

[Kevin Buzzard]

import data.finset

example {α : Type*} [_inst_1 : decidable_eq α] (s₁ s₂ : finset α) : s₁ ∪ s₂ = s₂ ∪ s₁ :=
begin
  finish,
end