Grace/Cumulus/Real/RationalEmbedding.g17

Open in Workbench Download source

Imports

Natural · Rat.Density

Declarations

Source

1-- The embedding of the rationals in the reals preserves 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.Real.RationalEmbedding8import Natural9import Rat.Density1011-- The cut of a sum is the sum of the cuts. A rational below p + q splits as12-- a + b with a below p and b below q, by density; the converse is monotonicity.13theorem rationalCut.add (p q : Rational)14  shows rationalCut(p + q) = rationalCut(p) + rationalCut(q)15proof16  have sumReal := rationalCut.real at p + q with *17  have cutForm := realAddValue.cut at rationalCut(p), rationalCut(q) with *18  have addReal := realAddValue.real at rationalCut(p), rationalCut(q) with *19  rw cutForm20  rw cutForm at addReal21  apply Real.extensionality22  . exact sumReal23  . exact addReal24  . intros r rInQ25    constructor26    . intro member27      obtain ⟨rMember, less⟩ := rationalCut.membership.forward with member28      have commuted := rationalAddValue.commutative at p, q with *29      rw commuted at less30      have shifted := rationalLess.sub_left at r, q, p with *31      obtain ⟨a, aInQ, aAbove, aBelow⟩ := rationalLess.dense at r - q, p with *32      have aMember : a ∈ rationalCut(p) := rationalCut.membership.backward with ⟨aInQ, aBelow⟩33      have moved := rationalLess.add_left_of_sub_left at r, q, a with *34      have commutedA := rationalAddValue.commutative at q, a with *35      rw commutedA at moved36      have shiftedA := rationalLess.sub_left at r, a, q with *37      obtain ⟨b, bInQ, bAbove, bBelow⟩ := rationalLess.dense at r - a, q with *38      have bMember : b ∈ rationalCut(q) := rationalCut.membership.backward with ⟨bInQ, bBelow⟩39      have below := rationalLess.add_left_of_sub_left at r, a, b with *40      rw rationalAddValue.notation at below41      exact realAddCut.membership_value.backward with ⟨rInQ, a, aMember, b, bMember, below⟩42    . intro member43      obtain ⟨rMember, a, aMember, b, bMember, below⟩ := realAddCut.membership_value.forward with member44      obtain ⟨aInQ, aBelow⟩ := rationalCut.membership.forward with aMember45      obtain ⟨bInQ, bBelow⟩ := rationalCut.membership.forward with bMember46      rw ← rationalAddValue.notation at below47      have first := rationalLess.add_right at a, p, b with *48      have second := rationalLess.add_left at b, q, p with *49      have chain := rationalLess.transitive at r, a + b, p + b with *50      have whole := rationalLess.transitive at r, p + b, p + q with *51      apply rationalCut.membership.backward52      constructor53      . exact rInQ54      . exact whole5556theorem rationalCut.zero57  shows rationalCut(rationalZero) = realZero58proof59  simp6061theorem rationalCut.one62  shows rationalCut(rationalOne) = realOne63proof64  simp6566theorem rationalCut.neg (q : Rational)67  shows rationalCut(-q) = -(rationalCut(q))68proof69  have cancel := rationalAddValue.neg_right at q with *70  have sum := rationalCut.add at q, -q with *71  rw [cancel, rationalCut.zero] at sum72  linarith7374theorem rationalCut.sub (p q : Rational)75  shows rationalCut(p - q) = rationalCut(p) - rationalCut(q)76proof77  have negation := rationalCut.neg at q with *78  unfold rationalSubValue79  have sum := rationalCut.add at p, -q with *80  rw [sum, negation]81  unfold realSubValue82  rfl8384-- The rational n, built like realNat so the two embeddings line up.85def rationalNat (n : Nat) → Set86  | zero => rationalZero87  | succ(k) => rationalAddValue(rationalNat(k), rationalOne)8889theorem rationalNat.zero90  shows rationalNat(0) = rationalZero91proof92  simp9394theorem rationalNat.succ (n : Nat)95  shows rationalNat(succ(n)) = (rationalNat(n):Q) + rationalOne96proof97  rw [rationalNat, rationalAddValue.notation]98  rfl99100theorem rationalNat.rational (n : Nat)101  shows Rational(rationalNat(n))102proof103  induction n104  | zero =>105    rw rationalNat.zero106    exact rationalZero.rational107  | succ(k) using ih =>108    rw rationalNat.succ109    exact rationalAddValue.rational at rationalNat(k), rationalOne with *110111theorem realNat.successor (n : Nat)112  shows realNat(succ(n)) = (realNat(n):R) + 1113proof114  rw realNat.succ115  unfold realAddValue116  unfold call2117  rfl118119theorem rationalCut.natural (n : Nat)120  shows rationalCut(rationalNat(n)) = realNat(n)121proof122  induction n123  | zero =>124    rw [rationalNat.zero, realNat.zero]125    exact rationalCut.zero126  | succ(k) using ih =>127    rw rationalNat.succ128    have sum := rationalCut.add at rationalNat(k), rationalOne with *129    rw [sum, ih, rationalCut.one, realNat.successor]130    rfl131132theorem rationalNat.class (n : Nat)133  shows rationalNat(n) = rationalClass(n, 0, 1)134proof135  induction n136  | zero =>137    rw rationalNat.zero138    unfold rationalZero139    rfl140  | succ(k) using ih =>141    rw [rationalNat.succ, ih]142    unfold rationalOne143    have oneNonzero : 1 ≠ 0144      intro bad145      have positive : 0 < 1 by arith146      rw bad at positive147      exact Less.irreflexive at 0 with *, positive148    rw rationalAddValue.notation149    have classes := rationalAddValue.classes at k, 0, 1, 1, 0, 1 with *150    rw classes151    unfold rationalClassSum152    have productNonzero : 1 * 1 ≠ 0153      have unit := mul.right_unit at 1 with *154      rwa unit155    have equivalent : 1 * (1 * k + 1 * 1) + (1 * 1) * 0 = (1 * 1) * succ(k) + 1 * (1 * 0 + 1 * 0) by ring156    exact rationalClass.eq at 1 * k + 1 * 1, 1 * 0 + 1 * 0, 1 * 1, succ(k), 0, 1 with *157158-- Multiplying a rational by the natural m scales its cut by realNat(m).159theorem rationalCut.mul_natural (q : Rational) (m : Nat)160  shows rationalCut(q * (rationalNat(m):Q)) = rationalCut(q) * realNat(m)161proof162  induction m163  | zero =>164    rw rationalNat.zero165    have zero := rationalMulValue.zero_right at q with *166    rw [zero, rationalCut.zero, realNat.zero]167    ring168  | succ(k) using ih =>169    rw rationalNat.succ170    have distribute := rationalMulValue.distributive_left at q, rationalNat(k), rationalOne with *171    rw distribute172    have unit := rationalMulValue.one_right at q with *173    rw unit174    have sum := rationalCut.add at q * (rationalNat(k):Q), q with *175    rw [sum, ih, realNat.successor]176    ring177178-- A rational a/m, written as the class of ((a, b), m), scales to the difference179-- of two naturals: (a − b)/m times m is a − b.180theorem rationalClass.mul_denominator (a b m : Nat)181  requires nonzero : m ≠ 0182  shows (rationalClass(a, b, m):Q) * (rationalNat(m):Q) = (rationalNat(a):Q) - (rationalNat(b):Q)183proof184  have oneNonzero : 1 ≠ 0185    intro bad186    have positive : 0 < 1 by arith187    rw bad at positive188    exact Less.irreflexive with *, positive189  have classA := rationalNat.class at a with *190  have classB := rationalNat.class at b with *191  have classM := rationalNat.class at m with *192  rw [classA, classB, classM]193  rw rationalMulValue.notation194  have product := rationalMulValue.classes at a, b, m, m, 0, 1 with *195  rw product196  unfold rationalClassMul197  unfold rationalSubValue198  rw rationalNegValue.notation199  have negation := rationalNegValue.classes at b, 0, 1 with *200  rw negation201  unfold rationalClassNeg202  rw rationalAddValue.notation203  have sum := rationalAddValue.classes at a, 0, 1, 0, b, 1 with *204  rw sum205  unfold rationalClassSum206  have mulNonzero : m * 1 ≠ 0207    have unit := mul.right_unit at m with *208    rwa unit209  have productNonzero : 1 * 1 ≠ 0210    have unit := mul.right_unit at 1 with *211    rwa unit212  have equivalent : (1 * 1) * (a * m + b * 0) + (m * 1) * (1 * 0 + 1 * b) = (m * 1) * (1 * a + 1 * 0) + (1 * 1) * (a * 0 + b * m)213    ring214  exact rationalClass.eq with *215216theorem rationalCut.scaled (a b m : Nat)217  requires nonzero : m ≠ 0218  shows (rationalCut(rationalClass(a, b, m)):R) * (realNat(m):R) = (realNat(a):R) - (realNat(b):R)219proof220  have qRational := rationalClass.rational at a, b, m with *221  have scaled := rationalCut.mul_natural at rationalClass(a, b, m), m with *222  rw ← scaled223  have integer := rationalClass.mul_denominator at a, b, m with *224  rw integer225  have difference := rationalCut.sub at rationalNat(a), rationalNat(b) with *226  rw [difference, rationalCut.natural, rationalCut.natural]227  rfl228