Grace/Cumulus/Algebra/OrderedAdditive.g17

Open in Workbench Download source

Imports

Group.Core · Ring.Core

Declarations

Source

1-- The additive fragment of an ordered ring used by linear arithmetic2-- 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.Algebra.OrderedAdditive8import Group.Core9import Ring.Core1011-- An ordered ring supplies this interface through its additive group and12-- translation-invariant weak order. No multiplication law is needed by13-- affine arithmetic, so other ordered additive groups can use it as well.14predicate OrderedAdditiveGroup (A add zero neg le : Set) :=15  IsAbelianGroup(A, add, zero, neg) ∧16  (ReflexiveOn(A, le) ∧17    (TransitiveOn(A, le) ∧18      ((∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ A, ∀ w ∈ A,19          relates(le, x, y) → relates(le, z, w) →20          relates(le, call2(add, x, z), call2(add, y, w))) ∧21        ((∀ x ∈ A, ∀ y ∈ A,22            relates(le, x, y) → relates(le, neg(y), neg(x))) ∧23          (∀ x ∈ A, ∀ y ∈ A,24            relates(le, x, y) →25            relates(le, zero, call2(add, y, neg(x))))))))2627predicate OrderedRing (A add zero neg mul one le : Set) :=28  IsCommRing(A, add, zero, neg, mul, one) ∧29  (OrderedAdditiveGroup(A, add, zero, neg, le) ∧30    (AntisymmetricOn(A, le) ∧31      (∀ x ∈ A, ∀ y ∈ A,32        relates(le, zero, x) → relates(le, zero, y) →33        relates(le, zero, call2(mul, x, y)))))3435theorem OrderedRing.comm_ring (A add zero neg mul one le : Set)36  requires ordered : OrderedRing(A, add, zero, neg, mul, one, le)37  shows IsCommRing(A, add, zero, neg, mul, one)38proof39  rcases ordered with ⟨ring, additive, antisymmetric, positive⟩40  exact ring4142theorem OrderedRing.additive (A add zero neg mul one le : Set)43  requires ordered : OrderedRing(A, add, zero, neg, mul, one, le)44  shows OrderedAdditiveGroup(A, add, zero, neg, le)45proof46  rcases ordered with ⟨ring, additive, antisymmetric, positive⟩47  exact additive4849theorem OrderedAdditiveGroup.neg_closed (A add zero neg le x : Set)50  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)51  requires member : x ∈ A52  shows neg(x) ∈ A53proof54  rcases structure with ⟨group, rest⟩55  have ordinary := IsAbelianGroup.group with group56  exact IsGroup.inverse_closed with ordinary, member5758theorem OrderedAdditiveGroup.add_closed (A add zero neg le x y : Set)59  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)60  requires members : x ∈ A ∧ y ∈ A61  shows call2(add, x, y) ∈ A62proof63  rcases structure with ⟨group, rest⟩64  rcases members with ⟨hx, hy⟩65  have ordinary := IsAbelianGroup.group with group66  have monoid := IsGroup.monoid with ordinary67  exact IsMonoid.closed with monoid, hx, hy6869theorem OrderedAdditiveGroup.add_comm (A add zero neg le x y : Set)70  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)71  requires members : x ∈ A ∧ y ∈ A72  shows call2(add, x, y) = call2(add, y, x)73proof74  rcases structure with ⟨group, rest⟩75  rcases members with ⟨hx, hy⟩76  have commutes := IsAbelianGroup.commutative with group77  exact commutes with x, hx, y, hy7879theorem OrderedAdditiveGroup.add_assoc (A add zero neg le x y z : Set)80  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)81  requires members : x ∈ A ∧ y ∈ A ∧ z ∈ A82  shows call2(add, call2(add, x, y), z) = call2(add, x, call2(add, y, z))83proof84  rcases structure with ⟨group, rest⟩85  rcases members with ⟨hx, hy, hz⟩86  have ordinary := IsAbelianGroup.group with group87  have monoid := IsGroup.monoid with ordinary88  have associative := IsMonoid.associative with monoid89  exact Associative.law with associative, hx, hy, hz9091theorem OrderedAdditiveGroup.zero_left (A add zero neg le x : Set)92  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)93  requires member : x ∈ A94  shows call2(add, zero, x) = x95proof96  rcases structure with ⟨group, rest⟩97  have ordinary := IsAbelianGroup.group with group98  have monoid := IsGroup.monoid with ordinary99  exact IsMonoid.left_identity with monoid, member100101theorem OrderedAdditiveGroup.zero_right (A add zero neg le x : Set)102  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)103  requires member : x ∈ A104  shows call2(add, x, zero) = x105proof106  rcases structure with ⟨group, rest⟩107  have ordinary := IsAbelianGroup.group with group108  have monoid := IsGroup.monoid with ordinary109  exact IsMonoid.right_identity with monoid, member110111theorem OrderedAdditiveGroup.add_neg (A add zero neg le x : Set)112  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)113  requires member : x ∈ A114  shows call2(add, x, neg(x)) = zero115proof116  rcases structure with ⟨group, rest⟩117  have ordinary := IsAbelianGroup.group with group118  exact IsGroup.inverse_right with ordinary, member119120theorem OrderedAdditiveGroup.neg_add (A add zero neg le x : Set)121  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)122  requires member : x ∈ A123  shows call2(add, neg(x), x) = zero124proof125  rcases structure with ⟨group, rest⟩126  have ordinary := IsAbelianGroup.group with group127  exact IsGroup.inverse_left with ordinary, member128129theorem OrderedAdditiveGroup.neg_neg (A add zero neg le x : Set)130  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)131  requires member : x ∈ A132  shows neg(neg(x)) = x133proof134  rcases structure with ⟨group, rest⟩135  have ordinary := IsAbelianGroup.group with group136  exact IsGroup.inverse_involutive with ordinary, member137138theorem OrderedAdditiveGroup.add_swap (A add zero neg le x y z : Set)139  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)140  requires members : x ∈ A ∧ y ∈ A ∧ z ∈ A141  shows call2(add, x, call2(add, y, z)) =142    call2(add, y, call2(add, x, z))143proof144  rcases members with ⟨hx, hy, hz⟩145  have xyMembers : x ∈ A ∧ y ∈ A by refine ⟨hx, hy⟩146  have yxMembers : y ∈ A ∧ x ∈ A by refine ⟨hy, hx⟩147  have xyzMembers : x ∈ A ∧ y ∈ A ∧ z ∈ A by refine ⟨hx, hy, hz⟩148  have yxzMembers : y ∈ A ∧ x ∈ A ∧ z ∈ A by refine ⟨hy, hx, hz⟩149  have xy := OrderedAdditiveGroup.add_closed with structure, xyMembers150  have yx := OrderedAdditiveGroup.add_closed with structure, yxMembers151  have first := OrderedAdditiveGroup.add_assoc with structure, xyzMembers152  have swapped := OrderedAdditiveGroup.add_comm with structure, xyMembers153  have second := OrderedAdditiveGroup.add_assoc with structure, yxzMembers154  have step1 : call2(add, x, call2(add, y, z)) =155      call2(add, call2(add, x, y), z)156    rw first157    rfl158  have step2 : call2(add, call2(add, x, y), z) =159      call2(add, call2(add, y, x), z)160    rw swapped161    rfl162  calc163    call2(add, x, call2(add, y, z)) = call2(add, call2(add, x, y), z) := step1164    _ = call2(add, call2(add, y, x), z) := step2165    _ = call2(add, y, call2(add, x, z)) := second166167theorem OrderedAdditiveGroup.add_cancel_left (A add zero neg le x y : Set)168  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)169  requires members : x ∈ A ∧ y ∈ A170  shows call2(add, call2(add, x, y), neg(x)) = y171proof172  rcases members with ⟨hx, hy⟩173  have xyMembers : x ∈ A ∧ y ∈ A by refine ⟨hx, hy⟩174  have negative := OrderedAdditiveGroup.neg_closed with structure, hx175  have xynMembers : x ∈ A ∧ y ∈ A ∧ neg(x) ∈ A by refine ⟨hx, hy, negative⟩176  have ynMembers : y ∈ A ∧ neg(x) ∈ A by refine ⟨hy, negative⟩177  have xnyMembers : x ∈ A ∧ neg(x) ∈ A ∧ y ∈ A by refine ⟨hx, negative, hy⟩178  have regroup := OrderedAdditiveGroup.add_assoc with structure, xynMembers179  have swapped := OrderedAdditiveGroup.add_comm with structure, ynMembers180  have regroupBack := OrderedAdditiveGroup.add_assoc with structure, xnyMembers181  have cancel := OrderedAdditiveGroup.add_neg with structure, hx182  have identity := OrderedAdditiveGroup.zero_left with structure, hy183  have step2 : call2(add, x, call2(add, y, neg(x))) =184      call2(add, x, call2(add, neg(x), y))185    rw swapped186    rfl187  have step3 : call2(add, x, call2(add, neg(x), y)) =188      call2(add, call2(add, x, neg(x)), y)189    rw regroupBack190    rfl191  have step4 : call2(add, call2(add, x, neg(x)), y) =192      call2(add, zero, y)193    rw cancel194    rfl195  calc196    call2(add, call2(add, x, y), neg(x)) =197      call2(add, x, call2(add, y, neg(x))) := regroup198    _ = call2(add, x, call2(add, neg(x), y)) := step2199    _ = call2(add, call2(add, x, neg(x)), y) :=200      step3201    _ = call2(add, zero, y) := step4202    _ = y := identity203204theorem OrderedAdditiveGroup.reflexive (A add zero neg le x : Set)205  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)206  requires member : x ∈ A207  shows relates(le, x, x)208proof209  rcases structure with ⟨group, reflexive, rest⟩210  exact reflexive with x, member211212theorem OrderedAdditiveGroup.transitive (A add zero neg le x y z : Set)213  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)214  requires members : x ∈ A ∧ y ∈ A ∧ z ∈ A215  requires xy : relates(le, x, y)216  requires yz : relates(le, y, z)217  shows relates(le, x, z)218proof219  rcases structure with ⟨group, reflexive, transitive, rest⟩220  rcases members with ⟨hx, hy, hz⟩221  exact transitive with x, hx, y, hy, z, hz, xy, yz222223theorem OrderedAdditiveGroup.add (A add zero neg le x y z w : Set)224  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)225  requires members : x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ w ∈ A226  requires xy : relates(le, x, y)227  requires zw : relates(le, z, w)228  shows relates(le, call2(add, x, z), call2(add, y, w))229proof230  rcases structure with ⟨group, reflexive, transitive, monotone, rest⟩231  rcases members with ⟨hx, hy, hz, hw⟩232  exact monotone with x, hx, y, hy, z, hz, w, hw, xy, zw233234theorem OrderedAdditiveGroup.neg_reverse (A add zero neg le x y : Set)235  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)236  requires members : x ∈ A ∧ y ∈ A237  requires xy : relates(le, x, y)238  shows relates(le, neg(y), neg(x))239proof240  rcases structure with ⟨group, reflexive, transitive, monotone, reverse, rest⟩241  rcases members with ⟨hx, hy⟩242  exact reverse with x, hx, y, hy, xy243244theorem OrderedAdditiveGroup.nonnegative_sub (A add zero neg le x y : Set)245  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)246  requires members : x ∈ A ∧ y ∈ A247  requires xy : relates(le, x, y)248  shows relates(le, zero, call2(add, y, neg(x)))249proof250  rcases structure with ⟨group, reflexive, transitive, monotone, reverse, positive⟩251  rcases members with ⟨hx, hy⟩252  exact positive with x, hx, y, hy, xy253