-- The additive fragment of an ordered ring used by linear arithmetic
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.OrderedAdditive
import Group.Core
import Ring.Core

-- An ordered ring supplies this interface through its additive group and
-- translation-invariant weak order. No multiplication law is needed by
-- affine arithmetic, so other ordered additive groups can use it as well.
predicate OrderedAdditiveGroup (A add zero neg le : Set) :=
  IsAbelianGroup(A, add, zero, neg) ∧
  (ReflexiveOn(A, le) ∧
    (TransitiveOn(A, le) ∧
      ((∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ A, ∀ w ∈ A,
          relates(le, x, y) → relates(le, z, w) →
          relates(le, call2(add, x, z), call2(add, y, w))) ∧
        ((∀ x ∈ A, ∀ y ∈ A,
            relates(le, x, y) → relates(le, neg(y), neg(x))) ∧
          (∀ x ∈ A, ∀ y ∈ A,
            relates(le, x, y) →
            relates(le, zero, call2(add, y, neg(x))))))))

predicate OrderedRing (A add zero neg mul one le : Set) :=
  IsCommRing(A, add, zero, neg, mul, one) ∧
  (OrderedAdditiveGroup(A, add, zero, neg, le) ∧
    (AntisymmetricOn(A, le) ∧
      (∀ x ∈ A, ∀ y ∈ A,
        relates(le, zero, x) → relates(le, zero, y) →
        relates(le, zero, call2(mul, x, y)))))

theorem OrderedRing.comm_ring (A add zero neg mul one le : Set)
  requires ordered : OrderedRing(A, add, zero, neg, mul, one, le)
  shows IsCommRing(A, add, zero, neg, mul, one)
proof
  rcases ordered with ⟨ring, additive, antisymmetric, positive⟩
  exact ring

theorem OrderedRing.additive (A add zero neg mul one le : Set)
  requires ordered : OrderedRing(A, add, zero, neg, mul, one, le)
  shows OrderedAdditiveGroup(A, add, zero, neg, le)
proof
  rcases ordered with ⟨ring, additive, antisymmetric, positive⟩
  exact additive

theorem OrderedAdditiveGroup.neg_closed (A add zero neg le x : Set)
  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)
  requires member : x ∈ A
  shows neg(x) ∈ A
proof
  rcases structure with ⟨group, rest⟩
  have ordinary := IsAbelianGroup.group with group
  exact IsGroup.inverse_closed with ordinary, member

theorem OrderedAdditiveGroup.add_closed (A add zero neg le x y : Set)
  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)
  requires members : x ∈ A ∧ y ∈ A
  shows call2(add, x, y) ∈ A
proof
  rcases structure with ⟨group, rest⟩
  rcases members with ⟨hx, hy⟩
  have ordinary := IsAbelianGroup.group with group
  have monoid := IsGroup.monoid with ordinary
  exact IsMonoid.closed with monoid, hx, hy

theorem OrderedAdditiveGroup.add_comm (A add zero neg le x y : Set)
  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)
  requires members : x ∈ A ∧ y ∈ A
  shows call2(add, x, y) = call2(add, y, x)
proof
  rcases structure with ⟨group, rest⟩
  rcases members with ⟨hx, hy⟩
  have commutes := IsAbelianGroup.commutative with group
  exact commutes with x, hx, y, hy

theorem OrderedAdditiveGroup.add_assoc (A add zero neg le x y z : Set)
  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)
  requires members : x ∈ A ∧ y ∈ A ∧ z ∈ A
  shows call2(add, call2(add, x, y), z) = call2(add, x, call2(add, y, z))
proof
  rcases structure with ⟨group, rest⟩
  rcases members with ⟨hx, hy, hz⟩
  have ordinary := IsAbelianGroup.group with group
  have monoid := IsGroup.monoid with ordinary
  have associative := IsMonoid.associative with monoid
  exact Associative.law with associative, hx, hy, hz

theorem OrderedAdditiveGroup.zero_left (A add zero neg le x : Set)
  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)
  requires member : x ∈ A
  shows call2(add, zero, x) = x
proof
  rcases structure with ⟨group, rest⟩
  have ordinary := IsAbelianGroup.group with group
  have monoid := IsGroup.monoid with ordinary
  exact IsMonoid.left_identity with monoid, member

theorem OrderedAdditiveGroup.zero_right (A add zero neg le x : Set)
  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)
  requires member : x ∈ A
  shows call2(add, x, zero) = x
proof
  rcases structure with ⟨group, rest⟩
  have ordinary := IsAbelianGroup.group with group
  have monoid := IsGroup.monoid with ordinary
  exact IsMonoid.right_identity with monoid, member

theorem OrderedAdditiveGroup.add_neg (A add zero neg le x : Set)
  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)
  requires member : x ∈ A
  shows call2(add, x, neg(x)) = zero
proof
  rcases structure with ⟨group, rest⟩
  have ordinary := IsAbelianGroup.group with group
  exact IsGroup.inverse_right with ordinary, member

theorem OrderedAdditiveGroup.neg_add (A add zero neg le x : Set)
  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)
  requires member : x ∈ A
  shows call2(add, neg(x), x) = zero
proof
  rcases structure with ⟨group, rest⟩
  have ordinary := IsAbelianGroup.group with group
  exact IsGroup.inverse_left with ordinary, member

theorem OrderedAdditiveGroup.neg_neg (A add zero neg le x : Set)
  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)
  requires member : x ∈ A
  shows neg(neg(x)) = x
proof
  rcases structure with ⟨group, rest⟩
  have ordinary := IsAbelianGroup.group with group
  exact IsGroup.inverse_involutive with ordinary, member

theorem OrderedAdditiveGroup.add_swap (A add zero neg le x y z : Set)
  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)
  requires members : x ∈ A ∧ y ∈ A ∧ z ∈ A
  shows call2(add, x, call2(add, y, z)) =
    call2(add, y, call2(add, x, z))
proof
  rcases members with ⟨hx, hy, hz⟩
  have xyMembers : x ∈ A ∧ y ∈ A by refine ⟨hx, hy⟩
  have yxMembers : y ∈ A ∧ x ∈ A by refine ⟨hy, hx⟩
  have xyzMembers : x ∈ A ∧ y ∈ A ∧ z ∈ A by refine ⟨hx, hy, hz⟩
  have yxzMembers : y ∈ A ∧ x ∈ A ∧ z ∈ A by refine ⟨hy, hx, hz⟩
  have xy := OrderedAdditiveGroup.add_closed with structure, xyMembers
  have yx := OrderedAdditiveGroup.add_closed with structure, yxMembers
  have first := OrderedAdditiveGroup.add_assoc with structure, xyzMembers
  have swapped := OrderedAdditiveGroup.add_comm with structure, xyMembers
  have second := OrderedAdditiveGroup.add_assoc with structure, yxzMembers
  have step1 : call2(add, x, call2(add, y, z)) =
      call2(add, call2(add, x, y), z)
    rw first
    rfl
  have step2 : call2(add, call2(add, x, y), z) =
      call2(add, call2(add, y, x), z)
    rw swapped
    rfl
  calc
    call2(add, x, call2(add, y, z)) = call2(add, call2(add, x, y), z) := step1
    _ = call2(add, call2(add, y, x), z) := step2
    _ = call2(add, y, call2(add, x, z)) := second

theorem OrderedAdditiveGroup.add_cancel_left (A add zero neg le x y : Set)
  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)
  requires members : x ∈ A ∧ y ∈ A
  shows call2(add, call2(add, x, y), neg(x)) = y
proof
  rcases members with ⟨hx, hy⟩
  have xyMembers : x ∈ A ∧ y ∈ A by refine ⟨hx, hy⟩
  have negative := OrderedAdditiveGroup.neg_closed with structure, hx
  have xynMembers : x ∈ A ∧ y ∈ A ∧ neg(x) ∈ A by refine ⟨hx, hy, negative⟩
  have ynMembers : y ∈ A ∧ neg(x) ∈ A by refine ⟨hy, negative⟩
  have xnyMembers : x ∈ A ∧ neg(x) ∈ A ∧ y ∈ A by refine ⟨hx, negative, hy⟩
  have regroup := OrderedAdditiveGroup.add_assoc with structure, xynMembers
  have swapped := OrderedAdditiveGroup.add_comm with structure, ynMembers
  have regroupBack := OrderedAdditiveGroup.add_assoc with structure, xnyMembers
  have cancel := OrderedAdditiveGroup.add_neg with structure, hx
  have identity := OrderedAdditiveGroup.zero_left with structure, hy
  have step2 : call2(add, x, call2(add, y, neg(x))) =
      call2(add, x, call2(add, neg(x), y))
    rw swapped
    rfl
  have step3 : call2(add, x, call2(add, neg(x), y)) =
      call2(add, call2(add, x, neg(x)), y)
    rw regroupBack
    rfl
  have step4 : call2(add, call2(add, x, neg(x)), y) =
      call2(add, zero, y)
    rw cancel
    rfl
  calc
    call2(add, call2(add, x, y), neg(x)) =
      call2(add, x, call2(add, y, neg(x))) := regroup
    _ = call2(add, x, call2(add, neg(x), y)) := step2
    _ = call2(add, call2(add, x, neg(x)), y) :=
      step3
    _ = call2(add, zero, y) := step4
    _ = y := identity

theorem OrderedAdditiveGroup.reflexive (A add zero neg le x : Set)
  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)
  requires member : x ∈ A
  shows relates(le, x, x)
proof
  rcases structure with ⟨group, reflexive, rest⟩
  exact reflexive with x, member

theorem OrderedAdditiveGroup.transitive (A add zero neg le x y z : Set)
  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)
  requires members : x ∈ A ∧ y ∈ A ∧ z ∈ A
  requires xy : relates(le, x, y)
  requires yz : relates(le, y, z)
  shows relates(le, x, z)
proof
  rcases structure with ⟨group, reflexive, transitive, rest⟩
  rcases members with ⟨hx, hy, hz⟩
  exact transitive with x, hx, y, hy, z, hz, xy, yz

theorem OrderedAdditiveGroup.add (A add zero neg le x y z w : Set)
  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)
  requires members : x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ w ∈ A
  requires xy : relates(le, x, y)
  requires zw : relates(le, z, w)
  shows relates(le, call2(add, x, z), call2(add, y, w))
proof
  rcases structure with ⟨group, reflexive, transitive, monotone, rest⟩
  rcases members with ⟨hx, hy, hz, hw⟩
  exact monotone with x, hx, y, hy, z, hz, w, hw, xy, zw

theorem OrderedAdditiveGroup.neg_reverse (A add zero neg le x y : Set)
  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)
  requires members : x ∈ A ∧ y ∈ A
  requires xy : relates(le, x, y)
  shows relates(le, neg(y), neg(x))
proof
  rcases structure with ⟨group, reflexive, transitive, monotone, reverse, rest⟩
  rcases members with ⟨hx, hy⟩
  exact reverse with x, hx, y, hy, xy

theorem OrderedAdditiveGroup.nonnegative_sub (A add zero neg le x y : Set)
  requires structure : OrderedAdditiveGroup(A, add, zero, neg, le)
  requires members : x ∈ A ∧ y ∈ A
  requires xy : relates(le, x, y)
  shows relates(le, zero, call2(add, y, neg(x)))
proof
  rcases structure with ⟨group, reflexive, transitive, monotone, reverse, positive⟩
  rcases members with ⟨hx, hy⟩
  exact positive with x, hx, y, hy, xy