Grace/Cumulus/Cardinal/Enumeration.g17

Open in Workbench Download source

Imports

Set.Indicator · ListSupport

Declarations

Source

1-- Counting is independent of a finite enumeration.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Cardinal.Enumeration8import Set.Indicator9import ListSupport1011predicate DistinctValues (f n : Set) :=12  ∀ i ∈ n, ∀ j ∈ n, f[i] = f[j] → i = j1314predicate Occurs (f n x : Set) := ∃ i ∈ n, f[i] = x1516theorem membership.into_successor (x : Set, n : Nat)17  requires before : x ∈ n18  shows x ∈ succ(n)19proof20  simp2122theorem DistinctValues.prefix (f : Set, n : Nat)23  requires distinct : DistinctValues(f, succ(n))24  shows DistinctValues(f, n)25proof26  intros i hi j hj same27  have iNext := membership.into_successor with hi28  have jNext := membership.into_successor with hj29  exact distinct with i, iNext, j, jNext, same3031theorem DistinctValues.last_fresh (f : Set, n : Nat)32  requires distinct : DistinctValues(f, succ(n))33  shows ∀ i ∈ n, f[i] ≠ f[n]34proof35  intros i hi same36  have iNext := membership.into_successor with hi37  have nNext := membership.self_successor at n38  have equal := distinct with i, iNext, n, nNext, same39  rw equal at hi40  exact membership.irreflexive with hi4142theorem countMembers.absent (A f : Set, n : Nat)43  shows (∀ i ∈ n, ¬(f[i] ∈ A)) → countMembers(A, f, n) = 044proof45  induction n46  | zero =>47    intro absent48    rw countMembers49    rfl50  | succ(k) using ih =>51    intro absent52    have prefix : ∀ i ∈ k, ¬(f[i] ∈ A) by simp53    have last := absent with k, membership.self_successor at k with assumption54    have previous := ih with prefix55    have value := indicator.absent with last56    rw [countMembers, previous, value]57    simp [add]5859theorem countMembers.singleton_one (f x : Set, n : Nat)60  shows DistinctValues(f, n) → Occurs(f, n, x) → countMembers({x}, f, n) = 161proof62  induction n63  | zero =>64    intros distinct occurs65    rcases occurs with ⟨i, impossible, same⟩66    exfalso67    simp [nat.zero, set.empty]68  | succ(k) using ih =>69    intros distinct occurs70    have alternatives : f[k] = x ∨ f[k] ≠ x by tauto71    cases alternatives with last | other72    . have fresh := DistinctValues.last_fresh at f, k with assumption, distinct73      have absent : ∀ i ∈ k, ¬(f[i] ∈ {x}) by simp74      have previous := countMembers.absent with assumption, absent75      have member := singleton.membership.backward with last76      have value := indicator.member with member77      rw [countMembers, previous, value]78      simp [add]79    . obtain ⟨position, before, equal⟩ := Occurs.forward at f, succ(k), x with occurs80      have shape := membership.successor_forward{n := k} with before81      have earlier : position ∈ k by simp82      have prefix := DistinctValues.prefix with assumption, distinct83      have occurrence : Occurs(f, k, x)84        unfold Occurs85        refine ⟨position, earlier, equal⟩86      have previous := ih with prefix, occurrence87      have absent : ¬(f[k] ∈ {x}) by simp88      have value := indicator.absent with absent89      rw [countMembers, previous, value]90      simp [add.right_unit]9192-- The weighted equality matrix is symmetric. Its row sum selects a single93-- occurrence, so its two iterated sums count the same subset in either order.9495def matchWeight (A x y : Set) : Set := mul(indicator(A, x), indicator({x}, y))9697theorem matchWeight.symmetric (A x y : Set)98  shows matchWeight(A, x, y) = matchWeight(A, y, x)99proof100  have alternatives : x = y ∨ x ≠ y by tauto101  cases alternatives with same | different102  . rw same103    rfl104  . have xy : ¬(y ∈ {x}) by simp105    have yx : ¬(x ∈ {y}) by simp106    have leftZero := indicator.absent with xy107    have rightZero := indicator.absent with yx108    simp [matchWeight, leftZero, rightZero, mul.right_zero]109110def matchRow (A f x : Set, n : Nat) → Set111  | A, f, x, zero => 0112  | A, f, x, succ(k) => add(matchRow(A, f, x, k), matchWeight(A, x, f[k]))113114def matchTotal (A f g : Set, n m : Nat) → Set115  | A, f, g, n, zero => 0116  | A, f, g, n, succ(k) => add(matchTotal(A, f, g, n, k), matchRow(A, f, g[k], n))117  descends m118119theorem matchWeight.natural (A x y : Set)120  shows Nat(matchWeight(A, x, y))121proof122  unfold matchWeight123  typecheck124125theorem matchRow.natural (A f x : Set, n : Nat)126  shows Nat(matchRow(A, f, x, n))127proof128  induction n129  | zero =>130    rw matchRow131    typecheck132  | succ(k) using ih =>133    rw matchRow134    typecheck135136theorem matchTotal.natural (A f g : Set, n m : Nat)137  shows Nat(matchTotal(A, f, g, n, m))138proof139  induction m140  | zero =>141    rw matchTotal142    typecheck143  | succ(k) using ih =>144    rw matchTotal145    have value := matchRow.natural at A, f, g[k], n with assumption146    typecheck147148theorem matchRow.factor (A f x : Set, n : Nat)149  shows matchRow(A, f, x, n) = mul(indicator(A, x), countMembers({x}, f, n))150proof151  induction n152  | zero =>153    rw [matchRow, countMembers]154    simp [mul.right_zero]155  | succ(k) using ih =>156    rw [matchRow, countMembers, ih]157    unfold matchWeight158    have b := countMembers.natural at {x}, f, k with assumption159    ring160161theorem matchTotal.empty_left (A f g : Set, m : Nat)162  shows matchTotal(A, f, g, 0, m) = 0163proof164  induction m165  | zero =>166    rw matchTotal167    rfl168  | succ(k) using ih =>169    rw [matchTotal, matchRow, ih]170    simp [add]171172theorem matchTotal.extend_left (A f g : Set, n m : Nat)173  shows matchTotal(A, f, g, succ(n), m) =174    add(matchTotal(A, f, g, n, m), matchRow(A, g, f[n], m))175proof176  induction m177  | zero =>178    simp [matchTotal, matchRow, add]179  | succ(k) using ih =>180    rw [matchTotal, matchTotal, matchRow, matchRow, ih]181    have symmetric := matchWeight.symmetric at A, g[k], f[n]182    rw symmetric183    have a := matchTotal.natural at A, f, g, n, k with *184    have b := matchRow.natural at A, g, f[n], k with assumption185    have c := matchRow.natural at A, f, g[k], n with assumption186    have d := matchWeight.natural at A, f[n], g[k]187    exact add.four_shuffle with a, b, c, d188189theorem matchTotal.transpose (A f g : Set, m n : Nat)190  shows matchTotal(A, f, g, n, m) = matchTotal(A, g, f, m, n)191proof192  induction n193  | zero =>194    rw [matchTotal.empty_left, matchTotal]195    rfl196  | succ(k) using ih =>197    rw [matchTotal.extend_left, matchTotal, ih]198    rfl199200theorem matchTotal.count (A f g : Set, n m : Nat)201  requires distinct : DistinctValues(f, n)202  shows (∀ j ∈ m, Occurs(f, n, g[j])) →203    matchTotal(A, f, g, n, m) = countMembers(A, g, m)204proof205  induction m206  | zero =>207    intro covered208    simp [matchTotal, countMembers]209  | succ(k) using ih =>210    intro covered211    have prefix : ∀ j ∈ k, Occurs(f, n, g[j]) by simp212    have last := covered with k, membership.self_successor at k with assumption213    have singletonCount := countMembers.singleton_one with assumption, distinct, last214    have factored := matchRow.factor at A, f, g[k], n with assumption215    rw singletonCount at factored216    have previous := ih with prefix217    rw [matchTotal, countMembers, previous, factored]218    simp [mul.right_unit]219220theorem countMembers.same_entries (A f g : Set, n m : Nat)221  requires distinctF : DistinctValues(f, n)222  requires distinctG : DistinctValues(g, m)223  requires coveredF : ∀ i ∈ n, Occurs(g, m, f[i])224  requires coveredG : ∀ j ∈ m, Occurs(f, n, g[j])225  shows countMembers(A, f, n) = countMembers(A, g, m)226proof227  have left := Enumeration.matchTotal.count at A, g, f, m, n with *228  have right := Enumeration.matchTotal.count at A, f, g, n, m with *229  have transpose := Enumeration.matchTotal.transpose at A, f, g, m, n with *230  rw [← left, ← right]231  symm232  exact transpose233234theorem Injective.distinct_values (f X V : Set)235  requires injective : InjectiveBetween(f, X, V)236  shows DistinctValues(f, X)237proof238  rcases injective with ⟨fn, unique⟩239  intros i hi j hj equal240  have value := FunctionBetween.apply_closed with fn, hi241  have left := FunctionBetween.relates_apply with fn, hi242  have right := FunctionBetween.relates_apply with fn, hj243  rw ← equal at right244  exact unique with i, hi, j, hj, f[i], value, left, right245246theorem Surjective.occurs (f X V x : Set)247  requires surjective : SurjectiveBetween(f, X, V)248  requires member : x ∈ V249  shows Occurs(f, X, x)250proof251  rcases surjective with ⟨fn, onto⟩252  obtain ⟨i, hi, related⟩ := onto with x, member253  have equal := FunctionBetween.apply_value with fn, hi, related254  unfold Occurs255  refine ⟨i, hi, equal⟩256257theorem countMembers.reindex (A V f g : Set, n m : Nat)258  requires enumerationF : BijectiveBetween(f, n, V)259  requires enumerationG : BijectiveBetween(g, m, V)260  shows countMembers(A, f, n) = countMembers(A, g, m)261proof262  have injF := Bijective.injective with enumerationF263  have injG := Bijective.injective with enumerationG264  have surjF := Bijective.surjective with enumerationF265  have surjG := Bijective.surjective with enumerationG266  have fnF := Injective.function with injF267  have fnG := Injective.function with injG268  have distinctF := Injective.distinct_values with injF269  have distinctG := Injective.distinct_values with injG270  have coveredF : ∀ i ∈ n, Occurs(g, m, f[i])271    intros i hi272    have value := FunctionBetween.apply_closed with fnF, hi273    exact Surjective.occurs with surjG, value274  have coveredG : ∀ j ∈ m, Occurs(f, n, g[j])275    intros j hj276    have value := FunctionBetween.apply_closed with fnG, hj277    exact Surjective.occurs with surjF, value278  exact countMembers.same_entries with distinctF, distinctG, coveredF, coveredG279280theorem countMembers.all (A f : Set, n : Nat)281  shows (∀ i ∈ n, f[i] ∈ A) → countMembers(A, f, n) = n282proof283  induction n284  | zero =>285    intro covered286    rw countMembers287    rfl288  | succ(k) using ih =>289    intro covered290    have prefix : ∀ i ∈ k, f[i] ∈ A by simp291    have last := covered with k, membership.self_successor at k with assumption292    have value := indicator.member with last293    have previous := ih with prefix294    rw [countMembers, previous, value]295    exact add.right_one with assumption296297theorem Bijective.natural_domain_unique (V f g : Set, n m : Nat)298  requires enumerationF : BijectiveBetween(f, n, V)299  requires enumerationG : BijectiveBetween(g, m, V)300  shows n = m301proof302  have injF := Bijective.injective with enumerationF303  have injG := Bijective.injective with enumerationG304  have fnF := Injective.function with injF305  have fnG := Injective.function with injG306  have coveredF : ∀ i ∈ n, f[i] ∈ V307    intros i hi308    exact FunctionBetween.apply_closed with fnF, hi309  have coveredG : ∀ j ∈ m, g[j] ∈ V310    intros j hj311    exact FunctionBetween.apply_closed with fnG, hj312  have countF := countMembers.all with coveredF313  have countG := countMembers.all with coveredG314  have equal := countMembers.reindex at V, V, f, g, n, m with *315  rwa [countF, countG] at equal316317theorem HasCardinality.unique (V n m : Set)318  requires first : HasCardinality(V, n)319  requires second : HasCardinality(V, m)320  shows n = m321proof322  rcases first with ⟨naturalN, f, forwardF⟩323  rcases second with ⟨naturalM, g, forwardG⟩324  have inverseF := converse.bijective with forwardF325  have inverseG := converse.bijective with forwardG326  exact Bijective.natural_domain_unique with naturalN, naturalM, inverseF, inverseG327328theorem Bijective.values (f X V : Set)329  requires enumeration : BijectiveBetween(f, X, V)330  shows ∀ i ∈ X, f[i] ∈ V331proof332  have injective := Bijective.injective with enumeration333  have fn := Injective.function with injective334  intros i hi335  exact FunctionBetween.apply_closed with fn, hi336337-- Finite cardinality has a canonical value because its witness is unique.338-- The correctness law requires finiteness.339defunique cardinality (A : Set) (n ∈ ℕ) := HasCardinality(A, n)340requires finite : Finite(A)341proof342  rcases finite with ⟨n, natural, equivalent⟩343  witness n344  constructor345  . exact nat.omega.forward at n with natural346  . unfold HasCardinality347    refine ⟨natural, equivalent⟩348349uniqueness350  intros n nMember first m mMember second351  exact HasCardinality.unique with first, second352353theorem cardinality.correct (A : Set)354  requires finite : Finite(A)355  shows HasCardinality(A, cardinality(A))356proof357  simp [cardinality.selected]358359theorem cardinality.eq_of_has (A n : Set)360  requires given : HasCardinality(A, n)361  shows cardinality(A) = n362proof363  have finite := Finite.from_cardinality with given364  have correct := cardinality.correct with finite365  exact HasCardinality.unique with correct, given366367theorem cardinality.natural (n : Nat)368  shows cardinality(n) = n369proof370  have own : HasCardinality(n, n)371    unfold HasCardinality372    refine ⟨assumption, Equipotent.reflexive at n⟩373  exact cardinality.eq_of_has with own374375theorem cardinality.singleton (x : Set)376  shows cardinality({x}) = 1377proof378  have one : HasCardinality({x}, 1)379    constructor380    . exact Naturals.constructor.succ at 0 with Naturals.constructor.zero381    . exact Equipotent.singleton_one at x382  exact cardinality.eq_of_has with one383384theorem cardinality.empty385  shows cardinality(∅) = 0386proof387  exact cardinality.eq_of_has with HasCardinality.empty_set388