Grace/Cumulus/Cardinal/DoubleCounting.g17

Open in Workbench Download source

Imports

NaturalSum

Declarations

Source

1-- Double counting: the size of a finite relation is the sum, over the2-- first coordinates, of the sizes of its fibres3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Cardinal.DoubleCounting9import NaturalSum1011def fiber (I D r : Set) : Set := { d ∈ D | (r, d) ∈ I }1213theorem fiber.finite (I D r : Set)14  requires finite : Finite(D)15  shows Finite(fiber(I, D, r))16proof17  have inside : fiber(I, D, r) ⊆ D18    intros d hd19    have parts := fiber.membership.forward with hd20    exact parts.left21  exact Finite.subset with finite, inside2223defgraph fiberSize (I R D : Set) (r ∈ R) : ℕ := cardinality(fiber(I, D, r))24requires finiteD : Finite(D)25proof26  have finite := fiber.finite at I, D, r with finiteD27  have correct := cardinality.correct with finite28  exact nat.omega.forward with correct.left2930-- The row of the relation over a point is a copy of its fibre.31theorem fiber.row (I D a : Set)32  shows I ∩ ({a} × D) = {a} × fiber(I, D, a)33proof34  have self : a ∈ {a} by simp [singleton.membership]35  ext p36  constructor37  . intro hp38    have both := intersection.membership.forward with hp39    obtain ⟨bound, x, hx, d, hd, shape⟩ := product.membership.forward with both.right40    have same := singleton.membership.forward with hx41    rw same at shape42    have inI := both.left43    rw shape at inI44    have member : d ∈ fiber(I, D, a) := fiber.membership.backward with ⟨hd, inI⟩45    rw shape46    exact product.pair with self, member47  . intro hp48    obtain ⟨bound, x, hx, d, hd, shape⟩ := product.membership.forward with hp49    have same := singleton.membership.forward with hx50    rw same at shape51    have parts := fiber.membership.forward with hd52    apply intersection.membership.backward53    rw shape54    exact ⟨parts.right, (product.pair with self, parts.left)⟩5556theorem fiber.restrict (I D R r : Set)57  requires hr : r ∈ R58  shows fiber(I ∩ (R × D), D, r) = fiber(I, D, r)59proof60  ext d61  constructor62  . intro hd63    have parts := fiber.membership.forward with hd64    have both := intersection.membership.forward with parts.right65    exact fiber.membership.backward with ⟨parts.left, both.left⟩66  . intro hd67    have parts := fiber.membership.forward with hd68    apply fiber.membership.backward69    refine ⟨parts.left, ?_⟩70    apply intersection.membership.backward71    exact ⟨parts.right, (product.pair with hr, parts.left)⟩7273-- Splitting a relation at a point of its domain.74theorem relation.split (I R D a : Set)75  requires inside : I ⊆ R × D76  requires ha : a ∈ R77  shows I = (I ∩ ((R ∖ {a}) × D)) ∪ ({a} × fiber(I, D, a))78proof79  rw ← fiber.row80  ext p81  constructor82  . intro hp83    obtain ⟨bound, r, hr, d, hd, shape⟩ := product.membership.forward with (inside with p, hp)84    have split : r = a ∨ r ≠ a by tauto85    cases split with same | different86    . apply union2.right87      apply intersection.membership.backward88      refine ⟨hp, ?_⟩89      rw [shape, same]90      have self : a ∈ {a} by simp [singleton.membership]91      exact product.pair with self, hd92    . apply union2.left93      apply intersection.membership.backward94      refine ⟨hp, ?_⟩95      rw shape96      have kept : r ∈ R ∖ {a} := difference.singleton_membership.backward with ⟨hr, different⟩97      exact product.pair with kept, hd98  . intro hp99    have split := union2.membership.forward with hp100    cases split with left | right101    . have both := intersection.membership.forward with left102      exact both.left103    . have both := intersection.membership.forward with right104      exact both.left105106theorem relation.split_disjoint (I R D a : Set)107  shows Disjoint(I ∩ ((R ∖ {a}) × D), {a} × fiber(I, D, a))108proof109  apply Disjoint.iff.backward110  intros p hp hp2111  have both := intersection.membership.forward with hp112  obtain ⟨bound, r, hr, d, hd, shape⟩ := product.membership.forward with both.right113  rw shape at hp2114  have coordinates := product.pair_membership.forward with hp2115  have same := singleton.membership.forward with coordinates.left116  have parts := difference.singleton_membership.forward with hr117  exact parts.right with same118119-- The count.120theorem relation.count (I R D : Set, n : Nat)121  requires finiteR : Finite(R)122  requires finiteD : Finite(D)123  requires size : cardinality(R) = n124  requires inside : I ⊆ R × D125  shows cardinality(I) = natSum(R, fiberSize(I, R, D))126proof127  induction n generalizing R I128  | zero =>129    intros I R finiteR size inside130    have has := cardinality.correct with finiteR131    rw size at has132    have empty := HasCardinality.empty_of_zero at R with has133    have emptyI : I = ∅134      apply Subset.antisymmetric135      . intros p hp136        have bound := inside with p, hp137        rw [empty, product.left_empty] at bound138        exact bound139      . exact empty.subset at I140    rw [emptyI, empty, natSum.empty]141    rw ← nat.zero142    exact cardinality.natural at 0143  | succ(k) using ih =>144    intros I R finiteR size inside145    have has := cardinality.correct with finiteR146    rw size at has147    obtain ⟨a, ha⟩ := HasCardinality.exists_member with has148    have removed := cardinality.remove with finiteR, ha149    rw size at removed150    have smaller := Naturals.injective.succ with removed151    have restSize : cardinality(R ∖ {a}) = k152      symm153      exact smaller154    have restFinite := Finite.subset with finiteR, (difference.subset_left at R, {a})155    have restInside : I ∩ ((R ∖ {a}) × D) ⊆ (R ∖ {a}) × D := intersection.subset_right at I, (R ∖ {a}) × D156    have restCount := ih with I ∩ ((R ∖ {a}) × D), R ∖ {a}, restFinite, restSize, restInside157    have graph := fiberSize.function at I, R, D with finiteD158    have restGraph := fiberSize.function at I ∩ ((R ∖ {a}) × D), R ∖ {a}, D with finiteD159    have agree : ∀ r ∈ R ∖ {a}, fiberSize(I ∩ ((R ∖ {a}) × D), R ∖ {a}, D)(r) = fiberSize(I, R, D)(r)160      intros r hr161      have hrR := difference.subset_left at R, {a} with r, hr162      have valueRest := fiberSize.value at I ∩ ((R ∖ {a}) × D), R ∖ {a}, D, r with finiteD163      have value := fiberSize.value at I, R, D, r with finiteD164      have restricted := fiber.restrict at I, D, R ∖ {a}, r with hr165      rw [valueRest, value, restricted]166      rfl167    have sameSum := natSum.congr with agree168    have weights : ∀ r ∈ R ∖ {a}, fiberSize(I, R, D)(r) ∈ ℕ169      intros r hr170      have hrR := difference.subset_left at R, {a} with r, hr171      exact FunctionBetween.apply_closed with graph, hrR172    have weightA := FunctionBetween.apply_closed with graph, ha173    have fresh : ¬a ∈ R ∖ {a}174      intro inside2175      have parts := difference.singleton_membership.forward with inside2176      apply parts.right177      rfl178    have inserted := natSum.insert with restFinite, weights, weightA, fresh179    have restore := insert.restore with ha180    rw restore at inserted181    have split := relation.split with inside, ha182    have disjoint := relation.split_disjoint at I, R, D, a183    have finiteI := Finite.subset with (Finite.product with finiteR, finiteD), inside184    have finiteRest := Finite.subset with finiteI, (intersection.subset_left at I, (R ∖ {a}) × D)185    have finiteRow := Finite.product with (Finite.singleton at a), (fiber.finite at I, D, a with finiteD)186    have added := cardinality.union_disjoint with finiteRest, finiteRow, disjoint187    have rowCount := cardinality.singleton_product at a, fiber(I, D, a) with (fiber.finite at I, D, a with finiteD)188    have valueA := fiberSize.value at I, R, D, a with finiteD189    have leftCount : cardinality(I) = cardinality((I ∩ ((R ∖ {a}) × D)) ∪ ({a} × fiber(I, D, a)))190      rw ← split191      rfl192    rw [leftCount, added, rowCount, restCount, sameSum, inserted, valueA]193    rfl194