Grace/Cumulus/Combinatorics/Functions.g17

Open in Workbench Download source

Imports

Binomial

Declarations

Source

1-- Counting functions: a set of size m has n ^ m maps into a set of size n,2-- by splitting a function on insert(a, A) into its restriction to A and its3-- value at a; words of length m over an alphabet are functions on the4-- numeral m5-- 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.Functions11import Binomial1213theorem functionSpace.finite (A B : Set)14  requires finiteA : Finite(A)15  requires finiteB : Finite(B)16  shows Finite(functionSpace(A, B))17proof18  have product := Finite.product with finiteA, finiteB19  have powers := Finite.powerset with product20  exact Finite.subset with powers, (functionSpace.subset_powerset at A, B)2122theorem functionSpace.empty_domain_count (B : Set)23  shows cardinality(functionSpace(∅, B)) = 124proof25  rw functionSpace.empty_domain26  exact cardinality.singleton at ∅2728theorem functionSpace.empty_codomain_count (A : Set)29  requires nonempty : Nonempty(A)30  shows cardinality(functionSpace(A, ∅)) = 031proof32  have empty := functionSpace.empty_codomain with nonempty33  rw empty34  exact cardinality.empty3536theorem insert.subset_self (A a : Set)37  shows A ⊆ insert(a, A)38proof39  intros x hx40  exact insert.contains with hx4142-- A function on insert(a, A) is its restriction to A together with its43-- value at a.44defgraph functionSplit (A B a : Set) (f ∈ functionSpace(insert(a, A), B)) : functionSpace(A, B) × B :=45  (restrict(f, A), f(a))46proof47  have function := functionSpace.mem_iff.forward with member48  have subset := insert.subset_self at A, a49  have restricted := restrict.domain_function with function, subset50  have value := FunctionBetween.apply_closed with51    function, (insert.self at a, A)52  apply product.pair53  . exact functionSpace.mem_iff.backward with restricted54  . exact value5556theorem functionSplit.injective (A B a : Set)57  shows58    InjectiveBetween(functionSplit(A, B, a), functionSpace(insert(a, A), B), functionSpace(A, B) × B)59proof60  have function := functionSplit.function at A, B, a61  have subset := insert.subset_self at A, a62  apply Injective.of_pointwise with function63  intros f hf g hg same64  have valueF := functionSplit.value at A, B, a, f with hf65  have valueG := functionSplit.value at A, B, a, g with hg66  rw [valueF, valueG] at same67  have parts := orderedPair.injective with same68  have fFunction := functionSpace.mem_iff.forward with hf69  have gFunction := functionSpace.mem_iff.forward with hg70  apply FunctionBetween.ext with fFunction, gFunction71  intros x hx72  have split := insert.membership.forward with hx73  cases split with isA | inA74  . rw isA75    exact parts.right76  . have restrictF := restrict.domain_apply with fFunction, subset, inA77    have restrictG := restrict.domain_apply with gFunction, subset, inA78    rw [← restrictF, ← restrictG, parts.left]79    rfl8081theorem functionSplit.adjoin_member (A B a g b : Set)82  requires fresh : ¬a ∈ A83  requires hg : g ∈ functionSpace(A, B)84  requires hb : b ∈ B85  shows adjoinMap(g, a, b) ∈ functionSpace(insert(a, A), B)86proof87  have gFunction := functionSpace.mem_iff.forward with hg88  have extended := adjoinMap.function at g, A, B, a, b with gFunction, fresh89  have absorb := insert.eq_of_member with hb90  rw absorb at extended91  exact functionSpace.mem_iff.backward with extended9293theorem functionSplit.adjoin_value (A B a g b : Set)94  requires fresh : ¬a ∈ A95  requires hg : g ∈ functionSpace(A, B)96  requires hb : b ∈ B97  shows functionSplit(A, B, a)(adjoinMap(g, a, b)) = (g, b)98proof99  have subset := insert.subset_self at A, a100  have gFunction := functionSpace.mem_iff.forward with hg101  have inSpace := functionSplit.adjoin_member with fresh, hg, hb102  have extended := functionSpace.mem_iff.forward with inSpace103  have value := functionSplit.value at A, B, a, adjoinMap(g, a, b) with inSpace104  have valueA : adjoinMap(g, a, b)(a) = b105    exact FunctionBetween.apply_value with extended, (insert.self at a, A), (adjoinMap.relates_new at g, a, b)106  have restricted : restrict(adjoinMap(g, a, b), A) = g107    have restrictFunction := restrict.domain_function with extended, subset108    apply FunctionBetween.ext with restrictFunction, gFunction109    intros x hx110    have step := restrict.domain_apply with extended, subset, hx111    rw step112    have related := adjoinMap.relates_old at g, a, b, x, g(x) with (FunctionBetween.relates_apply with gFunction, hx)113    exact FunctionBetween.apply_value with extended, (subset with x, hx), related114  rw [value, restricted, valueA]115  rfl116117theorem functionSplit.surjective (A B a : Set)118  requires fresh : ¬a ∈ A119  shows120    SurjectiveBetween(functionSplit(A, B, a), functionSpace(insert(a, A), B), functionSpace(A, B) × B)121proof122  have function := functionSplit.function at A, B, a123  unfold SurjectiveBetween124  refine ⟨function, ?_⟩125  intros p hp126  obtain ⟨bound, g, hg, b, hb, shape⟩ := product.membership.forward with hp127  have inSpace := functionSplit.adjoin_member with fresh, hg, hb128  have target := functionSplit.adjoin_value with fresh, hg, hb129  refine ⟨adjoinMap(g, a, b), inSpace, ?_⟩130  rw [shape, ← target]131  exact FunctionBetween.relates_apply with function, inSpace132133theorem functionSplit.bijective (A B a : Set)134  requires fresh : ¬a ∈ A135  shows136    BijectiveBetween(functionSplit(A, B, a), functionSpace(insert(a, A), B), functionSpace(A, B) × B)137proof138  have injective := functionSplit.injective at A, B, a139  have surjective := functionSplit.surjective at A, B, a with fresh140  exact ⟨injective, surjective⟩141142theorem functionSpace.insert_equipotent (A B a : Set)143  requires fresh : ¬a ∈ A144  shows functionSpace(insert(a, A), B) ≃ functionSpace(A, B) × B145proof146  witness functionSplit(A, B, a)147  exact functionSplit.bijective with fresh148149-- The number of functions from an m-element set to an n-element set.150theorem functionSpace.cardinality (m : Nat)151  shows ∀ A, ∀ B, ∀ n, Nat(n) → HasCardinality(A, m) → HasCardinality(B, n) →152    HasCardinality(functionSpace(A, B), n ^ m)153proof154  induction m155  | zero =>156    intros A B n nNat countedA countedB157    have empty := HasCardinality.empty_of_zero at A with countedA158    rw [empty, functionSpace.empty_domain, pow.zero]159    constructor160    . exact Naturals.constructor.succ at 0 with Naturals.constructor.zero161    . exact Equipotent.singleton_one at ∅162  | k + 1 using ih =>163    intros A B n nNat countedA countedB164    have hk : k + 1 = succ(k) := add.right_one with *165    rw hk at countedA166    obtain ⟨a, member⟩ := HasCardinality.exists_member with countedA167    have rest := HasCardinality.remove at A, a, k with countedA, member168    have fresh : ¬a ∈ A ∖ {a} by simp [difference.membership, singleton.membership]169    have restored := insert.restore with member170    have restCount := ih with A ∖ {a}, B, n, nNat, rest, countedB171    have product := HasCardinality.product with restCount, countedB172    have split := functionSpace.insert_equipotent at A ∖ {a}, B, a with fresh173    rw restored at split174    have powNat := pow.closed at n, k175    have shape : n ^ (k + 1) = mul(n ^ k, n)176      rw [hk, pow.succ]177      ring178    rw shape179    constructor180    . exact HasCardinality.natural with product181    . exact Equipotent.transitive with split, (HasCardinality.equipotent with product)182183theorem functionSpace.count (A B : Set)184  requires finiteA : Finite(A)185  requires finiteB : Finite(B)186  shows cardinality(functionSpace(A, B)) = cardinality(B) ^ cardinality(A)187proof188  have countedA := cardinality.correct with finiteA189  have countedB := cardinality.correct with finiteB190  have natA := cardinality.nat with finiteA191  have natB := cardinality.nat with finiteB192  have all := functionSpace.cardinality at cardinality(A)193  have counted := all with A, B, cardinality(B), natB, countedA, countedB194  exact cardinality.eq_of_has with counted195196theorem functionSpace.self_count (A : Set)197  requires finite : Finite(A)198  shows cardinality(functionSpace(A, A)) = cardinality(A) ^ cardinality(A)199proof200  exact functionSpace.count with finite, finite201202theorem pow.one_base (m : Nat)203  shows 1 ^ m = 1204proof205  induction m206  | zero => exact pow.zero at 1207  | k + 1 using ih =>208    have hk : k + 1 = succ(k) := add.right_one with *209    rw [hk, pow.succ, ih]210    compute211212theorem functionSpace.singleton_codomain_count (A y : Set)213  requires finite : Finite(A)214  shows cardinality(functionSpace(A, {y})) = 1215proof216  have count := functionSpace.count with finite, (Finite.singleton at y)217  rw [count, cardinality.singleton]218  have natA := cardinality.nat with finite219  exact pow.one_base at cardinality(A)220221-- Functions into a two-element set are as many as subsets.222theorem functionSpace.two_count (A : Set)223  requires finite : Finite(A)224  shows cardinality(functionSpace(A, 2)) = 2 ^ cardinality(A)225proof226  have two : Nat(2) by typecheck227  have count := functionSpace.count with finite, (Finite.natural at 2)228  rw [count, cardinality.natural]229  rfl230231theorem functionSpace.two_equipotent_powerset (A : Set)232  requires finite : Finite(A)233  shows functionSpace(A, 2) ≃ 𝒫(A)234proof235  have two : Nat(2) by typecheck236  have finiteSpace := functionSpace.finite with finite, (Finite.natural at 2)237  have finitePower := Finite.powerset with finite238  have same : cardinality(functionSpace(A, 2)) = cardinality(𝒫(A))239    have left := functionSpace.two_count with finite240    have right := powerset.count with finite241    rw [left, right]242    rfl243  exact cardinality.equipotent_of_eq with finiteSpace, finitePower, same244245-- Words of length m over an alphabet are functions on the numeral m.246def words (A : Set, m : Nat) : Set := functionSpace(m, A)247248theorem words.membership (w A : Set, m : Nat)249  shows w ∈ words(A, m) ↔ w : m → A250proof251  simp [words, functionSpace.mem_iff]252253theorem words.finite (A : Set, m : Nat)254  requires finite : Finite(A)255  shows Finite(words(A, m))256proof257  unfold words258  exact functionSpace.finite with (Finite.natural at m), finite259260theorem words.zero (A : Set)261  shows words(A, 0) = {∅}262proof263  unfold words264  have shape := functionSpace.empty_domain at A265  rw nat.zero266  exact shape267268theorem words.count (A : Set, m : Nat)269  requires finite : Finite(A)270  shows cardinality(words(A, m)) = cardinality(A) ^ m271proof272  unfold words273  have count := functionSpace.count with (Finite.natural at m), finite274  rw [count, cardinality.natural]275  rfl276277theorem words.binary_count (m : Nat)278  shows cardinality(words(2, m)) = 2 ^ m279proof280  have two : Nat(2) by typecheck281  have count := words.count at 2, m with (Finite.natural at 2)282  rw [count, cardinality.natural]283  rfl284285theorem words.letter (w A x : Set, m : Nat)286  requires word : w ∈ words(A, m)287  requires position : x ∈ m288  shows w(x) ∈ A289proof290  have function := words.membership.forward with word291  exact FunctionBetween.apply_closed with function, position292