Zulip Chat Archive

Stream: general

Topic: missing instances?


view this post on Zulip Johan Commelin (Mar 07 2019 at 15:47):

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:)

view this post on Zulip Johan Commelin (Mar 07 2019 at 15:50):

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...

view this post on Zulip Mario Carneiro (Mar 07 2019 at 15:52):

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

view this post on Zulip Johan Commelin (Mar 07 2019 at 15:53):

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

view this post on Zulip Mario Carneiro (Mar 07 2019 at 15:53):

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

view this post on Zulip Mario Carneiro (Mar 07 2019 at 15:53):

which might explain why it isn't defined

view this post on Zulip Johan Commelin (Mar 07 2019 at 15:54):

Hmm.. I already had

local attribute [instance, priority 0] classical.prop_decidable

at the top of my file...

view this post on Zulip Mario Carneiro (Mar 07 2019 at 15:55):

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

view this post on Zulip Mario Carneiro (Mar 07 2019 at 15:55):

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

view this post on Zulip Johan Commelin (Mar 07 2019 at 15:56):

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

view this post on Zulip Johan Commelin (Mar 07 2019 at 15:57):

Or is it not even defined as a regular definition?

view this post on Zulip Mario Carneiro (Mar 07 2019 at 15:57):

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

view this post on Zulip Johan Commelin (Mar 08 2019 at 07:34):

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?

view this post on Zulip Johan Commelin (Mar 08 2019 at 07:35):

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

view this post on Zulip Johan Commelin (Mar 08 2019 at 07:35):

Does this mean that I should not be using finsets?

view this post on Zulip Mario Carneiro (Mar 08 2019 at 07:37):

there are some lemmas to prove about what these mean

view this post on Zulip Mario Carneiro (Mar 08 2019 at 07:37):

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

view this post on Zulip Johan Commelin (Mar 08 2019 at 07:38):

Ok, let me try that

view this post on Zulip Johan Commelin (Mar 08 2019 at 07:44):

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?

view this post on Zulip Johan Commelin (Mar 08 2019 at 07:46):

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

view this post on Zulip Mario Carneiro (Mar 08 2019 at 07:55):

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)

view this post on Zulip Johan Commelin (Mar 08 2019 at 07:56):

But prod is taking the product over the whole finset.

view this post on Zulip Johan Commelin (Mar 08 2019 at 07:57):

I guess I'll just stick with sets

view this post on Zulip Mario Carneiro (Mar 08 2019 at 08:00):

finset.prod is the cartesian product of two finsets

view this post on Zulip Mario Carneiro (Mar 08 2019 at 08:00):

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

view this post on Zulip Mario Carneiro (Mar 08 2019 at 08:01):

or is it finset.product?

view this post on Zulip Johan Commelin (Mar 08 2019 at 08:01):

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.

view this post on Zulip Kenny Lau (Mar 08 2019 at 09:34):

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

view this post on Zulip Johan Commelin (Mar 08 2019 at 09:35):

Thanks Kenny!


Last updated: May 08 2021 at 20:11 UTC