Grace/Cumulus/Rat/Operations.g17

Open in Workbench Download source

Imports

Order · Algebra.Ring.Core

Declarations

Source

1-- Rational operations lifted from 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.Operations8import Order9import Algebra.Ring.Core1011-- The rational represented by (a-b)/m. The nonzero side condition belongs to12-- the theorems that use this construction; the definition itself is total.13def rationalClass (a b m : Set) : Set :=14  ⟦((a, b), m)⟧[rationalRepresentatives, rationalEquivalent]1516def rationalZero : Rational := rationalClass(0, 0, 1)17def rationalOne : Rational := rationalClass(1, 0, 1)1819def rationalClassNeg (a b m : Set) : Set := rationalClass(b, a, m)2021-- (a-b)/m + (c-d)/n = ((n*a+m*c)-(n*b+m*d))/(m*n).22def rationalRepresentativeSum (a b m c d n : Set) : Set :=23  ((n * a + m * c, n * b + m * d), m * n)2425def rationalClassSum (a b m c d n : Set) : Set :=26  rationalClass(n * a + m * c, n * b + m * d, m * n)2728-- (a-b)(c-d) = (a*c+b*d)-(a*d+b*c).29def rationalRepresentativeMul (a b m c d n : Set) : Set :=30  ((a * c + b * d, a * d + b * c), m * n)3132def rationalClassMul (a b m c d n : Set) : Set :=33  rationalClass(a * c + b * d, a * d + b * c, m * n)3435-- Quotient-level operations are set-theoretic function graphs. Their36-- witnesses retain the representative calculation, while the bounded carrier37-- makes every public input and output a rational number.38def rationalAdd : Set :=39  { p ∈ ((ℚ × ℚ) × ℚ) |40    ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ m, Nat(m) ∧ m ≠ 0 ∧41    ∃ c, Nat(c) ∧ ∃ d, Nat(d) ∧ ∃ n, Nat(n) ∧ n ≠ 0 ∧42      p = ((rationalClass(a, b, m), rationalClass(c, d, n)) ↦43        rationalClassSum(a, b, m, c, d, n)) }4445def rationalMul : Set :=46  { p ∈ ((ℚ × ℚ) × ℚ) |47    ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ m, Nat(m) ∧ m ≠ 0 ∧48    ∃ c, Nat(c) ∧ ∃ d, Nat(d) ∧ ∃ n, Nat(n) ∧ n ≠ 0 ∧49      p = ((rationalClass(a, b, m), rationalClass(c, d, n)) ↦50        rationalClassMul(a, b, m, c, d, n)) }5152def rationalNeg : Set :=53  { p ∈ (ℚ × ℚ) |54    ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ m, Nat(m) ∧ m ≠ 0 ∧55      p = (rationalClass(a, b, m) ↦ rationalClassNeg(a, b, m)) }5657def rationalAddValue (x y : Rational) : Rational := rationalAdd((x, y))58def rationalMulValue (x y : Rational) : Rational := rationalMul((x, y))59def rationalNegValue (x : Rational) : Rational := rationalNeg(x)6061theorem rationalClass.rational (a b m : Nat)62  requires nonzero : m ≠ 063  shows Rational(rationalClass(a, b, m))64proof65  unfold Rational66  unfold ℚ67  unfold rationalClass68  apply quotient.contains_class69  . exact rationalEquivalent.equivalence70  . have representative := rationalRepresentatives.pair at a, b, m71    specialize representative with *{1}72    exact representative7374-- On displayed rational classes, strict order is exactly the familiar75-- cross-multiplication inequality.  This is the quotient boundary used by76-- arithmetic clients: representative transport stays inside the API.77theorem rationalLess.classes (a b m c d n : Nat)78  requires mNonzero : m ≠ 079  requires nNonzero : n ≠ 080  shows relates(rationalLess, rationalClass(a, b, m), rationalClass(c, d, n)) ↔81    n * a + m * d < m * c + n * b82proof83  constructor84  . intro less85    have leftRational := rationalClass.rational at a, b, m with mNonzero86    have rightRational := rationalClass.rational at c, d, n with nNonzero87    unfold rationalClass at leftRational88    unfold rationalClass at rightRational89    unfold rationalClass at less90    obtain ⟨u, uInLeft, uRepresentative, v, vInRight, vRepresentative, representativeLess⟩ :=91      rationalLess.representatives at92        ⟦((a, b), m)⟧[rationalRepresentatives, rationalEquivalent],93        ⟦((c, d), n)⟧[rationalRepresentatives, rationalEquivalent] with94        leftRational, rightRational, less95    have leftRepresentative := rationalRepresentatives.pair at a, b, m with mNonzero96    have rightRepresentative := rationalRepresentatives.pair at c, d, n with nNonzero97    have leftSelf := equivalenceClass.self with rationalEquivalent.equivalence, leftRepresentative98    have rightSelf := equivalenceClass.self with rationalEquivalent.equivalence, rightRepresentative99    have leftEquivalent := Rational.members_related at100      ⟦((a, b), m)⟧[rationalRepresentatives, rationalEquivalent],101      u, ((a, b), m) with leftRational, uInLeft, leftSelf102    have rightEquivalent := Rational.members_related at103      ⟦((c, d), n)⟧[rationalRepresentatives, rationalEquivalent],104      v, ((c, d), n) with rightRational, vInRight, rightSelf105    have displayedLess := rationalRepresentativeLess.transport with106      uRepresentative, vRepresentative, leftRepresentative, rightRepresentative, leftEquivalent, rightEquivalent, representativeLess107    exact rationalRepresentativeLess.pair.forward with mNonzero, nNonzero, displayedLess108  . intro crossLess109    unfold rationalClass110    exact rationalLess.of_representatives with mNonzero, nNonzero, crossLess111112theorem Rational.coordinates (q : Set)113  requires rational : Rational(q)114  shows ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ m, Nat(m) ∧ m ≠ 0 ∧115    q = rationalClass(a, b, m)116proof117  unfold Rational at rational118  unfold ℚ at rational119  have quotientMember := quotient.membership.forward at120    rationalRepresentatives, rationalEquivalent, q121  specialize quotientMember with rational122  rcases quotientMember with ⟨bounded, u, uRepresentative, classShape⟩123  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, representativeShape⟩ := rationalRepresentatives.coordinates with uRepresentative124  witness a125  witness b126  witness m127  constructor128  exact mNonzero129  unfold rationalClass130  rw ← representativeShape131  exact classShape132133theorem rationalClass.eq (a b m c d n : Nat)134  requires mNonzero : m ≠ 0135  requires nNonzero : n ≠ 0136  requires equivalent : n * a + m * d = m * c + n * b137  shows rationalClass(a, b, m) = rationalClass(c, d, n)138proof139  unfold rationalClass140  apply equivalenceClass.eq141  . exact rationalEquivalent.equivalence142  . have left := rationalRepresentatives.pair at a, b, m with mNonzero143    exact left144  . have right := rationalRepresentatives.pair at c, d, n with nNonzero145    exact right146  . have characterization := rationalEquivalent.relates_representatives at a, b, m, c, d, n147    specialize characterization with *{2}148    apply characterization.backward149    exact equivalent150151theorem rationalClass.equivalent_of_eq (a b m c d n : Nat)152  requires mNonzero : m ≠ 0153  requires nNonzero : n ≠ 0154  requires same : rationalClass(a, b, m) = rationalClass(c, d, n)155  shows n * a + m * d = m * c + n * b156proof157  have left := rationalRepresentatives.pair at a, b, m with *158  have right := rationalRepresentatives.pair at c, d, n with *159  have related := equivalenceClass.related_of_eq at160    rationalRepresentatives, rationalEquivalent,161    ((a, b), m), ((c, d), n)162  simp [rationalClass] at same163  specialize related with rationalEquivalent.equivalence, left, right, same164  have characterization := rationalEquivalent.relates_representatives at a, b, m, c, d, n with *165  apply characterization.forward166  exact related167168theorem rationalZero.rational169  shows Rational(rationalZero)170proof171  unfold rationalZero172  apply rationalClass.rational173  . have oneNonzero := Naturals.disjoint.zero.succ at 0174    intro oneZero175    apply oneNonzero176    simp177178theorem rationalOne.rational179  shows Rational(rationalOne)180proof181  unfold rationalOne182  apply rationalClass.rational183  . have oneNonzero := Naturals.disjoint.zero.succ at 0184    intro oneZero185    apply oneNonzero186    simp187188theorem rationalClassNeg.well_defined (a b m c d n : Nat)189  requires mNonzero : m ≠ 0190  requires nNonzero : n ≠ 0191  requires equivalent : n * a + m * d = m * c + n * b192  shows rationalClassNeg(a, b, m) = rationalClassNeg(c, d, n)193proof194  unfold rationalClassNeg195  have reversed : n * b + m * c = m * d + n * a by linear_combination equivalent196  exact rationalClass.eq with *197198theorem rationalClassNeg.rational (a b m : Nat)199  requires nonzero : m ≠ 0200  shows Rational(rationalClassNeg(a, b, m))201proof202  unfold rationalClassNeg203  exact rationalClass.rational with *204205theorem rationalRepresentativeSum.representative (a b m c d n : Nat)206  requires mNonzero : m ≠ 0207  requires nNonzero : n ≠ 0208  shows rationalRepresentativeSum(a, b, m, c, d, n) ∈ rationalRepresentatives209proof210  unfold rationalRepresentativeSum211  apply rationalRepresentatives.pair212  . exact mul.nonzero with mNonzero, nNonzero213214-- Two equivalent choices for each summand produce equivalent sum215-- representatives. The certificate is the familiar common-denominator216-- calculation, expressed as a linear combination of the two input equations.217theorem rationalClassSum.well_defined (a b m a2 b2 m2 c d n c2 d2 n2 : Nat)218  requires mNonzero : m ≠ 0219  requires m2Nonzero : m2 ≠ 0220  requires nNonzero : n ≠ 0221  requires n2Nonzero : n2 ≠ 0222  requires leftEquivalent : m2 * a + m * b2 = m * a2 + m2 * b223  requires rightEquivalent : n2 * c + n * d2 = n * c2 + n2 * d224  shows rationalClassSum(a, b, m, c, d, n) =225    rationalClassSum(a2, b2, m2, c2, d2, n2)226proof227  unfold rationalClassSum228  apply rationalClass.eq229  . exact mul.nonzero with mNonzero, nNonzero230  . exact mul.nonzero with m2Nonzero, n2Nonzero231  . linear_combination n * n2 * leftEquivalent + m * m2 * rightEquivalent232233theorem rationalClassSum.rational (a b m c d n : Nat)234  requires mNonzero : m ≠ 0235  requires nNonzero : n ≠ 0236  shows Rational(rationalClassSum(a, b, m, c, d, n))237proof238  unfold rationalClassSum239  apply rationalClass.rational240  . exact mul.nonzero with mNonzero, nNonzero241242theorem rationalClassSum.zero_right (a b m : Nat)243  requires nonzero : m ≠ 0244  shows rationalClassSum(a, b, m, 0, 0, 1) = rationalClass(a, b, m)245proof246  simp [rationalClassSum, mul.left_unit, mul.right_unit, mul.right_zero, add.right_unit]247248theorem rationalClassSum.commutative (a b m c d n : Nat)249  requires mNonzero : m ≠ 0250  requires nNonzero : n ≠ 0251  shows rationalClassSum(a, b, m, c, d, n) = rationalClassSum(c, d, n, a, b, m)252proof253  unfold rationalClassSum254  apply rationalClass.eq255  . exact mul.nonzero with mNonzero, nNonzero256  . exact mul.nonzero with nNonzero, mNonzero257  . ring258259theorem rationalClassSum.associative (a b m c d n e f k : Nat)260  requires mNonzero : m ≠ 0261  requires nNonzero : n ≠ 0262  requires kNonzero : k ≠ 0263  shows rationalClassSum(n * a + m * c, n * b + m * d, m * n, e, f, k) =264    rationalClassSum(a, b, m, k * c + n * e, k * d + n * f, n * k)265proof266  unfold rationalClassSum267  apply rationalClass.eq268  . have mnNonzero := mul.nonzero with mNonzero, nNonzero269    exact mul.nonzero with mnNonzero, kNonzero270  . have nkNonzero := mul.nonzero with nNonzero, kNonzero271    exact mul.nonzero with mNonzero, nkNonzero272  . ring273274theorem rationalClassSum.neg_right (a b m : Nat)275  requires nonzero : m ≠ 0276  shows rationalClassSum(a, b, m, b, a, m) = rationalZero277proof278  unfold rationalClassSum279  unfold rationalZero280  apply rationalClass.eq281  . exact mul.nonzero with nonzero, nonzero282  . have oneNonzero := Naturals.disjoint.zero.succ at 0283    intro oneZero284    apply oneNonzero285    simp286  . ring287288theorem rationalRepresentativeMul.representative (a b m c d n : Nat)289  requires mNonzero : m ≠ 0290  requires nNonzero : n ≠ 0291  shows rationalRepresentativeMul(a, b, m, c, d, n) ∈ rationalRepresentatives292proof293  unfold rationalRepresentativeMul294  apply rationalRepresentatives.pair295  . exact mul.nonzero with mNonzero, nNonzero296297-- Multiplication respects both quotient arguments. Expanding signed products298-- turns the goal into a polynomial combination of the two equivalence299-- equations; no representative is selected and no cancellation is assumed.300theorem rationalClassMul.well_defined (a b m a2 b2 m2 c d n c2 d2 n2 : Nat)301  requires mNonzero : m ≠ 0302  requires m2Nonzero : m2 ≠ 0303  requires nNonzero : n ≠ 0304  requires n2Nonzero : n2 ≠ 0305  requires leftEquivalent : m2 * a + m * b2 = m * a2 + m2 * b306  requires rightEquivalent : n2 * c + n * d2 = n * c2 + n2 * d307  shows rationalClassMul(a, b, m, c, d, n) =308    rationalClassMul(a2, b2, m2, c2, d2, n2)309proof310  unfold rationalClassMul311  apply rationalClass.eq312  . exact mul.nonzero with mNonzero, nNonzero313  . exact mul.nonzero with m2Nonzero, n2Nonzero314  . linear_combination n2 * c * leftEquivalent - n2 * d * leftEquivalent + m * a2 * rightEquivalent - m * b2 * rightEquivalent315316theorem rationalClassMul.rational (a b m c d n : Nat)317  requires mNonzero : m ≠ 0318  requires nNonzero : n ≠ 0319  shows Rational(rationalClassMul(a, b, m, c, d, n))320proof321  unfold rationalClassMul322  apply rationalClass.rational323  . exact mul.nonzero with mNonzero, nNonzero324325theorem rationalClassMul.one_right (a b m : Nat)326  requires nonzero : m ≠ 0327  shows rationalClassMul(a, b, m, 1, 0, 1) = rationalClass(a, b, m)328proof329  settle with rationalClassMul, mul.left_unit, mul.right_unit, mul.left_zero,330    mul.right_zero, add.left_unit, add.right_unit331332theorem rationalClassMul.commutative (a b m c d n : Nat)333  requires mNonzero : m ≠ 0334  requires nNonzero : n ≠ 0335  shows rationalClassMul(a, b, m, c, d, n) = rationalClassMul(c, d, n, a, b, m)336proof337  unfold rationalClassMul338  apply rationalClass.eq339  . exact mul.nonzero with mNonzero, nNonzero340  . exact mul.nonzero with nNonzero, mNonzero341  . ring342343theorem rationalClassMul.associative (a b m c d n e f k : Nat)344  requires mNonzero : m ≠ 0345  requires nNonzero : n ≠ 0346  requires kNonzero : k ≠ 0347  shows rationalClassMul(a * c + b * d, a * d + b * c, m * n, e, f, k) =348    rationalClassMul(a, b, m, c * e + d * f, c * f + d * e, n * k)349proof350  unfold rationalClassMul351  apply rationalClass.eq352  . have mnNonzero := mul.nonzero with mNonzero, nNonzero353    exact mul.nonzero with mnNonzero, kNonzero354  . have nkNonzero := mul.nonzero with nNonzero, kNonzero355    exact mul.nonzero with mNonzero, nkNonzero356  . ring357358theorem rationalClassMul.distributive_left (a b m c d n e f k : Nat)359  requires mNonzero : m ≠ 0360  requires nNonzero : n ≠ 0361  requires kNonzero : k ≠ 0362  shows rationalClassMul(a, b, m, k * c + n * e, k * d + n * f, n * k) =363    rationalClassSum(364      a * c + b * d, a * d + b * c, m * n,365      a * e + b * f, a * f + b * e, m * k)366proof367  unfold rationalClassMul368  unfold rationalClassSum369  apply rationalClass.eq370  . have nkNonzero := mul.nonzero with nNonzero, kNonzero371    exact mul.nonzero with mNonzero, nkNonzero372  . have mnNonzero := mul.nonzero with mNonzero, nNonzero373    have mkNonzero := mul.nonzero at m, k with *374    exact mul.nonzero with mnNonzero, mkNonzero375  . ring376377theorem rationalNeg.relates (a b m : Nat)378  requires mNonzero : m ≠ 0379  shows relates(rationalNeg, rationalClass(a, b, m), rationalClassNeg(a, b, m))380proof381  unfold relates382  apply rationalNeg.membership.backward383  constructor384  . apply product.pair at rationalClass(a, b, m), rationalClassNeg(a, b, m), ℚ, ℚ385    . have input := rationalClass.rational at a, b, m with386        *{3}, mNonzero387      exact input388    . have output := rationalClassNeg.rational at a, b, m with389        *{3}, mNonzero390      exact output391  . refine ⟨a, assumption, b, assumption, m, assumption, mNonzero, rfl⟩392393theorem rationalNeg.factors (x y : Set)394  requires mapped : relates(rationalNeg, x, y)395  shows ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ m, Nat(m) ∧ m ≠ 0 ∧396    x = rationalClass(a, b, m) ∧ y = rationalClassNeg(a, b, m)397proof398  unfold relates at mapped399  simp [rationalNeg.membership] at mapped400  rcases mapped with ⟨bounded, a, aNat, b, bNat, m, mNat, mNonzero, shape⟩401  obtain ⟨inputShape, outputShape⟩ := orderedPair.injective with shape402  refine ⟨a, aNat, b, bNat, m, mNat, mNonzero, inputShape, outputShape⟩403404theorem rationalNeg.total405  shows TotalBetween(rationalNeg, ℚ, ℚ)406proof407  intros x xRational408  have typedX : Rational(x) by exact xRational409  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ := Rational.coordinates with typedX410  witness rationalClassNeg(a, b, m)411  constructor412  . have output := rationalClassNeg.rational at a, b, m with413      aNat, bNat, mNat, mNonzero414    exact output415  . rw xShape416    exact rationalNeg.relates with aNat, bNat, mNat, mNonzero417418theorem rationalNeg.functional419  shows Functional(rationalNeg)420proof421  intros x y xy z xz422  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, inputFirst, outputFirst⟩ := rationalNeg.factors with xy423  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, inputSecond, outputSecond⟩ := rationalNeg.factors with xz424  rw inputFirst at inputSecond425  have equivalent := rationalClass.equivalent_of_eq with426    aNat, bNat, mNat, cNat, dNat, nNat, mNonzero, nNonzero, inputSecond427  have sameNegative := rationalClassNeg.well_defined with428    aNat, bNat, mNat, cNat, dNat, nNat, mNonzero, nNonzero, equivalent429  rwa [outputFirst, outputSecond]430431theorem rationalNeg.function432  shows rationalNeg : ℚ → ℚ433proof434  constructor435    intros p hp436    simp [rationalNeg.membership] at hp437    rcases hp with ⟨bounded, witnesses⟩438    exact bounded439  . constructor440    . exact rationalNeg.functional441    . exact rationalNeg.total442443theorem rationalAdd.relates (a b m c d n : Nat)444  requires mNonzero : m ≠ 0445  requires nNonzero : n ≠ 0446  shows relates(rationalAdd,447    (rationalClass(a, b, m), rationalClass(c, d, n)),448    rationalClassSum(a, b, m, c, d, n))449proof450  unfold relates451  apply rationalAdd.membership.backward at452    ((rationalClass(a, b, m), rationalClass(c, d, n)) ↦453      rationalClassSum(a, b, m, c, d, n))454  constructor455  . apply product.pair at456      (rationalClass(a, b, m), rationalClass(c, d, n)),457      rationalClassSum(a, b, m, c, d, n), ℚ × ℚ, ℚ458    . apply product.pair at rationalClass(a, b, m), rationalClass(c, d, n), ℚ, ℚ459      . have left := rationalClass.rational at a, b, m with mNonzero460        exact left461      . have right := rationalClass.rational at c, d, n with nNonzero462        exact right463    . have sum := rationalClassSum.rational at a, b, m, c, d, n464      specialize sum with *{2}465      exact sum466  refine ⟨a, assumption, b, assumption, m, assumption, mNonzero, c, assumption, d, assumption, n, assumption, nNonzero, rfl⟩467468theorem rationalAdd.factors (x y : Set)469  requires h : relates(rationalAdd, x, y)470  shows ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ m, Nat(m) ∧ m ≠ 0 ∧471    ∃ c, Nat(c) ∧ ∃ d, Nat(d) ∧ ∃ n, Nat(n) ∧ n ≠ 0 ∧472      x = (rationalClass(a, b, m), rationalClass(c, d, n)) ∧473      y = rationalClassSum(a, b, m, c, d, n)474proof475  unfold relates at h476  simp [rationalAdd.membership] at h477  rcases h with ⟨bounded, a, aNat, b, bNat, m, mNat, mNonzero, c, cNat, d, dNat, n, nNat, nNonzero, shape⟩478  have coordinates := orderedPair.injective at x, y,479    (rationalClass(a, b, m), rationalClass(c, d, n)),480    rationalClassSum(a, b, m, c, d, n)481  specialize coordinates with shape482  rcases coordinates with ⟨inputShape, outputShape⟩483  refine ⟨a, aNat, b, bNat, m, mNat, mNonzero, c, cNat, d, dNat, n, nNat, nNonzero, inputShape, outputShape⟩484485theorem rationalAdd.total486  shows TotalBetween(rationalAdd, ℚ × ℚ, ℚ)487proof488  intros input hInput489  obtain ⟨bounded, q, qRational, r, rRational, inputShape⟩ := product.membership.forward with hInput490  have qTyped : Rational(q) by exact qRational491  have rTyped : Rational(r) by exact rRational492  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, qShape⟩ := Rational.coordinates with qTyped493  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, rShape⟩ := Rational.coordinates with rTyped494  witness rationalClassSum(a, b, m, c, d, n)495  constructor496  . exact rationalClassSum.rational at a, b, m, c, d, n with mNonzero, nNonzero497  . rw [inputShape, qShape, rShape]498    exact rationalAdd.relates with aNat, bNat, mNat, cNat, dNat, nNat, mNonzero, nNonzero499500theorem rationalAdd.functional501  shows Functional(rationalAdd)502proof503  intros input y hY z hZ504  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, c, cNat, d, dNat, n, nNat, nNonzero, inputFirst, outputFirst⟩ := rationalAdd.factors with hY505  obtain ⟨a2, a2Nat, b2, b2Nat, m2, m2Nat, m2Nonzero, c2, c2Nat, d2, d2Nat, n2, n2Nat, n2Nonzero, inputSecond, outputSecond⟩ := rationalAdd.factors with hZ506  rw inputFirst at inputSecond507  have inputs := orderedPair.injective at508    rationalClass(a, b, m), rationalClass(c, d, n),509    rationalClass(a2, b2, m2), rationalClass(c2, d2, n2)510  specialize inputs with inputSecond511  rcases inputs with ⟨leftSame, rightSame⟩512  have leftEquivalent := rationalClass.equivalent_of_eq with513    aNat, bNat, mNat, a2Nat, b2Nat, m2Nat, mNonzero, m2Nonzero, leftSame514  have rightEquivalent := rationalClass.equivalent_of_eq with515    cNat, dNat, nNat, c2Nat, d2Nat, n2Nat, nNonzero, n2Nonzero, rightSame516  have sameSum := rationalClassSum.well_defined at517    a, b, m, a2, b2, m2, c, d, n, c2, d2, n2518  specialize sameSum with519    mNonzero, m2Nonzero, nNonzero, n2Nonzero, leftEquivalent, rightEquivalent520  rwa [outputFirst, outputSecond]521522theorem rationalAdd.function523  shows rationalAdd : ℚ × ℚ → ℚ524proof525  constructor526    intros p hp527    simp [rationalAdd.membership] at hp528    rcases hp with ⟨bounded, witnesses⟩529    exact bounded530  . constructor531    . exact rationalAdd.functional532    . exact rationalAdd.total533534theorem rationalMul.relates (a b m c d n : Nat)535  requires mNonzero : m ≠ 0536  requires nNonzero : n ≠ 0537  shows relates(rationalMul,538    (rationalClass(a, b, m), rationalClass(c, d, n)),539    rationalClassMul(a, b, m, c, d, n))540proof541  unfold relates542  apply rationalMul.membership.backward at543    ((rationalClass(a, b, m), rationalClass(c, d, n)) ↦544      rationalClassMul(a, b, m, c, d, n))545  constructor546  . apply product.pair at547      (rationalClass(a, b, m), rationalClass(c, d, n)),548      rationalClassMul(a, b, m, c, d, n), ℚ × ℚ, ℚ549    . apply product.pair at rationalClass(a, b, m), rationalClass(c, d, n), ℚ, ℚ550      . have left := rationalClass.rational at a, b, m with mNonzero551        exact left552      . have right := rationalClass.rational at c, d, n with nNonzero553        exact right554    . have product := rationalClassMul.rational at a, b, m, c, d, n555      specialize product with *{2}556      exact product557  refine ⟨a, assumption, b, assumption, m, assumption, mNonzero, c, assumption, d, assumption, n, assumption, nNonzero, rfl⟩558559theorem rationalMul.factors (x y : Set)560  requires h : relates(rationalMul, x, y)561  shows ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ m, Nat(m) ∧ m ≠ 0 ∧562    ∃ c, Nat(c) ∧ ∃ d, Nat(d) ∧ ∃ n, Nat(n) ∧ n ≠ 0 ∧563      x = (rationalClass(a, b, m), rationalClass(c, d, n)) ∧564      y = rationalClassMul(a, b, m, c, d, n)565proof566  unfold relates at h567  simp [rationalMul.membership] at h568  rcases h with ⟨bounded, a, aNat, b, bNat, m, mNat, mNonzero, c, cNat, d, dNat, n, nNat, nNonzero, shape⟩569  have coordinates := orderedPair.injective at x, y,570    (rationalClass(a, b, m), rationalClass(c, d, n)),571    rationalClassMul(a, b, m, c, d, n)572  specialize coordinates with shape573  rcases coordinates with ⟨inputShape, outputShape⟩574  refine ⟨a, aNat, b, bNat, m, mNat, mNonzero, c, cNat, d, dNat, n, nNat, nNonzero, inputShape, outputShape⟩575576theorem rationalMul.total577  shows TotalBetween(rationalMul, ℚ × ℚ, ℚ)578proof579  intros input hInput580  obtain ⟨bounded, q, qRational, r, rRational, inputShape⟩ := product.membership.forward with hInput581  have qTyped : Rational(q) by exact qRational582  have rTyped : Rational(r) by exact rRational583  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, qShape⟩ := Rational.coordinates with qTyped584  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, rShape⟩ := Rational.coordinates with rTyped585  witness rationalClassMul(a, b, m, c, d, n)586  constructor587  . exact rationalClassMul.rational at a, b, m, c, d, n with mNonzero, nNonzero588  . rw [inputShape, qShape, rShape]589    exact rationalMul.relates with aNat, bNat, mNat, cNat, dNat, nNat, mNonzero, nNonzero590591theorem rationalMul.functional592  shows Functional(rationalMul)593proof594  intros input y hY z hZ595  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, c, cNat, d, dNat, n, nNat, nNonzero, inputFirst, outputFirst⟩ := rationalMul.factors with hY596  obtain ⟨a2, a2Nat, b2, b2Nat, m2, m2Nat, m2Nonzero, c2, c2Nat, d2, d2Nat, n2, n2Nat, n2Nonzero, inputSecond, outputSecond⟩ := rationalMul.factors with hZ597  rw inputFirst at inputSecond598  have inputs := orderedPair.injective at599    rationalClass(a, b, m), rationalClass(c, d, n),600    rationalClass(a2, b2, m2), rationalClass(c2, d2, n2)601  specialize inputs with inputSecond602  rcases inputs with ⟨leftSame, rightSame⟩603  have leftEquivalent := rationalClass.equivalent_of_eq with604    aNat, bNat, mNat, a2Nat, b2Nat, m2Nat, mNonzero, m2Nonzero, leftSame605  have rightEquivalent := rationalClass.equivalent_of_eq with606    cNat, dNat, nNat, c2Nat, d2Nat, n2Nat, nNonzero, n2Nonzero, rightSame607  have sameProduct := rationalClassMul.well_defined at608    a, b, m, a2, b2, m2, c, d, n, c2, d2, n2609  specialize sameProduct with610    mNonzero, m2Nonzero, nNonzero, n2Nonzero, leftEquivalent, rightEquivalent611  rwa [outputFirst, outputSecond]612613theorem rationalMul.function614  shows rationalMul : ℚ × ℚ → ℚ615proof616  constructor617    intros p hp618    simp [rationalMul.membership] at hp619    rcases hp with ⟨bounded, witnesses⟩620    exact bounded621  . constructor622    . exact rationalMul.functional623    . exact rationalMul.total624625instance rationalAdd.operation626  shows AddOperation(ℚ, rationalAdd)627proof628  exact rationalAdd.function629630instance rationalMul.operation631  shows MulOperation(ℚ, rationalMul)632proof633  exact rationalMul.function634635instance rationalNeg.operation636  shows NegOperation(ℚ, rationalNeg)637proof638  exact rationalNeg.function639640instance rationalZero.of_nat641  shows OfNat(ℚ, 0, rationalZero)642proof643  constructor644  . typecheck645  . exact rationalZero.rational646647instance rationalOne.of_nat648  shows OfNat(ℚ, 1, rationalOne)649proof650  constructor651  . typecheck652  . exact rationalOne.rational653654notation infixl 60 "+" => call2 via AddOperation(ℚ, _) for Rational655notation infixl 70 "*" => call2 via MulOperation(ℚ, _) for Rational656notation prefix 75 "-" => apply via NegOperation(ℚ, _) for Rational657notation numeral "0" via OfNat(ℚ, 0, _) for Rational658notation numeral "1" via OfNat(ℚ, 1, _) for Rational659def rationalSubValue (x y : Rational) : Rational := x + (-y)660notation infixl 60 "-" => rationalSubValue for Rational661662-- Compatibility equations connect the instance-selected graph presentation663-- to the established public value names.664theorem rationalAddValue.notation (x y : Set)665  shows rationalAdd(x, y) = rationalAddValue(x, y)666proof667  unfold call2668  unfold rationalAddValue669  rfl670671theorem rationalMulValue.notation (x y : Set)672  shows rationalMul(x, y) = rationalMulValue(x, y)673proof674  unfold call2675  unfold rationalMulValue676  rfl677678theorem rationalNegValue.notation (x : Set)679  shows rationalNeg(x) = rationalNegValue(x)680proof681  unfold rationalNegValue682  rfl683684theorem rationalNegValue.rational (x : Rational)685  shows Rational(-x)686proof687  rw rationalNegValue.notation688  have xMember : x ∈ ℚ by simp [Rational]689  obtain ⟨y, yMember, mapped⟩ := FunctionBetween.exists_value with rationalNeg.function, xMember690  have applied := FunctionBetween.apply_value with rationalNeg.function, mapped691  unfold rationalNegValue692  rw applied693  exact yMember694695theorem rationalNegValue.classes (a b m : Nat)696  requires mNonzero : m ≠ 0697  shows rationalNegValue(rationalClass(a, b, m)) = rationalClassNeg(a, b, m)698proof699  have input := rationalClass.rational at a, b, m with700    *{3}, mNonzero701  have inputMember := input702  unfold Rational at inputMember703  have mapped := rationalNeg.relates at a, b, m with704    *{3}, mNonzero705  unfold rationalNegValue706  exact FunctionBetween.apply_value with rationalNeg.function, inputMember, mapped707708theorem rationalAddValue.rational (x y : Rational)709  shows Rational(x + y)710proof711  rw rationalAddValue.notation712  have xMember : x ∈ ℚ by simp [Rational]713  have yMember : y ∈ ℚ by simp [Rational]714  have inputMember := product.pair with xMember, yMember715  obtain ⟨z, zMember, mapped⟩ := FunctionBetween.exists_value with rationalAdd.function, inputMember716  have applied := FunctionBetween.apply_value with rationalAdd.function, inputMember, mapped717  unfold rationalAddValue718  rw applied719  exact zMember720721theorem rationalMulValue.rational (x y : Rational)722  shows Rational(x * y)723proof724  rw rationalMulValue.notation725  have xMember : x ∈ ℚ by simp [Rational]726  have yMember : y ∈ ℚ by simp [Rational]727  have inputMember := product.pair with xMember, yMember728  obtain ⟨z, zMember, mapped⟩ := FunctionBetween.exists_value with rationalMul.function, inputMember729  have applied := FunctionBetween.apply_value with rationalMul.function, inputMember, mapped730  unfold rationalMulValue731  rw applied732  exact zMember733734theorem rationalNegValue.rational_raw (x : Rational)735  shows Rational(rationalNegValue(x))736proof737  have result := rationalNegValue.rational at x738  rwa rationalNegValue.notation at result739740theorem rationalAddValue.rational_raw (x y : Rational)741  shows Rational(rationalAddValue(x, y))742proof743  have result := rationalAddValue.rational at x, y with *744  rwa rationalAddValue.notation at result745746theorem rationalMulValue.rational_raw (x y : Rational)747  shows Rational(rationalMulValue(x, y))748proof749  have result := rationalMulValue.rational at x, y with *750  rwa rationalMulValue.notation at result751752-- The public operations compute by choosing the unique graph value. These753-- equations let a proof move cleanly between quotient notation and a concrete754-- representative calculation without unfolding the function graph.755theorem rationalAddValue.classes (a b m c d n : Nat)756  requires mNonzero : m ≠ 0757  requires nNonzero : n ≠ 0758  shows rationalAddValue(rationalClass(a, b, m), rationalClass(c, d, n)) =759    rationalClassSum(a, b, m, c, d, n)760proof761  have left := rationalClass.rational at a, b, m with *762  have right := rationalClass.rational at c, d, n with *763  have input := product.pair at764    rationalClass(a, b, m), rationalClass(c, d, n), ℚ, ℚ765  specialize input with left, right766  have mapped := rationalAdd.relates at a, b, m, c, d, n with767    *{6},768    mNonzero, nNonzero769  unfold rationalAddValue770  exact FunctionBetween.apply_value with rationalAdd.function, input, mapped771772theorem rationalMulValue.classes (a b m c d n : Nat)773  requires mNonzero : m ≠ 0774  requires nNonzero : n ≠ 0775  shows rationalMulValue(rationalClass(a, b, m), rationalClass(c, d, n)) =776    rationalClassMul(a, b, m, c, d, n)777proof778  have left := rationalClass.rational at a, b, m with *779  have right := rationalClass.rational at c, d, n with *780  have input := product.pair at781    rationalClass(a, b, m), rationalClass(c, d, n), ℚ, ℚ782  specialize input with left, right783  have mapped := rationalMul.relates at a, b, m, c, d, n with784    *{6},785    mNonzero, nNonzero786  unfold rationalMulValue787  exact FunctionBetween.apply_value with rationalMul.function, input, mapped788789theorem rationalAddValue.commutative (x y : Rational)790  shows x + y = y + x791proof792  rw [rationalAddValue.notation, rationalAddValue.notation]793  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=794    Rational.coordinates at x with assumption795  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, yShape⟩ :=796    Rational.coordinates at y with assumption797  have mnNonzero := mul.nonzero with mNonzero, nNonzero798  rw [xShape, yShape, rationalAddValue.classes, rationalAddValue.classes]799  exact rationalClassSum.commutative with aNat, bNat, mNat, cNat, dNat, nNat, mNonzero, nNonzero800801theorem rationalAddValue.zero_right (x : Rational)802  shows x + 0 = x803proof804  rw rationalAddValue.notation805  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=806    Rational.coordinates with assumption807  have zeroNat : Nat(0) by typecheck808  have oneNat : Nat(1) by typecheck809  have oneNonzero : 1 ≠ 0810    intro oneZero811    arith812  have computed := rationalAddValue.classes with813    aNat, bNat, mNat, zeroNat, zeroNat, oneNat, mNonzero, oneNonzero814  have identity := rationalClassSum.zero_right with aNat, bNat, mNat, mNonzero815  have computedZero : rationalAddValue(rationalClass(a, b, m), rationalZero) = rationalClassSum(a, b, m, 0, 0, 1)816    simpa [rationalZero] using computed817  have classIdentity : rationalAddValue(rationalClass(a, b, m), rationalZero) = rationalClass(a, b, m)818    calc819      rationalAddValue(rationalClass(a, b, m), rationalZero) =820        rationalClassSum(a, b, m, 0, 0, 1) := computedZero821      _ = rationalClass(a, b, m) := identity822  simpa [xShape] using classIdentity823824theorem rationalAddValue.zero_left (x : Rational)825  shows 0 + x = x826proof827  calc828    rationalZero + x = x + rationalZero :=829      rationalAddValue.commutative at rationalZero, x with830        rationalZero.rational, assumption831    _ = x := rationalAddValue.zero_right at x with assumption832833theorem rationalAddValue.neg_right (x : Rational)834  shows x + (-x) = 0835proof836  rw [rationalAddValue.notation, rationalNegValue.notation]837  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=838    Rational.coordinates with assumption839  have negative := rationalNegValue.classes with aNat, bNat, mNat, mNonzero840  have sum := rationalAddValue.classes with aNat, bNat, mNat, bNat, aNat, mNat, mNonzero, mNonzero841  have sumNegative : rationalAddValue(rationalClass(a, b, m), rationalClassNeg(a, b, m)) = rationalClassSum(a, b, m, b, a, m)842    simpa [rationalClassNeg] using sum843  have inverse := rationalClassSum.neg_right with aNat, bNat, mNat, mNonzero844  have classInverse : rationalAddValue(rationalClass(a, b, m), rationalNegValue(rationalClass(a, b, m))) = rationalZero845    rwa [negative, sumNegative]846  simpa [xShape] using classInverse847848theorem rationalAddValue.neg_left (x : Rational)849  shows (-x) + x = 0850proof851  calc852    (-x) + x = x + (-x) :=853      rationalAddValue.commutative at -x, x with854        rationalNegValue.rational with *{2}855    _ = rationalZero := rationalAddValue.neg_right at x with assumption856857theorem rationalAddValue.associative (x y z : Rational)858  shows (x + y) + z = x + (y + z)859proof860  rw [rationalAddValue.notation, rationalAddValue.notation, rationalAddValue.notation, rationalAddValue.notation]861  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=862    Rational.coordinates at x with assumption863  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, yShape⟩ :=864    Rational.coordinates at y with assumption865  obtain ⟨e, eNat, f, fNat, k, kNat, kNonzero, zShape⟩ :=866    Rational.coordinates at z with assumption867  have leftNumeratorNat : Nat(n * a + m * c) by typecheck868  have leftDenumeratorNat : Nat(n * b + m * d) by typecheck869  have mnNat : Nat(m * n) by typecheck870  have rightNumeratorNat : Nat(k * c + n * e) by typecheck871  have rightDenumeratorNat : Nat(k * d + n * f) by typecheck872  have nkNat : Nat(n * k) by typecheck873  have mnNonzero := mul.nonzero with mNat, nNat, mNonzero, nNonzero874  have nkNonzero := mul.nonzero with nNat, kNat, nNonzero, kNonzero875  have leftOuterClasses := rationalAddValue.classes with876    leftNumeratorNat, leftDenumeratorNat, mnNat, eNat, fNat, kNat, mnNonzero, kNonzero877  have leftOuter : rationalAddValue(rationalClassSum(a, b, m, c, d, n), rationalClass(e, f, k)) = rationalClassSum(n * a + m * c, n * b + m * d, m * n, e, f, k)878    simpa [rationalClassSum] using leftOuterClasses879  have rightOuterClasses := rationalAddValue.classes with880    aNat, bNat, mNat, rightNumeratorNat, rightDenumeratorNat, nkNat, mNonzero, nkNonzero881  have rightOuter : rationalAddValue(rationalClass(a, b, m), rationalClassSum(c, d, n, e, f, k)) = rationalClassSum(a, b, m, k * c + n * e, k * d + n * f, n * k)882    simpa [rationalClassSum] using rightOuterClasses883  rw [xShape, yShape, zShape, rationalAddValue.classes, rationalAddValue.classes, leftOuter, rightOuter]884  exact rationalClassSum.associative with885    aNat, bNat, mNat, cNat, dNat, nNat, eNat, fNat, kNat, mNonzero, nNonzero, kNonzero886887theorem rationalMulValue.commutative (x y : Rational)888  shows x * y = y * x889proof890  rw [rationalMulValue.notation, rationalMulValue.notation]891  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=892    Rational.coordinates at x with assumption893  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, yShape⟩ :=894    Rational.coordinates at y with assumption895  rw [xShape, yShape, rationalMulValue.classes, rationalMulValue.classes]896  exact rationalClassMul.commutative with mNonzero, nNonzero897898theorem rationalMulValue.associative (x y z : Rational)899  shows (x * y) * z = x * (y * z)900proof901  rw [rationalMulValue.notation, rationalMulValue.notation, rationalMulValue.notation, rationalMulValue.notation]902  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=903    Rational.coordinates at x with assumption904  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, yShape⟩ :=905    Rational.coordinates at y with assumption906  obtain ⟨e, eNat, f, fNat, k, kNat, kNonzero, zShape⟩ :=907    Rational.coordinates at z with assumption908  have leftNumeratorNat : Nat(a * c + b * d) by typecheck909  have leftDenominatorNat : Nat(a * d + b * c) by typecheck910  have mnNat : Nat(m * n) by typecheck911  have rightNumeratorNat : Nat(c * e + d * f) by typecheck912  have rightDenominatorNat : Nat(c * f + d * e) by typecheck913  have nkNat : Nat(n * k) by typecheck914  have mnNonzero := mul.nonzero with mNat, nNat, mNonzero, nNonzero915  have nkNonzero := mul.nonzero with nNat, kNat, nNonzero, kNonzero916  have leftOuterClasses := rationalMulValue.classes with917    leftNumeratorNat, leftDenominatorNat, mnNat, eNat, fNat, kNat, mnNonzero, kNonzero918  have leftOuter : rationalMulValue(919      rationalClassMul(a, b, m, c, d, n), rationalClass(e, f, k)) =920      rationalClassMul(a * c + b * d, a * d + b * c, m * n, e, f, k)921    simpa [rationalClassMul] using leftOuterClasses922  have rightOuterClasses := rationalMulValue.classes with923    aNat, bNat, mNat, rightNumeratorNat, rightDenominatorNat, nkNat, mNonzero, nkNonzero924  have rightOuter : rationalMulValue(925      rationalClass(a, b, m), rationalClassMul(c, d, n, e, f, k)) =926      rationalClassMul(a, b, m,927        c * e + d * f, c * f + d * e, n * k)928    simpa [rationalClassMul] using rightOuterClasses929  rw [xShape, yShape, zShape, rationalMulValue.classes, rationalMulValue.classes, leftOuter, rightOuter]930  exact rationalClassMul.associative with mNonzero, nNonzero, kNonzero931932theorem rationalMulValue.one_right (x : Rational)933  shows x * rationalOne = x934proof935  rw rationalMulValue.notation936  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=937    Rational.coordinates with assumption938  have oneNonzero : 1 ≠ 0939    intro oneZero940    arith941  rw xShape942  unfold rationalOne943  have computed := rationalMulValue.classes at944    a, b, m, 1, 0, 1 with mNonzero, oneNonzero945  rw computed946  exact rationalClassMul.one_right with mNonzero947948theorem rationalMulValue.one_left (x : Rational)949  shows rationalOne * x = x950proof951  calc952    rationalOne * x = x * rationalOne :=953      rationalMulValue.commutative at rationalOne, x with954        rationalOne.rational, assumption955    _ = x := rationalMulValue.one_right at x with assumption956957theorem rationalMulValue.zero_right (x : Rational)958  shows x * rationalZero = rationalZero959proof960  rw rationalMulValue.notation961  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=962    Rational.coordinates with assumption963  have oneNonzero : 1 ≠ 0964    intro oneZero965    arith966  rw xShape967  unfold rationalZero968  rw rationalMulValue.classes969  unfold rationalClassMul970  apply rationalClass.eq971  . exact mul.nonzero with mNonzero, oneNonzero972  . exact oneNonzero973  . ring974975theorem rationalMulValue.zero_left (x : Rational)976  shows rationalZero * x = rationalZero977proof978  calc979    rationalZero * x = x * rationalZero :=980      rationalMulValue.commutative at rationalZero, x with981        rationalZero.rational, assumption982    _ = rationalZero := rationalMulValue.zero_right at x with assumption983984theorem rationalMulValue.neg_right (x y : Rational)985  shows x * (-y) = -(x * y)986proof987  rw [rationalMulValue.notation, rationalNegValue.notation, rationalNegValue.notation, rationalMulValue.notation]988  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=989    Rational.coordinates at x with assumption990  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, yShape⟩ :=991    Rational.coordinates at y with assumption992  have productDenominatorNonzero := mul.nonzero with mNonzero, nNonzero993  rw [xShape, yShape, rationalNegValue.classes]994  unfold rationalClassNeg995  rw rationalMulValue.classes996  unfold rationalClassMul997  rw rationalMulValue.classes998  unfold rationalClassMul999  have negComputed := rationalNegValue.classes at1000    a * c + b * d, a * d + b * c, m * n with1001      productDenominatorNonzero1002  rw negComputed1003  unfold rationalClassNeg1004  apply rationalClass.eq1005  . exact productDenominatorNonzero1006  . exact productDenominatorNonzero1007  . ring10081009theorem rationalMulValue.neg_left (x y : Rational)1010  shows (-x) * y = -(x * y)1011proof1012  have commutativeLeft := rationalMulValue.commutative at -x, y with1013    rationalNegValue.rational with *{2}1014  have commutativeRight := rationalMulValue.commutative at y, x with1015    *{2}1016  rw [commutativeLeft, rationalMulValue.neg_right, commutativeRight]1017  rfl10181019theorem rationalMulValue.distributive_left (x y z : Rational)1020  shows x * (y + z) = x * y + x * z1021proof1022  rw [rationalMulValue.notation, rationalAddValue.notation, rationalMulValue.notation, rationalMulValue.notation, rationalAddValue.notation]1023  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=1024    Rational.coordinates at x with assumption1025  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, yShape⟩ :=1026    Rational.coordinates at y with assumption1027  obtain ⟨e, eNat, f, fNat, k, kNat, kNonzero, zShape⟩ :=1028    Rational.coordinates at z with assumption1029  have nkNonzero := mul.nonzero with nNonzero, kNonzero1030  have mnNonzero := mul.nonzero with mNonzero, nNonzero1031  have mkNonzero := mul.nonzero with mNonzero, kNonzero1032  have sumComputed := rationalAddValue.classes at1033    c, d, n, e, f, k with nNonzero, kNonzero1034  have leftComputed := rationalMulValue.classes at1035    a, b, m, k * c + n * e, k * d + n * f, n * k with1036    mNonzero, nkNonzero1037  have xyComputed := rationalMulValue.classes at1038    a, b, m, c, d, n with mNonzero, nNonzero1039  have xzComputed := rationalMulValue.classes at1040    a, b, m, e, f, k with mNonzero, kNonzero1041  have rightComputed := rationalAddValue.classes at1042    a * c + b * d, a * d + b * c, m * n,1043    a * e + b * f, a * f + b * e, m * k with1044    mnNonzero, mkNonzero1045  rw [xShape, yShape, zShape]1046  calc1047    rationalMulValue(rationalClass(a, b, m),1048      rationalAddValue(rationalClass(c, d, n), rationalClass(e, f, k))) =1049        rationalMulValue(rationalClass(a, b, m),1050          rationalClassSum(c, d, n, e, f, k)) := by simp [sumComputed]1051    _ = rationalClassMul(a, b, m,1052        k * c + n * e, k * d + n * f, n * k) :=1053      by simpa [rationalClassSum] using leftComputed1054    _ = rationalClassSum(1055        a * c + b * d, a * d + b * c, m * n,1056        a * e + b * f, a * f + b * e, m * k) :=1057      rationalClassMul.distributive_left at1058        a, b, m, c, d, n, e, f, k with1059        mNonzero, nNonzero, kNonzero1060    _ = rationalAddValue(1061        rationalClassMul(a, b, m, c, d, n),1062        rationalClassMul(a, b, m, e, f, k)) :=1063      by simpa [rationalClassMul] using rightComputed1064    _ = rationalAddValue(1065        rationalMulValue(rationalClass(a, b, m), rationalClass(c, d, n)),1066        rationalMulValue(rationalClass(a, b, m), rationalClass(e, f, k))) :=1067      by simp [xyComputed, xzComputed]10681069theorem rationalMulValue.distributive_right (x y z : Rational)1070  shows (x + y) * z = x * z + y * z1071proof1072  have sumRational := rationalAddValue.rational at x, y with1073    *{2}1074  have outerCommutative := rationalMulValue.commutative at x + y, z with1075    sumRational, assumption1076  have distributed := rationalMulValue.distributive_left at z, x, y with1077    *{3}1078  have firstCommutative := rationalMulValue.commutative at z, x with1079    *{2}1080  have secondCommutative := rationalMulValue.commutative at z, y with1081    *{2}1082  rw [outerCommutative, distributed, firstCommutative, secondCommutative]1083  rfl10841085theorem rationalSubValue.rational (x y : Rational)1086  shows Rational(x - y)1087proof1088  unfold rationalSubValue1089  exact rationalAddValue.rational at x, -y with1090    assumption, rationalNegValue.rational at y with assumption10911092theorem rationalAddValue.add_sub_cancel_left (x y : Rational)1093  shows x + (y - x) = y1094proof1095  unfold rationalSubValue1096  have associative := rationalAddValue.associative at x, y, -x with1097    *{2}, rationalNegValue.rational at x with assumption1098  have associativeYX := rationalAddValue.associative at y, x, -x with1099    *{2}, rationalNegValue.rational at x with assumption1100  have commutative := rationalAddValue.commutative at x, y with1101    *{2}1102  have inverse := rationalAddValue.neg_right at x1103  have identity := rationalAddValue.zero_right at y1104  have regroup : x + (y + (-x)) = (x + y) + (-x)1105    rw associative1106    rfl1107  have swap : (x + y) + (-x) = (y + x) + (-x)1108    rw commutative1109    rfl1110  have cancel : y + (x + (-x)) = y + rationalZero1111    rw inverse1112    rfl1113  calc1114    x + (y + (-x)) = (x + y) + (-x) := regroup1115    _ = (y + x) + (-x) := swap1116    _ = y + (x + (-x)) := associativeYX1117    _ = y + rationalZero := cancel1118    _ = y := identity11191120theorem rationalAddValue.add_sub_cancel_right (x y : Rational)1121  shows (x + y) - y = x1122proof1123  unfold rationalSubValue1124  have associative := rationalAddValue.associative at x, y, -y with1125    *{2}, rationalNegValue.rational at y with assumption1126  have inverse := rationalAddValue.neg_right at y1127  have identity := rationalAddValue.zero_right at x1128  have cancel : x + (y + (-y)) = x + rationalZero1129    rw inverse1130    rfl1131  calc1132    (x + y) + (-y) = x + (y + (-y)) := associative1133    _ = x + rationalZero := cancel1134    _ = x := identity11351136theorem rationalAddValue.sum_sub_left (x y : Rational)1137  shows (x + y) - x = y1138proof1139  have commutative := rationalAddValue.commutative at x, y with1140    *{2}1141  have swapped : (x + y) - x = (y + x) - x1142    rw commutative1143    rfl1144  calc1145    (x + y) - x = (y + x) - x := swapped1146    _ = y := rationalAddValue.add_sub_cancel_right at y, x with1147      *{2}11481149-- Subtracting a sum from its left summand leaves the negative right summand.1150-- The statement stays at the quotient level; representative arithmetic is1151-- used only as the checked certificate below.1152theorem rationalSubValue.sub_sum_left (x y : Rational)1153  shows x - (x + y) = -y1154proof1155  obtain ⟨a, aNatural, b, bNatural, m, mNatural, mNonzero, xShape⟩ :=1156    Rational.coordinates at x with assumption1157  obtain ⟨c, cNatural, d, dNatural, n, nNatural, nNonzero, yShape⟩ :=1158    Rational.coordinates at y with assumption1159  have mnNonzero := mul.nonzero with mNonzero, nNonzero1160  have sumComputed := rationalAddValue.classes at1161    a, b, m, c, d, n with mNonzero, nNonzero1162  have negSumComputed := rationalNegValue.classes at1163    n * a + m * c, n * b + m * d, m * n with mnNonzero1164  have outerComputed := rationalAddValue.classes at1165    a, b, m,1166    n * b + m * d, n * a + m * c, m * n with1167    mNonzero, mnNonzero1168  have negYComputed := rationalNegValue.classes at c, d, n with nNonzero1169  rw ← rationalAddValue.notation at sumComputed1170  rw ← rationalNegValue.notation at negSumComputed1171  rw ← rationalAddValue.notation at outerComputed1172  rw ← rationalNegValue.notation at negYComputed1173  have negSumShape : rationalNeg(rationalClassSum(a, b, m, c, d, n)) =1174      rationalClassNeg(n * a + m * c, n * b + m * d, m * n)1175    unfold rationalClassSum1176    exact negSumComputed1177  have outerShape : call2(rationalAdd, rationalClass(a, b, m),1178      rationalClassNeg(n * a + m * c, n * b + m * d, m * n)) =1179      rationalClassSum(a, b, m,1180        n * b + m * d, n * a + m * c, m * n)1181    unfold rationalClassNeg1182    exact outerComputed1183  have computedEquality : rationalClass(1184      (m * n) * a + m * (n * b + m * d),1185      (m * n) * b + m * (n * a + m * c),1186      m * (m * n)) = rationalClass(d, c, n)1187    apply rationalClass.eq1188    . exact mul.nonzero at m, m * n with mNonzero, mnNonzero1189    . exact nNonzero1190    . ring1191  simpa [xShape, yShape, rationalSubValue,1192    rationalClassSum, rationalClassNeg] using computedEquality11931194theorem rationalNegValue.involutive (x : Rational)1195  shows -(-x) = x1196proof1197  rw [rationalNegValue.notation, rationalNegValue.notation]1198  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, xShape⟩ :=1199    Rational.coordinates with assumption1200  have first := rationalNegValue.classes with aNat, bNat, mNat, mNonzero1201  have second := rationalNegValue.classes with bNat, aNat, mNat, mNonzero1202  rw [xShape, first]1203  simpa [rationalClassNeg] using second12041205-- The quotient operations form the same checked algebraic interface used by1206-- ring normalization on the reals. All laws above were proved on ℚ.1207instance rationalAdd.comm_monoid1208  shows IsCommMonoid(ℚ, rationalAdd, rationalZero)1209proof1210  constructor1211    constructor1212      constructor1213        exact rationalAdd.function1214        intros A rationalA B rationalB C rationalC1215        have typedA : Rational(A) by typecheck1216        have typedB : Rational(B) by typecheck1217        have typedC : Rational(C) by typecheck1218        simpa [rationalAddValue.notation] using rationalAddValue.associative at A, B, C with typedA, typedB, typedC1219      constructor1220      . exact rationalZero.rational1221      . intros A rationalA1222        have typedA : Rational(A) by typecheck1223        constructor1224        . simpa [rationalAddValue.notation] using rationalAddValue.zero_left at A with typedA1225        . simpa [rationalAddValue.notation] using rationalAddValue.zero_right at A with typedA1226    intros A rationalA B rationalB1227    have typedA : Rational(A) by typecheck1228    have typedB : Rational(B) by typecheck1229    simpa [rationalAddValue.notation] using rationalAddValue.commutative at A, B with typedA, typedB12301231instance rationalAdd.abelian_group1232  shows IsAbelianGroup(ℚ, rationalAdd, rationalZero, rationalNeg)1233proof1234  constructor1235    constructor1236    . have additive := rationalAdd.comm_monoid1237      simp [IsCommMonoid]1238      constructor1239      . exact rationalNeg.function1240      . intros A rationalA1241        have typedA : Rational(A) by typecheck1242        constructor1243        . simpa [rationalAddValue.notation, rationalNegValue.notation] using rationalAddValue.neg_left at A with typedA1244        . simpa [rationalAddValue.notation, rationalNegValue.notation] using rationalAddValue.neg_right at A with typedA1245  . have additive := rationalAdd.comm_monoid1246    simp [IsCommMonoid]12471248instance rationalMul.monoid1249  shows IsMonoid(ℚ, rationalMul, rationalOne)1250proof1251  constructor1252    constructor1253      exact rationalMul.function1254      intros A rationalA B rationalB C rationalC1255      have typedA : Rational(A) by typecheck1256      have typedB : Rational(B) by typecheck1257      have typedC : Rational(C) by typecheck1258      simpa [rationalMulValue.notation] using rationalMulValue.associative at A, B, C with typedA, typedB, typedC1259    constructor1260    . exact rationalOne.rational1261    . intros A rationalA1262      have typedA : Rational(A) by typecheck1263      constructor1264      . simpa [rationalMulValue.notation] using rationalMulValue.one_left at A with typedA1265      . simpa [rationalMulValue.notation] using rationalMulValue.one_right at A with typedA12661267instance rationalMul.distributive1268  shows Distributive(ℚ, rationalAdd, rationalMul)1269proof1270  intros A rationalA B rationalB C rationalC1271  have typedA : Rational(A) by typecheck1272  have typedB : Rational(B) by typecheck1273  have typedC : Rational(C) by typecheck1274  constructor1275  . simpa [rationalAddValue.notation, rationalMulValue.notation] using rationalMulValue.distributive_left at A, B, C with typedA, typedB, typedC1276  . simpa [rationalAddValue.notation, rationalMulValue.notation] using rationalMulValue.distributive_right at A, B, C with typedA, typedB, typedC12771278instance rationalMul.commutative1279  shows Commutative(ℚ, rationalMul)1280proof1281  intros A rationalA B rationalB1282  have typedA : Rational(A) by typecheck1283  have typedB : Rational(B) by typecheck1284  simpa [rationalMulValue.notation] using rationalMulValue.commutative at A, B with typedA, typedB12851286instance rationals.comm_ring1287  shows IsCommRing(ℚ, rationalAdd, rationalZero, rationalNeg, rationalMul, rationalOne)1288proof1289  constructor1290    constructor1291    . exact rationalAdd.abelian_group1292    . constructor1293      . exact rationalMul.monoid1294      . exact rationalMul.distributive1295  . exact rationalMul.commutative1296