Grace/Cumulus/Combinatorics/Partitions.g17

Open in Workbench Download source

Imports

Permutations

Declarations

Source

1-- Counting by fibres: a finite set is the sum of the sizes of the preimages2-- of a function on it, sums of constant and bounded weights, the3-- generalized pigeonhole principle, and the size of a disjoint union of a4-- finite family5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Combinatorics.Partitions11import Permutations1213-- Preimages of single points.14theorem functionPreimage.point_membership (f A b x : Set)15  shows x ∈ functionPreimage(f, A, {b}) ↔ x ∈ A ∧ f(x) = b16proof17  constructor18  . intro member19    have parts := functionPreimage.membership.forward with member20    have equal := singleton.membership.forward with parts.right21    exact ⟨parts.left, equal⟩22  . intro parts23    apply functionPreimage.membership.backward24    refine ⟨parts.left, ?_⟩25    rw parts.right26    exact singleton.self at b2728theorem functionPreimage.point_finite (f A b : Set)29  requires finite : Finite(A)30  shows Finite(functionPreimage(f, A, {b}))31proof32  exact Finite.subset with finite, (functionPreimage.subset at f, A, {b})3334theorem functionPreimage.point_nonempty (f A B b : Set)35  requires surjective : SurjectiveBetween(f, A, B)36  requires hb : b ∈ B37  shows Nonempty(functionPreimage(f, A, {b}))38proof39  have function := Surjective.function with surjective40  obtain ⟨x, hx, related⟩ := surjective.right with b, hb41  have value := FunctionBetween.apply_value with function, hx, related42  exact ⟨x, functionPreimage.point_membership.backward with ⟨hx, value⟩⟩4344theorem functionPreimage.point_le_one (f A B b : Set)45  requires injective : InjectiveBetween(f, A, B)46  shows cardinality(functionPreimage(f, A, {b})) ≤ 147proof48  have alternatives : Nonempty(functionPreimage(f, A, {b})) ∨ ¬Nonempty(functionPreimage(f, A, {b})) by tauto49  cases alternatives with nonempty | empty50  . obtain ⟨x, hx⟩ := nonempty51    have partsX := functionPreimage.point_membership.forward with hx52    have inside : functionPreimage(f, A, {b}) ⊆ {x}53      intros y hy54      have partsY := functionPreimage.point_membership.forward with hy55      have same : f(y) = f(x)56        rw [partsX.right, partsY.right]57        rfl58      have equal := Injective.apply_cancel with59        injective, partsY.left, partsX.left, same60      rw equal61      exact singleton.self at x62    exact cardinality.le_one_of_subset_singleton with inside63  . have isEmpty : functionPreimage(f, A, {b}) = ∅64      by_contra different65      apply empty66      exact Nonempty.of_ne_empty with different67    rw [isEmpty, cardinality.empty]68    arith6970-- The fibre of the converse over a point is the preimage of that point.71theorem fiber.converse_point (f A B b : Set)72  requires function : f : A → B73  shows fiber(converse(f, A, B), A, b) = functionPreimage(f, A, {b})74proof75  ext x76  constructor77  . intro hx78    have parts := fiber.membership.forward with hx79    have converseParts := converse.membership.forward with parts.right80    obtain ⟨u, hu, y, hy, shape, related⟩ := converseParts.right81    have coordinates := orderedPair.injective with shape82    rw [coordinates.left, coordinates.right]83    have value := FunctionBetween.apply_value with function, hu, related84    exact functionPreimage.point_membership.backward with ⟨hu, value⟩85  . intro hx86    have parts := functionPreimage.point_membership.forward with hx87    have related := FunctionBetween.relates_apply with function, parts.left88    rw parts.right at related89    have inB : b ∈ B90      rw ← parts.right91      exact FunctionBetween.apply_closed with function, parts.left92    have member := converse.relates with parts.left, inB, related93    have inConverse : (b, x) ∈ converse(f, A, B) := member94    exact fiber.membership.backward with ⟨parts.left, inConverse⟩9596defgraph preimageSize (f A B : Set) (b ∈ B) : ℕ := cardinality(functionPreimage(f, A, {b}))97requires finiteA : Finite(A)98proof99  have finite := functionPreimage.point_finite at f, A, b with finiteA100  have natural := cardinality.nat with finite101  exact nat.omega.forward with natural102103-- The converse graph of a function is a copy of its domain.104defgraph converseEntry (f A B : Set) (x ∈ A) : converse(f, A, B) := (f(x), x)105requires function : f : A → B106proof107  have value := FunctionBetween.apply_closed with function, member108  have related := FunctionBetween.relates_apply with function, member109  exact converse.relates with member, value, related110111theorem converseEntry.injective (f A B : Set)112  requires function : f : A → B113  shows InjectiveBetween(converseEntry(f, A, B), A, converse(f, A, B))114proof115  have graph := converseEntry.function at f, A, B with function116  apply Injective.of_pointwise with graph117  intros x hx y hy same118  have valueX := converseEntry.value at f, A, B, x with function, hx119  have valueY := converseEntry.value at f, A, B, y with function, hy120  rw [valueX, valueY] at same121  have coordinates := orderedPair.injective with same122  exact coordinates.right123124theorem converseEntry.surjective (f A B : Set)125  requires function : f : A → B126  shows SurjectiveBetween(converseEntry(f, A, B), A, converse(f, A, B))127proof128  have graph := converseEntry.function at f, A, B with function129  unfold SurjectiveBetween130  refine ⟨graph, ?_⟩131  intros p hp132  have parts := converse.membership.forward with hp133  obtain ⟨x, hx, y, hy, shape, related⟩ := parts.right134  have value := FunctionBetween.apply_value with function, hx, related135  have entry := converseEntry.value at f, A, B, x with function, hx136  refine ⟨x, hx, ?_⟩137  have target : converseEntry(f, A, B)(x) = p138    rw [entry, shape, value]139    rfl140  rw ← target141  exact FunctionBetween.relates_apply with graph, hx142143theorem converseEntry.bijective (f A B : Set)144  requires function : f : A → B145  shows BijectiveBetween(converseEntry(f, A, B), A, converse(f, A, B))146proof147  have injective := converseEntry.injective with function148  have surjective := converseEntry.surjective with function149  exact ⟨injective, surjective⟩150151theorem converse.count (f A B : Set)152  requires function : f : A → B153  requires finite : Finite(A)154  shows cardinality(converse(f, A, B)) = cardinality(A)155proof156  have bijective := converseEntry.bijective with function157  symm158  exact cardinality.bijective with finite, bijective159160theorem converse.finite_of_function (f A B : Set)161  requires function : f : A → B162  requires finite : Finite(A)163  shows Finite(converse(f, A, B))164proof165  have bijective := converseEntry.bijective with function166  exact Finite.of_equipotent with finite, ⟨converseEntry(f, A, B), bijective⟩167168-- A finite set is the sum of the sizes of the preimages of the points of169-- the codomain.170theorem cardinality.sum_of_preimages (f A B : Set)171  requires function : f : A → B172  requires finiteA : Finite(A)173  requires finiteB : Finite(B)174  shows cardinality(A) = natSum(B, preimageSize(f, A, B))175proof176  have inside : converse(f, A, B) ⊆ B × A := converse.relation at f, A, B177  have size : cardinality(B) = cardinality(B) by rfl178  have natB := cardinality.nat with finiteB179  have count := relation.count at converse(f, A, B), B, A, cardinality(B) with180    finiteB, finiteA, size, inside181  have graph := converse.count with function, finiteA182  rw graph at count183  have agree : ∀ b ∈ B, fiberSize(converse(f, A, B), B, A)(b) = preimageSize(f, A, B)(b)184    intros b hb185    have left := fiberSize.value at converse(f, A, B), B, A, b with finiteA, hb186    have right := preimageSize.value at f, A, B, b with finiteA, hb187    have same := fiber.converse_point at f, A, B, b with function188    rw [left, right, same]189    rfl190  rw count191  exact natSum.congr with agree192193-- Sums of constant and of bounded weights.194theorem natSum.constant_of_cardinality (n : Nat)195  shows ∀ V, ∀ w, ∀ c, Nat(c) → HasCardinality(V, n) → (∀ v ∈ V, w(v) = c) →196    natSum(V, w) = n * c197proof198  induction n199  | zero =>200    intros V w c cNat counted agree201    have empty := HasCardinality.empty_of_zero at V with counted202    rw [empty, natSum.empty]203    ring204  | k + 1 using ih =>205    intros V w c cNat counted agree206    have hk : k + 1 = succ(k) := add.right_one with *207    rw hk at counted208    obtain ⟨a, member⟩ := HasCardinality.exists_member with counted209    have rest := HasCardinality.remove at V, a, k with counted, member210    have fresh : ¬a ∈ V ∖ {a} by simp [difference.membership, singleton.membership]211    have restored := insert.restore with member212    have restAgree : ∀ v ∈ V ∖ {a}, w(v) = c213      intros v hv214      exact agree with v, (difference.subset_left at V, {a} with v, hv)215    have restSum := ih with V ∖ {a}, w, c, cNat, rest, restAgree216    have restFinite := Finite.from_cardinality with rest217    have cMember := nat.omega.forward at c with cNat218    have weights : ∀ v ∈ V ∖ {a}, w(v) ∈ ℕ219      intros v hv220      have same := restAgree with v, hv221      rw same222      exact cMember223    have valueA := agree with a, member224    have weight : w(a) ∈ ℕ225      rw valueA226      exact cMember227    have split := natSum.insert at V ∖ {a}, w, a with228      restFinite, weights, weight, fresh229    rw restored at split230    rw [split, restSum, valueA]231    ring232233theorem natSum.constant (V w : Set) (c : Nat)234  requires finite : Finite(V)235  requires agree : ∀ v ∈ V, w(v) = c236  shows natSum(V, w) = cardinality(V) * c237proof238  have counted := cardinality.correct with finite239  have natV := cardinality.nat with finite240  have all := natSum.constant_of_cardinality at cardinality(V)241  exact all with V, w, c, assumption, counted, agree242243theorem natSum.bounded_of_cardinality (n : Nat)244  shows ∀ V, ∀ w, ∀ c, Nat(c) → HasCardinality(V, n) →245    (∀ v ∈ V, w(v) ∈ ℕ ∧ LessEqual(w(v), c)) → natSum(V, w) ≤ n * c246proof247  induction n248  | zero =>249    intros V w c cNat counted bounds250    have empty := HasCardinality.empty_of_zero at V with counted251    rw [empty, natSum.empty]252    have zero : 0 * c = 0 by ring253    rw zero254    arith255  | k + 1 using ih =>256    intros V w c cNat counted bounds257    have hk : k + 1 = succ(k) := add.right_one with *258    rw hk at counted259    obtain ⟨a, member⟩ := HasCardinality.exists_member with counted260    have rest := HasCardinality.remove at V, a, k with counted, member261    have fresh : ¬a ∈ V ∖ {a} by simp [difference.membership, singleton.membership]262    have restored := insert.restore with member263    have restBounds : ∀ v ∈ V ∖ {a}, w(v) ∈ ℕ ∧ LessEqual(w(v), c)264      intros v hv265      exact bounds with v, (difference.subset_left at V, {a} with v, hv)266    have restSum := ih with V ∖ {a}, w, c, cNat, rest, restBounds267    have restFinite := Finite.from_cardinality with rest268    have weights : ∀ v ∈ V ∖ {a}, w(v) ∈ ℕ269      intros v hv270      have parts := restBounds with v, hv271      exact parts.left272    have boundA := bounds with a, member273    have weight := boundA.left274    have weightNat := nat.omega.backward with weight275    have split := natSum.insert at V ∖ {a}, w, a with276      restFinite, weights, weight, fresh277    rw restored at split278    rw split279    have expand : (k + 1) * c = k * c + c by ring280    rw expand281    have sumNat := natSum.natural with restFinite, weights282    have productNat : Nat(k * c) by typecheck283    have valueBound := boundA.right284    arith285286theorem natSum.le_of_bounded (V w : Set) (c : Nat)287  requires finite : Finite(V)288  requires bounds : ∀ v ∈ V, w(v) ∈ ℕ ∧ LessEqual(w(v), c)289  shows natSum(V, w) ≤ cardinality(V) * c290proof291  have counted := cardinality.correct with finite292  have natV := cardinality.nat with finite293  have all := natSum.bounded_of_cardinality at cardinality(V)294  exact all with V, w, c, assumption, counted, bounds295296theorem natSum.lower_of_cardinality (n : Nat)297  shows ∀ V, ∀ w, ∀ c, Nat(c) → HasCardinality(V, n) →298    (∀ v ∈ V, w(v) ∈ ℕ ∧ LessEqual(c, w(v))) → n * c ≤ natSum(V, w)299proof300  induction n301  | zero =>302    intros V w c cNat counted bounds303    have empty := HasCardinality.empty_of_zero at V with counted304    rw [empty, natSum.empty]305    have zero : 0 * c = 0 by ring306    rw zero307    arith308  | k + 1 using ih =>309    intros V w c cNat counted bounds310    have hk : k + 1 = succ(k) := add.right_one with *311    rw hk at counted312    obtain ⟨a, member⟩ := HasCardinality.exists_member with counted313    have rest := HasCardinality.remove at V, a, k with counted, member314    have fresh : ¬a ∈ V ∖ {a} by simp [difference.membership, singleton.membership]315    have restored := insert.restore with member316    have restBounds : ∀ v ∈ V ∖ {a}, w(v) ∈ ℕ ∧ LessEqual(c, w(v))317      intros v hv318      exact bounds with v, (difference.subset_left at V, {a} with v, hv)319    have restSum := ih with V ∖ {a}, w, c, cNat, rest, restBounds320    have restFinite := Finite.from_cardinality with rest321    have weights : ∀ v ∈ V ∖ {a}, w(v) ∈ ℕ322      intros v hv323      have parts := restBounds with v, hv324      exact parts.left325    have boundA := bounds with a, member326    have weight := boundA.left327    have weightNat := nat.omega.backward with weight328    have split := natSum.insert at V ∖ {a}, w, a with329      restFinite, weights, weight, fresh330    rw restored at split331    rw split332    have expand : (k + 1) * c = k * c + c by ring333    rw expand334    have sumNat := natSum.natural with restFinite, weights335    have productNat : Nat(k * c) by typecheck336    have valueBound := boundA.right337    arith338339theorem natSum.ge_of_bounded (V w : Set) (c : Nat)340  requires finite : Finite(V)341  requires bounds : ∀ v ∈ V, w(v) ∈ ℕ ∧ LessEqual(c, w(v))342  shows cardinality(V) * c ≤ natSum(V, w)343proof344  have counted := cardinality.correct with finite345  have natV := cardinality.nat with finite346  have all := natSum.lower_of_cardinality at cardinality(V)347  exact all with V, w, c, assumption, counted, bounds348349-- The generalized pigeonhole principle: more than k · |B| points cannot350-- all land in preimages of size at most k.351theorem pigeonhole.large_preimage (f A B : Set) (k : Nat)352  requires function : f : A → B353  requires finiteA : Finite(A)354  requires finiteB : Finite(B)355  requires more : k * cardinality(B) < cardinality(A)356  shows ∃ b ∈ B, k < cardinality(functionPreimage(f, A, {b}))357proof358  by_contra none359  have bounds : ∀ b ∈ B, preimageSize(f, A, B)(b) ∈ ℕ ∧ LessEqual(preimageSize(f, A, B)(b), k)360    intros b hb361    have value := preimageSize.value at f, A, B, b with finiteA, hb362    have finitePre := functionPreimage.point_finite at f, A, b with finiteA363    have natPre := cardinality.nat with finitePre364    rw value365    constructor366    . exact nat.omega.forward with natPre367    . have notMore : ¬k < cardinality(functionPreimage(f, A, {b}))368        intro h369        apply none370        exact ⟨b, hb, h⟩371      exact LessEqual.of_not_Less with notMore372  have total := natSum.le_of_bounded at B, preimageSize(f, A, B), k with373    finiteB, bounds374  have sum := cardinality.sum_of_preimages with function, finiteA, finiteB375  rw ← sum at total376  have natA := cardinality.nat with finiteA377  have natB := cardinality.nat with finiteB378  have commute : cardinality(B) * k = k * cardinality(B) by ring379  rw commute at total380  have strict := Less.transitive_LessEqual with more, total381  exact Less.irreflexive at k * cardinality(B) with strict382383theorem pigeonhole.small_preimage (f A B : Set) (k : Nat)384  requires function : f : A → B385  requires finiteA : Finite(A)386  requires finiteB : Finite(B)387  requires fewer : cardinality(A) < k * cardinality(B)388  shows ∃ b ∈ B, cardinality(functionPreimage(f, A, {b})) < k389proof390  by_contra none391  have bounds : ∀ b ∈ B, preimageSize(f, A, B)(b) ∈ ℕ ∧ LessEqual(k, preimageSize(f, A, B)(b))392    intros b hb393    have value := preimageSize.value at f, A, B, b with finiteA, hb394    have finitePre := functionPreimage.point_finite at f, A, b with finiteA395    have natPre := cardinality.nat with finitePre396    rw value397    constructor398    . exact nat.omega.forward with natPre399    . have notFewer : ¬cardinality(functionPreimage(f, A, {b})) < k400        intro h401        apply none402        exact ⟨b, hb, h⟩403      exact LessEqual.of_not_Less with notFewer404  have total := natSum.ge_of_bounded at B, preimageSize(f, A, B), k with405    finiteB, bounds406  have sum := cardinality.sum_of_preimages with function, finiteA, finiteB407  rw ← sum at total408  have natA := cardinality.nat with finiteA409  have natB := cardinality.nat with finiteB410  have commute : cardinality(B) * k = k * cardinality(B) by ring411  rw commute at total412  have strict := Less.transitive_LessEqual with fewer, total413  exact Less.irreflexive at cardinality(A) with strict414415-- Disjoint unions of finite families.416predicate PairwiseDisjoint (F : Set) := ∀ S ∈ F, ∀ T ∈ F, S ≠ T → Disjoint(S, T)417418theorem PairwiseDisjoint.subset (F G : Set)419  requires subset : G ⊆ F420  requires disjoint : PairwiseDisjoint(F)421  shows PairwiseDisjoint(G)422proof423  intros S hS T hT different424  exact disjoint with S, (subset with S, hS), T, (subset with T, hT), different425426theorem PairwiseDisjoint.member_union (F S : Set)427  requires disjoint : PairwiseDisjoint(insert(S, F))428  requires fresh : ¬S ∈ F429  shows Disjoint(S, ⋃F)430proof431  apply Disjoint.iff.backward432  intros x hx inUnion433  obtain ⟨T, hT, hxT⟩ := union.membership.forward with inUnion434  have different : S ≠ T435    intro equal436    apply fresh437    rw equal438    exact hT439  have pair := disjoint with S, (insert.self at S, F), T, (insert.contains with440    hT), different441  have free := Disjoint.iff.forward with pair442  exact free with x, hx, hxT443444defgraph sizeMap (F : Set) (S ∈ F) : ℕ := cardinality(S)445requires members : ∀ S ∈ F, Finite(S)446proof447  have finite := members with S, member448  have natural := cardinality.nat with finite449  exact nat.omega.forward with natural450451theorem cardinality.big_union_of_cardinality (n : Nat)452  shows ∀ F, HasCardinality(F, n) → (∀ S ∈ F, Finite(S)) → PairwiseDisjoint(F) →453    cardinality(⋃F) = natSum(F, sizeMap(F))454proof455  induction n456  | zero =>457    intros F counted members disjoint458    have empty := HasCardinality.empty_of_zero at F with counted459    rw [empty, union.empty, natSum.empty]460    exact cardinality.empty461  | k + 1 using ih =>462    intros F counted members disjoint463    have hk : k + 1 = succ(k) := add.right_one with *464    rw hk at counted465    obtain ⟨S, member⟩ := HasCardinality.exists_member with counted466    have rest := HasCardinality.remove at F, S, k with counted, member467    have fresh : ¬S ∈ F ∖ {S} by simp [difference.membership, singleton.membership]468    have restored := insert.restore with member469    have restSubset := difference.subset_left at F, {S}470    have restMembers : ∀ T ∈ F ∖ {S}, Finite(T)471      intros T hT472      exact members with T, (restSubset with T, hT)473    have restDisjoint := PairwiseDisjoint.subset with restSubset, disjoint474    have restCount := ih with F ∖ {S}, rest, restMembers, restDisjoint475    have restFinite := Finite.from_cardinality with rest476    have finiteS := members with S, member477    have finiteUnion := Finite.big_union with restFinite, restMembers478    rw ← restored at disjoint479    have separated := PairwiseDisjoint.member_union with disjoint, fresh480    have split := union.insert at F ∖ {S}, S481    rw restored at split482    have count := cardinality.union_disjoint with483      finiteS, finiteUnion, separated484    have weights : ∀ T ∈ F ∖ {S}, sizeMap(F)(T) ∈ ℕ485      intros T hT486      have value := sizeMap.value at F, T with members, (restSubset with T, hT)487      rw value488      exact nat.omega.forward with (cardinality.nat with (members with T, (restSubset with T, hT)))489    have weight : sizeMap(F)(S) ∈ ℕ490      have value := sizeMap.value at F, S with members, member491      rw value492      exact nat.omega.forward with (cardinality.nat with finiteS)493    have sum := natSum.insert at F ∖ {S}, sizeMap(F), S with494      restFinite, weights, weight, fresh495    rw restored at sum496    have agree : ∀ T ∈ F ∖ {S}, sizeMap(F)(T) = sizeMap(F ∖ {S})(T)497      intros T hT498      have left := sizeMap.value at F, T with members, (restSubset with T, hT)499      have right := sizeMap.value at F ∖ {S}, T with restMembers, hT500      rw [left, right]501      rfl502    have same := natSum.congr with agree503    have valueS := sizeMap.value at F, S with members, member504    rw [split, count, restCount, sum, same, valueS]505    have natS := cardinality.nat with finiteS506    have restWeights : ∀ T ∈ F ∖ {S}, sizeMap(F ∖ {S})(T) ∈ ℕ507      intros T hT508      have value := sizeMap.value at F ∖ {S}, T with restMembers, hT509      rw value510      exact nat.omega.forward with (cardinality.nat with (restMembers with T, hT))511    have sumNat := natSum.natural at F ∖ {S}, sizeMap(F ∖ {S}) with512      restFinite, restWeights513    exact add.commutative at natSum(F ∖ {S}, sizeMap(F ∖ {S})), cardinality(S) with sumNat, natS514515-- The size of a disjoint union of a finite family of finite sets.516theorem cardinality.big_union_disjoint (F : Set)517  requires finite : Finite(F)518  requires members : ∀ S ∈ F, Finite(S)519  requires disjoint : PairwiseDisjoint(F)520  shows cardinality(⋃F) = natSum(F, sizeMap(F))521proof522  have counted := cardinality.correct with finite523  have natF := cardinality.nat with finite524  have all := cardinality.big_union_of_cardinality at cardinality(F)525  exact all with F, counted, members, disjoint526527theorem cardinality.big_union_constant (F : Set) (c : Nat)528  requires finite : Finite(F)529  requires members : ∀ S ∈ F, Finite(S)530  requires disjoint : PairwiseDisjoint(F)531  requires sizes : ∀ S ∈ F, cardinality(S) = c532  shows cardinality(⋃F) = cardinality(F) * c533proof534  have count := cardinality.big_union_disjoint with finite, members, disjoint535  have agree : ∀ S ∈ F, sizeMap(F)(S) = c536    intros S hS537    have value := sizeMap.value at F, S with members, hS538    rw value539    exact sizes with S, hS540  rw count541  exact natSum.constant with finite, agree542