-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(data/sym/card): Prove stars and bars (superseded by #11162) #10846
Changes from all commits
3fac454
9f6b414
5e9e42a
37d6351
524f951
8f8907b
aea8073
c3f861d
6c2f7c4
13be373
86a4334
6e456d3
d6f9d66
13a96c3
bdc5d3a
0ea8b9f
2d1b7e3
b5bde30
b2746c2
4a5971d
22bdf78
6057a94
11b9c25
653d124
6836823
5106953
f246759
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change | ||||
---|---|---|---|---|---|---|
|
@@ -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,117 @@ Prove the general case of stars and bars. | |||||
stars and bars | ||||||
-/ | ||||||
|
||||||
/-- Define the multichoose number using `fintype.card`. -/ | ||||||
def multichoose1 (n k : ℕ) := fintype.card (sym (fin n) k) | ||||||
|
||||||
/-- Define the multichoose number using `nat.choose`. -/ | ||||||
def multichoose2 (n k : ℕ) := (n + k - 1).choose k | ||||||
|
||||||
/-- The `encode` function produces a `sym (fin n) k.succ` if the input doesn't contain `fin.last n` | ||||||
by casting `fin n.succ` to `fin n`. Otherwise, the function removes an instance of `fin.last n` from | ||||||
the input and produces a `sym (fin n.succ) 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.erase (fin.last n) h) | ||||||
else begin | ||||||
refine sum.inl (x.map (λ a, ⟨if (a : ℕ) = n then 0 else a, _⟩)), | ||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||
{ 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 | ||||||
|
||||||
/-- From the output of `encode`, the `decode` function reconstructs the original input. If the | ||||||
output contains `k.succ` elements, the original input can be reconstructed by casting `fin n` back | ||||||
to `fin n.succ`. Otherwise, an instance of `fin.last n` has been removed and the input can be | ||||||
reconstructed by adding it back. -/ | ||||||
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 fin.cast_succ | ||||||
| (sum.inr x) := (fin.last n)::x | ||||||
|
||||||
/-- As `encode` and `decode` are inverses of each other, `sym (fin n.succ) k.succ` is equivalent | ||||||
to `sym (fin n) k.succ ⊕ sym (fin n.succ) k`. -/ | ||||||
def 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, w⟩, v, b⟩ := multiset.mem_map.mp h, | ||||||
rw [fin.cast_succ_mk, fin.last, subtype.mk_eq_mk] at b, | ||||||
rw b at w, | ||||||
exact nat.lt_asymm w w, }, | ||||||
{ 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, fin.cast_succ_mk] at h'', | ||||||
subst g, | ||||||
exact (nat.lt_asymm hg hg).elim, }, | ||||||
{ refl } } } }, | ||||||
{ rw [decode, encode], | ||||||
split_ifs, | ||||||
{ cases x, simp [sym.cons, sym.erase, multiset.cons_erase] }, | ||||||
{ 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] | ||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Oh what a nice short proof this was. Hopefully we can recover it somehow in the new version with some additional lemmas to help support manipulating equivalences and cardinalities. |
||||||
|
||||||
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 : ℕ) : | ||||||
huynhtrankhanh marked this conversation as resolved.
Show resolved
Hide resolved
|
||||||
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`. -/ | ||||||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it would make sense to generalize this to arbitrary types to have an Even More combinatorial proof:
There are some dependent type issues when trying to prove
equivalent
, though, because ofattach
. Maybe someone wants to figure it out?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is the point in this generalization that you no longer have to start with
fintype α
? If so, I guess this does make sense.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@eric-wieser The point is to show it doesn't depend on any properties of
fin
, and also that this might be a useful function beyond stars and bars.encode
is "remove or restrict".decode
might not need to exist on its own if there'ssym.map
since there ought to be a functionsum a b -> (a -> c) -> (b -> c) -> c
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would rather write it like
and then use
fintype.induction_empty_option
. Subtypes are nasty.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@YaelDillies That seems good and more natural. (Mine was more like something in terms of
nat.pred
, which no one really wants if they can help it.)