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

[huynhtrankhanh]

---

[kmill]

Took a pass at simplification

[huynhtrankhanh]

oh dear I accidentally tapped the request review button 😢 sorry for that mistake

feel absolutely free to ignore the request

[kmill]

I think it would make sense to generalize this to arbitrary types to have an Even More combinatorial proof:

def encode {k : ℕ} (v : α) (x : sym α k.succ) : sym {w // w ≠ v} k.succ ⊕ sym α k :=
if h : v ∈ x then
  sum.inr ⟨x.val.erase v, by { rw [multiset.card_erase_of_mem h, x.property], refl }⟩
else begin
  refine sum.inl ⟨x.val.attach.map (λ a, if h' : (a : α) = v then _ else _), _⟩,
  { rw ←h' at h,
    exact (h a.property).elim, },
  { use a, },
  { rw [multiset.card_map, multiset.card_attach, x.property], }
end

def decode {k : ℕ} (v : α) : sym {w // w ≠ v} k.succ ⊕ sym α k → sym α k.succ
| (sum.inl x) := ⟨x.val.map subtype.val, by simpa [multiset.card_map] using x.property⟩
| (sum.inr x) := sym.cons v x

There are some dependent type issues when trying to prove equivalent, though, because of attach. Maybe someone wants to figure it out?

lemma equivalent {k : ℕ} (v : α) : sym α k.succ ≃ sym {w // w ≠ v} k.succ ⊕ sym α k :=
{ to_fun := encode v,
  inv_fun := decode v,
  left_inv := sorry,
  right_inv := sorry }

[eric-wieser]

Is the point in this generalization that you no longer have to start with fintype α? If so, I guess this does make sense.

[kmill]

@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's sym.map since there ought to be a function sum a b -> (a -> c) -> (b -> c) -> c

[YaelDillies]

I would rather write it like

def encode {k : ℕ} (x : sym (option α) k.succ) : sym α k.succ ⊕ sym (option α) k :=

and then use fintype.induction_empty_option. Subtypes are nasty.

[kmill]

@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.)

[huynhtrankhanh]

I will temporarily place all the new definitions in the data.sym.card file. When I push the new code, you can tell me where to move the new definitions to.

[eric-wieser]

Suggested change

	refine sum.inl (x.map (λ a, ⟨if (a : ℕ) = n then 0 else a, _⟩)),
	refine sum.inl (x.map fin.cast_pred),

[kmill]

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.