-- The absolute-value cut on the Dedekind reals
-- 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.AbsoluteValue
import Squares
import Algebra.OrderedField.Core

-- Absolute value is the sum of the positive and negative parts. This
-- definition is canonical for lower cuts and avoids choosing a sign case.
def realAbsCut (A : Set) : Set :=
  realAddCut(realPositivePart(A), realNegativePart(A))

theorem realAbsCut.real (A : Real)
  shows Real(realAbsCut(A))
proof
  unfold realAbsCut
  exact realAddCut.real at realPositivePart(A), realNegativePart(A) with
    realPositivePart.real at A with assumption,
    realNegativePart.real at A with assumption

theorem realAbsCut.of_nonnegative (A : Real)
  requires nonnegative : 0 ≤ A
  shows realAbsCut(A) = A
proof
  have subset := realLe.subset with realZero.real, nonnegative
  have positive := realPositivePart.eq_of_nonnegative with subset
  have negative := realNegativePart.eq_zero_of_nonnegative with subset
  simp [realAbsCut, positive, negative, realAddCut.zero_right]

theorem realAbsCut.of_nonpositive (A : Real)
  requires nonpositive : A ≤ 0
  shows realAbsCut(A) = realNegCut(A)
proof
  have subset := realLe.subset at A, realZero with
    assumption, realZero.real, nonpositive
  have positive := realPositivePart.eq_zero_of_nonpositive with subset
  have negative := realNegativePart.eq_neg_of_nonpositive with subset
  simp [realAbsCut, positive, negative, realAddCut.zero_left]

-- Absolute value as a total function graph on the real carrier.
def realAbs : Set :=
  { p ∈ (ℝ × ℝ) | ∃ A ∈ ℝ, p = (A ↦ realAbsCut(A)) }

def abs (A : Real) : Real := realAbs(A)

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

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

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

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

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

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

theorem abs.cut (A : Real)
  shows abs(A) = realAbsCut(A)
proof
  have mapped := realAbs.relates at A
  unfold abs
  exact FunctionBetween.apply_value with realAbs.function, mapped

theorem abs.of_nonnegative (A : Real)
  requires nonnegative : 0 ≤ A
  shows abs(A) = A
proof
  calc
    abs(A) = realAbsCut(A) := abs.cut at A with assumption
    _ = A := realAbsCut.of_nonnegative at A with nonnegative

theorem abs.of_nonpositive (A : Real)
  requires nonpositive : A ≤ 0
  shows abs(A) = -A
proof
  have cut := realNegValue.cut at A
  calc
    abs(A) = realAbsCut(A) := abs.cut at A with assumption
    _ = realNegCut(A) := realAbsCut.of_nonpositive at A with
      assumption, nonpositive
    _ = -A := by simp [cut]

theorem abs.zero
  shows abs(0) = 0
proof
  have zeroLeZero := realLe.of_subset at realZero, realZero with
    realZero.real, realZero.real, Subset.reflexive at realZero
  exact abs.of_nonnegative with realZero.real, zeroLeZero

-- The Dedekind construction discharges the generic ordered-field interface
-- once, and the algebraic absolute-value laws below are inherited from it
-- instead of being reproved from cuts.
theorem realAbs.absolute_value
  shows AbsoluteValue(ℝ, realZero, realNeg, realLess, realAbs)
proof
  constructor
  . exact realAbs.function
  . constructor
    . have zero := abs.zero
      unfold abs at zero
      exact zero
    . intros A realA
      have typedA : Real(A) by exact realA
      constructor
      . intro positive
        have nonnegative := realLess.implies_le with realZero.real, positive
        have shape := abs.of_nonnegative with nonnegative
        unfold abs at shape
        assumption
      . intro negative
        have nonpositive := realLess.implies_le with typedA, realZero.real, negative
        have shape := abs.of_nonpositive with nonpositive
        unfold abs at shape
        assumption

theorem realLe.of_less_equal_by (A B : Real)
  requires order : LessEqualBy(ℝ, realLess, A, B)
  shows A ≤ B
proof
  rcases order with ⟨realA, realB, comparison⟩
  cases comparison with equal | less
  . rw equal
    exact realLe.reflexive with assumption
  . exact realLess.implies_le with less

theorem abs.nonnegative (A : Real)
  shows 0 ≤ abs(A)
proof
  have sign := Real.sign_cases at A
  cases sign with nonpositive | nonnegative
  . have leZero := realLe.of_subset at A, realZero with
      assumption, realZero.real, nonpositive
    have shape := abs.of_nonpositive with leZero
    have negSubset := realNegValue.nonnegative_of_nonpositive with nonpositive
    have result := realLe.of_subset with realZero.real, negSubset
    rwa shape
  . have result := realLe.of_subset at realZero, A with
      realZero.real, assumption, nonnegative
    have shape := abs.of_nonnegative with result
    rwa shape

theorem abs.eq_zero_iff (A : Real)
  shows abs(A) = 0 ↔ A = 0
proof
  have realA : A ∈ ℝ by simp [Real]
  have generic := AbsoluteValue.eq_zero_iff with reals.ordered_field, realAbs.absolute_value, realA
  constructor
  . intro zero
    apply generic.forward
    unfold abs at zero
    assumption
  . intro equal
    rw equal
    exact abs.zero

theorem abs.positive_of_ne (A : Real)
  requires nonzero : A ≠ 0
  shows 0 < abs(A)
proof
  have realA : A ∈ ℝ by simp [Real]
  have positive := AbsoluteValue.positive_of_ne with
    reals.ordered_field, realAbs.absolute_value, realA, nonzero
  unfold abs
  exact positive

theorem abs.neg (A : Real)
  shows abs(-A) = abs(A)
proof
  have realA : A ∈ ℝ by simp [Real]
  have generic := AbsoluteValue.neg with reals.ordered_field, realAbs.absolute_value, realA
  simp [abs]

theorem abs.mul (A B : Real)
  shows abs(A * B) = abs(A) * abs(B)
proof
  have realA : A ∈ ℝ by simp [Real]
  have realB : B ∈ ℝ by simp [Real]
  have generic := AbsoluteValue.mul with reals.ordered_field, realAbs.absolute_value, realA, realB
  simp [abs]

theorem abs.inv (A : Real)
  requires nonzero : A ≠ 0
  shows abs(realInvValue(A)) = realInvValue(abs(A))
proof
  have inverseReal := realInvValue.real at A
  have absANonzero : abs(A) ≠ 0
    intro absoluteZero
    apply nonzero
    exact abs.eq_zero_iff.forward with absoluteZero
  have inverseLaw := realInvValue.mul_right with nonzero
  have multiplicative := abs.mul at A, realInvValue(A) with
    assumption, inverseReal
  have oneNonnegative := realLess.implies_le with realZero.real, realOne.real, realZero.lt_one
  have absoluteOne := abs.of_nonnegative with realOne.real, oneNonnegative
  have candidateLaw : abs(A) * abs(realInvValue(A)) = 1
    calc
      abs(A) * abs(realInvValue(A)) = abs(A * realInvValue(A)) := by cc
      _ = abs(1) := by cc
      _ = 1 := absoluteOne
  exact realInvValue.eq_of_mul_right with absANonzero, candidateLaw

theorem abs.upper (A : Real)
  shows A ≤ abs(A)
proof
  have realA : A ∈ ℝ by simp [Real]
  have generic := AbsoluteValue.upper with reals.ordered_field, realAbs.absolute_value, realA
  have bound : LessEqualBy(ℝ, realLess, A, abs(A))
    unfold abs
    exact generic
  exact realLe.of_less_equal_by at A, abs(A) with
    assumption, abs.real at A with assumption, bound

theorem abs.upper_neg (A : Real)
  shows -A ≤ abs(A)
proof
  have realA : A ∈ ℝ by simp [Real]
  have generic := AbsoluteValue.upper_neg with reals.ordered_field, realAbs.absolute_value, realA
  have bound : LessEqualBy(ℝ, realLess, -A, abs(A))
    unfold abs
    exact generic
  exact realLe.of_less_equal_by at -A, abs(A) with
    realNegValue.real at A with assumption,
    abs.real at A with assumption, bound

-- Both A + B and -(A + B) lie below abs(A) + abs(B); the sign of
-- A + B selects the defining branch of absolute value.
theorem abs.triangle (A B : Real)
  shows abs(A + B) ≤ abs(A) + abs(B)
proof
  have sumReal := realAddValue.real at A, B with *
  have absAReal := abs.real at A
  have absBReal := abs.real at B
  have positiveBound := realLe.add at A, abs(A), B, abs(B) with
    assumption, absAReal, assumption, absBReal,
    abs.upper at A with assumption, abs.upper at B with assumption
  have negAReal := realNegValue.real at A
  have negBReal := realNegValue.real at B
  have negativeBound := realLe.add at -A, abs(A), -B, abs(B) with
    negAReal, absAReal, negBReal, absBReal,
    abs.upper_neg at A with assumption, abs.upper_neg at B with assumption
  have negSum := realNegValue.add at A, B with *
  rw ← negSum at negativeBound
  have sign := Real.sign_cases with sumReal
  cases sign with nonpositive | nonnegative
  . have sumLeZero := realLe.of_subset at A + B, realZero with
      sumReal, realZero.real, nonpositive
    have shape := abs.of_nonpositive with sumLeZero
    rwa shape
  . have zeroLeSum := realLe.of_subset at realZero, A + B with
      realZero.real, sumReal, nonnegative
    have shape := abs.of_nonnegative with zeroLeSum
    rwa shape