multiset.map_diff_le, list.map_diff_subset/subperm, counterexample

map_diff_subset.lean

/- Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Generalization.20of.20map_diff/near/280148939 -/

import data.multiset.basic

/- The stronger version `list.map_diff_sublist` doesn't hold; here is a counterexample. -/
def l₁ := [0,1,2]
def l₂ := [2]
def f : ℕ → ℕ | 1 := 1 | _ := 0

#eval (l₁.map f).diff (l₂.map f) /- [1, 0] -/
#eval (l₁.diff l₂).map f /- [0, 1] -/
#eval ((l₁.map f).diff (l₂.map f) <+ (l₁.diff l₂).map f : bool) /- ff -/

open multiset
variables {α β : Type*} [decidable_eq α] [decidable_eq β] (f : α → β)
lemma multiset.map_sub_le (s₁ : multiset α) (s₂ : multiset α) :
  s₁.map f - s₂.map f ≤ (s₁ - s₂).map f :=
begin
  rw [tsub_le_iff_right, le_iff_count],
  intro, simp only [count_add, count_map, ← card_add, ← filter_add],
  exact card_le_of_le (filter_le_filter _ $ tsub_le_iff_right.1 le_rfl),
end

variables (l₁ : list α) (l₂ : list α)
lemma list.map_diff_subperm : (l₁.map f).diff (l₂.map f) <+~ (l₁.diff l₂).map f :=
by { simp only [← coe_le, ← coe_sub, ← coe_map], apply multiset.map_sub_le }

lemma list.map_diff_subset : (l₁.map f).diff (l₂.map f) ⊆ (l₁.diff l₂).map f :=
(l₁.map_diff_subperm f l₂).subset