From ca47d53455581add5a5c29b30e4a7298356af169 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Wed, 6 Mar 2019 20:27:06 +1100
Subject: [PATCH] feat(data/list): lemmas about count and bag_inter

---
 src/data/finset.lean     |  4 +++
 src/data/list/basic.lean | 73 +++++++++++++++++++++++++++++++++++++++-
 src/data/multiset.lean   |  3 ++
 3 files changed, 79 insertions(+), 1 deletion(-)

diff --git a/src/data/finset.lean b/src/data/finset.lean
index 47f9e5dfc58a2..c45f310ea0483 100644
--- a/src/data/finset.lean
+++ b/src/data/finset.lean
@@ -713,6 +713,10 @@ finset.ext' $ by simp
         finset.union_idempotent] }
   end
 
+@[simp] lemma to_finset_inter (s t : multiset α) :
+  to_finset (s ∩ t) = to_finset s ∩ to_finset t :=
+finset.ext' $ by simp
+
 end multiset
 
 namespace list
diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean
index aeae66df96892..b0813f22e1813 100644
--- a/src/data/list/basic.lean
+++ b/src/data/list/basic.lean
@@ -2734,6 +2734,27 @@ theorem map_foldl_erase [decidable_eq β] {f : α → β} (finj : injective f) {
 by induction l₂ generalizing l₁; [refl,
 simp only [foldl_cons, map_erase finj, *]]
 
+@[simp] theorem count_erase_self (a : α) : ∀ (s : list α), count a (list.erase s a) = pred (count a s)
+| [] := by simp
+| (h :: t) :=
+begin
+  rw erase_cons,
+  by_cases p : h = a,
+  { rw [if_pos p, count_cons', if_pos p.symm], simp },
+  { rw [if_neg p, count_cons', count_cons', if_neg (λ x : a = h, p x.symm), count_erase_self],
+    simp, }
+end
+
+@[simp] theorem count_erase_of_ne {a b : α} (ab : a ≠ b) : ∀ (s : list α), count a (list.erase s b) = count a s
+| [] := by simp
+| (x :: xs) :=
+begin
+  rw erase_cons,
+  split_ifs with h,
+  { rw [count_cons', h, if_neg ab], simp },
+  { rw [count_cons', count_cons', count_erase_of_ne] }
+end
+
 end erase
 
 /- diff -/
@@ -3209,7 +3230,7 @@ begin
   simp only [erase_of_not_mem h, list.bag_inter, if_neg h]
 end
 
-theorem mem_bag_inter {a : α} : ∀ {l₁ l₂ : list α}, a ∈ l₁.bag_inter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂
+@[simp] theorem mem_bag_inter {a : α} : ∀ {l₁ l₂ : list α}, a ∈ l₁.bag_inter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂
 | []      l₂ := by simp only [nil_bag_inter, not_mem_nil, false_and]
 | (b::l₁) l₂ := begin
     by_cases b ∈ l₂,
@@ -3222,6 +3243,48 @@ theorem mem_bag_inter {a : α} : ∀ {l₁ l₂ : list α}, a ∈ l₁.bag_inter
       rintro ⟨rfl, h'⟩, exact h.elim h' }
   end
 
+@[simp] theorem count_bag_inter {a : α} :
+  ∀ {l₁ l₂ : list α}, count a (l₁.bag_inter l₂) = min (count a l₁) (count a l₂)
+| []         l₂ := by simp
+| l₁         [] := by simp
+| (h₁ :: l₁) (h₂ :: l₂) :=
+begin
+  dsimp [list.bag_inter],
+  simp,
+  by_cases p₁ : h₁ = h₂,
+  { simp [p₁],
+    repeat { rw count_cons' },
+    by_cases p₂ : h₂ = a,
+    { simp *,
+      rw min_add_add_left, },
+    { simp *,
+      rw if_neg (ne.symm p₂),
+      simp, } },
+  { simp *,
+    split_ifs,
+    { rw list.erase_cons,
+      rw if_neg (ne.symm p₁),
+      repeat { rw count_cons' },
+      rw count_bag_inter,
+      repeat { rw count_cons' },
+      split_ifs with p₂ p₃ p₃,
+      { exfalso, exact p₁ (eq.trans p₃.symm p₂), },
+      { simp, rw count_erase_of_ne p₃, },
+      { rw [←p₃, count_erase_self],
+        simp only [nat.add_zero],
+        rw ←min_add_add_right,
+        conv {to_lhs, congr, skip, rw [add_one] },
+        rw nat.succ_pred_eq_of_pos,
+        subst p₃,
+        exact count_pos.2 h },
+      { simp, rw count_erase_of_ne p₃, } },
+    { rw count_bag_inter,
+      by_cases p₂ : a = h₁,
+      { rw [p₂, count_cons', if_neg p₁, count_eq_zero_of_not_mem h],
+        simp },
+      { conv {to_rhs, rw [count_cons', if_neg p₂], simp } } } }
+end
+
 theorem bag_inter_sublist_left : ∀ l₁ l₂ : list α, l₁.bag_inter l₂ <+ l₁
 | []      l₂ := by simp [nil_sublist]
 | (b::l₁) l₂ := begin
@@ -3230,6 +3293,14 @@ theorem bag_inter_sublist_left : ∀ l₁ l₂ : list α, l₁.bag_inter l₂ <+
   { apply sublist_cons_of_sublist, apply bag_inter_sublist_left }
 end
 
+theorem bag_inter_nil_iff_inter_nil : ∀ l₁ l₂ : list α, l₁.bag_inter l₂ = [] ↔ l₁ ∩ l₂ = []
+| []      l₂ := by simp
+| (b::l₁) l₂ :=
+begin
+  by_cases h : b ∈ l₂; simp [h],
+  exact bag_inter_nil_iff_inter_nil l₁ l₂
+end
+
 end bag_inter
 
 /- pairwise relation (generalized no duplicate) -/
diff --git a/src/data/multiset.lean b/src/data/multiset.lean
index 6827ed927fac7..f3e12dd7388ec 100644
--- a/src/data/multiset.lean
+++ b/src/data/multiset.lean
@@ -1823,6 +1823,9 @@ quotient.induction_on₂ s t $ λ l₁ l₂, quotient.eq.trans perm_iff_count
 theorem ext' {s t : multiset α} : (∀ a, count a s = count a t) → s = t :=
 ext.2
 
+@[simp] theorem coe_inter (s t : list α) : (s ∩ t : multiset α) = (s.bag_inter t : list α) :=
+by ext; simp
+
 theorem le_iff_count {s t : multiset α} : s ≤ t ↔ ∀ a, count a s ≤ count a t :=
 ⟨λ h a, count_le_of_le a h, λ al,
  by rw ← (ext.2 (λ a, by simp [max_eq_right (al a)]) : s ∪ t = t);