Multiset functor map with erase_dup

Stream: Is there code for X?

[Yaël Dillies]

This should be pretty obvious, but I can't do it. Any idea?

import data.finset.basic
import data.multiset.functor

universes u

open multiset

variables {α β : Type u} [decidable_eq α] [decidable_eq β] {F : Type u → Type u} [applicative F]
  [is_comm_applicative F]

lemma multiset.to_finset_fmap_traverse_erase_dup (f : α → F β) (m : multiset α) :
  to_finset <$> traverse f m.erase_dup = to_finset <$> traverse f m :=
sorry

[Yaël Dillies]

cc @Eric Wieser because that's for #10980

[Yakov Pechersky]

Do you have this for lists? You can just lift it across the quotient then.

[Yaël Dillies]

What for lists? We have docs#list.traversable if it's what you mean.

[Yakov Pechersky]

Can you prove

lemma list.to_finset_fmap_traverse_erase_dup (f : α → F β) (l : list α) :
  list.to_finset <$> traverse f l.erase_dup = list.to_finset <$> traverse f l :=

[Yaël Dillies]

I have no idea. This is out of my comfort zone.

[Reid Barton]

This looks false, the right hand side will have the effects of f on repeated elements of m multiple times, but the left hand side won't

[Yakov Pechersky]

Right, I think you need an "injectivity" of f assumption.

[Yakov Pechersky]

lemma list.to_finset_fmap_traverse_erase_dup (f : α → F β) (l : list α) :
  list.to_finset <$> traverse f l.erase_dup = list.to_finset <$> traverse f l :=
begin
  induction l with hd tl IH,
  { simp },
  { by_cases h : hd ∈ tl,
    { simp only [h, list.erase_dup_cons_of_mem, list.traverse_cons],
      -- list.to_finset <$> traverse f tl.erase_dup =
      --   list.to_finset <$> (list.cons <$> f hd <*> traverse f tl)
      sorry },
    { sorry } }
end

[Yakov Pechersky]

That shows the issue of trying to erase_dup over f hd.

[Yaël Dillies]

Arf. I was trying to get away without injectivity :sad:

[Reid Barton]

I don't understand what you mean by "injectivity". You need something like f x is idempotent for each x.

[Yaël Dillies]

My idea was that the to_finset would squish whatever effect we had duplicated.

[Reid Barton]

e.g. in pseudo-math/Lean/Haskell, if m = {x, x}, then the left hand side is
do { y <- f x; return (to_finset [y]) }
but the right hand side is
do { y <- f x; y' <- f x; return (to_finset [y, y']) }
and there's no reason that these should be the same even if you ignore the return value, because f ran twice on the right hand side but only once on the left

[Reid Barton]

For example, F could be a monad which is counting the number of executions of f

[Yaël Dillies]

Welp, I'm giving up. #10980 is now ready for review.

[Yakov Pechersky]

Reid, you're right, I hand-waved "injectivity" to mean what you said clearer as idempotency.