-- Rationals as signed natural fractions -- Part of Cumulus, the Grace17 mathematics library. -- Copyright (c) 2026 Grant Passmore. -- Released under the Apache License 2.0. See LICENSE in the repository root. -- Authors: Grant Passmore module Grace.Cumulus.Rat.Defs import Int.Core -- ((a,b),m) represents (a-b)/m, with m nonzero. This presentation avoids -- choosing representatives from integer quotient classes. def positiveNaturals : Set := { n ∈ ℕ | n ≠ 0 } def rationalRepresentatives : Set := integerPairs × positiveNaturals def rationalEquivalent : Set := { p ∈ rationalRepresentatives × rationalRepresentatives | ∃ a ∈ ℕ, ∃ b ∈ ℕ, ∃ m ∈ positiveNaturals, ∃ c ∈ ℕ, ∃ d ∈ ℕ, ∃ n ∈ positiveNaturals, p = (((a, b), m), ((c, d), n)) ∧ n * a + m * d = m * c + n * b } def ℚ : Set := (rationalRepresentatives ⧸ rationalEquivalent) class Rational (q : Set) := q ∈ ℚ -- Quotient classes are sets of rational representatives. These two views -- keep client proofs at the rational level instead of reopening quotient -- membership every time a representative is used. theorem Rational.representative (q u : Set) requires rational : q ∈ ℚ requires member : u ∈ q shows u ∈ rationalRepresentatives proof unfold ℚ at rational have bounded := quotient.subset_powerset at rationalRepresentatives, rationalEquivalent have power := bounded with rational have subset := powerset.membership_iff.forward with power exact subset with member theorem rationalRepresentatives.pair (a b m : Nat) requires nonzero : m ≠ 0 shows ((a, b), m) ∈ rationalRepresentatives proof unfold rationalRepresentatives apply product.pair . exact integerPairs.pair with *{2} . apply positiveNaturals.membership.backward at m constructor . settle with nat.omega . exact nonzero theorem rationalRepresentatives.coordinates (p : Set) requires hp : p ∈ rationalRepresentatives shows ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ m, Nat(m) ∧ m ≠ 0 ∧ p = ((a, b), m) proof unfold rationalRepresentatives at hp simp [product.membership] at hp rcases hp with ⟨bounded, numerator, numeratorInteger, m, mPositive, shape⟩ obtain ⟨a, haNat, b, hbNat, numeratorShape⟩ := integerPairs.coordinates with numeratorInteger obtain ⟨mNatSet, mNonzero⟩ := positiveNaturals.membership.forward with mPositive have hmNat := nat.omega.backward with mNatSet witness a witness b witness m constructor exact mNonzero rwa numeratorShape at shape theorem rationalEquivalent.relation shows RelationOn(rationalEquivalent, rationalRepresentatives) proof intros p hp simp [rationalEquivalent.membership] at hp rcases hp with ⟨bounded, witnesses⟩ exact bounded theorem rationalEquivalent.reflexive_pair (a b m : Nat) requires nonzero : m ≠ 0 shows relates(rationalEquivalent, ((a, b), m), ((a, b), m)) proof unfold relates apply rationalEquivalent.membership.backward constructor . apply product.pair at ((a, b), m), ((a, b), m), rationalRepresentatives, rationalRepresentatives . exact rationalRepresentatives.pair with nonzero . exact rationalRepresentatives.pair with nonzero . witness a constructor . settle with nat.omega . witness b constructor . settle with nat.omega . witness m constructor . apply positiveNaturals.membership.backward at m constructor . settle with nat.omega . exact nonzero . witness a constructor . settle with nat.omega . witness b constructor . settle with nat.omega . witness m constructor . apply positiveNaturals.membership.backward at m constructor . settle with nat.omega . exact nonzero refine ⟨rfl, rfl⟩ theorem rationalEquivalent.relates_representatives (a b m c d n : Nat) requires mNonzero : m ≠ 0 requires nNonzero : n ≠ 0 shows relates(rationalEquivalent, ((a, b), m), ((c, d), n)) ↔ n * a + m * d = m * c + n * b proof constructor . intro h unfold relates at h simp [rationalEquivalent.membership] at h rcases h with ⟨bounded, wa, waNat, wb, wbNat, wm, wmPositive, wc, wcNat, wd, wdNat, wn, wnPositive, shape, equation⟩ obtain ⟨leftShape, rightShape⟩ := orderedPair.injective with shape obtain ⟨numeratorLeft, denominatorLeft⟩ := orderedPair.injective with leftShape obtain ⟨numeratorRight, denominatorRight⟩ := orderedPair.injective with rightShape obtain ⟨aEquals, bEquals⟩ := orderedPair.injective with numeratorLeft obtain ⟨cEquals, dEquals⟩ := orderedPair.injective with numeratorRight simp . intro equation unfold relates apply rationalEquivalent.membership.backward constructor . apply product.pair at ((a, b), m), ((c, d), n), rationalRepresentatives, rationalRepresentatives . exact rationalRepresentatives.pair with mNonzero . exact rationalRepresentatives.pair with nNonzero . witness a constructor . settle with nat.omega . witness b constructor . settle with nat.omega . witness m constructor . apply positiveNaturals.membership.backward at m constructor . settle with nat.omega . exact mNonzero . witness c constructor . settle with nat.omega . witness d constructor . settle with nat.omega . witness n constructor . apply positiveNaturals.membership.backward at n constructor . settle with nat.omega . exact nNonzero refine ⟨rfl, equation⟩ theorem rationalEquivalent.cross_symmetric (a b m c d n : Nat) requires h : n * a + m * d = m * c + n * b shows m * c + n * b = n * a + m * d proof simp theorem rationalEquivalent.cross_transitive_scaled (a b m c d n e f k : Nat) requires left : n * a + m * d = m * c + n * b requires right : k * c + n * f = n * e + k * d shows n * (k * a + m * f) = n * (m * e + k * b) proof linear_combination k * left + m * right theorem rationalEquivalent.cross_transitive (a b m c d n e f k : Nat) requires nNonzero : n ≠ 0 requires left : n * a + m * d = m * c + n * b requires right : k * c + n * f = n * e + k * d shows k * a + m * f = m * e + k * b proof have scaled := rationalEquivalent.cross_transitive_scaled at a, b, m, c, d, n, e, f, k with * exact mul.left_cancel_positive with nNonzero, scaled theorem rationalEquivalent.reflexive shows ReflexiveOn(rationalRepresentatives, rationalEquivalent) proof intros p hp obtain ⟨a, haNat, b, hbNat, m, hmNat, mNonzero, shape⟩ := rationalRepresentatives.coordinates with hp rw shape exact rationalEquivalent.reflexive_pair with haNat, hbNat, hmNat, mNonzero theorem rationalEquivalent.symmetric shows SymmetricOn(rationalRepresentatives, rationalEquivalent) proof intros p hp q hq hpq obtain ⟨a, haNat, b, hbNat, m, hmNat, mNonzero, pShape⟩ := rationalRepresentatives.coordinates with hp obtain ⟨c, hcNat, d, hdNat, n, hnNat, nNonzero, qShape⟩ := rationalRepresentatives.coordinates with hq rw [pShape, qShape] at hpq rw [pShape, qShape] have characterization := rationalEquivalent.relates_representatives with haNat, hbNat, hmNat, hcNat, hdNat, hnNat, mNonzero, nNonzero have equation := characterization.forward with hpq have reverse := rationalEquivalent.cross_symmetric with haNat, hbNat, hmNat, hcNat, hdNat, hnNat, equation have reverseCharacterization := rationalEquivalent.relates_representatives with hcNat, hdNat, hnNat, haNat, hbNat, hmNat, nNonzero, mNonzero apply reverseCharacterization.backward exact reverse theorem rationalEquivalent.transitive shows TransitiveOn(rationalRepresentatives, rationalEquivalent) proof intros p hp q hq r hr hpq hqr obtain ⟨a, haNat, b, hbNat, m, hmNat, mNonzero, pShape⟩ := rationalRepresentatives.coordinates with hp obtain ⟨c, hcNat, d, hdNat, n, hnNat, nNonzero, qShape⟩ := rationalRepresentatives.coordinates with hq obtain ⟨e, heNat, f, hfNat, k, hkNat, kNonzero, rShape⟩ := rationalRepresentatives.coordinates with hr rw [pShape, qShape] at hpq rw [qShape, rShape] at hqr rw [pShape, rShape] have firstCharacterization := rationalEquivalent.relates_representatives with haNat, hbNat, hmNat, hcNat, hdNat, hnNat, mNonzero, nNonzero have firstEquation := firstCharacterization.forward with hpq have secondCharacterization := rationalEquivalent.relates_representatives with hcNat, hdNat, hnNat, heNat, hfNat, hkNat, nNonzero, kNonzero have secondEquation := secondCharacterization.forward with hqr have combined := rationalEquivalent.cross_transitive with haNat, hbNat, hmNat, hcNat, hdNat, hnNat, heNat, hfNat, hkNat, nNonzero, firstEquation, secondEquation have resultCharacterization := rationalEquivalent.relates_representatives with haNat, hbNat, hmNat, heNat, hfNat, hkNat, mNonzero, kNonzero apply resultCharacterization.backward exact combined theorem rationalEquivalent.equivalence shows Equivalence(rationalRepresentatives, rationalEquivalent) proof refine ⟨rationalEquivalent.relation, rationalEquivalent.reflexive, rationalEquivalent.symmetric, rationalEquivalent.transitive⟩ -- A rational class always has a representative. Client proofs -- should use this boundary instead of reopening quotient and Power Set data. theorem Rational.some_representative (q : Set) requires rational : q ∈ ℚ shows ∃ u ∈ q, u ∈ rationalRepresentatives proof have quotientMember := rational unfold ℚ at quotientMember obtain ⟨u, hu⟩ := quotient.member_nonempty with rationalEquivalent.equivalence, quotientMember have representative := Rational.representative with rational, hu refine ⟨u, hu, representative⟩ theorem Rational.members_related (q u v : Set) requires rational : q ∈ ℚ requires hu : u ∈ q requires hv : v ∈ q shows relates(rationalEquivalent, u, v) proof unfold ℚ at rational exact quotient.members_related with rationalEquivalent.equivalence, rational, hu, hv -- Related representatives determine the same rational point, regardless of -- which representatives were chosen from the two quotient classes. theorem Rational.eq_of_related_members (q r u v : Set) requires qRational : q ∈ ℚ requires rRational : r ∈ ℚ requires hu : u ∈ q requires hv : v ∈ r requires related : relates(rationalEquivalent, u, v) shows q = r proof have uRepresentative := Rational.representative with qRational, hu have vRepresentative := Rational.representative with rRational, hv have qQuotient := qRational unfold ℚ at qQuotient have rQuotient := rRational unfold ℚ at rQuotient have qClass := quotient.class_of_member with rationalEquivalent.equivalence, qQuotient, hu have rClass := quotient.class_of_member with rationalEquivalent.equivalence, rQuotient, hv have sameClass := equivalenceClass.eq with rationalEquivalent.equivalence, uRepresentative, vRepresentative, related rwa [qClass, rClass] theorem rationals.membership (q : Set) shows q ∈ ℚ ↔ q ∈ (rationalRepresentatives ⧸ rationalEquivalent) proof simp [ℚ]