Grace/Cumulus/Cardinal/NaturalSum.g17

Open in Workbench Download source

Imports

PowersetCount · Product · Set

Declarations

Source

1-- Sums of natural numbers over finite sets, as the size of the set of2-- weighted pairs (v, i) with i below the weight of v, so no enumeration3-- is chosen. Disjoint unions add up, and so does inserting a point.4-- 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.NaturalSum10import PowersetCount11import Product12import Set1314-- Disjoint unions add up.15theorem tags.disjoint_sets16  shows Disjoint({0}, {1})17proof18  apply Disjoint.iff.backward19  intros z hz hz220  have zero := singleton.membership.forward with hz21  have one := singleton.membership.forward with hz222  apply zero.ne_one23  rw [← zero, ← one]24  rfl2526theorem Equipotent.union_of_disjoint (A B : Set)27  requires disjoint : Disjoint(A, B)28  shows (A ⊎ B) ≃ (A ∪ B)29proof30  have left := firstProjection.bijective_singleton at A, 031  have right := firstProjection.bijective_singleton at B, 132  have domains : Disjoint(A × {0}, B × {1}) := product.disjoint_of_right with tags.disjoint_sets33  have joined := Bijective.union_disjoint with left, right, domains, disjoint34  witness firstProjection(A, {0}) ∪ firstProjection(B, {1})35  unfold disjointSum36  exact joined3738theorem cardinality.union_disjoint (A B : Set)39  requires finiteA : Finite(A)40  requires finiteB : Finite(B)41  requires disjoint : Disjoint(A, B)42  shows cardinality(A ∪ B) = cardinality(A) + cardinality(B)43proof44  have hasA := cardinality.correct with finiteA45  have hasB := cardinality.correct with finiteB46  have hasSum := HasCardinality.disjointSum with hasA, hasB47  have finiteSum := Finite.disjointSum with finiteA, finiteB48  obtain ⟨f, bijective⟩ := Equipotent.union_of_disjoint with disjoint49  have same := cardinality.bijective with finiteSum, bijective50  have value := cardinality.eq_of_has with hasSum51  rw [← same, value]52  rfl5354theorem cardinality.singleton_product (a B : Set)55  requires finite : Finite(B)56  shows cardinality({a} × B) = cardinality(B)57proof58  have finiteProduct := Finite.product with (Finite.singleton at a), finite59  exact cardinality.bijective with finiteProduct, (secondProjection.bijective_singleton at a, B)6061-- Weighted pairs and the sum.62def weightedPairs (V w : Set) : Set := { p ∈ V × ℕ | ∃ v ∈ V, ∃ i ∈ w(v), p = (v, i) }63def natSum (V w : Set) : Set := cardinality(weightedPairs(V, w))6465theorem weightedPairs.empty (w : Set)66  shows weightedPairs(∅, w) = ∅67proof68  ext p69  constructor70  . intro hp71    have parts := weightedPairs.membership.forward with hp72    obtain ⟨v, hv, i, hi, shape⟩ := parts.right73    exfalso74    exact empty.membership with v, hv75  . intro hp76    exfalso77    exact empty.membership with p, hp7879theorem weightedPairs.insert (V w a : Set)80  requires weight : w(a) ∈ ℕ81  shows weightedPairs(insert(a, V), w) = weightedPairs(V, w) ∪ ({a} × w(a))82proof83  have weightNat := nat.omega.backward with weight84  have self : a ∈ {a} by simp [singleton.membership]85  have aInserted : a ∈ insert(a, V)86    apply insert.membership.backward87    left88    rfl89  ext p90  constructor91  . intro hp92    have parts := weightedPairs.membership.forward with hp93    obtain ⟨v, hv, i, hi, shape⟩ := parts.right94    have bound := parts.left95    rw shape at bound96    have coordinates := product.pair_membership.forward with bound97    have split := insert.membership.forward with hv98    cases split with isA | inV99    . apply union2.right100      rw isA at hi101      rw [shape, isA]102      exact product.pair with self, hi103    . apply union2.left104      apply weightedPairs.membership.backward105      have bound2 : p ∈ V × ℕ106        rw shape107        exact product.pair with inV, coordinates.right108      refine ⟨bound2, v, inV, i, hi, shape⟩109  . intro hp110    have split := union2.membership.forward with hp111    cases split with inOld | inNew112    . have parts := weightedPairs.membership.forward with inOld113      obtain ⟨v, hv, i, hi, shape⟩ := parts.right114      have bound := parts.left115      rw shape at bound116      have coordinates := product.pair_membership.forward with bound117      have hvIns : v ∈ insert(a, V)118        apply insert.membership.backward119        right120        exact hv121      apply weightedPairs.membership.backward122      have bound2 : p ∈ insert(a, V) × ℕ123        rw shape124        exact product.pair with hvIns, coordinates.right125      refine ⟨bound2, v, hvIns, i, hi, shape⟩126    . obtain ⟨bound, x, hx, i, hi, shape⟩ := product.membership.forward with inNew127      have sameX := singleton.membership.forward with hx128      rw sameX at shape129      have naturals := natural.member_natural with weightNat130      have iNat := naturals with i, hi131      have hiN : i ∈ ℕ := nat.omega.forward with iNat132      apply weightedPairs.membership.backward133      have bound2 : p ∈ insert(a, V) × ℕ134        rw shape135        exact product.pair with aInserted, hiN136      refine ⟨bound2, a, aInserted, i, hi, shape⟩137138-- The pairs over a point: a copy of the weight.139theorem weightedPairs.point_count (w a : Set)140  requires weight : w(a) ∈ ℕ141  shows cardinality({a} × w(a)) = w(a)142proof143  have weightNat := nat.omega.backward with weight144  have finite := Finite.natural at w(a)145  have same := cardinality.singleton_product at a, w(a) with finite146  rw same147  exact cardinality.natural148149theorem weightedPairs.disjoint_point (V w a : Set)150  requires fresh : ¬a ∈ V151  shows Disjoint(weightedPairs(V, w), {a} × w(a))152proof153  apply Disjoint.iff.backward154  intros p hp hp2155  have parts := weightedPairs.membership.forward with hp156  obtain ⟨v, hv, i, hi, shape⟩ := parts.right157  rw shape at hp2158  have coordinates := product.pair_membership.forward with hp2159  have same := singleton.membership.forward with coordinates.left160  apply fresh161  rwa ← same162163-- Finiteness, by induction on the size of V.164theorem weightedPairs.finite (V w : Set, n : Nat)165  requires finite : Finite(V)166  requires size : cardinality(V) = n167  requires weights : ∀ v ∈ V, w(v) ∈ ℕ168  shows Finite(weightedPairs(V, w))169proof170  induction n generalizing V171  | zero =>172    intros V finite size weights173    have has := cardinality.correct with finite174    rw size at has175    have empty := HasCardinality.empty_of_zero at V with has176    rw [empty, weightedPairs.empty]177    exact Finite.empty178  | succ(k) using ih =>179    intros V finite size weights180    have has := cardinality.correct with finite181    rw size at has182    obtain ⟨a, ha⟩ := HasCardinality.exists_member with has183    have removed := cardinality.remove with finite, ha184    rw size at removed185    have smaller := Naturals.injective.succ with removed186    have restFinite := Finite.subset with finite, (difference.subset_left at V, {a})187    have restWeights : ∀ v ∈ V ∖ {a}, w(v) ∈ ℕ188      intros v hv189      have parts := difference.singleton_membership.forward with hv190      exact weights with v, parts.left191    have restSize : cardinality(V ∖ {a}) = k192      symm193      exact smaller194    have rest := ih with V ∖ {a}, restFinite, restSize, restWeights195    have restore := insert.restore with ha196    have weight := weights with a, ha197    have weightNat := nat.omega.backward with weight198    have split := weightedPairs.insert at V ∖ {a}, w, a with weight199    rw ← restore200    rw split201    apply Finite.union with rest202    exact Finite.product with (Finite.singleton at a), (Finite.natural at w(a))203204-- The sum laws.205theorem natSum.empty (w : Set)206  shows natSum(∅, w) = 0207proof208  unfold natSum209  rw [weightedPairs.empty, ← nat.zero]210  exact cardinality.natural211212theorem natSum.insert (V w a : Set)213  requires finite : Finite(V)214  requires weights : ∀ v ∈ V, w(v) ∈ ℕ215  requires weight : w(a) ∈ ℕ216  requires fresh : ¬a ∈ V217  shows natSum(insert(a, V), w) = natSum(V, w) + w(a)218proof219  have weightNat := nat.omega.backward with weight220  have split := weightedPairs.insert at V, w, a with weight221  have size : cardinality(V) = cardinality(V) by rfl222  have correct := cardinality.correct with finite223  have cardNat := correct.left224  have pairsFinite := weightedPairs.finite with finite, size, weights225  have pointFinite := Finite.product with (Finite.singleton at a), (Finite.natural at w(a))226  have disjoint := weightedPairs.disjoint_point at V, w, a with fresh227  have count := weightedPairs.point_count with weight228  have added := cardinality.union_disjoint with pairsFinite, pointFinite, disjoint229  rw count at added230  unfold natSum231  rw split232  exact added233234theorem natSum.natural (V w : Set)235  requires finite : Finite(V)236  requires weights : ∀ v ∈ V, w(v) ∈ ℕ237  shows Nat(natSum(V, w))238proof239  have size : cardinality(V) = cardinality(V) by rfl240  have correct := cardinality.correct with finite241  have cardNat := correct.left242  have pairsFinite := weightedPairs.finite with finite, size, weights243  have counted := cardinality.correct with pairsFinite244  unfold natSum245  exact counted.left246247-- Equal weights give equal sums.248theorem natSum.congr (V w v : Set)249  requires agree : ∀ x ∈ V, w(x) = v(x)250  shows natSum(V, w) = natSum(V, v)251proof252  have same : weightedPairs(V, w) = weightedPairs(V, v)253    ext p254    constructor255    . intro hp256      have parts := weightedPairs.membership.forward with hp257      obtain ⟨x, hx, i, hi, shape⟩ := parts.right258      have equal := agree with x, hx259      rw equal at hi260      exact weightedPairs.membership.backward with ⟨parts.left, x, hx, i, hi, shape⟩261    . intro hp262      have parts := weightedPairs.membership.forward with hp263      obtain ⟨x, hx, i, hi, shape⟩ := parts.right264      have equal := agree with x, hx265      rw ← equal at hi266      exact weightedPairs.membership.backward with ⟨parts.left, x, hx, i, hi, shape⟩267  unfold natSum268  rw same269270-- Sums of pointwise sums.271theorem natSum.add_pointwise_of_size (w u t : Set, n : Nat)272  shows ∀ V, Finite(V) → cardinality(V) = n → (∀ v ∈ V, u(v) ∈ ℕ) → (∀ v ∈ V, t(v) ∈ ℕ) →273    (∀ v ∈ V, w(v) = u(v) + t(v)) → natSum(V, w) = natSum(V, u) + natSum(V, t)274proof275  induction n276  | zero =>277    intros V finite size weightsU weightsT agree278    have has := cardinality.correct with finite279    rw size at has280    have empty := HasCardinality.empty_of_zero at V with has281    rw [empty, natSum.empty, natSum.empty, natSum.empty]282    have zeroNat : Nat(0) by typecheck283    rw add.right_unit284    rfl285  | succ(k) using ih =>286    intros V finite size weightsU weightsT agree287    have has := cardinality.correct with finite288    rw size at has289    obtain ⟨a, ha⟩ := HasCardinality.exists_member with has290    have removed := cardinality.remove with finite, ha291    rw size at removed292    have smaller := Naturals.injective.succ with removed293    have restSize : cardinality(V ∖ {a}) = k294      symm295      exact smaller296    have restFinite := Finite.subset with finite, (difference.subset_left at V, {a})297    have restInside := difference.subset_left at V, {a}298    have restU : ∀ v ∈ V ∖ {a}, u(v) ∈ ℕ299      intros v hv300      exact weightsU with v, (restInside with v, hv)301    have restT : ∀ v ∈ V ∖ {a}, t(v) ∈ ℕ302      intros v hv303      exact weightsT with v, (restInside with v, hv)304    have restAgree : ∀ v ∈ V ∖ {a}, w(v) = u(v) + t(v)305      intros v hv306      exact agree with v, (restInside with v, hv)307    have restW : ∀ v ∈ V ∖ {a}, w(v) ∈ ℕ308      intros v hv309      have equal := restAgree with v, hv310      rw equal311      have uNat := nat.omega.backward with (restU with v, hv)312      have tNat := nat.omega.backward with (restT with v, hv)313      have sumNat : Nat(u(v) + t(v)) by typecheck314      exact nat.omega.forward with sumNat315    have rest := ih with V ∖ {a}, restFinite, restSize, restU, restT, restAgree316    have fresh : ¬a ∈ V ∖ {a}317      intro inside318      have parts := difference.singleton_membership.forward with inside319      apply parts.right320      rfl321    have restore := insert.restore with ha322    have weightU := weightsU with a, ha323    have weightT := weightsT with a, ha324    have weightW : w(a) ∈ ℕ325      have equal := agree with a, ha326      rw equal327      have uNat := nat.omega.backward with weightU328      have tNat := nat.omega.backward with weightT329      have sumNat : Nat(u(a) + t(a)) by typecheck330      exact nat.omega.forward with sumNat331    have insertedW := natSum.insert with restFinite, restW, weightW, fresh332    have insertedU := natSum.insert with restFinite, restU, weightU, fresh333    have insertedT := natSum.insert with restFinite, restT, weightT, fresh334    have equalA := agree with a, ha335    rw ← restore336    rw [insertedW, insertedU, insertedT, rest, equalA]337    have sumU := natSum.natural with restFinite, restU338    have sumT := natSum.natural with restFinite, restT339    have uNat := nat.omega.backward with weightU340    have tNat := nat.omega.backward with weightT341    exact add.four_shuffle at natSum(V ∖ {a}, u), natSum(V ∖ {a}, t), u(a), t(a)342343-- An injection preserves the size of a finite set of inputs.344345346-- The same for a finite set, with no size parameter.347theorem natSum.add_pointwise (V w u t : Set)348  requires finite : Finite(V)349  requires weightsU : ∀ v ∈ V, u(v) ∈ ℕ350  requires weightsT : ∀ v ∈ V, t(v) ∈ ℕ351  requires agree : ∀ v ∈ V, w(v) = u(v) + t(v)352  shows natSum(V, w) = natSum(V, u) + natSum(V, t)353proof354  have correct := cardinality.correct with finite355  have natural := correct.left356  have size : cardinality(V) = cardinality(V) by rfl357  exact natSum.add_pointwise_of_size at w, u, t, cardinality(V)358    with natural, V, finite, size, weightsU, weightsT, agree359360theorem cardinality.injective_image (f A B S : Set)361  requires injective : InjectiveBetween(f, A, B)362  requires subset : S ⊆ A363  requires finite : Finite(S)364  shows cardinality(functionImage(f, S, B)) = cardinality(S)365proof366  have function := Injective.function with injective367  have restricted := restrict.injective with injective, subset368  have corestricted := Injective.corestrict with restricted369  have surjective := functionImage.surjective with (Injective.function with restricted)370  have bijective : BijectiveBetween(restrict(f, S), S, functionImage(restrict(f, S), S, B)) := ⟨corestricted, surjective⟩371  have same := cardinality.bijective with finite, bijective372  have image := functionImage.restrict with function, subset373  rw image at same374  symm375  exact same376