/-

Copyright (c) 2015 Microsoft Corporation. All rights reserved.

Released under Apache 2.0 license as described in the file LICENSE.

Authors: Mario Carneiro

-/

import data.set.list

import data.list.perm

/-!

# Multisets

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.

> Any changes to this file require a corresponding PR to mathlib4.

These are implemented as the quotient of a list by permutations.

## Notation

We define the global infix notation `::ₘ` for `multiset.cons`.

-/

open function list nat subtype

variables {α : Type*} {β : Type*} {γ : Type*}

/-- `multiset α` is the quotient of `list α` by list permutation. The result

is a type of finite sets with duplicates allowed. -/

def {u} multiset (α : Type u) : Type u :=

quotient (list.is_setoid α)

namespace multiset

instance : has_coe (list α) (multiset α) := ⟨quot.mk _⟩

@[simp] theorem quot_mk_to_coe (l : list α) : @eq (multiset α) ⟦l⟧ l := rfl

@[simp] theorem quot_mk_to_coe' (l : list α) : @eq (multiset α) (quot.mk (≈) l) l := rfl

@[simp] theorem quot_mk_to_coe'' (l : list α) : @eq (multiset α) (quot.mk setoid.r l) l := rfl

@[simp] theorem coe_eq_coe {l₁ l₂ : list α} : (l₁ : multiset α) = l₂ ↔ l₁ ~ l₂ := quotient.eq

instance has_decidable_eq [decidable_eq α] : decidable_eq (multiset α)

| s₁ s₂ := quotient.rec_on_subsingleton₂ s₁ s₂ $ λ l₁ l₂,

decidable_of_iff' _ quotient.eq

/-- defines a size for a multiset by referring to the size of the underlying list -/

protected def sizeof [has_sizeof α] (s : multiset α) : ℕ :=

quot.lift_on s sizeof $ λ l₁ l₂, perm.sizeof_eq_sizeof

instance has_sizeof [has_sizeof α] : has_sizeof (multiset α) := ⟨multiset.sizeof⟩

/-! ### Empty multiset -/

/-- `0 : multiset α` is the empty set -/

protected def zero : multiset α := @nil α

instance : has_zero (multiset α) := ⟨multiset.zero⟩

instance : has_emptyc (multiset α) := ⟨0⟩

instance inhabited_multiset : inhabited (multiset α) := ⟨0⟩

@[simp] theorem coe_nil : (@nil α : multiset α) = 0 := rfl

@[simp] theorem empty_eq_zero : (∅ : multiset α) = 0 := rfl

@[simp] theorem coe_eq_zero (l : list α) : (l : multiset α) = 0 ↔ l = [] :=

iff.trans coe_eq_coe perm_nil

lemma coe_eq_zero_iff_empty (l : list α) : (l : multiset α) = 0 ↔ l.empty :=

iff.trans (coe_eq_zero l) (empty_iff_eq_nil).symm

/-! ### `multiset.cons` -/

/-- `cons a s` is the multiset which contains `s` plus one more

instance of `a`. -/

def cons (a : α) (s : multiset α) : multiset α :=

quot.lift_on s (λ l, (a :: l : multiset α))

(λ l₁ l₂ p, quot.sound (p.cons a))

infixr ` ::ₘ `:67 := multiset.cons

instance : has_insert α (multiset α) := ⟨cons⟩

@[simp] theorem insert_eq_cons (a : α) (s : multiset α) :

insert a s = a ::ₘ s := rfl

@[simp] theorem cons_coe (a : α) (l : list α) :

(a ::ₘ l : multiset α) = (a::l : list α) := rfl

@[simp] theorem cons_inj_left {a b : α} (s : multiset α) :

a ::ₘ s = b ::ₘ s ↔ a = b :=

⟨quot.induction_on s $ λ l e,

have [a] ++ l ~ [b] ++ l, from quotient.exact e,

singleton_perm_singleton.1 $ (perm_append_right_iff _).1 this, congr_arg _⟩

@[simp] theorem cons_inj_right (a : α) : ∀{s t : multiset α}, a ::ₘ s = a ::ₘ t ↔ s = t :=

by rintros ⟨l₁⟩ ⟨l₂⟩; simp

@[recursor 5] protected theorem induction {p : multiset α → Prop}

(h₁ : p 0) (h₂ : ∀ ⦃a : α⦄ {s : multiset α}, p s → p (a ::ₘ s)) : ∀s, p s :=

by rintros ⟨l⟩; induction l with _ _ ih; [exact h₁, exact h₂ ih]

@[elab_as_eliminator] protected theorem induction_on {p : multiset α → Prop}

(s : multiset α) (h₁ : p 0) (h₂ : ∀ ⦃a : α⦄ {s : multiset α}, p s → p (a ::ₘ s)) : p s :=

multiset.induction h₁ h₂ s

theorem cons_swap (a b : α) (s : multiset α) : a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s :=

quot.induction_on s $ λ l, quotient.sound $ perm.swap _ _ _

section rec

variables {C : multiset α → Sort*}

/-- Dependent recursor on multisets.

TODO: should be @[recursor 6], but then the definition of `multiset.pi` fails with a stack

overflow in `whnf`.

-/

protected def rec

(C_0 : C 0)

(C_cons : Πa m, C m → C (a ::ₘ m))

(C_cons_heq : ∀ a a' m b, C_cons a (a' ::ₘ m) (C_cons a' m b) ==

C_cons a' (a ::ₘ m) (C_cons a m b))

(m : multiset α) : C m :=

quotient.hrec_on m (@list.rec α (λl, C ⟦l⟧) C_0 (λa l b, C_cons a ⟦l⟧ b)) $

assume l l' h,

h.rec_heq

(assume a l l' b b' hl, have ⟦l⟧ = ⟦l'⟧, from quot.sound hl, by cc)

(assume a a' l, C_cons_heq a a' ⟦l⟧)

/-- Companion to `multiset.rec` with more convenient argument order. -/

@[elab_as_eliminator]

protected def rec_on (m : multiset α)

(C_0 : C 0)

(C_cons : Πa m, C m → C (a ::ₘ m))

(C_cons_heq : ∀a a' m b, C_cons a (a' ::ₘ m) (C_cons a' m b) ==

C_cons a' (a ::ₘ m) (C_cons a m b)) :

C m :=

multiset.rec C_0 C_cons C_cons_heq m

variables {C_0 : C 0} {C_cons : Πa m, C m → C (a ::ₘ m)}

{C_cons_heq : ∀a a' m b, C_cons a (a' ::ₘ m) (C_cons a' m b) ==

C_cons a' (a ::ₘ m) (C_cons a m b)}

@[simp] lemma rec_on_0 : @multiset.rec_on α C (0:multiset α) C_0 C_cons C_cons_heq = C_0 :=

rfl

@[simp] lemma rec_on_cons (a : α) (m : multiset α) :

(a ::ₘ m).rec_on C_0 C_cons C_cons_heq = C_cons a m (m.rec_on C_0 C_cons C_cons_heq) :=

quotient.induction_on m $ assume l, rfl

end rec

section mem

/-- `a ∈ s` means that `a` has nonzero multiplicity in `s`. -/

def mem (a : α) (s : multiset α) : Prop :=

quot.lift_on s (λ l, a ∈ l) (λ l₁ l₂ (e : l₁ ~ l₂), propext $ e.mem_iff)

instance : has_mem α (multiset α) := ⟨mem⟩

@[simp] lemma mem_coe {a : α} {l : list α} : a ∈ (l : multiset α) ↔ a ∈ l := iff.rfl

instance decidable_mem [decidable_eq α] (a : α) (s : multiset α) : decidable (a ∈ s) :=

quot.rec_on_subsingleton s $ list.decidable_mem a

@[simp] theorem mem_cons {a b : α} {s : multiset α} : a ∈ b ::ₘ s ↔ a = b ∨ a ∈ s :=

quot.induction_on s $ λ l, iff.rfl

lemma mem_cons_of_mem {a b : α} {s : multiset α} (h : a ∈ s) : a ∈ b ::ₘ s :=

mem_cons.2 $ or.inr h

@[simp] theorem mem_cons_self (a : α) (s : multiset α) : a ∈ a ::ₘ s :=

mem_cons.2 (or.inl rfl)

theorem forall_mem_cons {p : α → Prop} {a : α} {s : multiset α} :

(∀ x ∈ (a ::ₘ s), p x) ↔ p a ∧ ∀ x ∈ s, p x :=

quotient.induction_on' s $ λ L, list.forall_mem_cons

theorem exists_cons_of_mem {s : multiset α} {a : α} : a ∈ s → ∃ t, s = a ::ₘ t :=

quot.induction_on s $ λ l (h : a ∈ l),

let ⟨l₁, l₂, e⟩ := mem_split h in

e.symm ▸ ⟨(l₁++l₂ : list α), quot.sound perm_middle⟩

@[simp] theorem not_mem_zero (a : α) : a ∉ (0 : multiset α) := id

theorem eq_zero_of_forall_not_mem {s : multiset α} : (∀x, x ∉ s) → s = 0 :=

quot.induction_on s $ λ l H, by rw eq_nil_iff_forall_not_mem.mpr H; refl

theorem eq_zero_iff_forall_not_mem {s : multiset α} : s = 0 ↔ ∀ a, a ∉ s :=

⟨λ h, h.symm ▸ λ _, not_false, eq_zero_of_forall_not_mem⟩

theorem exists_mem_of_ne_zero {s : multiset α} : s ≠ 0 → ∃ a : α, a ∈ s :=

quot.induction_on s $ assume l hl,

match l, hl with

| [] := assume h, false.elim $ h rfl

| (a :: l) := assume _, ⟨a, by simp⟩

end

lemma empty_or_exists_mem (s : multiset α) : s = 0 ∨ ∃ a, a ∈ s :=

or_iff_not_imp_left.mpr multiset.exists_mem_of_ne_zero

@[simp] lemma zero_ne_cons {a : α} {m : multiset α} : 0 ≠ a ::ₘ m :=

assume h, have a ∈ (0:multiset α), from h.symm ▸ mem_cons_self _ _, not_mem_zero _ this

@[simp] lemma cons_ne_zero {a : α} {m : multiset α} : a ::ₘ m ≠ 0 := zero_ne_cons.symm

lemma cons_eq_cons {a b : α} {as bs : multiset α} :

a ::ₘ as = b ::ₘ bs ↔ ((a = b ∧ as = bs) ∨ (a ≠ b ∧ ∃cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs)) :=

begin

haveI : decidable_eq α := classical.dec_eq α,

split,

{ assume eq,

by_cases a = b,

{ subst h, simp * at * },

{ have : a ∈ b ::ₘ bs, from eq ▸ mem_cons_self _ _,

have : a ∈ bs, by simpa [h],

rcases exists_cons_of_mem this with ⟨cs, hcs⟩,

simp [h, hcs],

have : a ::ₘ as = b ::ₘ a ::ₘ cs, by simp [eq, hcs],

have : a ::ₘ as = a ::ₘ b ::ₘ cs, by rwa [cons_swap],

simpa using this } },

{ assume h,

rcases h with ⟨eq₁, eq₂⟩ | ⟨h, cs, eq₁, eq₂⟩,

{ simp * },

{ simp [*, cons_swap a b] } }

end

end mem

/-! ### Singleton -/

instance : has_singleton α (multiset α) := ⟨λ a, a ::ₘ 0⟩

instance : is_lawful_singleton α (multiset α) := ⟨λ a, rfl⟩

@[simp] theorem cons_zero (a : α) : a ::ₘ 0 = {a} := rfl

@[simp, norm_cast] theorem coe_singleton (a : α) : ([a] : multiset α) = {a} := rfl

@[simp] theorem mem_singleton {a b : α} : b ∈ ({a} : multiset α) ↔ b = a :=

by simp only [←cons_zero, mem_cons, iff_self, or_false, not_mem_zero]

theorem mem_singleton_self (a : α) : a ∈ ({a} : multiset α) :=

by { rw ←cons_zero, exact mem_cons_self _ _ }

@[simp] theorem singleton_inj {a b : α} : ({a} : multiset α) = {b} ↔ a = b :=

by { simp_rw [←cons_zero], exact cons_inj_left _ }

@[simp, norm_cast] lemma coe_eq_singleton {l : list α} {a : α} : (l : multiset α) = {a} ↔ l = [a] :=

by rw [←coe_singleton, coe_eq_coe, list.perm_singleton]

@[simp] lemma singleton_eq_cons_iff {a b : α} (m : multiset α) : {a} = b ::ₘ m ↔ a = b ∧ m = 0 :=

by { rw [←cons_zero, cons_eq_cons], simp [eq_comm] }

theorem pair_comm (x y : α) : ({x, y} : multiset α) = {y, x} := cons_swap x y 0

/-! ### `multiset.subset` -/

section subset

/-- `s ⊆ t` is the lift of the list subset relation. It means that any

element with nonzero multiplicity in `s` has nonzero multiplicity in `t`,

but it does not imply that the multiplicity of `a` in `s` is less or equal than in `t`;

see `s ≤ t` for this relation. -/

protected def subset (s t : multiset α) : Prop := ∀ ⦃a : α⦄, a ∈ s → a ∈ t

instance : has_subset (multiset α) := ⟨multiset.subset⟩

instance : has_ssubset (multiset α) := ⟨λ s t, s ⊆ t ∧ ¬ t ⊆ s⟩

@[simp] theorem coe_subset {l₁ l₂ : list α} : (l₁ : multiset α) ⊆ l₂ ↔ l₁ ⊆ l₂ := iff.rfl

@[simp] theorem subset.refl (s : multiset α) : s ⊆ s := λ a h, h

theorem subset.trans {s t u : multiset α} : s ⊆ t → t ⊆ u → s ⊆ u :=

λ h₁ h₂ a m, h₂ (h₁ m)

theorem subset_iff {s t : multiset α} : s ⊆ t ↔ (∀⦃x⦄, x ∈ s → x ∈ t) := iff.rfl

theorem mem_of_subset {s t : multiset α} {a : α} (h : s ⊆ t) : a ∈ s → a ∈ t := @h _

@[simp] theorem zero_subset (s : multiset α) : 0 ⊆ s :=

λ a, (not_mem_nil a).elim

lemma subset_cons (s : multiset α) (a : α) : s ⊆ a ::ₘ s := λ _, mem_cons_of_mem

lemma ssubset_cons {s : multiset α} {a : α} (ha : a ∉ s) : s ⊂ a ::ₘ s :=

⟨subset_cons _ _, λ h, ha $ h $ mem_cons_self _ _⟩

@[simp] theorem cons_subset {a : α} {s t : multiset α} : (a ::ₘ s) ⊆ t ↔ a ∈ t ∧ s ⊆ t :=

by simp [subset_iff, or_imp_distrib, forall_and_distrib]

lemma cons_subset_cons {a : α} {s t : multiset α} : s ⊆ t → a ::ₘ s ⊆ a ::ₘ t :=

quotient.induction_on₂ s t $ λ _ _, cons_subset_cons _

theorem eq_zero_of_subset_zero {s : multiset α} (h : s ⊆ 0) : s = 0 :=

eq_zero_of_forall_not_mem h

theorem subset_zero {s : multiset α} : s ⊆ 0 ↔ s = 0 :=

⟨eq_zero_of_subset_zero, λ xeq, xeq.symm ▸ subset.refl 0⟩

lemma induction_on' {p : multiset α → Prop} (S : multiset α)

(h₁ : p 0) (h₂ : ∀ {a s}, a ∈ S → s ⊆ S → p s → p (insert a s)) : p S :=

@multiset.induction_on α (λ T, T ⊆ S → p T) S (λ _, h₁) (λ a s hps hs,

let ⟨hS, sS⟩ := cons_subset.1 hs in h₂ hS sS (hps sS)) (subset.refl S)

end subset

/-! ### `multiset.to_list` -/

section to_list

/-- Produces a list of the elements in the multiset using choice. -/

noncomputable def to_list (s : multiset α) := s.out'

@[simp, norm_cast]

lemma coe_to_list (s : multiset α) : (s.to_list : multiset α) = s := s.out_eq'

@[simp] lemma to_list_eq_nil {s : multiset α} : s.to_list = [] ↔ s = 0 :=

by rw [← coe_eq_zero, coe_to_list]

@[simp] lemma empty_to_list {s : multiset α} : s.to_list.empty ↔ s = 0 :=

empty_iff_eq_nil.trans to_list_eq_nil

@[simp] lemma to_list_zero : (multiset.to_list 0 : list α) = [] := to_list_eq_nil.mpr rfl

@[simp] lemma mem_to_list {a : α} {s : multiset α} : a ∈ s.to_list ↔ a ∈ s :=

by rw [← mem_coe, coe_to_list]

@[simp] lemma to_list_eq_singleton_iff {a : α} {m : multiset α} : m.to_list = [a] ↔ m = {a} :=

by rw [←perm_singleton, ←coe_eq_coe, coe_to_list, coe_singleton]

@[simp] lemma to_list_singleton (a : α) : ({a} : multiset α).to_list = [a] :=

multiset.to_list_eq_singleton_iff.2 rfl

end to_list

/-! ### Partial order on `multiset`s -/

/-- `s ≤ t` means that `s` is a sublist of `t` (up to permutation).

Equivalently, `s ≤ t` means that `count a s ≤ count a t` for all `a`. -/

protected def le (s t : multiset α) : Prop :=

quotient.lift_on₂ s t (<+~) $ λ v₁ v₂ w₁ w₂ p₁ p₂,

propext (p₂.subperm_left.trans p₁.subperm_right)

instance : partial_order (multiset α) :=

{ le := multiset.le,

le_refl := by rintros ⟨l⟩; exact subperm.refl _,

le_trans := by rintros ⟨l₁⟩ ⟨l₂⟩ ⟨l₃⟩; exact @subperm.trans _ _ _ _,

le_antisymm := by rintros ⟨l₁⟩ ⟨l₂⟩ h₁ h₂; exact quot.sound (subperm.antisymm h₁ h₂) }

instance decidable_le [decidable_eq α] : decidable_rel ((≤) : multiset α → multiset α → Prop) :=

λ s t, quotient.rec_on_subsingleton₂ s t list.decidable_subperm

section

variables {s t : multiset α} {a : α}

lemma subset_of_le : s ≤ t → s ⊆ t := quotient.induction_on₂ s t $ λ l₁ l₂, subperm.subset

alias subset_of_le ← le.subset

lemma mem_of_le (h : s ≤ t) : a ∈ s → a ∈ t := mem_of_subset (subset_of_le h)

lemma not_mem_mono (h : s ⊆ t) : a ∉ t → a ∉ s := mt $ @h _

@[simp] theorem coe_le {l₁ l₂ : list α} : (l₁ : multiset α) ≤ l₂ ↔ l₁ <+~ l₂ := iff.rfl

@[elab_as_eliminator] theorem le_induction_on {C : multiset α → multiset α → Prop}

{s t : multiset α} (h : s ≤ t)

(H : ∀ {l₁ l₂ : list α}, l₁ <+ l₂ → C l₁ l₂) : C s t :=

quotient.induction_on₂ s t (λ l₁ l₂ ⟨l, p, s⟩,

(show ⟦l⟧ = ⟦l₁⟧, from quot.sound p) ▸ H s) h

theorem zero_le (s : multiset α) : 0 ≤ s :=

quot.induction_on s $ λ l, (nil_sublist l).subperm

instance : order_bot (multiset α) := ⟨0, zero_le⟩

/-- This is a `rfl` and `simp` version of `bot_eq_zero`. -/

@[simp] theorem bot_eq_zero : (⊥ : multiset α) = 0 := rfl

lemma le_zero : s ≤ 0 ↔ s = 0 := le_bot_iff

theorem lt_cons_self (s : multiset α) (a : α) : s < a ::ₘ s :=

quot.induction_on s $ λ l,

suffices l <+~ a :: l ∧ (¬l ~ a :: l),

by simpa [lt_iff_le_and_ne],

⟨(sublist_cons _ _).subperm,

λ p, ne_of_lt (lt_succ_self (length l)) p.length_eq⟩

theorem le_cons_self (s : multiset α) (a : α) : s ≤ a ::ₘ s :=

le_of_lt $ lt_cons_self _ _

lemma cons_le_cons_iff (a : α) : a ::ₘ s ≤ a ::ₘ t ↔ s ≤ t :=

quotient.induction_on₂ s t $ λ l₁ l₂, subperm_cons a

lemma cons_le_cons (a : α) : s ≤ t → a ::ₘ s ≤ a ::ₘ t := (cons_le_cons_iff a).2

lemma le_cons_of_not_mem (m : a ∉ s) : s ≤ a ::ₘ t ↔ s ≤ t :=

begin

refine ⟨_, λ h, le_trans h $ le_cons_self _ _⟩,

suffices : ∀ {t'} (_ : s ≤ t') (_ : a ∈ t'), a ::ₘ s ≤ t',

{ exact λ h, (cons_le_cons_iff a).1 (this h (mem_cons_self _ _)) },

introv h, revert m, refine le_induction_on h _,

introv s m₁ m₂,

rcases mem_split m₂ with ⟨r₁, r₂, rfl⟩,

exact perm_middle.subperm_left.2 ((subperm_cons _).2 $

((sublist_or_mem_of_sublist s).resolve_right m₁).subperm)

end

@[simp] theorem singleton_ne_zero (a : α) : ({a} : multiset α) ≠ 0 :=

ne_of_gt (lt_cons_self _ _)

@[simp] theorem singleton_le {a : α} {s : multiset α} : {a} ≤ s ↔ a ∈ s :=

⟨λ h, mem_of_le h (mem_singleton_self _),

λ h, let ⟨t, e⟩ := exists_cons_of_mem h in e.symm ▸ cons_le_cons _ (zero_le _)⟩

end

/-! ### Additive monoid -/

/-- The sum of two multisets is the lift of the list append operation.

This adds the multiplicities of each element,

i.e. `count a (s + t) = count a s + count a t`. -/

protected def add (s₁ s₂ : multiset α) : multiset α :=

quotient.lift_on₂ s₁ s₂ (λ l₁ l₂, ((l₁ ++ l₂ : list α) : multiset α)) $

λ v₁ v₂ w₁ w₂ p₁ p₂, quot.sound $ p₁.append p₂

instance : has_add (multiset α) := ⟨multiset.add⟩

@[simp] theorem coe_add (s t : list α) : (s + t : multiset α) = (s ++ t : list α) := rfl

@[simp] theorem singleton_add (a : α) (s : multiset α) : {a} + s = a ::ₘ s := rfl

private theorem add_le_add_iff_left' {s t u : multiset α} : s + t ≤ s + u ↔ t ≤ u :=

quotient.induction_on₃ s t u $ λ l₁ l₂ l₃, subperm_append_left _

instance : covariant_class (multiset α) (multiset α) (+) (≤) :=

⟨λ s t u, add_le_add_iff_left'.2⟩

instance : contravariant_class (multiset α) (multiset α) (+) (≤) :=

⟨λ s t u, add_le_add_iff_left'.1⟩

instance : ordered_cancel_add_comm_monoid (multiset α) :=

{ zero := 0,

add := (+),

add_comm := λ s t, quotient.induction_on₂ s t $ λ l₁ l₂, quot.sound perm_append_comm,

add_assoc := λ s₁ s₂ s₃, quotient.induction_on₃ s₁ s₂ s₃ $ λ l₁ l₂ l₃,

congr_arg coe $ append_assoc l₁ l₂ l₃,

zero_add := λ s, quot.induction_on s $ λ l, rfl,

add_zero := λ s, quotient.induction_on s $ λ l, congr_arg coe $ append_nil l,

add_le_add_left := λ s₁ s₂, add_le_add_left,

le_of_add_le_add_left := λ s₁ s₂ s₃, le_of_add_le_add_left,

..@multiset.partial_order α }

theorem le_add_right (s t : multiset α) : s ≤ s + t :=

by simpa using add_le_add_left (zero_le t) s

theorem le_add_left (s t : multiset α) : s ≤ t + s :=

by simpa using add_le_add_right (zero_le t) s

theorem le_iff_exists_add {s t : multiset α} : s ≤ t ↔ ∃ u, t = s + u :=

⟨λ h, le_induction_on h $ λ l₁ l₂ s,

let ⟨l, p⟩ := s.exists_perm_append in ⟨l, quot.sound p⟩,

λ ⟨u, e⟩, e.symm ▸ le_add_right _ _⟩

instance : canonically_ordered_add_monoid (multiset α) :=

{ le_self_add := le_add_right,

exists_add_of_le := λ a b h, le_induction_on h $ λ l₁ l₂ s,

let ⟨l, p⟩ := s.exists_perm_append in ⟨l, quot.sound p⟩,

..multiset.order_bot,

..multiset.ordered_cancel_add_comm_monoid }

@[simp] theorem cons_add (a : α) (s t : multiset α) : a ::ₘ s + t = a ::ₘ (s + t) :=

by rw [← singleton_add, ← singleton_add, add_assoc]

@[simp] theorem add_cons (a : α) (s t : multiset α) : s + a ::ₘ t = a ::ₘ (s + t) :=

by rw [add_comm, cons_add, add_comm]

@[simp] theorem mem_add {a : α} {s t : multiset α} : a ∈ s + t ↔ a ∈ s ∨ a ∈ t :=

quotient.induction_on₂ s t $ λ l₁ l₂, mem_append

lemma mem_of_mem_nsmul {a : α} {s : multiset α} {n : ℕ} (h : a ∈ n • s) : a ∈ s :=

begin

induction n with n ih,

{ rw zero_nsmul at h,

exact absurd h (not_mem_zero _) },

{ rw [succ_nsmul, mem_add] at h,

exact h.elim id ih },

end

@[simp]

lemma mem_nsmul {a : α} {s : multiset α} {n : ℕ} (h0 : n ≠ 0) : a ∈ n • s ↔ a ∈ s :=

begin

refine ⟨mem_of_mem_nsmul, λ h, _⟩,

obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero h0,

rw [succ_nsmul, mem_add],

exact or.inl h

end

lemma nsmul_cons {s : multiset α} (n : ℕ) (a : α) : n • (a ::ₘ s) = n • {a} + n • s :=

by rw [←singleton_add, nsmul_add]

/-! ### Cardinality -/

/-- The cardinality of a multiset is the sum of the multiplicities

of all its elements, or simply the length of the underlying list. -/

def card : multiset α →+ ℕ :=

{ to_fun := λ s, quot.lift_on s length $ λ l₁ l₂, perm.length_eq,

map_zero' := rfl,

map_add' := λ s t, quotient.induction_on₂ s t length_append }

@[simp] theorem coe_card (l : list α) : card (l : multiset α) = length l := rfl

@[simp] theorem length_to_list (s : multiset α) : s.to_list.length = s.card :=

by rw [← coe_card, coe_to_list]

@[simp] theorem card_zero : @card α 0 = 0 := rfl

theorem card_add (s t : multiset α) : card (s + t) = card s + card t :=

card.map_add s t

lemma card_nsmul (s : multiset α) (n : ℕ) :

(n • s).card = n * s.card :=

by rw [card.map_nsmul s n, nat.nsmul_eq_mul]

@[simp] theorem card_cons (a : α) (s : multiset α) : card (a ::ₘ s) = card s + 1 :=

quot.induction_on s $ λ l, rfl

@[simp] theorem card_singleton (a : α) : card ({a} : multiset α) = 1 :=

by simp only [←cons_zero, card_zero, eq_self_iff_true, zero_add, card_cons]

lemma card_pair (a b : α) : ({a, b} : multiset α).card = 2 :=

by rw [insert_eq_cons, card_cons, card_singleton]

theorem card_eq_one {s : multiset α} : card s = 1 ↔ ∃ a, s = {a} :=

⟨quot.induction_on s $ λ l h,

(list.length_eq_one.1 h).imp $ λ a, congr_arg coe,

λ ⟨a, e⟩, e.symm ▸ rfl⟩

theorem card_le_of_le {s t : multiset α} (h : s ≤ t) : card s ≤ card t :=

le_induction_on h $ λ l₁ l₂, sublist.length_le

@[mono] theorem card_mono : monotone (@card α) := λ a b, card_le_of_le

theorem eq_of_le_of_card_le {s t : multiset α} (h : s ≤ t) : card t ≤ card s → s = t :=

le_induction_on h $ λ l₁ l₂ s h₂, congr_arg coe $ s.eq_of_length_le h₂

theorem card_lt_of_lt {s t : multiset α} (h : s < t) : card s < card t :=

lt_of_not_ge $ λ h₂, ne_of_lt h $ eq_of_le_of_card_le (le_of_lt h) h₂

theorem lt_iff_cons_le {s t : multiset α} : s < t ↔ ∃ a, a ::ₘ s ≤ t :=

⟨quotient.induction_on₂ s t $ λ l₁ l₂ h,

subperm.exists_of_length_lt (le_of_lt h) (card_lt_of_lt h),

λ ⟨a, h⟩, lt_of_lt_of_le (lt_cons_self _ _) h⟩

@[simp] theorem card_eq_zero {s : multiset α} : card s = 0 ↔ s = 0 :=

⟨λ h, (eq_of_le_of_card_le (zero_le _) (le_of_eq h)).symm, λ e, by simp [e]⟩

theorem card_pos {s : multiset α} : 0 < card s ↔ s ≠ 0 :=

pos_iff_ne_zero.trans $ not_congr card_eq_zero

theorem card_pos_iff_exists_mem {s : multiset α} : 0 < card s ↔ ∃ a, a ∈ s :=

quot.induction_on s $ λ l, length_pos_iff_exists_mem

lemma card_eq_two {s : multiset α} : s.card = 2 ↔ ∃ x y, s = {x, y} :=

⟨quot.induction_on s (λ l h, (list.length_eq_two.mp h).imp

(λ a, Exists.imp (λ b, congr_arg coe))), λ ⟨a, b, e⟩, e.symm ▸ rfl⟩

lemma card_eq_three {s : multiset α} : s.card = 3 ↔ ∃ x y z, s = {x, y, z} :=

⟨quot.induction_on s (λ l h, (list.length_eq_three.mp h).imp

(λ a, Exists.imp (λ b, Exists.imp (λ c, congr_arg coe)))), λ ⟨a, b, c, e⟩, e.symm ▸ rfl⟩

/-! ### Induction principles -/

/-- A strong induction principle for multisets:

If you construct a value for a particular multiset given values for all strictly smaller multisets,

you can construct a value for any multiset.

-/

@[elab_as_eliminator] def strong_induction_on {p : multiset α → Sort*} :

∀ (s : multiset α), (∀ s, (∀t < s, p t) → p s) → p s

| s := λ ih, ih s $ λ t h,

have card t < card s, from card_lt_of_lt h,

strong_induction_on t ih

using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf card⟩]}

theorem strong_induction_eq {p : multiset α → Sort*}

(s : multiset α) (H) : @strong_induction_on _ p s H =

H s (λ t h, @strong_induction_on _ p t H) :=

by rw [strong_induction_on]

@[elab_as_eliminator] lemma case_strong_induction_on {p : multiset α → Prop}

(s : multiset α) (h₀ : p 0) (h₁ : ∀ a s, (∀t ≤ s, p t) → p (a ::ₘ s)) : p s :=

multiset.strong_induction_on s $ assume s,

multiset.induction_on s (λ _, h₀) $ λ a s _ ih, h₁ _ _ $

λ t h, ih _ $ lt_of_le_of_lt h $ lt_cons_self _ _

/-- Suppose that, given that `p t` can be defined on all supersets of `s` of cardinality less than

`n`, one knows how to define `p s`. Then one can inductively define `p s` for all multisets `s` of

cardinality less than `n`, starting from multisets of card `n` and iterating. This

can be used either to define data, or to prove properties. -/

def strong_downward_induction {p : multiset α → Sort*} {n : ℕ} (H : ∀ t₁, (∀ {t₂ : multiset α},

t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁) :

∀ (s : multiset α), s.card ≤ n → p s

| s := H s (λ t ht h, have n - card t < n - card s,

from (tsub_lt_tsub_iff_left_of_le ht).2 (card_lt_of_lt h),

strong_downward_induction t ht)

using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ (t : multiset α), n - t.card)⟩]}

lemma strong_downward_induction_eq {p : multiset α → Sort*} {n : ℕ} (H : ∀ t₁, (∀ {t₂ : multiset α},

t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁) (s : multiset α) :

strong_downward_induction H s = H s (λ t ht hst, strong_downward_induction H t ht) :=

by rw strong_downward_induction

/-- Analogue of `strong_downward_induction` with order of arguments swapped. -/

@[elab_as_eliminator] def strong_downward_induction_on {p : multiset α → Sort*} {n : ℕ} :

∀ (s : multiset α), (∀ t₁, (∀ {t₂ : multiset α}, t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n →

p t₁) → s.card ≤ n → p s :=

λ s H, strong_downward_induction H s

lemma strong_downward_induction_on_eq {p : multiset α → Sort*} (s : multiset α) {n : ℕ} (H : ∀ t₁,

(∀ {t₂ : multiset α}, t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁) :

s.strong_downward_induction_on H = H s (λ t ht h, t.strong_downward_induction_on H ht) :=

by { dunfold strong_downward_induction_on, rw strong_downward_induction }

/-- Another way of expressing `strong_induction_on`: the `(<)` relation is well-founded. -/

lemma well_founded_lt : well_founded ((<) : multiset α → multiset α → Prop) :=

subrelation.wf (λ _ _, multiset.card_lt_of_lt) (measure_wf multiset.card)

instance is_well_founded_lt : _root_.well_founded_lt (multiset α) := ⟨well_founded_lt⟩

/-! ### `multiset.replicate` -/

/-- `replicate n a` is the multiset containing only `a` with multiplicity `n`. -/

def replicate (n : ℕ) (a : α) : multiset α := replicate n a

lemma coe_replicate (n : ℕ) (a : α) : (list.replicate n a : multiset α) = replicate n a := rfl

@[simp] lemma replicate_zero (a : α) : replicate 0 a = 0 := rfl

@[simp] lemma replicate_succ (a : α) (n) : replicate (n + 1) a = a ::ₘ replicate n a := rfl

lemma replicate_add (m n : ℕ) (a : α) : replicate (m + n) a = replicate m a + replicate n a :=

congr_arg _ $ list.replicate_add _ _ _

/-- `multiset.replicate` as an `add_monoid_hom`. -/

@[simps] def replicate_add_monoid_hom (a : α) : ℕ →+ multiset α :=

{ to_fun := λ n, replicate n a,

map_zero' := replicate_zero a,

map_add' := λ _ _, replicate_add _ _ a }

lemma replicate_one (a : α) : replicate 1 a = {a} := rfl

@[simp] lemma card_replicate : ∀ n (a : α), card (replicate n a) = n := length_replicate

lemma mem_replicate {a b : α} {n : ℕ} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a := mem_replicate

theorem eq_of_mem_replicate {a b : α} {n} : b ∈ replicate n a → b = a := eq_of_mem_replicate

theorem eq_replicate_card {a : α} {s : multiset α} : s = replicate s.card a ↔ ∀ b ∈ s, b = a :=

quot.induction_on s $ λ l, coe_eq_coe.trans $ perm_replicate.trans eq_replicate_length

alias eq_replicate_card ↔ _ eq_replicate_of_mem

theorem eq_replicate {a : α} {n} {s : multiset α} :

s = replicate n a ↔ card s = n ∧ ∀ b ∈ s, b = a :=

⟨λ h, h.symm ▸ ⟨card_replicate _ _, λ b, eq_of_mem_replicate⟩,

λ ⟨e, al⟩, e ▸ eq_replicate_of_mem al⟩

lemma replicate_right_injective {n : ℕ} (hn : n ≠ 0) :

function.injective (replicate n : α → multiset α) :=

λ a b h, (eq_replicate.1 h).2 _ $ mem_replicate.2 ⟨hn, rfl⟩

@[simp] lemma replicate_right_inj {a b : α} {n : ℕ} (h : n ≠ 0) :

replicate n a = replicate n b ↔ a = b :=

(replicate_right_injective h).eq_iff

theorem replicate_left_injective (a : α) : function.injective (λ n, replicate n a) :=

λ m n h, by rw [← (eq_replicate.1 h).1, card_replicate]

theorem replicate_subset_singleton : ∀ n (a : α), replicate n a ⊆ {a} := replicate_subset_singleton

theorem replicate_le_coe {a : α} {n} {l : list α} :

replicate n a ≤ l ↔ list.replicate n a <+ l :=

⟨λ ⟨l', p, s⟩, (perm_replicate.1 p) ▸ s, sublist.subperm⟩

theorem nsmul_singleton (a : α) (n) : n • ({a} : multiset α) = replicate n a :=

begin

refine eq_replicate.mpr ⟨_, λ b hb, mem_singleton.mp (mem_of_mem_nsmul hb)⟩,

rw [card_nsmul, card_singleton, mul_one]

end

lemma nsmul_replicate {a : α} (n m : ℕ) : n • replicate m a = replicate (n * m) a :=

((replicate_add_monoid_hom a).map_nsmul _ _).symm

lemma replicate_le_replicate (a : α) {k n : ℕ} :

replicate k a ≤ replicate n a ↔ k ≤ n :=

replicate_le_coe.trans $ list.replicate_sublist_replicate _

lemma le_replicate_iff {m : multiset α} {a : α} {n : ℕ} :

m ≤ replicate n a ↔ ∃ (k ≤ n), m = replicate k a :=

⟨λ h, ⟨m.card, (card_mono h).trans_eq (card_replicate _ _), eq_replicate_card.2 $

λ b hb, eq_of_mem_replicate $ subset_of_le h hb⟩,

λ ⟨k, hkn, hm⟩, hm.symm ▸ (replicate_le_replicate _).2 hkn⟩

lemma lt_replicate_succ {m : multiset α} {x : α} {n : ℕ} :

m < replicate (n + 1) x ↔ m ≤ replicate n x :=

begin

rw lt_iff_cons_le,

split,

{ rintros ⟨x', hx'⟩,

have := eq_of_mem_replicate (mem_of_le hx' (mem_cons_self _ _)),

rwa [this, replicate_succ, cons_le_cons_iff] at hx' },

{ intro h,

rw replicate_succ,

exact ⟨x, cons_le_cons _ h⟩ }

end

/-! ### Erasing one copy of an element -/

section erase

variables [decidable_eq α] {s t : multiset α} {a b : α}

/-- `erase s a` is the multiset that subtracts 1 from the

multiplicity of `a`. -/

def erase (s : multiset α) (a : α) : multiset α :=

quot.lift_on s (λ l, (l.erase a : multiset α))

(λ l₁ l₂ p, quot.sound (p.erase a))

@[simp] theorem coe_erase (l : list α) (a : α) :

erase (l : multiset α) a = l.erase a := rfl

@[simp] theorem erase_zero (a : α) : (0 : multiset α).erase a = 0 := rfl

@[simp] theorem erase_cons_head (a : α) (s : multiset α) : (a ::ₘ s).erase a = s :=

quot.induction_on s $ λ l, congr_arg coe $ erase_cons_head a l

@[simp, priority 990]

theorem erase_cons_tail {a b : α} (s : multiset α) (h : b ≠ a) :

(b ::ₘ s).erase a = b ::ₘ s.erase a :=

quot.induction_on s $ λ l, congr_arg coe $ erase_cons_tail l h

@[simp] theorem erase_singleton (a : α) : ({a} : multiset α).erase a = 0 := erase_cons_head a 0

@[simp, priority 980]

theorem erase_of_not_mem {a : α} {s : multiset α} : a ∉ s → s.erase a = s :=

quot.induction_on s $ λ l h, congr_arg coe $ erase_of_not_mem h

@[simp, priority 980]

theorem cons_erase {s : multiset α} {a : α} : a ∈ s → a ::ₘ s.erase a = s :=

quot.induction_on s $ λ l h, quot.sound (perm_cons_erase h).symm

theorem le_cons_erase (s : multiset α) (a : α) : s ≤ a ::ₘ s.erase a :=

if h : a ∈ s then le_of_eq (cons_erase h).symm

else by rw erase_of_not_mem h; apply le_cons_self

lemma add_singleton_eq_iff {s t : multiset α} {a : α} :

s + {a} = t ↔ a ∈ t ∧ s = t.erase a :=

begin

rw [add_comm, singleton_add], split,

{ rintro rfl, exact ⟨s.mem_cons_self a, (s.erase_cons_head a).symm⟩ },

{ rintro ⟨h, rfl⟩, exact cons_erase h },

end

theorem erase_add_left_pos {a : α} {s : multiset α} (t) : a ∈ s → (s + t).erase a = s.erase a + t :=

quotient.induction_on₂ s t $ λ l₁ l₂ h, congr_arg coe $ erase_append_left l₂ h

theorem erase_add_right_pos {a : α} (s) {t : multiset α} (h : a ∈ t) :

(s + t).erase a = s + t.erase a :=

by rw [add_comm, erase_add_left_pos s h, add_comm]

theorem erase_add_right_neg {a : α} {s : multiset α} (t) :

a ∉ s → (s + t).erase a = s + t.erase a :=

quotient.induction_on₂ s t $ λ l₁ l₂ h, congr_arg coe $ erase_append_right l₂ h

theorem erase_add_left_neg {a : α} (s) {t : multiset α} (h : a ∉ t) :

(s + t).erase a = s.erase a + t :=

by rw [add_comm, erase_add_right_neg s h, add_comm]

theorem erase_le (a : α) (s : multiset α) : s.erase a ≤ s :=

quot.induction_on s $ λ l, (erase_sublist a l).subperm

@[simp] theorem erase_lt {a : α} {s : multiset α} : s.erase a < s ↔ a ∈ s :=

⟨λ h, not_imp_comm.1 erase_of_not_mem (ne_of_lt h),

λ h, by simpa [h] using lt_cons_self (s.erase a) a⟩

theorem erase_subset (a : α) (s : multiset α) : s.erase a ⊆ s :=

subset_of_le (erase_le a s)

theorem mem_erase_of_ne {a b : α} {s : multiset α} (ab : a ≠ b) : a ∈ s.erase b ↔ a ∈ s :=

quot.induction_on s $ λ l, list.mem_erase_of_ne ab

theorem mem_of_mem_erase {a b : α} {s : multiset α} : a ∈ s.erase b → a ∈ s :=

mem_of_subset (erase_subset _ _)

theorem erase_comm (s : multiset α) (a b : α) : (s.erase a).erase b = (s.erase b).erase a :=

quot.induction_on s $ λ l, congr_arg coe $ l.erase_comm a b

theorem erase_le_erase {s t : multiset α} (a : α) (h : s ≤ t) : s.erase a ≤ t.erase a :=

le_induction_on h $ λ l₁ l₂ h, (h.erase _).subperm

theorem erase_le_iff_le_cons {s t : multiset α} {a : α} : s.erase a ≤ t ↔ s ≤ a ::ₘ t :=

⟨λ h, le_trans (le_cons_erase _ _) (cons_le_cons _ h),

λ h, if m : a ∈ s

then by rw ← cons_erase m at h; exact (cons_le_cons_iff _).1 h

else le_trans (erase_le _ _) ((le_cons_of_not_mem m).1 h)⟩

@[simp] theorem card_erase_of_mem {a : α} {s : multiset α} :

a ∈ s → card (s.erase a) = pred (card s) :=

quot.induction_on s $ λ l, length_erase_of_mem

@[simp] lemma card_erase_add_one {a : α} {s : multiset α} :

a ∈ s → (s.erase a).card + 1 = s.card :=

quot.induction_on s $ λ l, length_erase_add_one

theorem card_erase_lt_of_mem {a : α} {s : multiset α} : a ∈ s → card (s.erase a) < card s :=

λ h, card_lt_of_lt (erase_lt.mpr h)

theorem card_erase_le {a : α} {s : multiset α} : card (s.erase a) ≤ card s :=

card_le_of_le (erase_le a s)

theorem card_erase_eq_ite {a : α} {s : multiset α} :

card (s.erase a) = if a ∈ s then pred (card s) else card s :=

begin

by_cases h : a ∈ s,

{ rwa [card_erase_of_mem h, if_pos] },

{ rwa [erase_of_not_mem h, if_neg] }

end

end erase

@[simp] theorem coe_reverse (l : list α) : (reverse l : multiset α) = l :=

quot.sound $ reverse_perm _

/-! ### `multiset.map` -/

/-- `map f s` is the lift of the list `map` operation. The multiplicity

of `b` in `map f s` is the number of `a ∈ s` (counting multiplicity)

such that `f a = b`. -/

def map (f : α → β) (s : multiset α) : multiset β :=

quot.lift_on s (λ l : list α, (l.map f : multiset β))

(λ l₁ l₂ p, quot.sound (p.map f))

@[congr]

theorem map_congr {f g : α → β} {s t : multiset α} :

s = t → (∀ x ∈ t, f x = g x) → map f s = map g t :=

begin

rintros rfl h,

induction s using quot.induction_on,

exact congr_arg coe (map_congr h)

end

lemma map_hcongr {β' : Type*} {m : multiset α} {f : α → β} {f' : α → β'}

(h : β = β') (hf : ∀a∈m, f a == f' a) : map f m == map f' m :=

begin subst h, simp at hf, simp [map_congr rfl hf] end

theorem forall_mem_map_iff {f : α → β} {p : β → Prop} {s : multiset α} :

(∀ y ∈ s.map f, p y) ↔ (∀ x ∈ s, p (f x)) :=

quotient.induction_on' s $ λ L, list.forall_mem_map_iff

@[simp] theorem coe_map (f : α → β) (l : list α) : map f ↑l = l.map f := rfl

@[simp] theorem map_zero (f : α → β) : map f 0 = 0 := rfl

@[simp] theorem map_cons (f : α → β) (a s) : map f (a ::ₘ s) = f a ::ₘ map f s :=

quot.induction_on s $ λ l, rfl

theorem map_comp_cons (f : α → β) (t) : map f ∘ cons t = cons (f t) ∘ map f :=

by { ext, simp }

@[simp] theorem map_singleton (f : α → β) (a : α) : ({a} : multiset α).map f = {f a} := rfl

@[simp] theorem map_replicate (f : α → β) (a : α) (k : ℕ) :

(replicate k a).map f = replicate k (f a) :=

by simp only [← coe_replicate, coe_map, map_replicate]

@[simp] theorem map_add (f : α → β) (s t) : map f (s + t) = map f s + map f t :=

quotient.induction_on₂ s t $ λ l₁ l₂, congr_arg coe $ map_append _ _ _

/-- If each element of `s : multiset α` can be lifted to `β`, then `s` can be lifted to

`multiset β`. -/

instance can_lift (c) (p) [can_lift α β c p] :

can_lift (multiset α) (multiset β) (map c) (λ s, ∀ x ∈ s, p x) :=

{ prf := by { rintro ⟨l⟩ hl, lift l to list β using hl, exact ⟨l, coe_map _ _⟩ } }

/-- `multiset.map` as an `add_monoid_hom`. -/

def map_add_monoid_hom (f : α → β) : multiset α →+ multiset β :=

{ to_fun := map f,

map_zero' := map_zero _,

map_add' := map_add _ }

@[simp] lemma coe_map_add_monoid_hom (f : α → β) :

(map_add_monoid_hom f : multiset α → multiset β) = map f := rfl

theorem map_nsmul (f : α → β) (n : ℕ) (s) : map f (n • s) = n • (map f s) :=

(map_add_monoid_hom f).map_nsmul _ _

@[simp] theorem mem_map {f : α → β} {b : β} {s : multiset α} :

b ∈ map f s ↔ ∃ a, a ∈ s ∧ f a = b :=

quot.induction_on s $ λ l, mem_map

@[simp] theorem card_map (f : α → β) (s) : card (map f s) = card s :=

quot.induction_on s $ λ l, length_map _ _

@[simp] theorem map_eq_zero {s : multiset α} {f : α → β} : s.map f = 0 ↔ s = 0 :=

by rw [← multiset.card_eq_zero, multiset.card_map, multiset.card_eq_zero]

theorem mem_map_of_mem (f : α → β) {a : α} {s : multiset α} (h : a ∈ s) : f a ∈ map f s :=

mem_map.2 ⟨_, h, rfl⟩

lemma map_eq_singleton {f : α → β} {s : multiset α} {b : β} :

map f s = {b} ↔ ∃ a : α, s = {a} ∧ f a = b :=

begin

split,

{ intro h,

obtain ⟨a, ha⟩ : ∃ a, s = {a},

{ rw [←card_eq_one, ←card_map, h, card_singleton] },

refine ⟨a, ha, _⟩,

rw [←mem_singleton, ←h, ha, map_singleton, mem_singleton] },

{ rintro ⟨a, rfl, rfl⟩,

simp }

end

lemma map_eq_cons [decidable_eq α] (f : α → β) (s : multiset α) (t : multiset β) (b : β) :

(∃ a ∈ s, f a = b ∧ (s.erase a).map f = t) ↔ s.map f = b ::ₘ t :=

begin

split,

{ rintro ⟨a, ha, rfl, rfl⟩,

rw [←map_cons, multiset.cons_erase ha] },

{ intro h,

have : b ∈ s.map f,

{ rw h, exact mem_cons_self _ _ },

obtain ⟨a, h1, rfl⟩ := mem_map.mp this,

obtain ⟨u, rfl⟩ := exists_cons_of_mem h1,

rw [map_cons, cons_inj_right] at h,

refine ⟨a, mem_cons_self _ _, rfl, _⟩,

rw [multiset.erase_cons_head, h] }

end

theorem mem_map_of_injective {f : α → β} (H : function.injective f) {a : α} {s : multiset α} :

f a ∈ map f s ↔ a ∈ s :=

quot.induction_on s $ λ l, mem_map_of_injective H

@[simp] theorem map_map (g : β → γ) (f : α → β) (s : multiset α) :

map g (map f s) = map (g ∘ f) s :=

quot.induction_on s $ λ l, congr_arg coe $ list.map_map _ _ _

theorem map_id (s : multiset α) : map id s = s :=

quot.induction_on s $ λ l, congr_arg coe $ map_id _

@[simp] lemma map_id' (s : multiset α) : map (λx, x) s = s := map_id s

@[simp] theorem map_const (s : multiset α) (b : β) :

map (function.const α b) s = replicate s.card b :=

quot.induction_on s $ λ l, congr_arg coe $ map_const _ _

-- Not a `simp` lemma because `function.const` is reducibel in Lean 3

theorem map_const' (s : multiset α) (b : β) : map (λ _, b) s = replicate s.card b := map_const s b

theorem eq_of_mem_map_const {b₁ b₂ : β} {l : list α} (h : b₁ ∈ map (function.const α b₂) l) :

b₁ = b₂ :=

eq_of_mem_replicate $ by rwa map_const at h

@[simp] theorem map_le_map {f : α → β} {s t : multiset α} (h : s ≤ t) : map f s ≤ map f t :=

le_induction_on h $ λ l₁ l₂ h, (h.map f).subperm

@[simp] lemma map_lt_map {f : α → β} {s t : multiset α} (h : s < t) : s.map f < t.map f :=

begin

refine (map_le_map h.le).lt_of_not_le (λ H, h.ne $ eq_of_le_of_card_le h.le _),

rw [←s.card_map f, ←t.card_map f],

exact card_le_of_le H,

end

lemma map_mono (f : α → β) : monotone (map f) := λ _ _, map_le_map

lemma map_strict_mono (f : α → β) : strict_mono (map f) := λ _ _, map_lt_map

@[simp] theorem map_subset_map {f : α → β} {s t : multiset α} (H : s ⊆ t) : map f s ⊆ map f t :=

λ b m, let ⟨a, h, e⟩ := mem_map.1 m in mem_map.2 ⟨a, H h, e⟩

lemma map_erase [decidable_eq α] [decidable_eq β]

(f : α → β) (hf : function.injective f) (x : α) (s : multiset α) :

(s.erase x).map f = (s.map f).erase (f x) :=

begin

induction s using multiset.induction_on with y s ih,

{ simp },

by_cases hxy : y = x,

{ cases hxy, simp },

{ rw [s.erase_cons_tail hxy, map_cons, map_cons, (s.map f).erase_cons_tail (hf.ne hxy), ih] }

end

lemma map_surjective_of_surjective {f : α → β} (hf : function.surjective f) :

function.surjective (map f) :=

begin

intro s,

induction s using multiset.induction_on with x s ih,

{ exact ⟨0, map_zero _⟩ },

{ obtain ⟨y, rfl⟩ := hf x,

obtain ⟨t, rfl⟩ := ih,

exact ⟨y ::ₘ t, map_cons _ _ _⟩ }

end

/-! ### `multiset.fold` -/

/-- `foldl f H b s` is the lift of the list operation `foldl f b l`,

which folds `f` over the multiset. It is well defined when `f` is right-commutative,

that is, `f (f b a₁) a₂ = f (f b a₂) a₁`. -/

def foldl (f : β → α → β) (H : right_commutative f) (b : β) (s : multiset α) : β :=

quot.lift_on s (λ l, foldl f b l)

(λ l₁ l₂ p, p.foldl_eq H b)