multiset question

Stream: new members

[Amelia Livingston]

Hi! I got stuck doing this; can anyone help? Thanks!

import data.finset

variables (α : Type*) [decidable_eq α]

example (m : multiset α) : m.to_finset = ∅ → m = 0 := sorry

[Kevin Buzzard]

I have so far failed twice :-)

[Amelia Livingston]

Ah, this works, but it's kind of long

example (β: Type u) [decidable_eq β] (m : multiset β) : m.to_finset = ∅ → m = 0 :=
begin
  rw [multiset.to_finset, ←finset.val_inj],
  intro H,
  change erase_dup m = ∅ at H,
  apply eq_zero_of_forall_not_mem,
  intro x,
  assume H',
  rw [←mem_erase_dup, H] at H',
  exact absurd H' (not_mem_empty x),
end

[Kevin Buzzard]

Looking at it now I'm wondering if it should be in the library

[Kevin Buzzard]

import data.finset

variables (α : Type*) [decidable_eq α]

example (m : multiset α) (h : m.to_finset = ∅) : m = 0 :=
begin
  apply multiset.eq_zero_of_forall_not_mem,
  rw finset.eq_empty_iff_forall_not_mem at h,
  intros x hx,
  rw ←multiset.mem_to_finset at hx,
  exact h x hx,
end

Maybe this is a bit better

[Kenny Lau]

import data.finset

variables (α : Type*) [decidable_eq α]

example (m : multiset α) : m.to_finset = ∅ → m = 0 :=
multiset.induction_on m (λ _, rfl) (λ _ _ _ H, absurd H $ by simp)

[Amelia Livingston]

thank you :D

[Mario Carneiro]

Ah, yes there is a missing library function

namespace multiset
theorem erase_dup_eq_zero {s : multiset α} : erase_dup s = 0 ↔ s = 0 :=
⟨λ h, eq_zero_of_subset_zero $ h ▸ subset_erase_dup _,
 λ h, h.symm ▸ erase_dup_zero⟩
end multiset

example (m : multiset α) (h : m.to_finset = ∅) : m = 0 :=
multiset.erase_dup_eq_zero.1 (finset.val_inj.2 h)

[Mario Carneiro]

well, this theorem itself is also a missing library function

theorem to_finset_eq_empty {m : multiset α} : m.to_finset = ∅ ↔ m = 0 :=
finset.val_inj.symm.trans multiset.erase_dup_eq_zero