Grace/Cumulus/Real/Ring.g17

Open in Workbench Download source

Imports

PositiveMultiplication · Algebra.OrderedAdditive

Declarations

Source

1-- Ring structure of the Dedekind real numbers2-- 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.Ring8import PositiveMultiplication9import Algebra.OrderedAdditive1011-- Distributivity for arbitrary nonnegative cuts.  Linear order leaves only12-- the zero boundary cases and the genuinely positive case proved by the13-- approximation argument in PositiveMultiplication.14theorem realPosMulCut.distributive_of_nonnegative (A B C : Real)15  requires nonnegativeA : realZero ⊆ A16  requires nonnegativeB : realZero ⊆ B17  requires nonnegativeC : realZero ⊆ C18  shows realPosMulCut(A, realAddCut(B, C)) =19    realAddCut(realPosMulCut(A, B), realPosMulCut(A, C))20proof21  have casesA := Real.nonnegative_cases with nonnegativeA22  have casesB := Real.nonnegative_cases with nonnegativeB23  have casesC := Real.nonnegative_cases with nonnegativeC24  cases casesA with zeroA | positiveA25  . simp [zeroA, realPosMulCut.zero_left,26      realAddCut.zero_left, realAddCut.zero_right]27  . cases casesB with zeroB | positiveB28    . simp [zeroB, realPosMulCut.zero_left, realPosMulCut.zero_right,29        realAddCut.zero_left, realAddCut.zero_right]30    . cases casesC with zeroC | positiveC31      . simp [zeroC, realPosMulCut.zero_left, realPosMulCut.zero_right,32          realAddCut.zero_left, realAddCut.zero_right]33      . exact realPosMulCut.distributive_of_positive at A, B, C with34          *{3},35          positiveA, positiveB, positiveC3637-- Non-strict translation laws for the cut order.  The strict versions live in38-- Negation; these forms are the convenient boundary for sign arithmetic.39theorem realAddValue.subset_right (A B C : Real)40  requires subset : A ⊆ B41  shows A + C ⊆ B + C42proof43  have cutSubset := realAddCut.subset_left at A, B, C with44    *{3}, subset45  have leftCut := realAddValue.cut at A, C with *46  have rightCut := realAddValue.cut at B, C with *47  rwa [← leftCut, ← rightCut] at cutSubset4849theorem realAddValue.subset_left (A B C : Real)50  requires subset : A ⊆ B51  shows C + A ⊆ C + B52proof53  have translated := realAddValue.subset_right at A, B, C with54    *{3}, subset55  have leftCommutative := realAddValue.commutative at A, C with56    *{2}57  have rightCommutative := realAddValue.commutative at B, C with58    *{2}59  rwa [leftCommutative, rightCommutative] at translated6061-- The typed non-strict order inherits its familiar algebraic laws directly62-- from inclusion of Dedekind cuts.63theorem realLe.reflexive (A : Real)64  shows A ≤ A65proof66  exact realLe.of_subset at A, A with67    *{2}, Subset.reflexive at A6869theorem realLe.transitive (A B C : Real)70  requires ab : A ≤ B71  requires bc : B ≤ C72  shows A ≤ C73proof74  have subsetAB := realLe.subset at A, B with *75  have subsetBC := realLe.subset at B, C with *76  have subsetAC := Subset.transitive with subsetAB, subsetBC77  exact realLe.of_subset with *7879theorem realLe.add_right (A B C : Real)80  requires le : A ≤ B81  shows A + C ≤ B + C82proof83  have subset := realLe.subset with *84  have translated := realAddValue.subset_right at A, B, C with85    *{3}, subset86  exact realLe.of_subset with translated8788theorem realLe.add_left (A B C : Real)89  requires le : A ≤ B90  shows C + A ≤ C + B91proof92  have subset := realLe.subset with *93  have translated := realAddValue.subset_left at A, B, C with94    *{3}, subset95  exact realLe.of_subset with translated9697theorem realLe.add (A B C D : Real)98  requires ab : A ≤ B99  requires cd : C ≤ D100  shows A + C ≤ B + D101proof102  have first := realLe.add_right at A, B, C with103    *{3}, ab104  have second := realLe.add_left at C, D, B with105    *{3}, cd106  exact realLe.transitive with first, second107108theorem realSubValue.le_left (X Y Z : Real)109  requires le : X ≤ Y110  shows X - Z ≤ Y - Z111proof112  have negative := realNegValue.real at Z113  have shifted := realLe.add_right at X, Y, -Z with114    *{2}, negative, le115  unfold realSubValue116  exact shifted117118theorem realSubValue.lt_left (X Y Z : Real)119  requires lt : X < Y120  shows X - Z < Y - Z121proof122  have negative := realNegValue.real at Z123  have shifted := realLess.add_right at X, Y, -Z with124    *{2}, negative, lt125  unfold realSubValue126  exact shifted127128theorem realAddValue.four_shuffle (A B C D : Real)129  shows (A + B) + (C + D) = (A + C) + (B + D)130proof131  have cdReal := realAddValue.real at C, D with *132  have bdReal := realAddValue.real at B, D with *133  have outerLeft := realAddValue.associative at A, B, C + D with134    *{2}, cdReal135  have middleLeft := realAddValue.associative at B, C, D with136    *{3}137  have swap := realAddValue.commutative at B, C with *138  have middleRight := realAddValue.associative at C, B, D with139    *{3}140  have outerRight := realAddValue.associative at A, C, B + D with141    *{2}, bdReal142  cc143144theorem realLess.implies_le (A B : Real)145  requires less : A < B146  shows A ≤ B147proof148  obtain ⟨realA, realB, proper⟩ := realLess.characterization.forward with less149  have subset := ProperSubset.subset with proper150  exact realLe.of_subset with subset151152theorem realLess.of_not_le (A B : Real)153  requires notLe : ¬(A ≤ B)154  shows B < A155proof156  have distinct : A ≠ B157    intro equal158    apply notLe159    rw equal160    exact realLe.reflexive with assumption161  have connected := realLess.connected_on162  have alternatives := connected with A, B, distinct163  cases alternatives with forward | reverse164  . exfalso165    apply notLe166    exact realLess.implies_le with forward167  . exact reverse168169theorem realLe.transitive_less (A B C : Real)170  requires ab : A ≤ B171  requires bc : B < C172  shows A < C173proof174  have subsetAB := realLe.subset with *175  obtain ⟨realB, realC, properBC⟩ := realLess.characterization.forward with bc176  have subsetBC := ProperSubset.subset with properBC177  have subsetAC := Subset.transitive with subsetAB, subsetBC178  have properAC : A ⊂ C179    constructor180    . exact subsetAC181    . intro equalAC182      apply ProperSubset.ne with properBC183      apply Subset.antisymmetric184      . exact subsetBC185      . rw ← equalAC186        exact subsetAB187  apply realLess.characterization.backward188  unfold RealLess189  tauto190191theorem realLe.neg_reverse (A B : Real)192  requires ordered : A ≤ B193  shows -B ≤ -A194proof195  by_contra notOrdered196  have strictNeg := realLess.of_not_le with notOrdered197  have strictNegView := realLess.characterization.forward with strictNeg198  have reversedView := RealLess.neg_reverse with strictNegView199  have reversed := realLess.characterization.backward with reversedView200  have involutiveA := realNegValue.involutive at A201  have involutiveB := realNegValue.involutive at B202  rw [involutiveA, involutiveB] at reversed203  have cycle := realLe.transitive_less with ordered, reversed204  have irreflexive := realLess.irreflexive_on205  exact irreflexive with A, cycle206207theorem realSubValue.le (A B C D : Real)208  requires left : A ≤ C209  requires right : D ≤ B210  shows A - B ≤ C - D211proof212  have reversed := realLe.neg_reverse with right213  have combined := realLe.add at A, C, -B, -D with214    *{2},215    realNegValue.real at B with assumption,216    realNegValue.real at D with assumption,217    left, reversed218  unfold realSubValue219  exact combined220221theorem realLess.transitive_le (A B C : Real)222  requires ab : A < B223  requires bc : B ≤ C224  shows A < C225proof226  obtain ⟨realA, realB, properAB⟩ := realLess.characterization.forward with ab227  have subsetAB := ProperSubset.subset with properAB228  have subsetBC := realLe.subset with *229  have subsetAC := Subset.transitive with subsetAB, subsetBC230  have properAC : A ⊂ C231    constructor232    . exact subsetAC233    . intro equalAC234      apply ProperSubset.ne with properAB235      apply Subset.antisymmetric236      . exact subsetAB237      . rw equalAC238        exact subsetBC239  apply realLess.characterization.backward240  unfold RealLess241  tauto242243theorem realAddValue.nonnegative (A B : Real)244  requires nonnegativeA : realZero ⊆ A245  requires nonnegativeB : realZero ⊆ B246  shows realZero ⊆ A + B247proof248  have translated := realAddValue.subset_left at realZero, B, A with249    realZero.real, *{2}, nonnegativeB250  rw realAddValue.zero_right at translated251  exact Subset.transitive with nonnegativeA, translated252253theorem realSubValue.add_right_cancel (A B : Real)254  shows (A - B) + B = A255proof256  unfold realSubValue257  have negBReal := realNegValue.real at B258  calc259    (A + (-B)) + B = A + ((-B) + B) :=260      realAddValue.associative at A, -B, B with261        assumption, negBReal, assumption262    _ = A + 0 := by simp [realAddValue.neg_left]263    _ = A := realAddValue.zero_right at A with assumption264265theorem realSubValue.nonnegative_of_subset (A B : Real)266  requires subset : A ⊆ B267  shows realZero ⊆ B - A268proof269  have negAReal := realNegValue.real at A270  have translated := realAddValue.subset_right at A, B, -A with271    *{2}, negAReal, subset272  rw realAddValue.neg_right at translated273  unfold realSubValue274  exact translated275276theorem realSubValue.nonnegative_of_le (X Y : Real)277  requires le : X ≤ Y278  shows (0:R) ≤ Y - X279proof280  have subset := realLe.subset with *281  have nonnegative := realSubValue.nonnegative_of_subset with subset282  exact realLe.of_subset with realZero.real, nonnegative283284instance reals.ordered_additive_group285  shows OrderedAdditiveGroup(ℝ, realAdd, realZero, realNeg, realLe)286proof287  constructor288  . exact realAdd.abelian_group289  . constructor290      intros x hx291      exact realLe.reflexive292    . constructor293        intros x hx y hy z hz xy yz294        exact realLe.transitive with xy, yz295      . constructor296        . intros x hx y hy z hz w hw xy zw297          exact realLe.add with xy, zw298        . constructor299          . intros x hx y hy xy300            exact realLe.neg_reverse with xy301          . intros x hx y hy xy302            have positive := realSubValue.nonnegative_of_le with xy303            unfold realSubValue at positive304            exact positive305306theorem realMulValue.distributive_of_nonnegative (A B C : Real)307  requires nonnegativeA : realZero ⊆ A308  requires nonnegativeB : realZero ⊆ B309  requires nonnegativeC : realZero ⊆ C310  shows A * (B + C) = A * B + A * C311proof312  have sumReal := realAddValue.real at B, C with *313  have abReal := realMulValue.real at A, B with *314  have acReal := realMulValue.real at A, C with *315  have sumNonnegative := realAddValue.nonnegative with nonnegativeB, nonnegativeC316  have leftCut := realMulValue.cut at A, B + C with assumption, sumReal317  have sumCut := realAddValue.cut at B, C with *318  have abCut := realMulValue.cut at A, B with *319  have acCut := realMulValue.cut at A, C with *320  have rightCut := realAddValue.cut with abReal, acReal321  have leftReduction := realMulCut.of_nonnegative at A, B + C with322    assumption, sumReal, nonnegativeA, sumNonnegative323  have abReduction := realMulCut.of_nonnegative with nonnegativeA, nonnegativeB324  have acReduction := realMulCut.of_nonnegative with nonnegativeA, nonnegativeC325  have sumShape : realPosMulCut(A, B + C) =326      realPosMulCut(A, realAddCut(B, C))327    rw sumCut328    rfl329  have productsReduce : realAddCut(330      realPosMulCut(A, B), realPosMulCut(A, C)) =331      realAddCut(realMulCut(A, B), realMulCut(A, C))332    rw [abReduction, acReduction]333    rfl334  have productsShape : realAddCut(335      realMulCut(A, B), realMulCut(A, C)) =336      realAddCut(A * B, A * C)337    rw [abCut, acCut]338    rfl339  have resultShape : realAddCut(A * B, A * C) = A * B + A * C340    rw rightCut341    rfl342  calc343    A * (B + C) = realMulCut(A, B + C) := leftCut344    _ = realPosMulCut(A, B + C) := leftReduction345    _ = realPosMulCut(A, realAddCut(B, C)) := sumShape346    _ = realAddCut(realPosMulCut(A, B), realPosMulCut(A, C)) :=347      realPosMulCut.distributive_of_nonnegative at A, B, C with348        *{3},349        nonnegativeA, nonnegativeB, nonnegativeC350    _ = realAddCut(realMulCut(A, B), realMulCut(A, C)) := productsReduce351    _ = realAddCut(A * B, A * C) := productsShape352    _ = A * B + A * C := resultShape353354-- Negation is additive.  We prove this through uniqueness of inverses in the355-- already established additive group; the calculation is the familiar356-- rearrangement (-A-B)+(A+B)=0.357theorem realNegValue.add (A B : Real)358  shows -(A + B) = (-A) + (-B)359proof360  have negAReal := realNegValue.real at A361  have negBReal := realNegValue.real at B362  have sumReal := realAddValue.real at A, B with *363  have negSumReal := realNegValue.real with sumReal364  have candidateReal := realAddValue.real with negAReal, negBReal365  have innerAssoc := realAddValue.associative at -B, A, B with366    negBReal, *{2}367  have innerComm := realAddValue.commutative at -B, A with368    negBReal, assumption369  have regroup := realAddValue.associative at A, -B, B with370    assumption, negBReal, assumption371  have candidateLeft : ((-A) + (-B)) + (A + B) = 0372    calc373      ((-A) + (-B)) + (A + B) =374          (-A) + ((-B) + (A + B)) :=375        realAddValue.associative at -A, -B, A + B with376          negAReal, negBReal, sumReal377      _ = (-A) + (((-B) + A) + B) := by cc378      _ = (-A) + ((A + (-B)) + B) := by cc379      _ = (-A) + (A + ((-B) + B)) := by cc380      _ = (-A) + (A + 0) := by simp [realAddValue.neg_left]381      _ = (-A) + A := by simp [realAddValue.zero_right]382      _ = 0 := realAddValue.neg_left at A with assumption383  have candidateRight : (A + B) + ((-A) + (-B)) = 0384    calc385      (A + B) + ((-A) + (-B)) = ((-A) + (-B)) + (A + B) :=386        realAddValue.commutative at A + B, (-A) + (-B) with387          sumReal, candidateReal388      _ = 0 := candidateLeft389  have monoid := realAdd.comm_monoid390  have sumInReals := sumReal391  have negSumInReals := negSumReal392  have candidateInReals := candidateReal393  apply IsInverse.unique at394    ℝ, realAdd, realZero, A + B, -(A + B), (-A) + (-B)395  . exact IsCommMonoid.monoid with monoid396  . unfold IsInverse397    refine ⟨sumInReals, negSumInReals, _, _⟩398    . exact realAddValue.neg_left with sumReal399    . exact realAddValue.neg_right with sumReal400  . unfold IsInverse401    refine ⟨sumInReals, candidateInReals, candidateLeft, candidateRight⟩402403theorem realSubValue.neg_swap (A B : Real)404  shows B - A = -(A - B)405proof406  have negAReal := realNegValue.real at A407  have negBReal := realNegValue.real at B408  have involutiveB := realNegValue.involutive at B409  have negatedSum := realNegValue.add at A, -B with410    assumption, negBReal411  unfold realSubValue412  have commutative := realAddValue.commutative at B, -A with413    assumption, negAReal414  cc415416theorem realSubValue.neg_neg (A B : Real)417  shows (-A) - (-B) = -(A - B)418proof419  have negAReal := realNegValue.real at A420  have involutiveB := realNegValue.involutive at B421  have swapped := realSubValue.neg_swap at A, B with *422  have commutes := realAddValue.commutative at -A, B with423    negAReal, assumption424  unfold realSubValue at swapped425  unfold realSubValue426  cc427428theorem realSubValue.add_add (A B C D : Real)429  shows (A + B) - (C + D) = (A - C) + (B - D)430proof431  have negSum := realNegValue.add at C, D with *432  have negCReal := realNegValue.real at C433  have negDReal := realNegValue.real at D434  have sumABReal := realAddValue.real at A, B with *435  have aNegCReal := realAddValue.real at A, -C with assumption, negCReal436  have outerAssoc := realAddValue.associative with sumABReal, negCReal, negDReal437  have firstAssoc := realAddValue.associative at A, B, -C with438    *{2}, negCReal439  have middleComm := realAddValue.commutative at B, -C with440    assumption, negCReal441  have secondAssoc := realAddValue.associative at A, -C, B with442    assumption, negCReal, assumption443  have finalAssoc := realAddValue.associative at A + (-C), B, -D with444    aNegCReal, assumption, negDReal445  unfold realSubValue446  rw negSum447  calc448    (A + B) + ((-C) + (-D)) = ((A + B) + (-C)) + (-D) := by cc449    _ = (A + (B + (-C))) + (-D) := by cc450    _ = (A + ((-C) + B)) + (-D) := by cc451    _ = ((A + (-C)) + B) + (-D) := by cc452    _ = (A + (-C)) + (B + (-D)) := by cc453454theorem realAddCut.neg_swap (A B : Real)455  shows realAddCut(B, realNegCut(A)) =456    realNegCut(realAddCut(A, realNegCut(B)))457proof458  have negAReal := realNegValue.real at A459  have negBReal := realNegValue.real at B460  have rightReal := realAddValue.real at A, -B with assumption, negBReal461  have swapped := realSubValue.neg_swap at A, B with *462  unfold realSubValue at swapped463  have negACut := realNegValue.cut at A464  have negBCut := realNegValue.cut at B465  have leftCut := realAddValue.cut at B, -A with assumption, negAReal466  have rightCut := realAddValue.cut at A, -B with assumption, negBReal467  have outerCut := realNegValue.cut with rightReal468  rwa [← negACut, ← negBCut, ← leftCut, ← rightCut, ← outerCut]469470theorem realAddCut.neg_swap_commuted (A B : Real)471  shows realAddCut(realNegCut(A), B) =472    realNegCut(realAddCut(realNegCut(B), A))473proof474  have negAReal := realNegCut.real at A475  have negBReal := realNegCut.real at B476  have leftComm := realAddCut.commutative at B, realNegCut(A) with477    assumption, negAReal478  have rightComm := realAddCut.commutative at A, realNegCut(B) with479    assumption, negBReal480  have swapped := realAddCut.neg_swap at A, B with *481  cc482483theorem realPositivePart.neg (A : Set)484  shows realPositivePart(realNegCut(A)) = realNegativePart(A)485proof486  unfold realNegativePart487  rfl488489theorem realNegativePart.neg (A : Real)490  shows realNegativePart(realNegCut(A)) = realPositivePart(A)491proof492  have involutive := realNegCut.involutive at A493  unfold realNegativePart494  cc495496-- Negating a nonnegative factor swaps its positive and negative parts.  The497-- signed product therefore reduces to the negative of the positive498-- product, as in elementary algebra.499theorem realMulCut.neg_left_of_nonnegative (A B : Real)500  requires nonnegativeA : realZero ⊆ A501  requires nonnegativeB : realZero ⊆ B502  shows realMulCut(realNegCut(A), B) = realNegCut(realMulCut(A, B))503proof504  have positiveA := realPositivePart.eq_of_nonnegative with nonnegativeA505  have positiveB := realPositivePart.eq_of_nonnegative with nonnegativeB506  have negativeA := realNegativePart.eq_zero_of_nonnegative with nonnegativeA507  have negativeB := realNegativePart.eq_zero_of_nonnegative with nonnegativeB508  have positiveNegA : realPositivePart(realNegCut(A)) = realZero509    calc510      realPositivePart(realNegCut(A)) = realNegativePart(A) :=511        realPositivePart.neg at A512      _ = realZero := negativeA513  have negativeNegA : realNegativePart(realNegCut(A)) = A514    calc515      realNegativePart(realNegCut(A)) = realPositivePart(A) :=516        realNegativePart.neg with assumption517      _ = A := positiveA518  have reduction := realMulCut.of_nonnegative with nonnegativeA, nonnegativeB519  simp [realMulCut, positiveNegA, negativeNegA, positiveB, negativeB,520    realPosMulCut.zero_left, realPosMulCut.zero_right,521    realAddCut.zero_left, realAddCut.zero_right, realNegCut.zero, reduction]522523-- The canonical signed product changes sign when either factor is negated.524-- Negation swaps A⁺ and A⁻; commutativity aligns the two cross-term sums,525-- and `realAddCut.neg_swap` performs the final difference reversal.526theorem realMulCut.neg_left (A B : Real)527  shows realMulCut(realNegCut(A), B) = realNegCut(realMulCut(A, B))528proof529  have positiveAReal := realPositivePart.real at A530  have negativeAReal := realNegativePart.real at A531  have positiveBReal := realPositivePart.real at B532  have negativeBReal := realNegativePart.real at B533  have pp := realPosMulCut.real with positiveAReal, positiveBReal534  have nn := realPosMulCut.real with negativeAReal, negativeBReal535  have pn := realPosMulCut.real with positiveAReal, negativeBReal536  have np := realPosMulCut.real with negativeAReal, positiveBReal537  have positiveSum := realAddCut.real with pp, nn538  have negativeSum := realAddCut.real with pn, np539  have positiveSwap := realAddCut.commutative with np, pn540  have negativeSwap := realAddCut.commutative with nn, pp541  have swapped := realAddCut.neg_swap at542    realAddCut(543      realPosMulCut(realPositivePart(A), realPositivePart(B)),544      realPosMulCut(realNegativePart(A), realNegativePart(B))),545    realAddCut(546      realPosMulCut(realPositivePart(A), realNegativePart(B)),547      realPosMulCut(realNegativePart(A), realPositivePart(B))) with548      positiveSum, negativeSum549  simp [realMulCut, realPositivePart.neg, realNegativePart.neg]550551theorem realMulCut.neg_right (A B : Real)552  shows realMulCut(A, realNegCut(B)) = realNegCut(realMulCut(A, B))553proof554  have negBReal := realNegCut.real at B555  have commutative := realMulCut.commutative at B, A with556    *{2}557  calc558    realMulCut(A, realNegCut(B)) = realMulCut(realNegCut(B), A) :=559      realMulCut.commutative with assumption, negBReal560    _ = realNegCut(realMulCut(B, A)) :=561      realMulCut.neg_left with *{2}562    _ = realNegCut(realMulCut(A, B)) := by cc563564theorem realMulValue.neg_left (A B : Real)565  shows (-A) * B = -(A * B)566proof567  have negAReal := realNegValue.real at A568  have productReal := realMulValue.real at A, B with *569  have negACut := realNegValue.cut at A570  have leftCut := realMulValue.cut at -A, B with negAReal, assumption571  have productCut := realMulValue.cut at A, B with *572  have outerNegCut := realNegValue.cut with productReal573  have cutLaw := realMulCut.neg_left at A, B with *574  rwa [leftCut, negACut, outerNegCut, productCut]575576theorem realMulValue.neg_right (A B : Real)577  shows A * (-B) = -(A * B)578proof579  have negBReal := realNegValue.real at B580  have productReal := realMulValue.real at A, B with *581  have negBCut := realNegValue.cut at B582  have leftCut := realMulValue.cut at A, -B with assumption, negBReal583  have productCut := realMulValue.cut at A, B with *584  have outerNegCut := realNegValue.cut with productReal585  have cutLaw := realMulCut.neg_right at A, B with *586  rwa [leftCut, negBCut, outerNegCut, productCut]587588theorem realMulValue.neg_both (A B : Real)589  shows (-A) * (-B) = A * B590proof591  have negBReal := realNegValue.real at B592  have productReal := realMulValue.real at A, B with *593  have first := realMulValue.neg_left at A, -B with594    assumption, negBReal595  have second := realMulValue.neg_right at A, B with *596  have involutive := realNegValue.involutive with productReal597  cc598599theorem realAddValue.solve_right (X Y Z : Real)600  requires equation : X = Y + Z601  shows Y = X + (-Z)602proof603  have negZReal := realNegValue.real at Z604  have associated := realAddValue.associative at Y, Z, -Z with605    *{2}, negZReal606  have inverse := realAddValue.neg_right at Z607  have identity := realAddValue.zero_right at Y608  cc609610theorem realAddValue.subtract_sum (X Y Z : Real)611  requires equation : X = Y + Z612  shows Y + (-X) = -Z613proof614  have negYReal := realNegValue.real at Y615  have negZReal := realNegValue.real at Z616  have negativeSum := realNegValue.add at Y, Z with *617  have associated := realAddValue.associative at Y, -Y, -Z with618    assumption, negYReal, negZReal619  have inverse := realAddValue.neg_right at Y620  have identity := realAddValue.zero_left with negZReal621  cc622623theorem realNegValue.nonnegative_of_nonpositive (A : Real)624  requires nonpositive : A ⊆ realZero625  shows realZero ⊆ -A626proof627  have reversed := realNegCut.subset_reverse at A, realZero with628    assumption, realZero.real, nonpositive629  rw realNegCut.zero at reversed630  have cut := realNegValue.cut at A631  rwa cut632633theorem realMulValue.distributive_nonnegative_left_nonpositive_right (A B C : Real)634  requires nonnegativeA : realZero ⊆ A635  requires nonpositiveB : B ⊆ realZero636  requires nonpositiveC : C ⊆ realZero637  shows A * (B + C) = A * B + A * C638proof639  have negBReal := realNegValue.real at B640  have negCReal := realNegValue.real at C641  have negBNonnegative := realNegValue.nonnegative_of_nonpositive with nonpositiveB642  have negCNonnegative := realNegValue.nonnegative_of_nonpositive with nonpositiveC643  have base := realMulValue.distributive_of_nonnegative at A, -B, -C with644    assumption, negBReal, negCReal,645    nonnegativeA, negBNonnegative, negCNonnegative646  have sumReal := realAddValue.real at B, C with *647  have abReal := realMulValue.real at A, B with *648  have acReal := realMulValue.real at A, C with *649  have negatedSum := realNegValue.add at B, C with *650  have leftNegative := realMulValue.neg_right at A, B + C with651    assumption, sumReal652  have rightNegativeB := realMulValue.neg_right at A, B with653    *{2}654  have rightNegativeC := realMulValue.neg_right at A, C with655    *{2}656  have negatedRight := realNegValue.add with abReal, acReal657  have leftProductReal := realMulValue.real at A, B + C with assumption, sumReal658  have rightSumReal := realAddValue.real with abReal, acReal659  have leftInvolutive := realNegValue.involutive with leftProductReal660  have rightInvolutive := realNegValue.involutive with rightSumReal661  cc662663theorem realMulValue.distributive_nonnegative_left_mixed (A B C : Real)664  requires nonnegativeA : realZero ⊆ A665  requires nonnegativeB : realZero ⊆ B666  requires nonpositiveC : C ⊆ realZero667  shows A * (B + C) = A * B + A * C668proof669  have negCReal := realNegValue.real at C670  have negCNonnegative := realNegValue.nonnegative_of_nonpositive with nonpositiveC671  have cutB := Real.characterization.forward at B with assumption672  have cutNegC := Real.characterization.forward with negCReal673  have comparison := DedekindCut.comparable with cutB, cutNegC674  have involutiveC := realNegValue.involutive at C675  have acNegative := realMulValue.neg_right at A, -C with676    assumption, negCReal677  cases comparison with bSubsetNegC | negCSubsetB678  . have differenceReal := realSubValue.real at -C, B with negCReal, assumption679    have differenceNonnegative := realSubValue.nonnegative_of_subset at B, -C with680      assumption, negCReal, bSubsetNegC681    have cancelled := realSubValue.add_right_cancel at -C, B with682      negCReal, assumption683    have base := realMulValue.distributive_of_nonnegative at684      A, (-C) - B, B with assumption, differenceReal, assumption,685      nonnegativeA, differenceNonnegative, nonnegativeB686    rw cancelled at base687    have atReal := realMulValue.real at A, (-C) - B with688      assumption, differenceReal689    have abReal := realMulValue.real at A, B with *690    have reordered : A * (-C) = A * B + A * ((-C) - B)691      have commutative := realAddValue.commutative with atReal, abReal692      cc693    have remainder := realAddValue.subtract_sum with reordered694    have negBReal := realNegValue.real at B695    have differenceShape : (-C) - B = (-C) + (-B)696      unfold realSubValue697      rfl698    have negatedDifference := realNegValue.add with negCReal, negBReal699    have involutiveB := realNegValue.involutive at B700    have sumCommutative := realAddValue.commutative at B, C with701      *{2}702    have sumShape : B + C = -((-C) - B) by cc703    have leftNegative := realMulValue.neg_right at A, (-C) - B with704      assumption, differenceReal705    have acShape : A * C = -(A * (-C)) by cc706    cc707  . have differenceReal := realSubValue.real at B, -C with assumption, negCReal708    have differenceNonnegative := realSubValue.nonnegative_of_subset with negCSubsetB709    have cancelled := realSubValue.add_right_cancel at B, -C with710      assumption, negCReal711    have base := realMulValue.distributive_of_nonnegative at712      A, B - (-C), -C with assumption, differenceReal, negCReal,713      nonnegativeA, differenceNonnegative, negCNonnegative714    rw cancelled at base715    have solved := realAddValue.solve_right with base716    have sumShape : B + C = B - (-C)717      unfold realSubValue718      cc719    have acShape : A * C = -(A * (-C)) by cc720    cc721722theorem realMulValue.distributive_nonnegative_left_mixed_reverse (A B C : Real)723  requires nonnegativeA : realZero ⊆ A724  requires nonpositiveB : B ⊆ realZero725  requires nonnegativeC : realZero ⊆ C726  shows A * (B + C) = A * B + A * C727proof728  have base := realMulValue.distributive_nonnegative_left_mixed with729    *{3}, nonnegativeA, nonnegativeC, nonpositiveB730  have sumCommutative := realAddValue.commutative at B, C with731    *{2}732  have abReal := realMulValue.real at A, B with *733  have acReal := realMulValue.real at A, C with *734  have productCommutative := realAddValue.commutative with abReal, acReal735  cc736737theorem Real.sign_cases (A : Real)738  shows A ⊆ realZero ∨ realZero ⊆ A739proof740  have cutA := Real.characterization.forward with assumption741  have cutZero := Real.characterization.forward with realZero.real742  exact DedekindCut.comparable with cutA, cutZero743744theorem realMulValue.distributive_of_nonnegative_left (A B C : Real)745  requires nonnegativeA : realZero ⊆ A746  shows A * (B + C) = A * B + A * C747proof748  have signB := Real.sign_cases at B749  have signC := Real.sign_cases at C750  cases signB with nonpositiveB | nonnegativeB751  . cases signC with nonpositiveC | nonnegativeC752    . exact realMulValue.distributive_nonnegative_left_nonpositive_right at753        A, B, C with *{3},754        nonnegativeA, nonpositiveB, nonpositiveC755    . exact realMulValue.distributive_nonnegative_left_mixed_reverse at756        A, B, C with *{3},757        nonnegativeA, nonpositiveB, nonnegativeC758  . cases signC with nonpositiveC2 | nonnegativeC2759    . exact realMulValue.distributive_nonnegative_left_mixed at760        A, B, C with *{3},761        nonnegativeA, nonnegativeB, nonpositiveC2762    . exact realMulValue.distributive_of_nonnegative at A, B, C with763        *{3},764        nonnegativeA, nonnegativeB, nonnegativeC2765766theorem realMulValue.distributive (A B C : Real)767  shows A * (B + C) = A * B + A * C768proof769  have signA := Real.sign_cases at A770  cases signA with nonpositiveA | nonnegativeA771  . have negAReal := realNegValue.real at A772    have negANonnegative := realNegValue.nonnegative_of_nonpositive with nonpositiveA773    have base := realMulValue.distributive_of_nonnegative_left at -A, B, C with774      negAReal, *{2}, negANonnegative775    have sumReal := realAddValue.real at B, C with *776    have abReal := realMulValue.real at A, B with *777    have acReal := realMulValue.real at A, C with *778    have leftNegative := realMulValue.neg_left at A, B + C with779      assumption, sumReal780    have rightNegativeB := realMulValue.neg_left at A, B with781      *{2}782    have rightNegativeC := realMulValue.neg_left at A, C with783      *{2}784    have rightNegative := realNegValue.add with abReal, acReal785    have leftReal := realMulValue.real at A, B + C with assumption, sumReal786    have rightReal := realAddValue.real with abReal, acReal787    have leftInvolutive := realNegValue.involutive with leftReal788    have rightInvolutive := realNegValue.involutive with rightReal789    cc790  . exact realMulValue.distributive_of_nonnegative_left at A, B, C with791      *{3}, nonnegativeA792793-- Associativity is stable when the sign of any one input is reversed.  These794-- three small transport lemmas keep the signed lift below algebraic: they use795-- only the multiplication-negation laws and congruence.796theorem realMulValue.associative.neg_left (A B C : Real)797  requires associative : (A * B) * C = A * (B * C)798  shows ((-A) * B) * C = (-A) * (B * C)799proof800  have abReal := realMulValue.real at A, B with *801  have bcReal := realMulValue.real at B, C with *802  have inner := realMulValue.neg_left at A, B with *803  have outer := realMulValue.neg_left at A * B, C with abReal, assumption804  have right := realMulValue.neg_left at A, B * C with assumption, bcReal805  cc806807theorem realMulValue.associative.neg_middle (A B C : Real)808  requires associative : (A * B) * C = A * (B * C)809  shows (A * (-B)) * C = A * ((-B) * C)810proof811  have abReal := realMulValue.real at A, B with *812  have bcReal := realMulValue.real at B, C with *813  have innerLeft := realMulValue.neg_right at A, B with *814  have outerLeft := realMulValue.neg_left at A * B, C with abReal, assumption815  have innerRight := realMulValue.neg_left at B, C with *816  have outerRight := realMulValue.neg_right at A, B * C with assumption, bcReal817  cc818819theorem realMulValue.associative.neg_right (A B C : Real)820  requires associative : (A * B) * C = A * (B * C)821  shows (A * B) * (-C) = A * (B * (-C))822proof823  have abReal := realMulValue.real at A, B with *824  have bcReal := realMulValue.real at B, C with *825  have left := realMulValue.neg_right at A * B, C with abReal, assumption826  have inner := realMulValue.neg_right at B, C with *827  have right := realMulValue.neg_right at A, B * C with assumption, bcReal828  cc829830theorem realMulValue.associative (A B C : Real)831  shows (A * B) * C = A * (B * C)832proof833  have signA := Real.sign_cases at A834  have signB := Real.sign_cases at B835  have signC := Real.sign_cases at C836  cases signA with nonpositiveA | nonnegativeA837  . have negAReal := realNegValue.real at A838    have nonnegativeNegA := realNegValue.nonnegative_of_nonpositive with nonpositiveA839    have involutiveA := realNegValue.involutive at A840    have negNegAReal := realNegValue.real with negAReal841    cases signB with nonpositiveB | nonnegativeB842    . have negBReal := realNegValue.real at B843      have nonnegativeNegB := realNegValue.nonnegative_of_nonpositive with nonpositiveB844      have involutiveB := realNegValue.involutive at B845      have negNegBReal := realNegValue.real with negBReal846      cases signC with nonpositiveCNNN | nonnegativeCNNP847      . have negCRealNNN := realNegValue.real at C848        have nonnegativeNegCNNN := realNegValue.nonnegative_of_nonpositive with nonpositiveCNNN849        have involutiveCNNN := realNegValue.involutive at C850        have associativeNNN := realMulValue.associative_of_nonnegative with851          negAReal, negBReal, negCRealNNN, nonnegativeNegA, nonnegativeNegB, nonnegativeNegCNNN852        have associativeNegANNN := realMulValue.associative.neg_left with853          negAReal, negBReal, negCRealNNN, associativeNNN854        have associativeNegABNNN := realMulValue.associative.neg_middle with855          negNegAReal, negBReal, negCRealNNN, associativeNegANNN856        have associativeNegABCNNN := realMulValue.associative.neg_right with857          negNegAReal, negNegBReal, negCRealNNN, associativeNegABNNN858        cc859      . have associativeNNP := realMulValue.associative_of_nonnegative at860          -A, -B, C with negAReal, negBReal, assumption,861          nonnegativeNegA, nonnegativeNegB, nonnegativeCNNP862        have associativeNegANNP := realMulValue.associative.neg_left with863          negAReal, negBReal, assumption, associativeNNP864        have associativeNegABNNP := realMulValue.associative.neg_middle with865          negNegAReal, negBReal, assumption, associativeNegANNP866        cc867    . cases signC with nonpositiveCNPN | nonnegativeCNPP868      . have negCRealNPN := realNegValue.real at C869        have nonnegativeNegCNPN := realNegValue.nonnegative_of_nonpositive with nonpositiveCNPN870        have involutiveCNPN := realNegValue.involutive at C871        have associativeNPN := realMulValue.associative_of_nonnegative at872          -A, B, -C with negAReal, assumption, negCRealNPN,873          nonnegativeNegA, nonnegativeB, nonnegativeNegCNPN874        have associativeNegANPN := realMulValue.associative.neg_left at875          -A, B, -C with negAReal, assumption, negCRealNPN, associativeNPN876        have associativeNegACNPN := realMulValue.associative.neg_right at877          -(-A), B, -C with negNegAReal, assumption, negCRealNPN,878          associativeNegANPN879        cc880      . have associativeNPP := realMulValue.associative_of_nonnegative at881          -A, B, C with negAReal, *{2},882          nonnegativeNegA, nonnegativeB, nonnegativeCNPP883        have associativeNegANPP := realMulValue.associative.neg_left with associativeNPP884        cc885  . cases signB with nonpositiveB | nonnegativeB886    . have negBReal := realNegValue.real at B887      have nonnegativeNegB := realNegValue.nonnegative_of_nonpositive with nonpositiveB888      have involutiveB := realNegValue.involutive at B889      have negNegBRealPN := realNegValue.real with negBReal890      cases signC with nonpositiveCPNN | nonnegativeCPNP891      . have negCRealPNN := realNegValue.real at C892        have nonnegativeNegCPNN := realNegValue.nonnegative_of_nonpositive with nonpositiveCPNN893        have involutiveCPNN := realNegValue.involutive at C894        have associativePNN := realMulValue.associative_of_nonnegative at895          A, -B, -C with assumption, negBReal, negCRealPNN,896          nonnegativeA, nonnegativeNegB, nonnegativeNegCPNN897        have associativeNegBPNN := realMulValue.associative.neg_middle at898          A, -B, -C with assumption, negBReal, negCRealPNN, associativePNN899        have associativeNegBCPNN := realMulValue.associative.neg_right at900          A, -(-B), -C with assumption, negNegBRealPN, negCRealPNN,901          associativeNegBPNN902        cc903      . have associativePNP := realMulValue.associative_of_nonnegative at904          A, -B, C with assumption, negBReal, assumption,905          nonnegativeA, nonnegativeNegB, nonnegativeCPNP906        have associativeNegBPNP := realMulValue.associative.neg_middle at907          A, -B, C with assumption, negBReal, assumption, associativePNP908        cc909    . cases signC with nonpositiveCPPN | nonnegativeCPPP910      . have negCRealPPN := realNegValue.real at C911        have nonnegativeNegCPPN := realNegValue.nonnegative_of_nonpositive with nonpositiveCPPN912        have involutiveCPPN := realNegValue.involutive at C913        have associativePPN := realMulValue.associative_of_nonnegative at914          A, B, -C with *{2}, negCRealPPN,915          nonnegativeA, nonnegativeB, nonnegativeNegCPPN916        have associativeNegCPPN := realMulValue.associative.neg_right at917          A, B, -C with *{2}, negCRealPPN, associativePPN918        cc919      . exact realMulValue.associative_of_nonnegative at A, B, C with920          *{3},921          nonnegativeA, nonnegativeB, nonnegativeCPPP922923instance realMul.associative924  shows Associative(ℝ, realMul)925proof926  intros A realA B realB C realC927  have typedA : Real(A) by typecheck928  have typedB : Real(B) by typecheck929  have typedC : Real(C) by typecheck930  exact realMulValue.associative with typedA, typedB, typedC931932instance realMul.monoid933  shows IsMonoid(ℝ, realMul, realOne)934proof935  constructor936    constructor937    . exact realMul.magma938    . exact realMul.associative939  . exact realMul.identity940941instance realMul.comm_monoid942  shows IsCommMonoid(ℝ, realMul, realOne)943proof944  constructor945  . exact realMul.monoid946  . exact realMul.commutative947948theorem realMulValue.distributive_right (A B C : Real)949  shows (A + B) * C = A * C + B * C950proof951  have sumReal := realAddValue.real at A, B with *952  have leftCommutative := realMulValue.commutative at A + B, C with953    sumReal, assumption954  have distributed := realMulValue.distributive at C, A, B with955    *{3}956  have firstCommutative := realMulValue.commutative at C, A with957    *{2}958  have secondCommutative := realMulValue.commutative at C, B with959    *{2}960  cc961962instance realMul.distributive963  shows Distributive(ℝ, realAdd, realMul)964proof965  intros A realA B realB C realC966  have typedA : Real(A) by typecheck967  have typedB : Real(B) by typecheck968  have typedC : Real(C) by typecheck969  constructor970  . exact realMulValue.distributive with typedA, typedB, typedC971  . exact realMulValue.distributive_right with typedA, typedB, typedC972973instance reals.comm_ring974  shows IsCommRing(ℝ, realAdd, realZero, realNeg, realMul, realOne)975proof976  constructor977    constructor978    . exact realAdd.abelian_group979    . constructor980      . exact realMul.monoid981      . exact realMul.distributive982  . exact realMul.commutative983984-- Section: Order helpers for linear arithmetic985986theorem realLess.not_self (A : Real)987  shows ¬(A < A)988proof989  intro less990  have irreflexive := realLess.irreflexive_on991  exact irreflexive with A, less992993-- Two reals compare one way, are equal, or compare the other way.994theorem realLess.trichotomy (A B : Real)995  shows A < B ∨ A = B ∨ B < A996proof997  by_contra none998  have distinct : A ≠ B999    intro equal1000    apply none1001    right1002    left1003    exact equal1004  have connected := realLess.connected_on1005  have comparison := connected with A, B, distinct1006  apply none1007  cases comparison with ab | ba1008  . left1009    exact ab1010  . right1011    right1012    exact ba10131014theorem realLe.not_less (A B : Real)1015  requires le : A ≤ B1016  shows ¬(B < A)1017proof1018  intro less1019  have cycle := realLe.transitive_less with *1020  exact realLess.not_self with cycle10211022theorem realLe.of_not_less (A B : Real)1023  requires notLess : ¬(B < A)1024  shows A ≤ B1025proof1026  by_contra notLe1027  apply notLess1028  exact realLess.of_not_le with *10291030theorem realLe.antisymmetric (A B : Real)1031  requires ab : A ≤ B1032  requires ba : B ≤ A1033  shows A = B1034proof1035  have abSubset := realLe.subset at A, B with *1036  have baSubset := realLe.subset at B, A with *1037  exact Subset.antisymmetric with abSubset, baSubset1038