feat(data/sym/card): Prove stars and bars (superseded by #11162)

src/data/sym/basic.lean

@@ -232,10 +232,14 @@ by simp [sym.map, subtype.mk.inj_eq]
   (a :: s).map f = (f a) :: s.map f :=
 by { cases s, simp [map, cons] }
 
+@[congr] lemma map_congr {β : Type*} {f g : α → β} {s : sym α n} (h: ∀ x ∈ s, f x = g x) :
+  map f s = map g s :=
+by simpa [map, subtype.mk.inj_eq] using multiset.map_congr h
+
 /-- Mapping an equivalence `α ≃ β` using `sym.map` gives an equivalence between `sym α n` and
 `sym β n`. -/
 @[simps]
-def equiv_congr {β : Type u} (e : α ≃ β) : sym α n ≃ sym β n :=
+def equiv_congr {α β : Type*} (e : α ≃ β) : sym α n ≃ sym β n :=
 { to_fun := map e,
   inv_fun := map e.symm,
   left_inv := λ x, by rw [map_map, equiv.symm_comp_self, map_id],

src/data/sym/card.lean

@@ -13,7 +13,7 @@ In this file, we prove the case `n = 2` of stars and bars.
 
 ## Informal statement
 
-If we have `n` objects to put in `k` boxes, we can do so in exactly `(n + k - 1).choose n` ways.
+If we have `n` objects to put in `k` boxes, we can do so in exactly `(n + k - 1).choose k` ways.
 
 ## Formal statement
 
@@ -22,9 +22,8 @@ elements in those boxes corresponds to choosing how many of each element of `α`
 of card `n`. `sym α n` being the subtype of `multiset α` of multisets of card `n`, writing stars
 and bars using types gives
 ```lean
--- TODO: this lemma is not yet proven
 lemma stars_and_bars {α : Type*} [fintype α] (n : ℕ) :
-  card (sym α n) = (card α + n - 1).choose (card α) := sorry
+  card (sym α n) = (card α + n - 1).choose n := sorry
 ```
 
 ## TODO
@@ -36,9 +35,108 @@ Prove the general case of stars and bars.
 stars and bars
 -/
 
+def multichoose1 (n k : ℕ) := fintype.card (sym (fin n) k)
+
+def multichoose2 (n k : ℕ) := (n + k - 1).choose k
+
+def encode (n k : ℕ) (x : sym (fin n.succ) k.succ) : sym (fin n) k.succ ⊕ sym (fin n.succ) k :=
+if h : fin.last n ∈ x then
+  sum.inr ⟨x.val.erase (fin.last n), by { rw [multiset.card_erase_of_mem h, x.property], refl }⟩
+else begin
+  refine sum.inl (x.map (λ a, ⟨if (a : ℕ) = n then 0 else a, _⟩)),
+  { split_ifs,
+    { rw pos_iff_ne_zero,
+      rintro rfl,
+      obtain ⟨w, r⟩ := @multiset.exists_mem_of_ne_zero _ x.val (λ h, by simpa [h] using x.property),
+      simpa [subsingleton.elim w 0] using r, },
+    { cases lt_or_eq_of_le (nat.le_of_lt_succ a.property); solve_by_elim } },
+end
+
+def decode (n k : ℕ) : sym (fin n) k.succ ⊕ sym (fin n.succ) k → sym (fin n.succ) k.succ
+| (sum.inl x) := x.map (λ a, ⟨a.val, a.property.step⟩)
+| (sum.inr x) := (fin.last n)::x
+
+lemma equivalent (n k : ℕ) : sym (fin n.succ) k.succ ≃ sym (fin n) k.succ ⊕ sym (fin n.succ) k :=
+{ to_fun := encode n k,
+  inv_fun := decode n k,
+  left_inv := λ x, begin
+    rw encode,
+    split_ifs,
+    { cases x,
+      simpa [decode, sym.cons, sym.erase, subtype.mk.inj_eq] using multiset.cons_erase h },
+    { simp only [decode, sym.map_map, subtype.mk.inj_eq, function.comp],
+      convert @sym.map_congr _ _ _ _ id _ _,
+      { rw sym.map_id },
+      { intros a h',
+        cases a,
+        split_ifs,
+        { norm_num at h_1,
+          simp_rw h_1 at h',
+          exact (h h').elim },
+        { norm_num } } },
+  end,
+  right_inv := begin
+    rintro (x|x),
+    { cases x with x hx,
+      rw [decode, encode],
+      split_ifs,
+      { obtain ⟨y, v, b⟩ := multiset.mem_map.mp h,
+        rw [fin.last, subtype.mk_eq_mk] at b,
+        have := y.property,
+        rw b at this,
+        exact nat.lt_asymm this this, },
+      { simp only [sym.map_map, function.comp, fin.val_eq_coe, subtype.mk_eq_mk, fin.coe_mk],
+        convert sym.map_congr _,
+        { rw multiset.map_id, },
+        { rintros ⟨g, hg⟩ h',
+          split_ifs with h'',
+          { simp only [fin.coe_mk] at h'',
+            subst g,
+            exact (nat.lt_asymm hg hg).elim, },
+          { refl } } } },
+    { rw [decode, encode],
+      split_ifs,
+      { cases x, simp [sym.cons] },
+      { apply h,
+        cases x,
+        simpa only [sym.cons] using multiset.mem_cons_self (fin.last n) x_val } }
+  end }
+
+lemma multichoose1_rec (n k : ℕ) :
+  multichoose1 n.succ k.succ = multichoose1 n k.succ + multichoose1 n.succ k :=
+by simpa only [multichoose1, fintype.card_sum.symm] using fintype.card_congr (equivalent n k)
+
+lemma multichoose2_rec (n k : ℕ) :
+  multichoose2 n.succ k.succ = multichoose2 n k.succ + multichoose2 n.succ k :=
+by simp [multichoose2, nat.choose_succ_succ, nat.add_comm, nat.add_succ]
+
+lemma multichoose1_eq_multichoose2 : ∀ (n k : ℕ), multichoose1 n k = multichoose2 n k
+| 0 0 := by simp [multichoose1, multichoose2]
+| 0 (k + 1) := by simp [multichoose1, multichoose2, fintype.card]
+| (n + 1) 0 := by simp [multichoose1, multichoose2]
+| (n + 1) (k + 1) :=
+by simp only [multichoose1_rec, multichoose2_rec, multichoose1_eq_multichoose2 n k.succ,
+  multichoose1_eq_multichoose2 n.succ k]
+
 open finset fintype
 
+namespace sym
+
+/-- The *stars and bars* lemma: the cardinality of `sym α n` is equal to
+`(card α + n - 1) choose n`. -/
+lemma stars_and_bars {α : Type*} [decidable_eq α] [fintype α] (n : ℕ) :
+  fintype.card (sym α n) = (fintype.card α + n - 1).choose n :=
+begin
+  have start := multichoose1_eq_multichoose2 (fintype.card α) n,
+  simp only [multichoose1, multichoose2] at start,
+  rw start.symm,
+  exact fintype.card_congr (equiv_congr ((@fintype.equiv_fin_of_card_eq α _ (fintype.card α) rfl))),
+end
+
+end sym
+
 namespace sym2
+
 variables {α : Type*} [decidable_eq α]
 
 /-- The `diag` of `s : finset α` is sent on a finset of `sym2 α` of card `s.card`. -/