missing instances?

Stream: general

[Johan Commelin]

Lean failed to find instances for functor finset and has_seq finset... But both shouldn't really be a problem right?
(I have no clue at all what has_seq is... so therefore I think finset ought to have such an instance :see_no_evil: :grinning: :upside_down:)

[Johan Commelin]

I want to take the pairwise product of all elements in two finsets. And a long time ago someone on Zulip suggested that ought to be written like this:

((*) <$> T₁ <*> T₂)

But that code doesn't typecheck for finsets...

[Mario Carneiro]

finset has a monad instance, but it requires decidable_eq of the base type

[Johan Commelin]

Aah, I see. That's not an issue.

[Mario Carneiro]

wait, actually as a monad it would need decidable_eq on all base types

[Mario Carneiro]

which might explain why it isn't defined

[Johan Commelin]

Hmm.. I already had

local attribute [instance, priority 0] classical.prop_decidable

at the top of my file...

[Mario Carneiro]

No, I mean the instance was probably not declared because it's classical

[Mario Carneiro]

monad doesn't let you define bind and return on only some types

[Johan Commelin]

I see... so I need to dig up the monad-def and locally make it an instance?

[Johan Commelin]

Or is it not even defined as a regular definition?

[Mario Carneiro]

you probably have to define it yourself, it's not hard - instance : monad finset := {pure := finset.singleton, bind := finset.bind}

[Johan Commelin]

Ok, so now I have the assumption ht : t ∈ has_mul.mul <$> T₁ <*> T₂. And T₁ and T₂ are two finsets. How do I turn ht into a t₁ ∈ T₁ and t₂ ∈ T₂ + hypotheses?

[Johan Commelin]

I tried rcases ht but rcases tactic failed: ht : quot.lift is not an inductive datatype.

[Johan Commelin]

Does this mean that I should not be using finsets?

[Mario Carneiro]

there are some lemmas to prove about what these mean

[Mario Carneiro]

it might be easier to just finset.image and finset.prod instead of this

[Johan Commelin]

Ok, let me try that

[Johan Commelin]

Hmmm, so what are the options I can use:

• T : finset A
• T : set A + [fintype T]
• T : set A + h : set.finite T
• [fintype T] + ι : T → A
• ...
  I guess it is not obvious which one should be chosen, right?

[Johan Commelin]

In the end I need to talk about { t₁ * t₂ | t₁ ∈ T₁, t₂ ∈ T₂ }. Which choice has the best API for that?

[Mario Carneiro]

I think finset.prod.image has the most lemmas, if you care about finiteness (you can also just use a set and forget about finite)

[Johan Commelin]

But prod is taking the product over the whole finset.

[Johan Commelin]

I guess I'll just stick with sets

[Mario Carneiro]

finset.prod is the cartesian product of two finsets

[Mario Carneiro]

if you map (*) over that with image you get your desired finset

[Mario Carneiro]

or is it finset.product?

[Johan Commelin]

finset.prod : Π {α : Type u} {β : Type v} [_inst_1 : comm_monoid β], finset α → (α → β) → β
prod s f is the product of f x as x ranges over the elements of the finite set s.

[Kenny Lau]

local attribute [instance, priority 0] classical.dec
noncomputable instance : monad finset :=
{pure := @finset.singleton, bind := λ _ _, finset.bind}

example {α : Type u} [has_mul α] (T₁ T₂ : finset α) (t : α) (ht : t ∈ (*) <$> T₁ <*> T₂) :
  ∃ t₁ ∈ T₁, ∃ t₂ ∈ T₂, t₁ * t₂ = t :=
let ⟨f, hf, hf2⟩ := finset.mem_bind.1 ht,
    ⟨t₁, h₁, hf⟩ := finset.mem_bind.1 hf,
    ⟨t₂, h₂, hf3⟩ := finset.mem_bind.1 hf2 in
⟨t₁, h₁, t₂, h₂, (finset.mem_singleton.1 hf3).symm ▸ (finset.mem_singleton.1 hf).symm ▸ rfl⟩

[Johan Commelin]

Thanks Kenny!