Grace/Cumulus/Rat/Defs.g17

Open in Workbench Download source

Imports

Int.Core

Declarations

Source

1-- Rationals as signed natural fractions2-- 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.Rat.Defs8import Int.Core910-- ((a,b),m) represents (a-b)/m, with m nonzero.  This presentation avoids11-- choosing representatives from integer quotient classes.12def positiveNaturals : Set := { n ∈ ℕ | n ≠ 0 }13def rationalRepresentatives : Set := integerPairs × positiveNaturals14def rationalEquivalent : Set :=15  { p ∈ rationalRepresentatives × rationalRepresentatives |16    ∃ a ∈ ℕ, ∃ b ∈ ℕ,17    ∃ m ∈ positiveNaturals, ∃ c ∈ ℕ,18    ∃ d ∈ ℕ, ∃ n ∈ positiveNaturals,19      p = (((a, b), m), ((c, d), n)) ∧20      n * a + m * d = m * c + n * b }2122def ℚ : Set := (rationalRepresentatives ⧸ rationalEquivalent)23class Rational (q : Set) := q ∈ ℚ2425-- Quotient classes are sets of rational representatives.  These two views26-- keep client proofs at the rational level instead of reopening quotient27-- membership every time a representative is used.28theorem Rational.representative (q u : Set)29  requires rational : q ∈ ℚ30  requires member : u ∈ q31  shows u ∈ rationalRepresentatives32proof33  unfold ℚ at rational34  have bounded := quotient.subset_powerset at rationalRepresentatives, rationalEquivalent35  have power := bounded with rational36  have subset := powerset.membership_iff.forward with power37  exact subset with member3839theorem rationalRepresentatives.pair (a b m : Nat)40  requires nonzero : m ≠ 041  shows ((a, b), m) ∈ rationalRepresentatives42proof43  unfold rationalRepresentatives44  apply product.pair45  . exact integerPairs.pair with *{2}46  . apply positiveNaturals.membership.backward at m47    constructor48    . settle with nat.omega49    . exact nonzero5051theorem rationalRepresentatives.coordinates (p : Set)52  requires hp : p ∈ rationalRepresentatives53  shows ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ m, Nat(m) ∧ m ≠ 0 ∧ p = ((a, b), m)54proof55  unfold rationalRepresentatives at hp56  simp [product.membership] at hp57  rcases hp with ⟨bounded, numerator, numeratorInteger, m, mPositive, shape⟩58  obtain ⟨a, haNat, b, hbNat, numeratorShape⟩ := integerPairs.coordinates with numeratorInteger59  obtain ⟨mNatSet, mNonzero⟩ := positiveNaturals.membership.forward with mPositive60  have hmNat := nat.omega.backward with mNatSet61  witness a62  witness b63  witness m64  constructor65  exact mNonzero66  rwa numeratorShape at shape6768theorem rationalEquivalent.relation69  shows RelationOn(rationalEquivalent, rationalRepresentatives)70proof71  intros p hp72  simp [rationalEquivalent.membership] at hp73  rcases hp with ⟨bounded, witnesses⟩74  exact bounded7576theorem rationalEquivalent.reflexive_pair (a b m : Nat)77  requires nonzero : m ≠ 078  shows relates(rationalEquivalent, ((a, b), m), ((a, b), m))79proof80  unfold relates81  apply rationalEquivalent.membership.backward82  constructor83  . apply product.pair at ((a, b), m), ((a, b), m), rationalRepresentatives, rationalRepresentatives84    . exact rationalRepresentatives.pair with nonzero85    . exact rationalRepresentatives.pair with nonzero86  . witness a87    constructor88    . settle with nat.omega89    . witness b90      constructor91      . settle with nat.omega92      . witness m93        constructor94        . apply positiveNaturals.membership.backward at m95          constructor96          . settle with nat.omega97          . exact nonzero98        . witness a99          constructor100          . settle with nat.omega101          . witness b102            constructor103            . settle with nat.omega104            . witness m105              constructor106              . apply positiveNaturals.membership.backward at m107                constructor108                . settle with nat.omega109                . exact nonzero110              refine ⟨rfl, rfl⟩111112theorem rationalEquivalent.relates_representatives (a b m c d n : Nat)113  requires mNonzero : m ≠ 0114  requires nNonzero : n ≠ 0115  shows relates(rationalEquivalent, ((a, b), m), ((c, d), n)) ↔ n * a + m * d = m * c + n * b116proof117  constructor118  . intro h119    unfold relates at h120    simp [rationalEquivalent.membership] at h121    rcases h with ⟨bounded, wa, waNat, wb, wbNat, wm, wmPositive, wc, wcNat, wd, wdNat, wn, wnPositive, shape, equation⟩122    obtain ⟨leftShape, rightShape⟩ := orderedPair.injective with shape123    obtain ⟨numeratorLeft, denominatorLeft⟩ := orderedPair.injective with leftShape124    obtain ⟨numeratorRight, denominatorRight⟩ := orderedPair.injective with rightShape125    obtain ⟨aEquals, bEquals⟩ := orderedPair.injective with numeratorLeft126    obtain ⟨cEquals, dEquals⟩ := orderedPair.injective with numeratorRight127    simp128  . intro equation129    unfold relates130    apply rationalEquivalent.membership.backward131    constructor132    . apply product.pair at ((a, b), m), ((c, d), n), rationalRepresentatives, rationalRepresentatives133      . exact rationalRepresentatives.pair with mNonzero134      . exact rationalRepresentatives.pair with nNonzero135    . witness a136      constructor137      . settle with nat.omega138      . witness b139        constructor140        . settle with nat.omega141        . witness m142          constructor143          . apply positiveNaturals.membership.backward at m144            constructor145            . settle with nat.omega146            . exact mNonzero147          . witness c148            constructor149            . settle with nat.omega150            . witness d151              constructor152              . settle with nat.omega153              . witness n154                constructor155                . apply positiveNaturals.membership.backward at n156                  constructor157                  . settle with nat.omega158                  . exact nNonzero159                refine ⟨rfl, equation⟩160161theorem rationalEquivalent.cross_symmetric (a b m c d n : Nat)162  requires h : n * a + m * d = m * c + n * b163  shows m * c + n * b = n * a + m * d164proof165  simp166167theorem rationalEquivalent.cross_transitive_scaled (a b m c d n e f k : Nat)168  requires left : n * a + m * d = m * c + n * b169  requires right : k * c + n * f = n * e + k * d170  shows n * (k * a + m * f) = n * (m * e + k * b)171proof172  linear_combination k * left + m * right173174theorem rationalEquivalent.cross_transitive (a b m c d n e f k : Nat)175  requires nNonzero : n ≠ 0176  requires left : n * a + m * d = m * c + n * b177  requires right : k * c + n * f = n * e + k * d178  shows k * a + m * f = m * e + k * b179proof180  have scaled := rationalEquivalent.cross_transitive_scaled at a, b, m, c, d, n, e, f, k with *181  exact mul.left_cancel_positive with nNonzero, scaled182183theorem rationalEquivalent.reflexive184  shows ReflexiveOn(rationalRepresentatives, rationalEquivalent)185proof186  intros p hp187  obtain ⟨a, haNat, b, hbNat, m, hmNat, mNonzero, shape⟩ := rationalRepresentatives.coordinates with hp188  rw shape189  exact rationalEquivalent.reflexive_pair with haNat, hbNat, hmNat, mNonzero190191theorem rationalEquivalent.symmetric192  shows SymmetricOn(rationalRepresentatives, rationalEquivalent)193proof194  intros p hp q hq hpq195  obtain ⟨a, haNat, b, hbNat, m, hmNat, mNonzero, pShape⟩ := rationalRepresentatives.coordinates with hp196  obtain ⟨c, hcNat, d, hdNat, n, hnNat, nNonzero, qShape⟩ := rationalRepresentatives.coordinates with hq197  rw [pShape, qShape] at hpq198  rw [pShape, qShape]199  have characterization := rationalEquivalent.relates_representatives with haNat, hbNat, hmNat, hcNat, hdNat, hnNat, mNonzero, nNonzero200  have equation := characterization.forward with hpq201  have reverse := rationalEquivalent.cross_symmetric with haNat, hbNat, hmNat, hcNat, hdNat, hnNat, equation202  have reverseCharacterization := rationalEquivalent.relates_representatives with hcNat, hdNat, hnNat, haNat, hbNat, hmNat, nNonzero, mNonzero203  apply reverseCharacterization.backward204  exact reverse205206theorem rationalEquivalent.transitive207  shows TransitiveOn(rationalRepresentatives, rationalEquivalent)208proof209  intros p hp q hq r hr hpq hqr210  obtain ⟨a, haNat, b, hbNat, m, hmNat, mNonzero, pShape⟩ := rationalRepresentatives.coordinates with hp211  obtain ⟨c, hcNat, d, hdNat, n, hnNat, nNonzero, qShape⟩ := rationalRepresentatives.coordinates with hq212  obtain ⟨e, heNat, f, hfNat, k, hkNat, kNonzero, rShape⟩ := rationalRepresentatives.coordinates with hr213  rw [pShape, qShape] at hpq214  rw [qShape, rShape] at hqr215  rw [pShape, rShape]216  have firstCharacterization := rationalEquivalent.relates_representatives with haNat, hbNat, hmNat, hcNat, hdNat, hnNat, mNonzero, nNonzero217  have firstEquation := firstCharacterization.forward with hpq218  have secondCharacterization := rationalEquivalent.relates_representatives with hcNat, hdNat, hnNat, heNat, hfNat, hkNat, nNonzero, kNonzero219  have secondEquation := secondCharacterization.forward with hqr220  have combined := rationalEquivalent.cross_transitive with haNat, hbNat, hmNat, hcNat, hdNat, hnNat, heNat, hfNat, hkNat, nNonzero, firstEquation, secondEquation221  have resultCharacterization := rationalEquivalent.relates_representatives with haNat, hbNat, hmNat, heNat, hfNat, hkNat, mNonzero, kNonzero222  apply resultCharacterization.backward223  exact combined224225theorem rationalEquivalent.equivalence226  shows Equivalence(rationalRepresentatives, rationalEquivalent)227proof228  refine ⟨rationalEquivalent.relation, rationalEquivalent.reflexive, rationalEquivalent.symmetric, rationalEquivalent.transitive⟩229230-- A rational class always has a representative. Client proofs231-- should use this boundary instead of reopening quotient and Power Set data.232theorem Rational.some_representative (q : Set)233  requires rational : q ∈ ℚ234  shows ∃ u ∈ q, u ∈ rationalRepresentatives235proof236  have quotientMember := rational237  unfold ℚ at quotientMember238  obtain ⟨u, hu⟩ := quotient.member_nonempty with rationalEquivalent.equivalence, quotientMember239  have representative := Rational.representative with rational, hu240  refine ⟨u, hu, representative⟩241242theorem Rational.members_related (q u v : Set)243  requires rational : q ∈ ℚ244  requires hu : u ∈ q245  requires hv : v ∈ q246  shows relates(rationalEquivalent, u, v)247proof248  unfold ℚ at rational249  exact quotient.members_related with rationalEquivalent.equivalence, rational, hu, hv250251-- Related representatives determine the same rational point, regardless of252-- which representatives were chosen from the two quotient classes.253theorem Rational.eq_of_related_members (q r u v : Set)254  requires qRational : q ∈ ℚ255  requires rRational : r ∈ ℚ256  requires hu : u ∈ q257  requires hv : v ∈ r258  requires related : relates(rationalEquivalent, u, v)259  shows q = r260proof261  have uRepresentative := Rational.representative with qRational, hu262  have vRepresentative := Rational.representative with rRational, hv263  have qQuotient := qRational264  unfold ℚ at qQuotient265  have rQuotient := rRational266  unfold ℚ at rQuotient267  have qClass := quotient.class_of_member with rationalEquivalent.equivalence, qQuotient, hu268  have rClass := quotient.class_of_member with rationalEquivalent.equivalence, rQuotient, hv269  have sameClass := equivalenceClass.eq with270    rationalEquivalent.equivalence, uRepresentative, vRepresentative, related271  rwa [qClass, rClass]272273theorem rationals.membership (q : Set)274  shows q ∈ ℚ ↔ q ∈ (rationalRepresentatives ⧸ rationalEquivalent)275proof276  simp [ℚ]277