Counting cardinalities in presence of partitions

Stream: new members

[Antoine Chambert-Loir]

The following MWE is arguably ugly, but I couldn't do better, in the presence of a docs#setoid.is_partition of a set which is known to be finite , to say that the cardinality of the ambient set is the sum of the cardinalities of its parts.
I struggled against coercions between finset (finset α) and set (set α).
Any advice or golfing is welcome !

In particular :

• Is there a better way to switch between close types, especially in the presence of finset.sum.

• On line 29, the suffices… is made to have Lean automatically insert the correct type; can one do better?

import data.setoid.partition
/-  {α : Type u_1} (c : set (set α)) :
    setoid.is_partition c =
      (∅ ∉ c ∧ ∀ (a : α), ∃! (b : set α) (H : b ∈ c), a ∈ b)
-/
import algebra.big_operators.order

variables {α : Type*}


open_locale big_operators classical


/-- The cardinal of ambient fintype equal the sum of cardinals of the parts of a partition (finset style)-/
lemma card_of_partition' [fintype α] {c : finset (finset α)} (hc : setoid.is_partition ({ s : set α | ∃ (t : finset α), s.to_finset = t ∧ t ∈ c } : set (set α))) :
  ∑ (s : finset α) in c, s.card = fintype.card α :=
begin
  rw ← mul_one (fintype.card α),
  rw ← finset.sum_card,
  intro a,
  rw finset.card_eq_one,
  obtain ⟨s, hs, hs'⟩ := hc.right a,
  simp only [exists_unique_iff_exists, exists_prop, and_imp, exists_eq_left', set.mem_set_of_eq] at hs hs',
  have hs'2 : ∀ (z : finset α), z ∈ c → a ∈ z → z = s.to_finset,
  { intros z hz ha,
    rw ← finset.coe_inj, simp,
    refine  hs' z _ (finset.mem_coe.mpr ha),
-- To get the correct type automatically and perform the rewrite
    suffices : ∀ {u v : finset α}, v ∈ c → u = v → u ∈ c,
    { refine this hz _,
      rw [← finset.coe_inj, set.coe_to_finset], },
    { intros u v hu huv, rw huv, exact hu, },
  },
  use s.to_finset,
  ext t,
  simp only [finset.mem_filter, finset.mem_singleton],
  split,
  { rintro ⟨ht,ha⟩,
    exact hs'2 t ht ha, },
  { intro ht,
    rw ← ht at hs, apply and.intro hs.left,
    rw ht, simp only [set.mem_to_finset],  exact hs.right,}
end

/-- The cardinal of ambient fintype equal the sum of cardinals of the parts of a partition (set style)-/
lemma card_of_partition [fintype α] {c : set (set α)} (hc : setoid.is_partition c) :
  ∑ (s : set α) in c.to_finset, s.to_finset.card = fintype.card α :=
begin
let c' : finset (finset α) := { s : finset (α) | (s : set α) ∈ c }.to_finset,
have hcc' : c = { s : set α | ∃ (t : finset α), s.to_finset = t ∧ t ∈ c' },
{ simp only [set.mem_to_finset, set.mem_set_of_eq, exists_eq_left', set.coe_to_finset, set.set_of_mem_eq] },
rw hcc' at hc,
rw ← card_of_partition'  hc,
have hi : ∀ (a : set α) (ha : a ∈ c.to_finset), a.to_finset ∈ c',
{ intros a ha,
  simp only [set.mem_to_finset, set.mem_set_of_eq, set.coe_to_finset],
  simpa only [set.mem_to_finset] using ha,  },
have hj : ∀ (a : finset α) (ha : a ∈ c'), (a : set α) ∈ c.to_finset,
{ intros a ha,
  simpa only [set.mem_to_finset] using ha, },
rw finset.sum_bij' _ hi _ _ hj,
{ intros a ha, simp only [set.coe_to_finset],  },
{ intros a ha,
  rw [← finset.coe_inj, set.coe_to_finset], },
{ intros a ha, refl, },
end

[Anatole Dedecker]

I’m not a big user of the finite cardinals API in Lean, but when working on the Burnside formula (docs#mul_action.sum_card_fixed_by_eq_card_orbits_mul_card_group) I found it really convenient to construct an equiv in calc mode and then just deduce the corresponding cardinal result

[Anatole Dedecker]

In particular I would definitely try using docs#finset.card_sigma in this case.

[Anatole Dedecker]

About the suffices I’m not sure if I understand your problem correctly, but do you know about docs#tactic.interactive.change ?

[Eric Wieser]

If you're working with finset.card, it should be much easier to use finpartition:

import algebra.big_operators.basic
import order.partition.finpartition

open_locale big_operators

/-- The cardinal of ambient fintype equal the sum of cardinals of the parts of a partition (set style)-/
example {α : Type*} [decidable_eq α] {x : finset α} (p : finpartition x) :
  ∑ s in p.parts, s.card = x.card :=
begin
  conv_rhs {rw ←p.sup_parts},
  rw [finset.sup_eq_bUnion, finset.card_bUnion p.sup_indep.pairwise_disjoint],
  refl
end

[Antoine Chambert-Loir]

… and using the ongoing PR to convert is_partition to finpartition? ;-)

[Eric Wieser]

Or maximally golfed:

example {α : Type*} [decidable_eq α] {x : finset α} (p : finpartition x) :
  ∑ s in p.parts, s.card = x.card :=
(finset.card_bUnion p.sup_indep.pairwise_disjoint).symm.trans $ congr_arg _ $
  (finset.sup_eq_bUnion _ _).symm.trans p.sup_parts

[Antoine Chambert-Loir]

Shouldn't such a function belong to mathlib?

[Johan Commelin]

I think it should

[Antoine Chambert-Loir]

Actually, it exists… docs#finpartition.sum_card_parts

[Antoine Chambert-Loir]

(I even had forgotten that PR #12459 was the very reason to be able to use it.)

[Antoine Chambert-Loir]

That leaves one of my initial questions still open. Maybe, PR #12459 should not only produce a finpartitionof set αbut also produce one of finset α when possible.

[Eric Wieser]

Can you post the statement you're thinking of here?

[Antoine Chambert-Loir]

Sure. And finally, I could prove it myself., but I did not succeed using finpartition.

import data.setoid.partition
import algebra.big_operators.order

open_locale big_operators classical

section partition

variables {α : Type*}

-- TODO : remove the finiteness assumption on α and put it on s
/-- Given a partition of the ambient finite type,
the cardinal of a set is the sum of the cardinalities of its trace on the parts of the partition -/
lemma setoid.is_partition.card_set_eq_sum_parts {α : Type*} [fintype α] {s : set α} {P : set (set α)}
  (hP : setoid.is_partition P) :
  s.to_finset.card =
    finset.sum P.to_finset (λ (t : set α), (s ∩ t).to_finset.card) :=
begin
  rw ← finset.card_bUnion,
  apply congr_arg,
  { rw ← finset.coe_inj, simp only [set.coe_to_finset, finset.coe_bUnion],
    rw [set.bUnion_eq_Union, ← set.inter_Union, ← set.sUnion_eq_Union],
    rw setoid.is_partition.sUnion_eq_univ hP,
    exact (set.inter_univ s).symm },
  { intros t ht u hu htu,
    simp only [set.mem_to_finset] at ht hu,
    simp only [set.to_finset_disjoint_iff],
    exact set.disjoint_of_subset (set.inter_subset_right s t) (set.inter_subset_right s u)
      (setoid.is_partition.pairwise_disjoint hP ht hu htu) }
end

/-- The cardinality of a finite type is
  the sum of the cardinalities of the parts of any partition -/
lemma setoid.is_partition.card_eq_sum_parts {α : Type*} [fintype α] {P : set (set α)}
  (hP : setoid.is_partition P) :
  fintype.card α =
    finset.sum P.to_finset (λ (t : set α), t.to_finset.card) :=
begin
  change finset.univ.card = _,
  have : (finset.univ : finset α) = (set.univ : set α).to_finset :=
  by rw [← finset.coe_inj, set.to_finset_univ],
  rw this,
  have h : ∀ (t : set α) (ht : t ∈ P.to_finset), t.to_finset.card = (set.univ ∩ t).to_finset.card,
  { intros t ht, apply congr_arg,
    rw set.to_finset_inj, exact (set.univ_inter t).symm,  },
  simp_rw finset.sum_congr rfl h,
  let z := @setoid.is_partition.card_set_eq_sum_parts _ _ (set.univ) P hP,
  simpa only [set.to_finset_univ, set.to_finset_card, fintype.card_of_finset]
    using z,
end

end partition

[Antoine Chambert-Loir]

(By the way, should I PR these two lemmas to somewhere after the definition of docs#setoid.is_partition ?)