-- Negation of Dedekind real numbers
-- 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.Real.Negation
import Addition
import Archimedean
import Algebra.OrderedField.Defs

-- The open reflected complement of a lower cut.  The strict inequality is
-- essential: it makes the result rounded without choosing endpoints.
def realNegCut (A : Set) : Set :=
  { q ∈ ℚ | ∃ r ∈ ℚ, ¬(r ∈ A) ∧ q < -r }

theorem realNegCut.subset_rationals (A : Set)
  shows realNegCut(A) ⊆ ℚ
proof
  simp

theorem realNegCut.nonempty (A : Real)
  shows Nonempty(realNegCut(A))
proof
  have cutA := Real.characterization.forward with assumption
  have properA := DedekindCut.proper with cutA
  obtain ⟨u, uInQ, uMissing⟩ := ProperSubset.missing with properA
  have uRational : Rational(u) by exact uInQ
  have negURational := rationalNegValue.rational with uRational
  obtain ⟨q, qInQ, qLessNegU⟩ := rationalLess.exists_below with negURational
  witness q
  exact realNegCut.membership.backward with ⟨qInQ, u, uInQ, uMissing, qLessNegU⟩

theorem realNegCut.proper (A : Real)
  shows realNegCut(A) ≠ ℚ
proof
  have cutA := Real.characterization.forward with assumption
  obtain ⟨a, aInA⟩ := DedekindCut.nonempty with cutA
  have subsetA := DedekindCut.subset_rationals with cutA
  have aInQ := subsetA with a, aInA
  have aRational : Rational(a) by exact aInQ
  have negARational := rationalNegValue.rational with aRational
  intro allRationals
  have negAInCut : -a ∈ realNegCut(A)
    rw allRationals
    exact negARational
  obtain ⟨negAInQ, r, rInQ, rMissing, negALessNegR⟩ := realNegCut.membership.forward with negAInCut
  have rRational : Rational(r) by exact rInQ
  have negated := rationalLess.neg_reverse at -a, -r with
    negARational, rationalNegValue.rational at r with rRational,
    negALessNegR
  have involutiveA := rationalNegValue.involutive with aRational
  have involutiveR := rationalNegValue.involutive with rRational
  rw [involutiveA, involutiveR] at negated
  have rInA := DedekindCut.downward with cutA, aInA, rInQ, negated
  exact rMissing with rInA

theorem realNegCut.downward (A p q : Set)
  requires qInNeg : q ∈ realNegCut(A)
  requires pInQ : p ∈ ℚ
  requires pLessQ : relates(rationalLess, p, q)
  shows p ∈ realNegCut(A)
proof
  obtain ⟨qInQ, r, rInQ, rMissing, qLessNegR⟩ := realNegCut.membership.forward with qInNeg
  have pRational : Rational(p) by exact pInQ
  have qRational : Rational(q) by exact qInQ
  have rRational : Rational(r) by exact rInQ
  have pLessNegR := rationalLess.transitive at p, q, -r with
    pRational, qRational, rationalNegValue.rational at r with rRational,
    pLessQ, qLessNegR
  exact realNegCut.membership.backward with ⟨pInQ, r, rInQ, rMissing, pLessNegR⟩

theorem realNegCut.no_greatest (A q : Set)
  requires qInNeg : q ∈ realNegCut(A)
  shows ∃ s ∈ realNegCut(A), relates(rationalLess, q, s)
proof
  obtain ⟨qInQ, r, rInQ, rMissing, qLessNegR⟩ := realNegCut.membership.forward with qInNeg
  obtain ⟨s, sInQ, qLessS, sLessNegR⟩ := rationalLess.dense with qLessNegR
  witness s
  constructor
  . apply realNegCut.membership.backward at A, s
    refine ⟨sInQ, r, rInQ, rMissing, sLessNegR⟩
  . exact qLessS

theorem realNegCut.cut (A : Real)
  shows DedekindCut(realNegCut(A))
proof
  unfold DedekindCut
  refine ⟨realNegCut.subset_rationals at A,
    realNegCut.nonempty at A with assumption,
    realNegCut.proper at A with assumption, _, _⟩
  . intros q qInNeg p pInQ pLessQ
    exact realNegCut.downward with qInNeg, pInQ, pLessQ
  . intros q qInNeg
    exact realNegCut.no_greatest with qInNeg

theorem realNegCut.real (A : Real)
  shows Real(realNegCut(A))
proof
  apply Real.characterization.backward
  exact realNegCut.cut with assumption

theorem realNegCut.subset_reverse (A B : Real)
  requires subset : A ⊆ B
  shows realNegCut(B) ⊆ realNegCut(A)
proof
  intros q qInNegB
  obtain ⟨qInQ, r, rInQ, rMissingB, qLessNegR⟩ := realNegCut.membership.forward with qInNegB
  have rMissingA : ¬(r ∈ A)
    intro rInA
    specialize subset with r, rInA
    exact rMissingB with subset
  exact realNegCut.membership.backward with ⟨qInQ, r, rInQ, rMissingA, qLessNegR⟩

-- Negation as a total set-valued function graph on the real carrier.
def realNeg : Set :=
  { p ∈ (ℝ × ℝ) | ∃ A ∈ ℝ, p = (A ↦ realNegCut(A)) }

def realNegValue (A : Real) : Real := realNeg(A)

theorem realNeg.relates (A : Real)
  shows relates(realNeg, A, realNegCut(A))
proof
  have realA : A ∈ ℝ by simp [Real]
  unfold relates
  apply realNeg.membership.backward
  constructor
  . apply product.pair at A, realNegCut(A), ℝ, ℝ
    . exact realA
    . exact realNegCut.real at A
  . refine ⟨A, realA, rfl⟩

theorem realNeg.factors (input output : Set)
  requires mapped : relates(realNeg, input, output)
  shows ∃ A ∈ ℝ, input = A ∧ output = realNegCut(A)
proof
  unfold relates at mapped
  simp [realNeg.membership] at mapped
  rcases mapped with ⟨bounded, A, realA, shape⟩
  obtain ⟨inputShape, outputShape⟩ := orderedPair.injective with shape
  refine ⟨A, realA, inputShape, outputShape⟩

theorem realNeg.total
  shows TotalBetween(realNeg, ℝ, ℝ)
proof
  intros A realA
  have typedA : Real(A) by exact realA
  refine ⟨realNegCut(A), realNegCut.real at A with typedA, realNeg.relates at A with typedA⟩

theorem realNeg.functional
  shows Functional(realNeg)
proof
  intros input y inputY z inputZ
  obtain ⟨A, realA, inputFirst, outputFirst⟩ := realNeg.factors with inputY
  obtain ⟨B, realB, inputSecond, outputSecond⟩ := realNeg.factors with inputZ
  rw inputFirst at inputSecond
  rw [outputFirst, outputSecond, inputSecond]
  rfl

theorem realNeg.function
  shows realNeg : ℝ → ℝ
proof
  constructor
    intros p member
    simp [realNeg.membership] at member
    rcases member with ⟨bounded, witnesses⟩
    exact bounded
  . constructor
    . exact realNeg.functional
    . exact realNeg.total

instance realNeg.operation
  shows NegOperation(ℝ, realNeg)
proof
  exact realNeg.function

notation prefix 75 "-" => apply via NegOperation(ℝ, _) for Real

theorem realNegValue.real (A : Real)
  shows Real(-A)
proof
  have realA : A ∈ ℝ by simp [Real]
  obtain ⟨B, realB, mapped⟩ := FunctionBetween.exists_value with realNeg.function, realA
  have applied := FunctionBetween.apply_value with realNeg.function, mapped
  rw applied
  exact realB

theorem realNegValue.cut (A : Real)
  shows -A = realNegCut(A)
proof
  have mapped := realNeg.relates at A
  exact FunctionBetween.apply_value with realNeg.function, mapped

theorem realNegCut.involutive (A : Real)
  shows realNegCut(realNegCut(A)) = A
proof
  ext q
  constructor
  . intro qInDoubleNeg
    obtain ⟨qInQ, r, rInQ, rMissingNegA, qLessNegR⟩ := realNegCut.membership.forward with qInDoubleNeg
    by_contra qMissingA
    have qRational : Rational(q) by exact qInQ
    have rRational : Rational(r) by exact rInQ
    have rLessNegQ := rationalLess.neg_reverse at q, -r with
      qRational, rationalNegValue.rational at r with rRational,
      qLessNegR
    have involutiveR := rationalNegValue.involutive with rRational
    rw involutiveR at rLessNegQ
    have rInNegA : r ∈ realNegCut(A) := realNegCut.membership.backward with ⟨rInQ, q, qInQ, qMissingA, rLessNegQ⟩
    exact rMissingNegA with rInNegA
  . intro qInA
    have cutA := Real.characterization.forward with assumption
    have subsetA := DedekindCut.subset_rationals with cutA
    have qInQ := subsetA with q, qInA
    obtain ⟨s, sInA, qLessS⟩ := DedekindCut.no_greatest with cutA, qInA
    have sInQ := subsetA with s, sInA
    have sRational : Rational(s) by typecheck
    have negSRational := rationalNegValue.rational with sRational
    have negSMissing : ¬(-s ∈ realNegCut(A))
      intro negSInNegA
      obtain ⟨negSInQ, u, uInQ, uMissingA, negSLessNegU⟩ := realNegCut.membership.forward with negSInNegA
      have uRational : Rational(u) by exact uInQ
      have uLessS := rationalLess.neg_reverse at -s, -u with
        negSRational, rationalNegValue.rational at u with uRational,
        negSLessNegU
      have involutiveS := rationalNegValue.involutive with sRational
      have involutiveU := rationalNegValue.involutive with uRational
      rw [involutiveS, involutiveU] at uLessS
      have uInA := DedekindCut.downward with cutA, sInA, uInQ, uLessS
      exact uMissingA with uInA
    apply realNegCut.membership.backward
    have involutiveS := rationalNegValue.involutive with sRational
    rw ← involutiveS at qLessS
    refine ⟨qInQ, -s, negSRational, negSMissing, qLessS⟩

theorem realNegValue.involutive (A : Real)
  shows -(-A) = A
proof
  have negReal := realNegValue.real at A
  calc
    -(-A) = realNegCut(-A) := realNegValue.cut at -A with negReal
    _ = realNegCut(realNegCut(A)) := by simp [realNegValue.cut]
    _ = A := realNegCut.involutive at A with assumption

-- A cut and its reflected complement add to the zero cut.  The reverse
-- inclusion is the one genuinely Archimedean step: choose an interior
-- rational s between q and zero, then cross the boundary of A within -s.
theorem realAddCut.neg_right (A : Real)
  shows realAddCut(A, realNegCut(A)) = realZero
proof
  have cutA := Real.characterization.forward with assumption
  have subsetA := DedekindCut.subset_rationals with cutA
  ext q
  constructor
  . intro qInSum
    obtain ⟨qInQ, a, aInA, b, bInNegA, qLessSum⟩ := realAddCut.membership_value.forward with qInSum
    obtain ⟨bInQ, r, rInQ, rMissingA, bLessNegR⟩ := realNegCut.membership.forward with bInNegA
    have aRational : Rational(a)
      unfold Rational
      exact subsetA with a, aInA
    have bRational : Rational(b) by exact bInQ
    have rRational : Rational(r) by exact rInQ
    have aLessR := DedekindCut.lt_missing with cutA, aInA, rInQ, rMissingA
    have sumBelowDifference := rationalLess.add_left at
      b, -r, a with bRational,
      rationalNegValue.rational at r with rRational,
      aRational, bLessNegR
    have differenceNegative := rationalLess.sub_self_negative with aLessR
    unfold rationalSubValue at differenceNegative
    rw ← rationalAddValue.notation at qLessSum
    have qRational : Rational(q) by exact qInQ
    have qBelowDifference := rationalLess.transitive with qLessSum, sumBelowDifference
    have qBelowZero := rationalLess.transitive with qBelowDifference, differenceNegative
    unfold realZero
    simp [rationalCut.membership]
  . intro qInZero
    unfold realZero at qInZero
    simp [rationalCut.membership] at qInZero
    rcases qInZero with ⟨qInQ, qLessZero⟩
    have qRational : Rational(q) by exact qInQ
    obtain ⟨s, sInQ, qLessS, sLessZero⟩ := rationalLess.dense with qRational, rationalZero.rational, qLessZero
    have sRational : Rational(s) by exact sInQ
    have negSRational := rationalNegValue.rational with sRational
    have epsilonPositive : rationalZero < -s
      have shifted := rationalLess.add_right with sRational, rationalZero.rational, negSRational, sLessZero
      have inverse := rationalAddValue.neg_right with sRational
      have identity := rationalAddValue.zero_left with negSRational
      rwa [inverse, identity] at shifted
    obtain ⟨p, pRational, pInA, boundaryMissing⟩ := DedekindCut.exists_boundary_within with
      cutA, epsilonPositive
    have rRational := rationalAddValue.rational_raw with pRational, negSRational
    have pMinusR := rationalSubValue.sub_sum_left with pRational, negSRational
    have involutiveS := rationalNegValue.involutive with sRational
    rw involutiveS at pMinusR
    rw ← pMinusR at qLessS
    unfold rationalSubValue at qLessS
    have rNotationRational := rationalAddValue.rational with pRational, negSRational
    have negRNotationRational := rationalNegValue.rational with rNotationRational
    have qMinusPLessNegR := rationalLess.sub_left with qRational, pRational, negRNotationRational, qLessS
    have qMinusPRational := rationalSubValue.rational with qRational, pRational
    obtain ⟨t, tInQ, qMinusPLessT, tLessNegR⟩ := rationalLess.dense with
      qMinusPRational, negRNotationRational, qMinusPLessNegR
    rw rationalAddValue.notation at tLessNegR
    have tInNegA : t ∈ realNegCut(A)
      apply realNegCut.membership.backward
      refine ⟨tInQ, rationalAddValue(p, -s), rRational,
        boundaryMissing, tLessNegR⟩
    have qLessSum := rationalLess.add_left_of_sub_left with qRational, pRational, qMinusPLessT
    apply realAddCut.membership_value.backward
    rw rationalAddValue.notation at qLessSum
    refine ⟨qInQ, p, pInA, t, tInNegA, qLessSum⟩

theorem realAddValue.neg_right (A : Real)
  shows A + (-A) = 0
proof
  calc
    A + (-A) = realAddCut(A, realNegCut(A)) := by simp [realAddValue.cut, realNegValue.cut]
    _ = realZero := realAddCut.neg_right at A with assumption

theorem realAddValue.neg_left (A : Real)
  shows (-A) + A = 0
proof
  have negReal := realNegValue.real at A
  calc
    (-A) + A = A + (-A) :=
      realAddValue.commutative with negReal, assumption
    _ = realZero := realAddValue.neg_right at A with assumption

instance realAdd.abelian_group
  shows IsAbelianGroup(ℝ, realAdd, realZero, realNeg)
proof
  constructor
    constructor
    . have additive := realAdd.comm_monoid
      simp [IsCommMonoid]
      constructor
      . exact realNeg.function
      . intros A realA
        have typedA : Real(A) by exact realA
        constructor
        . exact realAddValue.neg_left with typedA
        . exact realAddValue.neg_right with typedA
  . have additive := realAdd.comm_monoid
    simp [IsCommMonoid]

theorem realNegCut.strict_antitone (A B : Real)
  requires proper : A ⊂ B
  shows realNegCut(B) ⊂ realNegCut(A)
proof
  constructor
    intros q qInNegB
    obtain ⟨qInQ, r, rInQ, rMissingB, qLessNegR⟩ := realNegCut.membership.forward with qInNegB
    have subsetAB := ProperSubset.subset with proper
    have rMissingA : ¬(r ∈ A)
      intro rInA
      have rInB := subsetAB with r, rInA
      exact rMissingB with rInB
    exact realNegCut.membership.backward with ⟨qInQ, r, rInQ, rMissingA, qLessNegR⟩
  . intro equalNeg
    have involutiveA := realNegCut.involutive at A
    have involutiveB := realNegCut.involutive at B
    rw [equalNeg, involutiveA] at involutiveB
    have unequal := ProperSubset.ne with proper
    exact unequal with involutiveB

theorem RealLess.neg_reverse (A B : Real)
  requires less : RealLess(A, B)
  shows RealLess(-B, -A)
proof
  rcases less with ⟨realA, realB, proper⟩
  have negAReal := realNegValue.real with realA
  have negBReal := realNegValue.real with realB
  unfold RealLess
  refine ⟨negBReal, negAReal, _⟩
  have antitone := realNegCut.strict_antitone with realA, realB, proper
  have cutA := realNegValue.cut with realA
  have cutB := realNegValue.cut with realB
  rwa [cutA, cutB]

-- Translation preserves the strict order on the Dedekind reals.  The subset
-- direction is immediate from witnesses for cut addition; strictness follows
-- by cancelling the common summand in the additive group.
theorem realAddCut.subset_left (A B C : Real)
  requires subset : A ⊆ B
  shows realAddCut(A, C) ⊆ realAddCut(B, C)
proof
  intros q qInAC
  obtain ⟨qInQ, a, aInA, c, cInC, qLessSum⟩ := realAddCut.membership_value.forward with qInAC
  have aInB : a ∈ B by exact subset with a, aInA
  exact realAddCut.membership_value.backward with ⟨qInQ, a, aInB, c, cInC, qLessSum⟩

theorem realLess.add_right (A B C : Real)
  requires less : A < B
  shows A + C < B + C
proof
  obtain ⟨realA, realB, proper⟩ := realLess.characterization.forward with less
  have properSubset := ProperSubset.subset with proper
  have sumACReal := realAddValue.real at A, C with *
  have sumBCReal := realAddValue.real at B, C with *
  apply realLess.characterization.backward
  unfold RealLess
  refine ⟨sumACReal, sumBCReal, _⟩
  constructor
  . have cutSubset := realAddCut.subset_left at A, B, C with
      *{3}, properSubset
    have cutAC := realAddValue.cut at A, C with *
    have cutBC := realAddValue.cut at B, C with *
    rwa [← cutAC, ← cutBC] at cutSubset
  . intro equalSums
    have negCReal := realNegValue.real at C
    have equalCancelled : (A + C) + (-C) = (B + C) + (-C)
      rw equalSums
      rfl
    have leftCancel : (A + C) + (-C) = A
      calc
        (A + C) + (-C) = A + (C + (-C)) :=
          realAddValue.associative at A, C, -C with
            *{2}, negCReal
        _ = A + 0 := by simp [realAddValue.neg_right]
        _ = A := realAddValue.zero_right at A with assumption
    have rightCancel : (B + C) + (-C) = B
      calc
        (B + C) + (-C) = B + (C + (-C)) :=
          realAddValue.associative at B, C, -C with
            *{2}, negCReal
        _ = B + 0 := by simp [realAddValue.neg_right]
        _ = B := realAddValue.zero_right at B with assumption
    rw [leftCancel, rightCancel] at equalCancelled
    have unequal := ProperSubset.ne with proper
    exact unequal with equalCancelled

theorem realLess.add_left (A B C : Real)
  requires less : A < B
  shows C + A < C + B
proof
  have translated := realLess.add_right at A, B, C with
    *{3}, less
  have leftCommutative := realAddValue.commutative at A, C with
    *{2}
  have rightCommutative := realAddValue.commutative at B, C with
    *{2}
  rwa [leftCommutative, rightCommutative] at translated

theorem realLess.add (A B C D : Real)
  requires ab : A < B
  requires cd : C < D
  shows A + C < B + D
proof
  have first := realLess.add_right at A, B, C with
    *{3}, ab
  have second := realLess.add_left at C, D, B with
    *{3}, cd
  exact realLess.transitive with first, second

theorem realLess.add_right_iff (A B C : Real)
  shows A + C < B + C ↔ A < B
proof
  constructor
  . intro translated
    have sumACReal := realAddValue.real at A, C with *
    have sumBCReal := realAddValue.real at B, C with *
    have negCReal := realNegValue.real at C
    have cancelled := realLess.add_right with sumACReal, sumBCReal, negCReal, translated
    have leftCancel : (A + C) + (-C) = A
      calc
        (A + C) + (-C) = A + (C + (-C)) :=
          realAddValue.associative at A, C, -C with
            *{2}, negCReal
        _ = A + 0 := by simp [realAddValue.neg_right]
        _ = A := realAddValue.zero_right at A with assumption
    have rightCancel : (B + C) + (-C) = B
      calc
        (B + C) + (-C) = B + (C + (-C)) :=
          realAddValue.associative at B, C, -C with
            *{2}, negCReal
        _ = B + 0 := by simp [realAddValue.neg_right]
        _ = B := realAddValue.zero_right at B with assumption
    rwa [leftCancel, rightCancel] at cancelled
  . intro less
    exact realLess.add_right with less

-- Subtraction is addition of the additive inverse, exposed at the same typed
-- mathematical boundary as rational subtraction.
def realSubValue (A B : Real) : Real := A + (-B)
notation infixl 60 "-" => realSubValue for Real

theorem realSubValue.real (A B : Real)
  shows Real(A - B)
proof
  unfold realSubValue
  exact realAddValue.real at A, -B with
    assumption, realNegValue.real at B with assumption

theorem realNegValue.zero
  shows -realZero = realZero
proof
  have inverse := realAddValue.neg_right with realZero.real
  have negZeroReal := realNegValue.real with realZero.real
  have identity := realAddValue.zero_left with negZeroReal
  rwa identity at inverse

theorem realNegCut.zero
  shows realNegCut(realZero) = realZero
proof
  have cut := realNegValue.cut with realZero.real
  rw ← cut
  exact realNegValue.zero

theorem realSubValue.self (A : Real)
  shows A - A = 0
proof
  unfold realSubValue
  exact realAddValue.neg_right with assumption

theorem realSubValue.zero_right (A : Real)
  shows A - 0 = A
proof
  unfold realSubValue
  rw realNegValue.zero
  exact realAddValue.zero_right with assumption

theorem realSubValue.zero_left (A : Real)
  shows 0 - A = -A
proof
  unfold realSubValue
  exact realAddValue.zero_left at -A with
    realNegValue.real at A with assumption

theorem realSubValue.add_cancel_right (A B : Real)
  shows (A + B) - B = A
proof
  unfold realSubValue
  have negBReal := realNegValue.real at B
  calc
    (A + B) + (-B) = A + (B + (-B)) :=
      realAddValue.associative at A, B, -B with
        *{2}, negBReal
    _ = A + 0 := by simp [realAddValue.neg_right]
    _ = A := realAddValue.zero_right at A with assumption

theorem realSubValue.add_cancel_left (A B : Real)
  shows (A + B) - A = B
proof
  have commutes := realAddValue.commutative at A, B with
    *{2}
  calc
    (A + B) - A = (B + A) - A := by simp [commutes]
    _ = B := realSubValue.add_cancel_right at B, A with
      *{2}

theorem realLess.iff_pos_sub (A B : Real)
  shows A < B ↔ 0 < B - A
proof
  constructor
  . intro less
    have negAReal := realNegValue.real at A
    have shifted := realLess.add_left at A, B, -A with
      *{2}, negAReal, less
    have leftInverse := realAddValue.neg_left at A
    rw leftInverse at shifted
    have differenceCommutative := realAddValue.commutative at -A, B with
      negAReal, assumption
    rw differenceCommutative at shifted
    unfold realSubValue
    exact shifted
  . intro positive
    have differenceReal := realSubValue.real at B, A with
      *{2}
    have shifted := realLess.add_right at realZero, B - A, A with
      realZero.real, differenceReal, assumption, positive
    have leftIdentity := realAddValue.zero_left at A
    have rightCancel : (B - A) + A = B
      unfold realSubValue
      have negAReal := realNegValue.real at A
      calc
        (B + (-A)) + A = B + ((-A) + A) :=
          realAddValue.associative at B, -A, A with
            assumption, negAReal, assumption
        _ = B + 0 := by simp [realAddValue.neg_left]
        _ = B := realAddValue.zero_right at B with assumption
    rwa [leftIdentity, rightCancel] at shifted

instance realAdd.strict_mono
  shows AddStrictMono(ℝ, realAdd, realLess)
proof
  intros A realA B realB C realC less
  exact realLess.add_right with less

theorem realNegValue.type (A : Real)
  shows Real(realNegValue(A))
proof
  have closed := realNegValue.real with *
  unfold realNegValue
  exact closed