Grace/Cumulus/Cardinal/Sum.g17

Open in Workbench Download source

Imports

Finite

Declarations

Source

1-- Tagged disjoint unions and cardinal addition2-- 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.Sum8import Finite910-- Tags are Kuratowski pairs. Distinct von Neumann tags make the two11-- images disjoint even when the original carriers overlap.12def inl (x : Set) : Set := (x, 0)13def inr (y : Set) : Set := (y, 1)14def disjointSum (A B : Set) : Set := (A × {0}) ∪ (B × {1})15notation infixr 55 "⊎" => disjointSum16def sumMap (f g A B C D : Set) : Set := { p ∈ (A ⊎ B) × (C ⊎ D) | (∃ x ∈ A, ∃ y ∈ C, relates(f, x, y) ∧ p = (inl(x) ↦ inl(y))) ∨ (∃ x ∈ B, ∃ y ∈ D, relates(g, x, y) ∧ p = (inr(x) ↦ inr(y))) }17def rightProjection (n : Set) : Set := { p ∈ (0 ⊎ n) × n | ∃ y ∈ n, p = (inr(y) ↦ y) }1819def natSumEquiv (m n : Nat) → Set20  | zero, n => rightProjection(n)21  | succ(m), n => adjoinMap(natSumEquiv(m, n), inl(m), add(m, n))2223theorem disjointSum.left (x A B : Set)24  requires hx : x ∈ A25  shows inl(x) ∈ A ⊎ B26proof27  unfold inl28  unfold disjointSum29  apply union2.left30  apply product.pair31  exact hx32  exact singleton.self3334theorem disjointSum.right (y A B : Set)35  requires hy : y ∈ B36  shows inr(y) ∈ A ⊎ B37proof38  unfold inr39  unfold disjointSum40  apply union2.right41  apply product.pair42  exact hy43  exact singleton.self4445theorem disjointSum.membership (p A B : Set)46  shows p ∈ A ⊎ B ↔ ((∃ x ∈ A, p = inl(x)) ∨ (∃ y ∈ B, p = inr(y)))47proof48  constructor49  intro hp50  simp [disjointSum, union2.membership, product.membership, singleton.membership] at hp51  cases hp with hleft | hright52  simp [product.membership, singleton.membership] at hleft53  rcases hleft with (hbound, witnesses)54  obtain (x, hx) := witnesses55  rcases hx with (hxA, rest)56  obtain ⟨tag, tagZero, pairShape⟩ := rest57  simp [singleton.membership] at tagZero58  left59  witness x60  constructor61  exact hxA62  unfold inl63  cc64  simp [product.membership, singleton.membership] at hright65  rcases hright with ⟨hbound, y, hyB, tagRight, tagOne, pairShapeRight⟩66  simp [singleton.membership] at tagOne67  right68  witness y69  constructor70  exact hyB71  unfold inr72  cc73  intro hp74  cases hp with hleft | hright75  obtain ⟨xBack, hxBackA, pairShapeBack⟩ := hleft76  rw pairShapeBack77  exact disjointSum.left with hxBackA78  obtain ⟨yBack, hyBackB, pairShapeRightBack⟩ := hright79  rw pairShapeRightBack80  exact disjointSum.right with hyBackB8182theorem zero.ne_one83  shows 0 ≠ 184proof85  intro equal86  have member := next.contains at 087  have successorZero := next.natural at 088  rw [← successorZero, ← equal, nat.zero] at member89  simp9091theorem tags.disjoint (x y : Set)92  shows inl(x) ≠ inr(y)93proof94  intro equal95  unfold inl at equal96  unfold inr at equal97  obtain (first, tagsEqual) := orderedPair.injective with equal98  exact zero.ne_one with tagsEqual99100theorem inl.injective (x y : Set)101  requires h : inl(x) = inl(y)102  shows x = y103proof104  simp [inl] at h105  obtain (first, second) := orderedPair.injective with h106  exact first107108theorem inr.injective (x y : Set)109  requires h : inr(x) = inr(y)110  shows x = y111proof112  simp [inr] at h113  obtain (first, second) := orderedPair.injective with h114  exact first115116theorem sumMap.relates_left (f g A B C D x y : Set)117  requires hx : x ∈ A118  requires hy : y ∈ C119  requires hxy : relates(f, x, y)120  shows relates(sumMap(f, g, A, B, C, D), inl(x), inl(y))121proof122  unfold relates123  apply sumMap.membership.backward124  constructor125  apply product.pair126  exact disjointSum.left with hx127  exact disjointSum.left with hy128  left129  refine ⟨x, hx, y, hy, hxy, rfl⟩130131theorem sumMap.relates_right (f g A B C D x y : Set)132  requires hx : x ∈ B133  requires hy : y ∈ D134  requires hxy : relates(g, x, y)135  shows relates(sumMap(f, g, A, B, C, D), inr(x), inr(y))136proof137  unfold relates138  apply sumMap.membership.backward139  constructor140  apply product.pair141  exact disjointSum.right with hx142  exact disjointSum.right with hy143  right144  refine ⟨x, hx, y, hy, hxy, rfl⟩145146theorem sumMap.factors (f g A B C D u v : Set)147  requires h : relates(sumMap(f, g, A, B, C, D), u, v)148  shows (∃ x ∈ A, ∃ y ∈ C, u = inl(x) ∧ v = inl(y) ∧ relates(f, x, y)) ∨ (∃ x ∈ B, ∃ y ∈ D, u = inr(x) ∧ v = inr(y) ∧ relates(g, x, y))149proof150  unfold relates at h151  simp [sumMap.membership] at h152  rcases h with (hProduct, hShape)153  cases hShape with hleft | hright154  obtain ⟨x, hxA, y, hyC, hxy, hPair⟩ := hleft155  obtain (source, target) := orderedPair.injective with hPair156  left157  refine ⟨x, hxA, y, hyC, source, target, hxy⟩158  obtain ⟨xRight, hxB, yRight, hyD, hgxy, hPairRight⟩ := hright159  obtain (sourceRight, targetRight) := orderedPair.injective with hPairRight160  right161  refine ⟨xRight, hxB, yRight, hyD, sourceRight, targetRight, hgxy⟩162163theorem sumMap.relation (f g A B C D : Set)164  shows RelationBetween(sumMap(f, g, A, B, C, D), A ⊎ B, C ⊎ D)165proof166  simp [RelationBetween, Subset]167168theorem sumMap.total (f g A B C D : Set)169  requires hf : f : A → C170  requires hg : g : B → D171  shows TotalBetween(sumMap(f, g, A, B, C, D), A ⊎ B, C ⊎ D)172proof173  intros u hu174  have sourceShape := disjointSum.membership.forward with hu175  cases sourceShape with leftShape | rightShape176  obtain ⟨x, hxA, uShape⟩ := leftShape177  obtain ⟨y, hyC, hxy⟩ := FunctionBetween.exists_value with hf, hxA178  witness inl(y)179  constructor180  exact disjointSum.left with hyC181  rw uShape182  exact sumMap.relates_left with hxA, hyC, hxy183  obtain ⟨xRight, hxB, uShapeRight⟩ := rightShape184  obtain ⟨yRight, hyD, hgxy⟩ := FunctionBetween.exists_value with hg, hxB185  witness inr(yRight)186  constructor187  exact disjointSum.right with hyD188  rw uShapeRight189  exact sumMap.relates_right with hxB, hyD, hgxy190191theorem sumMap.functional (f g A B C D : Set)192  requires hf : f : A → C193  requires hg : g : B → D194  shows Functional(sumMap(f, g, A, B, C, D))195proof196  intros u v huv w huw197  have firstFactor := sumMap.factors with huv198  have secondFactor := sumMap.factors with huw199  cases firstFactor with firstLeft | firstRight200  cases secondFactor with secondLeft | secondRight201  obtain ⟨x1, hx1A, y1, hy1C, uLeft1, vLeft, hfxy1⟩ := firstLeft202  obtain ⟨x2, hx2A, y2, hy2C, uLeft2, wLeft, hfxy2⟩ := secondLeft203  rw uLeft1 at uLeft2204  have sameInput := inl.injective with uLeft2205  rw ← sameInput at hfxy2206  have unique := FunctionBetween.functional with hf, x1, y1, hfxy1, y2, hfxy2207  rw [vLeft, wLeft, unique]208  rfl209  obtain ⟨xLeftCross, hxLeftCrossA, yLeftCross, hyLeftCrossC, uLeftCross, hyLeftCrossLast⟩ := firstLeft210  obtain ⟨xr, hxrB, yr, hyrD, uRight2, hyrLast⟩ := secondRight211  rw uLeftCross at uRight2212  have impossible := tags.disjoint with uRight2213  contradiction214  cases secondFactor with secondLeftAfterRight | secondRightAfterRight215  obtain ⟨xl, hxlA, yl, hylC, uLeftAfterRight, hylLast⟩ := secondLeftAfterRight216  obtain ⟨xr1, hxr1B, yr1, hyr1D, uRight1, hyr1Last⟩ := firstRight217  rw uLeftAfterRight at uRight1218  have impossibleReverse := tags.disjoint with uRight1219  contradiction220  obtain ⟨xr2, hxr2B, yr2, hyr2D, uRight2b, wRight, hgxy2⟩ := secondRightAfterRight221  obtain ⟨xrFirst, hxrFirstB, yrFirst, hyrFirstD, uRightFirst, vRight, hgxyFirst⟩ := firstRight222  rw uRightFirst at uRight2b223  have sameInputRight := inr.injective with uRight2b224  rw ← sameInputRight at hgxy2225  have uniqueRight := FunctionBetween.functional with hg, xrFirst, yrFirst, hgxyFirst, yr2, hgxy2226  rw [vRight, wRight, uniqueRight]227  rfl228229theorem sumMap.function (f g A B C D : Set)230  requires hf : f : A → C231  requires hg : g : B → D232  shows sumMap(f, g, A, B, C, D) : A ⊎ B → C ⊎ D233proof234  constructor235  exact sumMap.relation236  constructor237  exact sumMap.functional with hf, hg238  exact sumMap.total with hf, hg239240theorem sumMap.surjective (f g A B C D : Set)241  requires hf : SurjectiveBetween(f, A, C)242  requires hg : SurjectiveBetween(g, B, D)243  shows SurjectiveBetween(sumMap(f, g, A, B, C, D), A ⊎ B, C ⊎ D)244proof245  constructor246  have fFunction := Surjective.function with hf247  have gFunction := Surjective.function with hg248  exact sumMap.function with fFunction, gFunction249  intros v hv250  have targetShape := disjointSum.membership.forward with hv251  cases targetShape with targetLeft | targetRight252  obtain ⟨y, hyC, vShape⟩ := targetLeft253  rcases hf with (fFunctionAgain, fOnto)254  specialize fOnto with y, hyC255  obtain ⟨x, hxA, hxy⟩ := fOnto256  witness inl(x)257  constructor258  exact disjointSum.left with hxA259  rw vShape260  exact sumMap.relates_left with hxA, hyC, hxy261  obtain ⟨yRight, hyD, vShapeRight⟩ := targetRight262  rcases hg with (gFunctionAgain, gOnto)263  specialize gOnto with yRight, hyD264  obtain ⟨xRight, hxB, hgxy⟩ := gOnto265  witness inr(xRight)266  constructor267  exact disjointSum.right with hxB268  rw vShapeRight269  exact sumMap.relates_right with hxB, hyD, hgxy270271theorem sumMap.injective (f g A B C D : Set)272  requires hf : InjectiveBetween(f, A, C)273  requires hg : InjectiveBetween(g, B, D)274  shows InjectiveBetween(sumMap(f, g, A, B, C, D), A ⊎ B, C ⊎ D)275proof276  constructor277  have fFunction := Injective.function with hf278  have gFunction := Injective.function with hg279  exact sumMap.function with fFunction, gFunction280  intros u hu v hv z hz huz hvz281  have firstFactor := sumMap.factors with huz282  have secondFactor := sumMap.factors with hvz283  cases firstFactor with firstLeft | firstRight284  cases secondFactor with secondLeft | secondRight285  obtain ⟨x1, hx1A, y1, hy1C, uLeft, zLeft1, hfxy1⟩ := firstLeft286  obtain ⟨x2, hx2A, y2, hy2C, vLeft, zLeft2, hfxy2⟩ := secondLeft287  rw zLeft1 at zLeft2288  have sameOutput := inl.injective with zLeft2289  rw ← sameOutput at hfxy2290  have sameInput := Injective.cancel with hf, hx1A, hx2A, hy1C, hfxy1, hfxy2291  rw [uLeft, vLeft, sameInput]292  rfl293  obtain ⟨xLeftCross, hxLeftCrossA, yLeftCross, hyLeftCrossC, uLeftCross, zLeftCross, hfLeftCross⟩ := firstLeft294  obtain ⟨xRightCross, hxRightCrossB, yRightCross, hyRightCrossD, vRightCross, zRightCross, hgRightCross⟩ := secondRight295  rw zLeftCross at zRightCross296  have impossible := tags.disjoint with zRightCross297  contradiction298  cases secondFactor with secondLeftAfterRight | secondRightAfterRight299  obtain ⟨xLeftAfterRight, hxLeftAfterRightA, yLeftAfterRight, hyLeftAfterRightC, vLeftAfterRight, zLeftAfterRight, hfLeftAfterRight⟩ := secondLeftAfterRight300  obtain ⟨xRightFirst, hxRightFirstB, yRightFirst, hyRightFirstD, uRightFirst, zRightFirst, hgRightFirst⟩ := firstRight301  rw zLeftAfterRight at zRightFirst302  have impossibleReverse := tags.disjoint with zRightFirst303  contradiction304  obtain ⟨xRight2, hxRight2B, yRight2, hyRight2D, vRight2, zRight2, hgxy2⟩ := secondRightAfterRight305  obtain ⟨xRight1, hxRight1B, yRight1, hyRight1D, uRight1, zRight1, hgxy1⟩ := firstRight306  rw zRight1 at zRight2307  have sameOutputRight := inr.injective with zRight2308  rw ← sameOutputRight at hgxy2309  have sameInputRight := Injective.cancel with hg, hxRight1B, hxRight2B, hyRight1D, hgxy1, hgxy2310  rw [uRight1, vRight2, sameInputRight]311  rfl312313theorem sumMap.bijective (f g A B C D : Set)314  requires hf : BijectiveBetween(f, A, C)315  requires hg : BijectiveBetween(g, B, D)316  shows BijectiveBetween(sumMap(f, g, A, B, C, D), A ⊎ B, C ⊎ D)317proof318  constructor319  have fInjective := Bijective.injective with hf320  have gInjective := Bijective.injective with hg321  exact sumMap.injective with fInjective, gInjective322  have fSurjective := Bijective.surjective with hf323  have gSurjective := Bijective.surjective with hg324  exact sumMap.surjective with fSurjective, gSurjective325326theorem Equipotent.disjointSum (A B C D : Set)327  requires hAC : Equipotent(A, C)328  requires hBD : Equipotent(B, D)329  shows Equipotent(A ⊎ B, C ⊎ D)330proof331  obtain (f, hf) := hAC332  obtain (g, hg) := hBD333  witness sumMap(f, g, A, B, C, D)334  exact sumMap.bijective with hf, hg335336theorem rightProjection.relates (y n : Set)337  requires hy : y ∈ n338  shows relates(rightProjection(n), inr(y), y)339proof340  unfold relates341  apply rightProjection.membership.backward342  constructor343  apply product.pair344  exact disjointSum.right with hy345  exact hy346  refine ⟨y, hy, rfl⟩347348theorem rightProjection.factors (u v n : Set)349  requires h : relates(rightProjection(n), u, v)350  shows v ∈ n ∧ u = inr(v)351proof352  simp [relates, rightProjection.membership, orderedPair.injective]353354theorem rightProjection.relation (n : Set)355  shows RelationBetween(rightProjection(n), 0 ⊎ n, n)356proof357  simp [RelationBetween, Subset]358359theorem rightProjection.total (n : Set)360  shows TotalBetween(rightProjection(n), 0 ⊎ n, n)361proof362  intros u hu363  have sourceShape := disjointSum.membership.forward with hu364  cases sourceShape with impossibleLeft | rightShape365  obtain ⟨x, hxZero, uLeft⟩ := impossibleLeft366  rw nat.zero at hxZero367  simp368  obtain ⟨y, hyN, uRight⟩ := rightShape369  witness y370  constructor371  exact hyN372  rw uRight373  exact rightProjection.relates with hyN374375theorem rightProjection.functional (n : Set)376  shows Functional(rightProjection(n))377proof378  simp [Functional, rightProjection.factors, inr.injective]379380theorem rightProjection.function (n : Set)381  shows rightProjection(n) : 0 ⊎ n → n382proof383  constructor384  exact rightProjection.relation385  constructor386  exact rightProjection.functional387  exact rightProjection.total at n388389theorem rightProjection.injective (n : Set)390  shows InjectiveBetween(rightProjection(n), 0 ⊎ n, n)391proof392  constructor393  exact rightProjection.function394  intros u hu v hv y hy huy hvy395  obtain (hyN, uShape) := rightProjection.factors with huy396  obtain (hyNAgain, vShape) := rightProjection.factors with hvy397  rw [uShape, vShape]398  rfl399400theorem rightProjection.surjective (n : Set)401  shows SurjectiveBetween(rightProjection(n), 0 ⊎ n, n)402proof403  constructor404  exact rightProjection.function405  intros y hy406  witness inr(y)407  constructor408  exact disjointSum.right with hy409  exact rightProjection.relates with hy410411theorem rightProjection.bijective (n : Set)412  shows BijectiveBetween(rightProjection(n), 0 ⊎ n, n)413proof414  refine ⟨rightProjection.injective at n, rightProjection.surjective at n⟩415416theorem inl.fresh (m n : Nat)417  shows ¬inl(m) ∈ m ⊎ n418proof419  intro member420  have shape := disjointSum.membership.forward with member421  cases shape with leftShape | rightShape422  obtain ⟨x, hxM, tagsEqual⟩ := leftShape423  have same := inl.injective with tagsEqual424  rw ← same at hxM425  have irreflexive := membership.irreflexive with hxM426  contradiction427  obtain ⟨y, hyN, tagsEqualRight⟩ := rightShape428  have disjoint := tags.disjoint with tagsEqualRight429  contradiction430431theorem disjointSum.successor_left (m n : Nat)432  shows succ(m) ⊎ n = insert(inl(m), m ⊎ n)433proof434  ext p435  constructor436  . intro hp437    have shape := disjointSum.membership.forward with hp438    cases shape with leftShape | rightShape439    . obtain (x, hx) := leftShape440      rcases hx with (hxSucc, pairShape)441      have successorShape := membership.successor_set{n := m}.forward with hxSucc442      cases successorShape with oldMember | newest443      . apply insert.contains at p, inl(m), m ⊎ n444        rw pairShape445        exact disjointSum.left with oldMember446      . rw [pairShape, newest]447        exact insert.self448    . obtain (y, hy) := rightShape449      rcases hy with (hyN, pairShape)450      apply insert.contains451      rw pairShape452      exact disjointSum.right with hyN453  . intro hp454    have shape := insert.membership.forward with hp455    cases shape with newest | oldMember456    . rw newest457      simp [disjointSum.membership, membership.successor_set]458    . have oldShape := disjointSum.membership.forward with oldMember459      cases oldShape with leftShape | rightShape460      . obtain (xOld, hxOld) := leftShape461        rcases hxOld with (hxM, pairShapeOld)462        rw pairShapeOld463        simp [disjointSum.membership, membership.successor_set]464      . obtain (yOld, hyOld) := rightShape465        rcases hyOld with (hyN, pairShapeRight)466        rw pairShapeRight467        exact disjointSum.right with hyN468469theorem natural.successor_as_insert (n : Nat)470  shows succ(n) = insert(n, n)471proof472  simp [next.natural, next, insert, union2.commutative]473474theorem natSumEquiv.bijective (n m : Nat)475  shows BijectiveBetween(natSumEquiv(m, n), m ⊎ n, add(m, n))476proof477  induction m478  | zero => settle with natSumEquiv, add, rightProjection.bijective479  | succ(k) using ih =>480    rw [natSumEquiv, add, disjointSum.successor_left, natural.successor_as_insert]481    apply adjoinMap.bijective482    . exact ih483    . intro member484      have shape := disjointSum.membership.forward with member485      cases shape with leftShape | rightShape486      . obtain (xFresh, hxFresh) := leftShape487        rcases hxFresh with (hxK, tagsEqual)488        have same := inl.injective with tagsEqual489        rw ← same at hxK490        have irreflexive := membership.irreflexive with hxK491        contradiction492      . obtain (yFresh, hyFresh) := rightShape493        rcases hyFresh with (hyN, tagsEqualRight)494        have disjoint := tags.disjoint with tagsEqualRight495        contradiction496    . exact membership.irreflexive at add(k, n)497498theorem Equipotent.nat_disjointSum (m n : Set)499  requires hm : Nat(m)500  requires hn : Nat(n)501  shows (m ⊎ n) ≃ add(m, n)502proof503  witness natSumEquiv(m, n)504  exact natSumEquiv.bijective with hn, hm505506theorem HasCardinality.disjointSum (A B m n : Set)507  requires hA : HasCardinality(A, m)508  requires hB : HasCardinality(B, n)509  shows HasCardinality(A ⊎ B, add(m, n))510proof511  rcases hA with (hm, equipotentA)512  rcases hB with (hn, equipotentB)513  constructor514  . exact Grace.Core.Nat.Algebra.add.closed at n, m515  . have tagged := Equipotent.disjointSum with equipotentA, equipotentB516    have numeric := Equipotent.nat_disjointSum with hm, hn517    exact Equipotent.transitive with tagged, numeric518519theorem Finite.disjointSum (A B : Set)520  requires finiteA : Finite(A)521  requires finiteB : Finite(B)522  shows Finite(A ⊎ B)523proof524  obtain (m, hA) := finiteA525  obtain (n, hB) := finiteB526  witness add(m, n)527  exact HasCardinality.disjointSum with hA, hB528