-- Order on rational quotient classes
-- 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.Rat.Order
import Defs
import Cumulus.Order

-- For representatives ((a,b),m) and ((c,d),n), the intended fractions are
-- (a-b)/m and (c-d)/n. Cross multiplication uses naturals only:
--   n*a + m*d < m*c + n*b.
predicate rationalRepresentativeLess (u v : Set) :=
  ∃ a ∈ ℕ, ∃ b ∈ ℕ,
  ∃ m ∈ positiveNaturals, ∃ c ∈ ℕ,
  ∃ d ∈ ℕ, ∃ n ∈ positiveNaturals,
    u = ((a, b), m) ∧ v = ((c, d), n) ∧
    n * a + m * d < m * c + n * b

-- On displayed representatives, rational order is exactly the familiar
-- cross-multiplication inequality. This is the arithmetic boundary used by
-- the quotient-level order proofs below.
theorem rationalRepresentativeLess.pair (a b m c d n : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  shows rationalRepresentativeLess(((a, b), m), ((c, d), n)) ↔
    n * a + m * d < m * c + n * b
proof
  constructor
  . intro less
    obtain ⟨wa, waNat, wb, wbNat, wm, wmPositive, wc, wcNat, wd, wdNat, wn, wnPositive, leftShape, rightShape, inequality⟩ := less
    obtain ⟨numeratorLeft, denominatorLeft⟩ := orderedPair.injective with leftShape
    obtain ⟨numeratorRight, denominatorRight⟩ := orderedPair.injective with rightShape
    obtain ⟨aEquals, bEquals⟩ := orderedPair.injective with numeratorLeft
    obtain ⟨cEquals, dEquals⟩ := orderedPair.injective with numeratorRight
    simpa [aEquals, bEquals, denominatorLeft, cEquals, dEquals, denominatorRight] using inequality
  . intro inequality
    have mPositive : m ∈ positiveNaturals by simp [nat.omega, positiveNaturals.membership]
    have nPositive : n ∈ positiveNaturals by simp [nat.omega, positiveNaturals.membership]
    unfold rationalRepresentativeLess
    refine ⟨a, _, b, _, m, mPositive, c, _, d, _, n, nPositive, rfl, rfl, inequality⟩
    . settle with nat.omega
    . settle with nat.omega
    . settle with nat.omega
    . settle with nat.omega

-- Replacing the right-hand fraction by an equivalent representative preserves
-- strict comparison. The certificate scales the comparison and equivalence
-- equation, combines them additively, then cancels the positive denominator.
theorem rationalRepresentativeLess.transport_right_cross (a b m c d n e f p : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  requires pNonzero : p ≠ 0
  requires less : n * a + m * d < m * c + n * b
  requires equivalent : p * c + n * f = n * e + p * d
  shows p * a + m * f < m * e + p * b
proof
  have scaledLess := Less.mul_left with pNonzero, less
  ring_nf at scaledLess
  have scaledEquivalent : m * (p * c + n * f) = m * (n * e + p * d) by linear_combination m * equivalent
  ring_nf at scaledEquivalent
  have combined := Less.replace_right with scaledLess, scaledEquivalent
  have scaledTarget : n * (p * a + m * f) < n * (m * e + p * b)
    ring_nf at combined
    ring_nf
    exact combined
  exact Less.mul_left_cancel_positive with nNonzero, scaledTarget

-- Replacing the left-hand fraction by an equivalent representative preserves
-- strict comparison. Clearing denominators reduces this to an ordered-additive
-- replacement, followed by cancellation of the positive common factor.
theorem rationalRepresentativeLess.transport_left_cross (a b m c d n e f p : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  requires pNonzero : p ≠ 0
  requires equivalent : p * a + m * f = m * e + p * b
  requires less : n * a + m * d < m * c + n * b
  shows n * e + p * d < p * c + n * f
proof
  have scaledLess := Less.mul_left with pNonzero, less
  ring_nf at scaledLess
  have scaledEquivalent : n * (p * a + m * f) = n * (m * e + p * b) by linear_combination n * equivalent
  ring_nf at scaledEquivalent
  have combined := Less.replace_left with scaledEquivalent, scaledLess
  have scaledTarget : m * (n * e + p * d) < m * (p * c + n * f)
    ring_nf at combined
    ring_nf
    exact combined
  exact Less.mul_left_cancel_positive with mNonzero, scaledTarget

-- Strict comparison of displayed representatives is transitive. The middle
-- representative disappears by scaling both comparisons to common products,
-- composing the resulting inequalities, and cancelling positive factors.
theorem rationalRepresentativeLess.transitive_cross (a b m c d n e f p : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  requires pNonzero : p ≠ 0
  requires left : n * a + m * d < m * c + n * b
  requires right : p * c + n * f < n * e + p * d
  shows p * a + m * f < m * e + p * b
proof
  have scaledLeft := Less.mul_left with pNonzero, left
  ring_nf at scaledLeft
  have scaledRight := Less.mul_left with mNonzero, right
  ring_nf at scaledRight
  have combined := Less.cross_transitive with scaledLeft, scaledRight
  have scaledTarget : n * (p * a + m * f) < n * (m * e + p * b)
    ring_nf at combined
    ring_nf
    exact combined
  exact Less.mul_left_cancel_positive with nNonzero, scaledTarget

theorem rationalRepresentativeLess.transport_right (u v w : Set)
  requires hu : u ∈ rationalRepresentatives
  requires hv : v ∈ rationalRepresentatives
  requires hw : w ∈ rationalRepresentatives
  requires less : rationalRepresentativeLess(u, v)
  requires equivalent : relates(rationalEquivalent, v, w)
  shows rationalRepresentativeLess(u, w)
proof
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, uShape⟩ := rationalRepresentatives.coordinates with hu
  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, vShape⟩ := rationalRepresentatives.coordinates with hv
  obtain ⟨e, eNat, f, fNat, p, pNat, pNonzero, wShape⟩ := rationalRepresentatives.coordinates with hw
  have displayedLess : rationalRepresentativeLess(
      ((a, b), m), ((c, d), n))
    simpa [uShape, vShape] using less
  have displayedEquivalent : relates(
      rationalEquivalent, ((c, d), n), ((e, f), p))
    simpa [vShape, wShape] using equivalent
  have crossLess := rationalRepresentativeLess.pair.forward with mNonzero, nNonzero, displayedLess
  have crossEquivalent := rationalEquivalent.relates_representatives.forward with
    nNonzero, pNonzero, displayedEquivalent
  have transported := rationalRepresentativeLess.transport_right_cross with
    mNonzero, nNonzero, pNonzero, crossLess, crossEquivalent
  have displayedResult := rationalRepresentativeLess.pair.backward with mNonzero, pNonzero, transported
  simpa [uShape, wShape] using displayedResult

theorem rationalRepresentativeLess.transport_left (u v w : Set)
  requires hu : u ∈ rationalRepresentatives
  requires hv : v ∈ rationalRepresentatives
  requires hw : w ∈ rationalRepresentatives
  requires equivalent : relates(rationalEquivalent, u, w)
  requires less : rationalRepresentativeLess(u, v)
  shows rationalRepresentativeLess(w, v)
proof
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, uShape⟩ := rationalRepresentatives.coordinates with hu
  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, vShape⟩ := rationalRepresentatives.coordinates with hv
  obtain ⟨e, eNat, f, fNat, p, pNat, pNonzero, wShape⟩ := rationalRepresentatives.coordinates with hw
  have displayedEquivalent : relates(
      rationalEquivalent, ((a, b), m), ((e, f), p))
    simpa [uShape, wShape] using equivalent
  have displayedLess : rationalRepresentativeLess(
      ((a, b), m), ((c, d), n))
    simpa [uShape, vShape] using less
  have crossEquivalent := rationalEquivalent.relates_representatives.forward with
    mNonzero, pNonzero, displayedEquivalent
  have crossLess := rationalRepresentativeLess.pair.forward with mNonzero, nNonzero, displayedLess
  have transported := rationalRepresentativeLess.transport_left_cross with
    mNonzero, nNonzero, pNonzero, crossEquivalent, crossLess
  have displayedResult := rationalRepresentativeLess.pair.backward with pNonzero, nNonzero, transported
  simpa [wShape, vShape] using displayedResult

theorem rationalRepresentativeLess.transport (u v uPrime vPrime : Set)
  requires hu : u ∈ rationalRepresentatives
  requires hv : v ∈ rationalRepresentatives
  requires huPrime : uPrime ∈ rationalRepresentatives
  requires hvPrime : vPrime ∈ rationalRepresentatives
  requires leftEquivalent : relates(rationalEquivalent, u, uPrime)
  requires rightEquivalent : relates(rationalEquivalent, v, vPrime)
  requires less : rationalRepresentativeLess(u, v)
  shows rationalRepresentativeLess(uPrime, vPrime)
proof
  have movedLeft := rationalRepresentativeLess.transport_left with hu, hv, huPrime, leftEquivalent, less
  exact rationalRepresentativeLess.transport_right with huPrime, hv, hvPrime, movedLeft, rightEquivalent

theorem rationalRepresentativeLess.transitive (u v w : Set)
  requires hu : u ∈ rationalRepresentatives
  requires hv : v ∈ rationalRepresentatives
  requires hw : w ∈ rationalRepresentatives
  requires left : rationalRepresentativeLess(u, v)
  requires right : rationalRepresentativeLess(v, w)
  shows rationalRepresentativeLess(u, w)
proof
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, uShape⟩ := rationalRepresentatives.coordinates with hu
  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, vShape⟩ := rationalRepresentatives.coordinates with hv
  obtain ⟨e, eNat, f, fNat, p, pNat, pNonzero, wShape⟩ := rationalRepresentatives.coordinates with hw
  have displayedLeft : rationalRepresentativeLess(
      ((a, b), m), ((c, d), n))
    simpa [uShape, vShape] using left
  have displayedRight : rationalRepresentativeLess(
      ((c, d), n), ((e, f), p))
    simpa [vShape, wShape] using right
  have leftCross := rationalRepresentativeLess.pair.forward with mNonzero, nNonzero, displayedLeft
  have rightCross := rationalRepresentativeLess.pair.forward with nNonzero, pNonzero, displayedRight
  have cross := rationalRepresentativeLess.transitive_cross with
    mNonzero, nNonzero, pNonzero, leftCross, rightCross
  have displayedResult := rationalRepresentativeLess.pair.backward with mNonzero, pNonzero, cross
  simpa [uShape, wShape] using displayedResult

predicate rationalLessWitness (p : Set) :=
  ∃ q ∈ ℚ, ∃ r ∈ ℚ,
    p = (q, r) ∧ ∃ u ∈ q, ∃ v ∈ r,
    rationalRepresentativeLess(u, v)

-- This graph is bounded by rationals × rationals, hence is a set.
-- Well-definedness under rationalEquivalent is the next arithmetic theorem;
-- the definition itself already exposes the exact representative semantics.
def rationalLess : Set :=
  { p ∈ ℚ × ℚ | rationalLessWitness(p) }

theorem rationalLess.bounded
  shows (rationalLess ⊆ ℚ × ℚ)
proof
  simp

theorem rationalLess.relation
  shows RelationOn(rationalLess, ℚ)
proof
  unfold RelationOn
  exact rationalLess.bounded

instance rationalLess.operation
  shows LessOperation(ℚ, rationalLess)
proof
  unfold LessOperation
  exact rationalLess.relation

notation infix 50 "<" => relates via LessOperation(ℚ, _) for Rational

theorem rationalLess.of_members (q r u v : Set)
  requires qRational : q ∈ ℚ
  requires rRational : r ∈ ℚ
  requires hu : u ∈ q
  requires hv : v ∈ r
  requires less : rationalRepresentativeLess(u, v)
  shows relates(rationalLess, q, r)
proof
  unfold relates
  apply rationalLess.membership.backward
  have bounded := product.pair with qRational, rRational
  constructor
  . exact bounded
  . unfold rationalLessWitness
    refine ⟨q, qRational, r, rRational, rfl, u, hu, v, hv, less⟩

-- Equivalent rational representatives denote the same quotient point, so a
-- strict representative comparison between them is impossible.
theorem rationalRepresentativeLess.not_equivalent (u v : Set)
  requires hu : u ∈ rationalRepresentatives
  requires hv : v ∈ rationalRepresentatives
  requires equivalent : relates(rationalEquivalent, u, v)
  shows ¬rationalRepresentativeLess(u, v)
proof
  intro less
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, uShape⟩ := rationalRepresentatives.coordinates with hu
  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, vShape⟩ := rationalRepresentatives.coordinates with hv
  have displayedEquivalent : relates(
      rationalEquivalent, ((a, b), m), ((c, d), n))
    simpa [uShape, vShape] using equivalent
  have displayedLess : rationalRepresentativeLess(
      ((a, b), m), ((c, d), n))
    simpa [uShape, vShape] using less
  have crossEqual := rationalEquivalent.relates_representatives.forward with
    mNonzero, nNonzero, displayedEquivalent
  have crossLess := rationalRepresentativeLess.pair.forward with mNonzero, nNonzero, displayedLess
  rw crossEqual at crossLess
  exact Less.irreflexive with crossLess

-- Elimination view for rational order. Client proofs receive representatives
-- together with their class memberships and ambient representative facts;
-- the quotient encoding stays behind this boundary.
theorem rationalLess.representatives (q r : Set)
  requires qRational : q ∈ ℚ
  requires rRational : r ∈ ℚ
  requires less : relates(rationalLess, q, r)
  shows ∃ u ∈ q, u ∈ rationalRepresentatives ∧
    ∃ v ∈ r, v ∈ rationalRepresentatives ∧ rationalRepresentativeLess(u, v)
proof
  unfold relates at less
  obtain ⟨_, left, _, right, _, shape, u, uMember, v, vMember, representativeLess⟩ := rationalLess.membership.forward with less
  obtain ⟨leftShape, rightShape⟩ := orderedPair.injective with shape
  rw ← leftShape at uMember
  rw ← rightShape at vMember
  have uRepresentative := Rational.representative with qRational, uMember
  have vRepresentative := Rational.representative with rRational, vMember
  refine ⟨u, uMember, uRepresentative, v, vMember, vRepresentative, representativeLess⟩

theorem rationalLess.irreflexive_on
  shows IrreflexiveOn(ℚ, rationalLess)
proof
  intros q qRational less
  obtain ⟨u, uInQ, uRepresentative, v, vInQ, vRepresentative, representativeLess⟩ := rationalLess.representatives with
    qRational, qRational, less
  have equivalent := Rational.members_related with qRational, uInQ, vInQ
  exact rationalRepresentativeLess.not_equivalent with
    uRepresentative, vRepresentative, equivalent, representativeLess

theorem rationalLess.transitive_on
  shows TransitiveOn(ℚ, rationalLess)
proof
  intros q qRational r rRational s sRational lessQR lessRS
  obtain ⟨u, uInQ, uRepresentative, v, vInR, vRepresentative, representativeLessUV⟩ := rationalLess.representatives with
    qRational, rRational, lessQR
  obtain ⟨vPrime, vPrimeInR, vPrimeRepresentative, w, wInS, wRepresentative, representativeLessVW⟩ := rationalLess.representatives with
    rRational, sRational, lessRS
  have middleEquivalent := Rational.members_related with rRational, vInR, vPrimeInR
  have aligned := rationalRepresentativeLess.transport_right with
    uRepresentative, vRepresentative, vPrimeRepresentative, representativeLessUV, middleEquivalent
  have representativeLessUW := rationalRepresentativeLess.transitive with
    uRepresentative, vPrimeRepresentative, wRepresentative, aligned, representativeLessVW
  exact rationalLess.of_members with qRational, sRational, uInQ, wInS, representativeLessUW

theorem rationalLess.connected_on
  shows ConnectedOn(ℚ, rationalLess)
proof
  intros q qRational r rRational distinct
  obtain ⟨u, uInQ, uRepresentative⟩ := Rational.some_representative with qRational
  obtain ⟨v, vInR, vRepresentative⟩ := Rational.some_representative with rRational
  obtain ⟨a, aNat, b, bNat, m, mNat, mNonzero, uShape⟩ := rationalRepresentatives.coordinates with uRepresentative
  obtain ⟨c, cNat, d, dNat, n, nNat, nNonzero, vShape⟩ := rationalRepresentatives.coordinates with vRepresentative
  have leftCrossNat : Nat(n * a + m * d) by typecheck
  have rightCrossNat : Nat(m * c + n * b) by typecheck
  have comparison := Less.trichotomy with leftCrossNat, rightCrossNat
  rcases comparison with less | equal | greater
  . left
    have representativeLess : rationalRepresentativeLess(u, v)
      simpa [uShape, vShape] using
        rationalRepresentativeLess.pair.backward with mNonzero, nNonzero, less
    exact rationalLess.of_members with qRational, rRational, uInQ, vInR, representativeLess
  . exfalso
    have representativeEquivalent : relates(rationalEquivalent, u, v)
      simpa [uShape, vShape] using
        rationalEquivalent.relates_representatives.backward with mNonzero, nNonzero, equal
    apply distinct
    exact Rational.eq_of_related_members with qRational, rRational, uInQ, vInR, representativeEquivalent
  . right
    have representativeGreater : rationalRepresentativeLess(v, u)
      simpa [uShape, vShape] using
        rationalRepresentativeLess.pair.backward with nNonzero, mNonzero, greater
    exact rationalLess.of_members with rRational, qRational, vInR, uInQ, representativeGreater

theorem rationalLess.strict_order
  shows StrictOrder(ℚ, rationalLess)
proof
  unfold StrictOrder
  have relation := rationalLess.relation
  refine ⟨relation, rationalLess.irreflexive_on, rationalLess.transitive_on⟩

theorem rationalLess.strict_linear_order
  shows StrictLinearOrder(ℚ, rationalLess)
proof
  refine ⟨rationalLess.strict_order, rationalLess.connected_on⟩

-- A strict comparison of representatives descends to a comparison of their
-- rational equivalence classes. No representative is chosen by the kernel:
-- the two displayed representatives are explicit witnesses in their classes.
theorem rationalLess.of_representatives (a b m c d n : Nat)
  requires mNonzero : m ≠ 0
  requires nNonzero : n ≠ 0
  requires crossLess : n * a + m * d < m * c + n * b
  shows relates(
    rationalLess,
    ⟦((a, b), m)⟧[rationalRepresentatives, rationalEquivalent],
    ⟦((c, d), n)⟧[rationalRepresentatives, rationalEquivalent])
proof
  have leftRepresentative := rationalRepresentatives.pair at a, b, m with mNonzero
  have rightRepresentative := rationalRepresentatives.pair at c, d, n with nNonzero
  have equivalence := rationalEquivalent.equivalence
  have leftRational := quotient.contains_class with equivalence, leftRepresentative
  have rightRational := quotient.contains_class with equivalence, rightRepresentative
  have leftSelf := equivalenceClass.self with equivalence, leftRepresentative
  have rightSelf := equivalenceClass.self with equivalence, rightRepresentative
  have representativeLess := rationalRepresentativeLess.pair.backward with mNonzero, nNonzero, crossLess
  exact rationalLess.of_members with leftSelf, rightSelf, representativeLess