-- Ordered-field definitions
-- 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.OrderedField.Defs
import Field.Core
import Order

-- Translation preserves strict order. Commutativity later gives either side.
predicate AddStrictMono (A add lt : Set) :=
  ∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ A,
    relates(lt, x, y) → relates(lt, call2(add, x, z), call2(add, y, z))

-- The product of two positive elements is positive.
predicate MulPositive (A mul zero lt : Set) :=
  ∀ x ∈ A, ∀ y ∈ A,
    relates(lt, zero, x) → relates(lt, zero, y) →
      relates(lt, zero, call2(mul, x, y))

-- A strict-order presentation of an ordered field. This is equivalent to the
-- usual non-strict interface, while matching the natural order on Dedekind
-- cuts: proper inclusion.
predicate IsOrderedField (A add zero neg mul one inv lt : Set) :=
  IsFieldWithInverse(A, add, zero, neg, mul, one, inv) ∧
  (StrictLinearOrder(A, lt) ∧
    (AddStrictMono(A, add, lt) ∧ MulPositive(A, mul, zero, lt)))

-- An absolute-value operation is characterized by its zero, positive, and
-- negative branches. Ordered-field theory supplies the laws derived from
-- these equations; concrete models need only prove the branch interface.
predicate AbsoluteValue (A zero neg lt abs : Set) :=
  FunctionBetween(abs, A, A) ∧
  (abs(zero) = zero ∧
    (∀ x ∈ A,
      (relates(lt, zero, x) → abs(x) = x) ∧
      (relates(lt, x, zero) → abs(x) = neg(x))))

-- The non-strict order canonically induced by a strict linear order.
predicate LessEqualBy (A lt x y : Set) :=
  x ∈ A ∧ y ∈ A ∧ (x = y ∨ relates(lt, x, y))

-- Division by two in any field, expressed through its graph operations.
def fieldHalf (add mul one inv x : Set) : Set :=
  call2(mul, inv(call2(add, one, one)), x)