Grace/Cumulus/Cardinal/Combinations.g17

Open in Workbench Download source

Imports

PowersetCount · Dominance · NumberTheory.Binomial

Declarations

Source

1-- A set with n elements has choose(n, k) subsets with k elements: the2-- k + 1 element subsets of insert(x, A) split into those avoiding x and those3-- containing it, and Pascal's rule counts the two halves4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Cardinal.Combinations10import PowersetCount11import Dominance12import NumberTheory.Binomial1314def subsetsOfSize (A k : Set) : Set := { S ∈ 𝒫(A) | HasCardinality(S, k) }1516-- Only the empty set has no elements.17theorem subsetsOfSize.zero (A : Set)18  shows subsetsOfSize(A, 0) = {∅}19proof20  ext S21  constructor22  . intro h23    have parts := subsetsOfSize.membership.forward with h24    have empty := HasCardinality.empty_of_zero with parts.right25    exact singleton.membership.backward with empty26  . intro h27    have equal := singleton.membership.forward with h28    apply subsetsOfSize.membership.backward29    rw equal30    constructor31    . exact powerset.membership_iff.backward with (empty.subset at A)32    . exact HasCardinality.empty_set3334theorem subsetsOfSize.zero_cardinality (A : Set)35  shows HasCardinality(subsetsOfSize(A, 0), 1)36proof37  have same := subsetsOfSize.zero at A38  rw same39  constructor40  . exact Naturals.constructor.succ at 0 with Naturals.constructor.zero41  . exact Equipotent.singleton_one at ∅4243-- The empty set has no nonempty subsets.44theorem subsetsOfSize.empty_succ (j : Nat)45  shows subsetsOfSize(∅, succ(j)) = ∅46proof47  ext S48  constructor49  . intro h50    have parts := subsetsOfSize.membership.forward with h51    obtain ⟨a, member⟩ := HasCardinality.exists_member with parts.right52    have subset := powerset.membership_iff.forward with parts.left53    have inEmpty := subset with a, member54    exfalso55    exact set.empty with inEmpty56  . intro h57    exfalso58    exact set.empty with h5960-- Removing a from a set of size j + 1 containing a leaves a set of size j.61theorem HasCardinality.remove (S a : Set) (j : Nat)62  requires counted : HasCardinality(S, succ(j))63  requires member : a ∈ S64  shows HasCardinality(S ∖ {a}, j)65proof66  have finite := Finite.from_cardinality with counted67  have count := cardinality.eq_of_has with counted68  have removal := cardinality.remove with finite, member69  rw count at removal70  have equal := Naturals.injective.succ with removal71  have finiteRest := Finite.subset with finite, (difference.subset_left at S, {a})72  have correct := cardinality.correct with finiteRest73  rwa ← equal at correct7475theorem HasCardinality.insert_fresh (T a : Set) (j : Nat)76  requires counted : HasCardinality(T, j)77  requires fresh : ¬a ∈ T78  shows HasCardinality(insert(a, T), succ(j))79proof80  have finite := Finite.from_cardinality with counted81  have count := cardinality.eq_of_has with counted82  have inserted := cardinality.insert with finite, fresh83  rw count at inserted84  have finiteInsert := Finite.insert at T, a with finite85  have correct := cardinality.correct with finiteInsert86  rwa inserted at correct8788-- Under the powerset split, the j + 1 element subsets of insert(a, B) go89-- exactly onto the j + 1 element subsets of B and the j element subsets of B.90theorem subsetsOfSize.insert_image (B a : Set) (j : Nat)91  requires fresh : ¬a ∈ B92  shows functionImage(powersetSplit(B, a), subsetsOfSize(insert(a, B), succ(j)), 𝒫(B) ⊎ 𝒫(B)) = subsetsOfSize(B, succ(j)) ⊎ subsetsOfSize(B, j)93proof94  have function := powersetSplit.function at B, a95  ext v96  constructor97  . intro hv98    have parts := functionImage.membership.forward with hv99    obtain ⟨S, hS, shape⟩ := parts.right100    have sParts := subsetsOfSize.membership.forward with hS101    have sPower := sParts.left102    have sCount := sParts.right103    have sSubset := powerset.membership_iff.forward with sPower104    have alternatives : a ∈ S ∨ ¬a ∈ S by tauto105    cases alternatives with present | absent106    . have related := powersetSplit.relates_present with sPower, present107      have value := FunctionBetween.apply_value with function, sPower, related108      rw value at shape109      rw shape110      apply disjointSum.right111      apply subsetsOfSize.membership.backward112      constructor113      . exact powerset.membership_iff.backward with (subset.without at B, a, S with sSubset)114      . exact HasCardinality.remove with sCount, present115    . have related := powersetSplit.relates_absent with sPower, absent116      have value := FunctionBetween.apply_value with function, sPower, related117      rw value at shape118      rw shape119      apply disjointSum.left120      apply subsetsOfSize.membership.backward121      constructor122      . exact powerset.membership_iff.backward with (subset.absent at B, a, S with sSubset, absent)123      . exact sCount124  . intro hv125    have split := disjointSum.membership.forward with hv126    cases split with leftCase | rightCase127    . obtain ⟨T, hT, shape⟩ := leftCase128      have tParts := subsetsOfSize.membership.forward with hT129      have tSubset := powerset.membership_iff.forward with tParts.left130      have absent : ¬a ∈ T131        intro h132        apply fresh133        exact tSubset with a, h134      have tPower : T ∈ 𝒫(insert(a, B))135        apply powerset.membership_iff.backward136        intros x hx137        have inB := tSubset with x, hx138        apply insert.membership.backward139        right140        exact inB141      have inSized : T ∈ subsetsOfSize(insert(a, B), succ(j))142        apply subsetsOfSize.membership.backward143        exact ⟨tPower, tParts.right⟩144      have related := powersetSplit.relates_absent with tPower, absent145      have value := FunctionBetween.apply_value with function, tPower, related146      apply functionImage.membership.backward147      constructor148      . rw shape149        exact disjointSum.left with tParts.left150      . witness T151        constructor152        . exact inSized153        . rw [shape, value]154          rfl155    . obtain ⟨T, hT, shape⟩ := rightCase156      have tParts := subsetsOfSize.membership.forward with hT157      have tSubset := powerset.membership_iff.forward with tParts.left158      have absent : ¬a ∈ T159        intro h160        apply fresh161        exact tSubset with a, h162      have counted := HasCardinality.insert_fresh with tParts.right, absent163      have sPower : insert(a, T) ∈ 𝒫(insert(a, B))164        apply powerset.membership_iff.backward165        intros x hx166        have where := insert.membership.forward with hx167        apply insert.membership.backward168        cases where with same | inT169        . left170          exact same171        . right172          exact tSubset with x, inT173      have inSized : insert(a, T) ∈ subsetsOfSize(insert(a, B), succ(j))174        apply subsetsOfSize.membership.backward175        exact ⟨sPower, counted⟩176      have present := insert.self at a, T177      have related := powersetSplit.relates_present with sPower, present178      have value := FunctionBetween.apply_value with function, sPower, related179      have removed := insert.remove_fresh with absent180      rw removed at value181      apply functionImage.membership.backward182      constructor183      . rw shape184        exact disjointSum.right with tParts.left185      . witness insert(a, T)186        constructor187        . exact inSized188        . rw [shape, value]189          rfl190191theorem subsetsOfSize.insert_equipotent (B a : Set) (j : Nat)192  requires fresh : ¬a ∈ B193  shows subsetsOfSize(insert(a, B), succ(j)) ≃ subsetsOfSize(B, succ(j)) ⊎ subsetsOfSize(B, j)194proof195  have injective := powersetSplit.injective at B, a196  have function := powersetSplit.function at B, a197  have subset : subsetsOfSize(insert(a, B), succ(j)) ⊆ 𝒫(insert(a, B))198    intros S hS199    have parts := subsetsOfSize.membership.forward with hS200    exact parts.left201  have restricted := restrict.injective with injective, subset202  have equipotent := Equipotent.image with restricted203  have sameImage := functionImage.restrict with function, subset204  have image := subsetsOfSize.insert_image with fresh205  rwa [sameImage, image] at equipotent206207theorem subsetsOfSize.insert_cardinality (B a : Set) (j p q : Nat)208  requires fresh : ¬a ∈ B209  requires countSucc : HasCardinality(subsetsOfSize(B, succ(j)), p)210  requires countJ : HasCardinality(subsetsOfSize(B, j), q)211  shows HasCardinality(subsetsOfSize(insert(a, B), succ(j)), add(p, q))212proof213  obtain ⟨natural, equivalent⟩ := HasCardinality.disjointSum with countSucc, countJ214  have split := subsetsOfSize.insert_equipotent at B, a, j with fresh215  constructor216  . exact natural217  . exact Equipotent.transitive with split, equivalent218219-- Induction on the size of the set, following Pascal's rule.220theorem subsetsOfSize.cardinality (n : Nat)221  shows ∀ A, HasCardinality(A, n) → ∀ k, Nat(k) → HasCardinality(subsetsOfSize(A, k), choose(n, k))222proof223  induction n224  | zero =>225    intros A counted k kNat226    have countedZero : HasCardinality(A, 0)227      exact counted228    have empty := HasCardinality.empty_of_zero at A with countedZero229    rw empty230    have split := natural.zero_or_successor at k231    cases split with isZero | isSucc232    . rw [isZero, choose.zero_right]233      exact subsetsOfSize.zero_cardinality at ∅234    . obtain ⟨j, jNat, shape⟩ := isSucc235      rw [shape, choose.zero_left]236      have none := subsetsOfSize.empty_succ at j237      rw none238      exact HasCardinality.empty_set239  | succ(m) using ih =>240    intros A counted k kNat241    obtain ⟨a, member⟩ := HasCardinality.exists_member with counted242    have rest := HasCardinality.remove at A, a, m with counted, member243    have fresh : ¬a ∈ A ∖ {a} by simp [difference.membership, singleton.membership]244    have restored := insert.restore with member245    have split := natural.zero_or_successor at k246    cases split with isZero | isSucc247    . rw [isZero, choose.zero_right]248      exact subsetsOfSize.zero_cardinality at A249    . obtain ⟨j, jNat, shape⟩ := isSucc250      rw [shape, choose.succ_succ]251      have sjNat : Nat(succ(j)) by typecheck252      have forRest := ih with A ∖ {a}, rest253      have forSucc := forRest with succ(j), sjNat254      have forJ := forRest with j, jNat255      have combined := subsetsOfSize.insert_cardinality at A ∖ {a}, a, j, choose(m, succ(j)), choose(m, j) with fresh, forSucc, forJ256      rw restored at combined257      have commute : add(choose(m, succ(j)), choose(m, j)) = choose(m, j) + choose(m, succ(j)) by ring258      rw commute at combined259      exact combined260261-- The number of k element subsets of a finite set.262theorem combinations.count (A : Set) (k : Nat)263  requires finite : Finite(A)264  shows cardinality(subsetsOfSize(A, k)) = choose(cardinality(A), k)265proof266  have counted := cardinality.correct with finite267  have natural := HasCardinality.natural with counted268  have all := subsetsOfSize.cardinality at cardinality(A)269  have forA := all with A, counted270  have result := forA with k271  exact cardinality.eq_of_has with result272