Grace/Cumulus/Real/Inverse.g17

Open in Workbench Download source

Imports

PositiveInverse

Declarations

Source

1-- Signed multiplicative inverses and the ordered-field structure of the reals2-- 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.Inverse8import PositiveInverse910-- The total inverse graph sends zero to zero.  Away from zero its two clauses11-- are the familiar positive reciprocal and the negative of the reciprocal of12-- the absolute value.  Keeping the sign split here lets all subsequent field13-- proofs speak only about multiplication and negation.14def realInv : Set :=15  { p ∈ (ℝ × ℝ) |16    ∃ A ∈ ℝ, (17      (A = 0 ∧ p = (A ↦ 0)) ∨18      (0 < A ∧ p = (A ↦ positiveRealInvCut(A))) ∨19      (A < 0 ∧20        p = (A ↦ realNegCut(positiveRealInvCut(realNegCut(A)))))) }2122theorem realInv.negative_argument_positive (A : Real)23  requires negative : A < 024  shows 0 < -A25proof26  have negativeView := realLess.characterization.forward with negative27  have reversedView := RealLess.neg_reverse with negativeView28  have reversed := realLess.characterization.backward with reversedView29  have negZero := realNegValue.zero30  rwa negZero at reversed3132theorem realInv.relates_zero33  shows relates(realInv, realZero, realZero)34proof35  unfold relates36  apply realInv.membership.backward37  have zeroInReals : realZero ∈ ℝ by exact realZero.real38  constructor39  . exact product.pair at realZero, realZero, ℝ, ℝ with40      zeroInReals, zeroInReals41  . witness realZero42    constructor43    . exact zeroInReals44    . left45      constructor46      . rfl47      . rfl4849theorem realInv.relates_positive (A : Real)50  requires positive : 0 < A51  shows relates(realInv, A, positiveRealInvCut(A))52proof53  have inverseReal := positiveRealInvCut.real with positive54  have realA : A ∈ ℝ by simp [Real]55  have realInverse : positiveRealInvCut(A) ∈ ℝ by exact inverseReal56  unfold relates57  apply realInv.membership.backward58  constructor59  . exact product.pair at A, positiveRealInvCut(A), ℝ, ℝ with60      realA, realInverse61  . witness A62    constructor63    . exact realA64    . right65      left66      constructor67      . exact positive68      . rfl6970theorem realInv.relates_negative (A : Real)71  requires negative : A < 072  shows relates(realInv, A,73    realNegCut(positiveRealInvCut(realNegCut(A))))74proof75  have positiveNegA := realInv.negative_argument_positive with negative76  have inverseReal := positiveRealInvCut.real with positiveNegA77  have negInverseReal := realNegValue.real with inverseReal78  have realA : A ∈ ℝ by simp [Real]79  have realInverse : realNegCut(positiveRealInvCut(realNegCut(A))) ∈ ℝ80    unfold Real at negInverseReal81    simpa [realNegValue.cut] using negInverseReal82  unfold relates83  apply realInv.membership.backward84  constructor85  . exact product.pair at A,86      realNegCut(positiveRealInvCut(realNegCut(A))), ℝ, ℝ with87      realA, realInverse88  . witness A89    constructor90    . exact realA91    . right92      right93      constructor94      . exact negative95      . rfl9697theorem realInv.total98  shows TotalBetween(realInv, ℝ, ℝ)99proof100  intros A realA101  have zeroCases : A = realZero ∨ A ≠ realZero102    by_contra neither103    apply neither104    right105    intro equal106    apply neither107    left108    exact equal109  cases zeroCases with zero | nonzero110  . witness realZero111    constructor112    . exact realZero.real113    . rw zero114      exact realInv.relates_zero115  . have connected := realLess.connected_on116    have signs := connected with A, realA, realZero, nonzero117    cases signs with negative | positive118    . have positiveNegA := realInv.negative_argument_positive with negative119      have inverseReal := positiveRealInvCut.real with positiveNegA120      have negInverseReal := realNegValue.real with inverseReal121      have cutInverseReal : Real(122          realNegCut(positiveRealInvCut(realNegCut(A))))123        simpa [realNegValue.cut] using negInverseReal124      witness realNegCut(positiveRealInvCut(realNegCut(A)))125      constructor126        exact cutInverseReal127      . exact realInv.relates_negative with negative128    . have inverseReal := positiveRealInvCut.real with positive129      witness positiveRealInvCut(A)130      constructor131        exact inverseReal132      . exact realInv.relates_positive with positive133134theorem realInv.negative_mul_eq_one (A : Real)135  requires negative : A < 0136  shows realMulValue(A,137    realNegCut(positiveRealInvCut(realNegCut(A)))) = realOne138proof139  have negAReal := realNegValue.real at A140  have positiveNegA := realInv.negative_argument_positive with negative141  have inverseReal := positiveRealInvCut.real with positiveNegA142  have positiveLaw := positiveRealInvCut.mul_eq_one with positiveNegA143  unfold realMulValue at positiveLaw144  have negatedProduct := realMulValue.neg_both with negAReal, inverseReal145  have involutiveA := realNegValue.involutive at A146  rw involutiveA at negatedProduct147  have law : A * (-positiveRealInvCut(-A)) = realOne148    rw negatedProduct149    unfold call2150    exact positiveLaw151  have negACut := realNegValue.cut at A152  have inverseNegCut := realNegValue.cut with inverseReal153  rw negACut at inverseNegCut154  rw [negACut, inverseNegCut] at law155  unfold call2 at law156  unfold realMulValue157  exact law158159theorem realLess.not_reverse (A B : Real)160  requires less : A < B161  shows ¬(B < A)162proof163  intro reverse164  have cycle := realLess.transitive with less, reverse165  have irreflexive := realLess.irreflexive_on166  exact irreflexive with A, cycle167168theorem realInv.factors (input output : Set)169  requires mapped : relates(realInv, input, output)170  shows ∃ A ∈ ℝ, input = A ∧171    ((A = 0 ∧ output = realZero) ∨172      (0 < A ∧173        output = positiveRealInvCut(A)) ∨174      (A < 0 ∧175        output = realNegCut(positiveRealInvCut(realNegCut(A)))))176proof177  unfold relates at mapped178  simp [realInv.membership] at mapped179  rcases mapped with ⟨bounded, A, realA, cases⟩180  witness A181  constructor182  . exact realA183  . cases cases with zero | nonzero184    . rcases zero with ⟨zeroA, shape⟩185      obtain ⟨inputA, outputZero⟩ := orderedPair.injective with shape186      constructor187      . exact inputA188      . left189        constructor190        . exact zeroA191        . exact outputZero192    . cases nonzero with positive | negative193      . rcases positive with ⟨positiveA, shape⟩194        obtain ⟨inputA, outputInverse⟩ := orderedPair.injective with shape195        constructor196        . exact inputA197        . right198          left199          constructor200          . exact positiveA201          . exact outputInverse202      . rcases negative with ⟨negativeA, shape⟩203        obtain ⟨inputA, outputInverse⟩ := orderedPair.injective with shape204        constructor205        . exact inputA206        . right207          right208          constructor209          . exact negativeA210          . exact outputInverse211212theorem realInv.functional213  shows Functional(realInv)214proof215  intros input y inputY z inputZ216  obtain ⟨A, realA, inputA, yCases⟩ := realInv.factors with inputY217  obtain ⟨B, realB, inputB, zCases⟩ := realInv.factors with inputZ218  have sameInput : A = B by cc219  rw ← sameInput at zCases220  cases yCases with yZero | yNonzero221  . rcases yZero with ⟨zeroA, yShape⟩222    cases zCases with zZero | zNonzero223    . rcases zZero with ⟨zeroAgain, zShape⟩224      cc225    . cases zNonzero with zPositive | zNegative226      . rcases zPositive with ⟨positiveA, zShape⟩227        rw zeroA at positiveA228        exfalso229        have impossible := realLess.not_reverse with realZero.real, realZero.real, positiveA230        exact impossible with positiveA231      . rcases zNegative with ⟨negativeA, zShape⟩232        rw zeroA at negativeA233        exfalso234        have impossible := realLess.not_reverse with realZero.real, realZero.real, negativeA235        exact impossible with negativeA236  . cases yNonzero with yPositive | yNegative237    . rcases yPositive with ⟨positiveA, yShape⟩238      cases zCases with zZero | zNonzero239      . rcases zZero with ⟨zeroA, zShape⟩240        rw zeroA at positiveA241        exfalso242        have impossible := realLess.not_reverse with realZero.real, realZero.real, positiveA243        exact impossible with positiveA244      . cases zNonzero with zPositive | zNegative245        . rcases zPositive with ⟨positiveAgain, zShape⟩246          cc247        . rcases zNegative with ⟨negativeA, zShape⟩248          exfalso249          have impossible := realLess.not_reverse with realZero.real, positiveA250          exact impossible with negativeA251    . rcases yNegative with ⟨negativeA, yShape⟩252      cases zCases with zZero | zNonzero253      . rcases zZero with ⟨zeroA, zShape⟩254        rw zeroA at negativeA255        exfalso256        have impossible := realLess.not_reverse with realZero.real, realZero.real, negativeA257        exact impossible with negativeA258      . cases zNonzero with zPositive | zNegative259        . rcases zPositive with ⟨positiveA, zShape⟩260          exfalso261          have impossible := realLess.not_reverse with realZero.real, positiveA262          exact impossible with negativeA263        . rcases zNegative with ⟨negativeAgain, zShape⟩264          cc265266theorem realInv.function267  shows realInv : ℝ → ℝ268proof269  constructor270    intros p member271    obtain ⟨bounded, witnesses⟩ := realInv.membership.forward with member272    exact bounded273  . constructor274    . exact realInv.functional275    . exact realInv.total276277-- Real division is the field operation x / y = x * y⁻¹.  Its graph is278-- obtained from the generic field construction, so `/` is selected by the279-- same notation machinery as `+` and `*`.280def realDiv : Set := fieldDiv(ℝ, realMul, realInv)281282theorem realDiv.function283  shows realDiv : ℝ × ℝ → ℝ284proof285  unfold realDiv286  exact fieldDiv.function with realMul.function, realInv.function287288instance realDiv.operation289  shows DivOperation(ℝ, realDiv)290proof291  exact realDiv.function292293notation infixl 70 "/" => call2 via DivOperation(ℝ, _) for Real294295def realInvValue (A : Real) : Real := realInv(A)296297theorem realInvValue.real (A : Real)298  shows Real(realInvValue(A))299proof300  have realA : A ∈ ℝ by simp [Real]301  obtain ⟨B, realB, mapped⟩ := FunctionBetween.exists_value with realInv.function, realA302  have applied := FunctionBetween.apply_value with realInv.function, mapped303  unfold realInvValue304  rw applied305  exact realB306307theorem realDiv.eq_mul_inv (A B : Real)308  shows A / B = A * realInvValue(B)309proof310  have realA : A ∈ ℝ by simp [Real]311  have realB : B ∈ ℝ by simp [Real]312  have mapped := fieldDiv.relates with realMul.function, realInv.function, realA, realB313  have inputInProduct := product.pair with realA, realB314  have mappedByRealDiv : relates(realDiv, (A, B),315      realMul(A, realInv(B)))316    unfold realDiv317    exact mapped318  have applied := FunctionBetween.apply_value with realDiv.function, inputInProduct, mappedByRealDiv319  unfold call2320  unfold realInvValue321  unfold call2 at applied322  exact applied323324theorem realDiv.real (A B : Real)325  shows Real(A / B)326proof327  have realA : A ∈ ℝ by simp [Real]328  have realB : B ∈ ℝ by simp [Real]329  have input := product.pair with realA, realB330  have closed := FunctionBetween.apply_closed with realDiv.function, input331  unfold call2332  exact closed333334theorem realDiv.zero_left (B : Real)335  shows 0 / B = 0336proof337  have inverseReal := realInvValue.real at B338  calc339    0 / B = 0 * realInvValue(B) :=340      realDiv.eq_mul_inv with realZero.real341    _ = 0 := realMulValue.zero_left at realInvValue(B) with inverseReal342343theorem realDiv.add_left (A B C : Real)344  shows (A + B) / C = A / C + B / C345proof346  have inverseReal := realInvValue.real at C347  have sumReal := realAddValue.real at A, B with *348  calc349    (A + B) / C = (A + B) * realInvValue(C) :=350      realDiv.eq_mul_inv with sumReal, assumption351    _ = A * realInvValue(C) + B * realInvValue(C) :=352      realMulValue.distributive_right at A, B, realInvValue(C) with353        *{2}, inverseReal354    _ = A / C + B / C := by simp [realDiv.eq_mul_inv]355356theorem realDiv.neg_left (A B : Real)357  shows (-A) / B = -(A / B)358proof359  have negAReal := realNegValue.real at A360  have inverseReal := realInvValue.real at B361  calc362    (-A) / B = (-A) * realInvValue(B) :=363      realDiv.eq_mul_inv with negAReal, assumption364    _ = -(A * realInvValue(B)) :=365      realMulValue.neg_left at A, realInvValue(B) with366        assumption, inverseReal367    _ = -(A / B) := by simp [realDiv.eq_mul_inv]368369theorem realInvValue.zero370  shows realInvValue(realZero) = realZero371proof372  have applied := FunctionBetween.apply_value with realInv.function, realInv.relates_zero373  unfold realInvValue374  exact applied375376theorem realInvValue.of_positive (A : Real)377  requires positive : 0 < A378  shows realInvValue(A) = positiveRealInvCut(A)379proof380  have mapped := realInv.relates_positive with positive381  have applied := FunctionBetween.apply_value with realInv.function, mapped382  unfold realInvValue383  exact applied384385theorem realInvValue.of_negative (A : Real)386  requires negative : A < 0387  shows realInvValue(A) =388    realNegCut(positiveRealInvCut(realNegCut(A)))389proof390  have mapped := realInv.relates_negative with negative391  have applied := FunctionBetween.apply_value with realInv.function, mapped392  unfold realInvValue393  exact applied394395theorem realInvValue.mul_right (A : Real)396  requires nonzero : A ≠ 0397  shows A * realInvValue(A) = 1398proof399  have connected := realLess.connected_on400  have signs := connected with A, realZero, nonzero401  cases signs with negative | positive402  . have value := realInvValue.of_negative with negative403    rw value404    have law := realInv.negative_mul_eq_one with negative405    unfold realMulValue at law406    unfold call2407    exact law408  . have value := realInvValue.of_positive with positive409    rw value410    have law := positiveRealInvCut.mul_eq_one with positive411    unfold realMulValue at law412    unfold call2413    exact law414415theorem realDiv.self (A : Real)416  requires nonzero : A ≠ 0417  shows A / A = 1418proof419  calc420    A / A = A * realInvValue(A) :=421      realDiv.eq_mul_inv with *{2}422    _ = 1 := realInvValue.mul_right at A with nonzero423424-- Multiplication by a nonzero denominator cancels division.425theorem realDiv.mul_left (A B : Real)426  requires nonzero : B ≠ 0427  shows B * (A / B) = A428proof429  have inverseReal := realInvValue.real at B430  have inverseLaw := realInvValue.mul_right with nonzero431  have oneA := realMulValue.one_left at A432  have associateBA := realMulValue.associative at433    B, A, realInvValue(B) with *{2}, inverseReal434  have commuteBA := realMulValue.commutative at B, A with435    *{2}436  have associateAB := realMulValue.associative at437    A, B, realInvValue(B) with *{2}, inverseReal438  have inverseProductReal := realMulValue.real at439    B, realInvValue(B) with assumption, inverseReal440  have commuteProduct := realMulValue.commutative at441    A, B * realInvValue(B) with assumption, inverseProductReal442  calc443    B * (A / B) = B * (A * realInvValue(B)) :=444      by simp [realDiv.eq_mul_inv]445    _ = (B * A) * realInvValue(B) := by cc446    _ = (A * B) * realInvValue(B) := by cc447    _ = A * (B * realInvValue(B)) := by cc448    _ = (B * realInvValue(B)) * A := commuteProduct449    _ = 1 * A := by simp [inverseLaw]450    _ = A := oneA451452theorem realDiv.mul_right (A B : Real)453  requires nonzero : B ≠ 0454  shows (A / B) * B = A455proof456  have quotientReal := realDiv.real at A, B with *457  have commute := realMulValue.commutative at A / B, B with458    quotientReal, assumption459  calc460    (A / B) * B = B * (A / B) := commute461    _ = A := realDiv.mul_left at A, B with nonzero462463-- Two quotients agree once the cross products agree.464theorem realDiv.eq_of_cross (P Q D E : Real)465  requires nonzeroQ : Q ≠ 0466  requires nonzeroE : E ≠ 0467  requires cross : D * Q = E * P468  shows P / Q = D / E469proof470  have leftView := realDiv.eq_mul_inv at P, Q471  have rightView := realDiv.eq_mul_inv at D, E472  have invQ := realInvValue.real at Q473  have invE := realInvValue.real at E474  have unitQ := realInvValue.mul_right with nonzeroQ475  have unitE := realInvValue.mul_right with nonzeroE476  rw [leftView, rightView]477  linear_combination (D * realInvValue(E)) * unitQ -478    (realInvValue(Q) * realInvValue(E)) * cross -479    (P * realInvValue(Q)) * unitE480481-- A factor in the numerator may be pulled outside division.482theorem realDiv.mul_numerator_left (A B C : Real)483  shows (A * B) / C = A * (B / C)484proof485  have productReal := realMulValue.real at A, B with *486  have inverseReal := realInvValue.real at C487  have associate := realMulValue.associative at488    A, B, realInvValue(C) with *{2}, inverseReal489  have wholeDivision := realDiv.eq_mul_inv at A * B, C with490    productReal, assumption491  have factorDivision := realDiv.eq_mul_inv at B, C with492    *{2}493  calc494    (A * B) / C = (A * B) * realInvValue(C) := wholeDivision495    _ = A * (B * realInvValue(C)) := associate496    _ = A * (B / C) := by cc497498theorem realInvValue.mul_left (A : Real)499  requires nonzero : A ≠ 0500  shows realInvValue(A) * A = 1501proof502  have inverseReal := realInvValue.real at A503  have commutative := realMulValue.commutative at realInvValue(A), A with504    inverseReal, assumption505  have right := realInvValue.mul_right with nonzero506  calc507    realInvValue(A) * A = A * realInvValue(A) := commutative508    _ = 1 := right509510theorem reals.multiplicative_inverse511  shows MultiplicativeInverse(ℝ, realMul, realZero, realOne, realInv)512proof513  constructor514  . exact realInv.function515  . intros A realA nonzero516    have left := realInvValue.mul_left with nonzero517    have right := realInvValue.mul_right with nonzero518    unfold realInvValue at left519    unfold realInvValue at right520    constructor521    . unfold call2522      unfold call2 at left523      exact left524    . unfold call2525      unfold call2 at right526      exact right527528instance reals.field529  shows IsFieldWithInverse(ℝ, realAdd, realZero, realNeg, realMul, realOne,530    realInv)531proof532  constructor533  . exact reals.comm_ring534  . constructor535    . exact reals.nontrivial536    . exact reals.multiplicative_inverse537538instance reals.ordered_field539  shows IsOrderedField(540    ℝ, realAdd, realZero, realNeg, realMul, realOne, realInv, realLess)541proof542  constructor543  . exact reals.field544  . constructor545    . exact realLess.strict_linear_order546    . constructor547      . exact realAdd.strict_mono548      . exact realMul.positive549550theorem realInvValue.nonzero (A : Real)551  requires nonzero : A ≠ 0552  shows realInvValue(A) ≠ 0553proof554  have inverseLaw := realInvValue.mul_right with nonzero555  intro inverseZero556  have zeroProduct := realMulValue.zero_right at A557  rw [inverseZero, zeroProduct] at inverseLaw558  apply realZero.ne_one559  exact inverseLaw560561-- A right inverse of a nonzero real is the inverse.  This tiny uniqueness562-- lemma keeps later reciprocal calculations close to their handwritten form.563theorem realInvValue.eq_of_mul_right (A B : Real)564  requires nonzero : A ≠ 0565  requires inverseLaw : A * B = 1566  shows B = realInvValue(A)567proof568  have inverseReal := realInvValue.real at A569  have canonical := realInvValue.mul_left with nonzero570  have associative := realMulValue.associative at571    realInvValue(A), A, B with inverseReal, *{2}572  have oneLeft := realMulValue.one_left at B573  have oneRight := realMulValue.one_right with inverseReal574  calc575    B = 1 * B := by cc576    _ = (realInvValue(A) * A) * B := by cc577    _ = realInvValue(A) * (A * B) := associative578    _ = realInvValue(A) * 1 := by cc579    _ = realInvValue(A) := oneRight580581theorem realInvValue.mul (A B : Real)582  requires nonzeroA : A ≠ 0583  requires nonzeroB : B ≠ 0584  shows realInvValue(A * B) = realInvValue(A) * realInvValue(B)585proof586  have inverseAReal := realInvValue.real at A587  have inverseBReal := realInvValue.real at B588  have productReal := realMulValue.real at A, B with *589  have inverseA := realInvValue.mul_right with nonzeroA590  have inverseB := realInvValue.mul_right with nonzeroB591  have inverseALeft := realInvValue.mul_left with nonzeroA592  have productNonzero : A * B ≠ 0593    intro productZero594    have zeroLeft := realMulValue.zero_right with inverseAReal595    have associative := realMulValue.associative at596      realInvValue(A), A, B with inverseAReal, *{2}597    have oneLeft := realMulValue.one_left at B598    apply nonzeroB599    cc600  have commute := realMulValue.commutative at B, realInvValue(A) with601    assumption, inverseAReal602  have candidateLaw : (A * B) *603      (realInvValue(A) * realInvValue(B)) = 1604    have oneMul := realMulValue.one_left with realOne.real605    have oneLeftB := realMulValue.one_left at B606    have oneRightA := realMulValue.one_right at A607    have oneRightInverseA := realMulValue.one_right with inverseAReal608    have assocABInvA := realMulValue.associative at609      A, B, realInvValue(A) with *{2}, inverseAReal610    have assocAInvAB := realMulValue.associative at611      A, realInvValue(A), B with assumption, inverseAReal, assumption612    have assocOuter := realMulValue.associative with productReal, inverseAReal, inverseBReal613    have assocFinal := realMulValue.associative at614      A, B, realInvValue(B) with *{2}, inverseBReal615    calc616      (A * B) * (realInvValue(A) * realInvValue(B)) =617          ((A * B) * realInvValue(A)) * realInvValue(B) := by cc618      _ = (A * (B * realInvValue(A))) * realInvValue(B) := by cc619      _ = (A * (realInvValue(A) * B)) * realInvValue(B) := by cc620      _ = ((A * realInvValue(A)) * B) * realInvValue(B) := by cc621      _ = (1 * B) * realInvValue(B) := by cc622      _ = B * realInvValue(B) := by cc623      _ = 1 := inverseB624  have unique := realInvValue.eq_of_mul_right with productNonzero, candidateLaw625  calc626    realInvValue(A * B) = realInvValue(A) * realInvValue(B) := by cc627