-- The standard metric 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.Metric
import AbsoluteValue
import Natural

-- The field-theoretic half of a real. Its laws come from the generic
-- ordered-field development rather than the Dedekind-cut construction.
def half (A : Real) : Real :=
  fieldHalf(realAdd, realMul, realOne, realInv, A)

theorem half.real (A : Real)
  shows Real(half(A))
proof
  unfold half
  unfold Real
  have realA : A ∈ ℝ by simp [Real]
  exact IsOrderedField.half_closed with reals.ordered_field, realA

theorem half.positive (A : Real)
  requires positive : 0 < A
  shows 0 < half(A)
proof
  unfold half
  exact IsOrderedField.half_positive with reals.ordered_field, positive

theorem half.add_self (A : Real)
  shows half(A) + half(A) = A
proof
  have realA : A ∈ ℝ by simp [Real]
  have generic := IsOrderedField.half_add_self with reals.ordered_field, realA
  unfold half
  exact generic

theorem half.lt_self (A : Real)
  requires positive : 0 < A
  shows half(A) < A
proof
  have halfReal := half.real at A
  have halfPositive := half.positive with positive
  have step := realLess.add_left with realZero.real, halfReal, halfReal, halfPositive
  have zero := realAddValue.zero_right with halfReal
  have doubled := half.add_self at A
  rwa [zero, doubled] at step

def dist (A B : Real) : Real := abs(A - B)

theorem dist.real (A B : Real)
  shows Real(dist(A, B))
proof
  unfold dist
  have differenceReal := realSubValue.real at A, B with *
  exact abs.real with differenceReal

theorem dist.nonnegative (A B : Real)
  shows 0 ≤ dist(A, B)
proof
  unfold dist
  have differenceReal := realSubValue.real at A, B with *
  exact abs.nonnegative with differenceReal

theorem dist.self (A : Real)
  shows dist(A, A) = 0
proof
  unfold dist
  have selfDifference := realSubValue.self at A
  rw selfDifference
  exact abs.zero

theorem realSubValue.eq_zero_iff (A B : Real)
  shows A - B = 0 ↔ A = B
proof
  constructor
  . intro differenceZero
    have cancelled := realSubValue.add_right_cancel at A, B with
      *{2}
    have zeroLeft := realAddValue.zero_left at B
    rw [differenceZero, zeroLeft] at cancelled
    rw cancelled
    rfl
  . intro equal
    rw equal
    exact realSubValue.self with assumption

theorem dist.eq_zero_iff (A B : Real)
  shows dist(A, B) = 0 ↔ A = B
proof
  constructor
  . intro zeroDistance
    unfold dist at zeroDistance
    have zeroDifference := abs.eq_zero_iff.forward with zeroDistance
    exact realSubValue.eq_zero_iff.forward with zeroDifference
  . intro equal
    unfold dist
    rw equal
    have selfDifference := realSubValue.self at B
    rw selfDifference
    exact abs.zero

theorem dist.positive_of_ne (A B : Real)
  requires unequal : A ≠ B
  shows 0 < dist(A, B)
proof
  unfold dist
  have differenceReal := realSubValue.real at A, B with
    *{2}
  apply abs.positive_of_ne with differenceReal
  intro differenceZero
  apply unequal
  exact realSubValue.eq_zero_iff.forward with differenceZero

theorem dist.symmetric (A B : Real)
  shows dist(A, B) = dist(B, A)
proof
  have differenceReal := realSubValue.real at A, B with *
  have swapped := realSubValue.neg_swap at A, B with *
  have absoluteNeg := abs.neg with differenceReal
  simp [dist]

theorem dist.triangle (A B C : Real)
  shows dist(A, C) ≤ dist(A, B) + dist(B, C)
proof
  have firstDifferenceReal := realSubValue.real at A, B with
    *{2}
  have secondDifferenceReal := realSubValue.real at B, C with
    *{2}
  have path : A - C = (A - B) + (B - C)
    unfold realSubValue
    have negBReal := realNegValue.real at B
    have negCReal := realNegValue.real at C
    have secondReal := realAddValue.real at B, -C with assumption, negCReal
    have outerAssoc := realAddValue.associative at A, -B, B + (-C) with
      assumption, negBReal, secondReal
    have innerAssoc := realAddValue.associative at -B, B, -C with
      negBReal, assumption, negCReal
    have inverse := realAddValue.neg_left at B
    have identity := realAddValue.zero_left with negCReal
    cc
  have triangle := abs.triangle with firstDifferenceReal, secondDifferenceReal
  unfold dist
  rwa path

def openBall (C E : Real) : Set :=
  { X ∈ ℝ | dist(X, C) < E }

theorem openBall.center (C E : Real)
  requires positive : 0 < E
  shows C ∈ openBall(C, E)
proof
  have typedC : Real(C) by typecheck
  have realC : C ∈ ℝ by simp [Real]
  have selfDistance := dist.self with typedC
  apply openBall.membership.backward
  constructor
  . exact realC
  . rw selfDistance
    exact positive

theorem openBall.symmetric (X C E : Real)
  shows X ∈ openBall(C, E) ↔ C ∈ openBall(X, E)
proof
  have symmetry := dist.symmetric at X, C with *
  have realX : X ∈ ℝ by simp [Real]
  have realC : C ∈ ℝ by simp [Real]
  constructor
  . intro member
    have data := openBall.membership.forward with member
    rcases data with ⟨realX, within⟩
    apply openBall.membership.backward
    constructor
    . exact realC
    . rw ← symmetry
      exact within
  . intro member
    have data := openBall.membership.forward with member
    rcases data with ⟨realC, within⟩
    apply openBall.membership.backward
    constructor
    . exact realX
    . rw symmetry
      exact within

theorem openBall.mono (X C E D : Real)
  requires member : X ∈ openBall(C, E)
  requires radii : E ≤ D
  shows X ∈ openBall(C, D)
proof
  obtain ⟨realX, within⟩ := openBall.membership.forward with member
  have typedX : Real(X) by exact realX
  have distanceReal := dist.real at X, C with typedX, assumption
  apply openBall.membership.backward
  constructor
  . exact realX
  . exact realLess.transitive_le at dist(X, C), E, D with
      distanceReal, *{2}, within, radii

-- Metric balls compose additively: an E-step followed by a D-step remains
-- inside the ball of radius E + D.
theorem openBall.triangle (X Y Z E D : Real)
  requires xy : X ∈ openBall(Y, E)
  requires yz : Y ∈ openBall(Z, D)
  shows X ∈ openBall(Z, E + D)
proof
  have xyData := openBall.membership.forward with xy
  have yzData := openBall.membership.forward with yz
  rcases xyData with ⟨realX, xyLess⟩
  rcases yzData with ⟨realY, yzLess⟩
  have typedX : Real(X) by exact realX
  have typedY : Real(Y) by exact realY
  have xyReal := dist.real with typedX, typedY
  have yzReal := dist.real at Y, Z with typedY, assumption
  have xzReal := dist.real at X, Z with typedX, assumption
  have sumDistancesReal := realAddValue.real with xyReal, yzReal
  have radiusReal := realAddValue.real at E, D with *
  have firstLess := realLess.add_right at
    dist(X, Y), E, dist(Y, Z) with
      xyReal, assumption, yzReal, xyLess
  have secondLess := realLess.add_left at
    dist(Y, Z), D, E with
      yzReal, *{2}, yzLess
  have sumLess := realLess.transitive with firstLess, secondLess
  have triangle := dist.triangle at X, Y, Z with typedX, typedY, assumption
  apply openBall.membership.backward
  constructor
  . exact realX
  . exact realLe.transitive_less at
      dist(X, Z), dist(X, Y) + dist(Y, Z), E + D with
        xzReal, sumDistancesReal,
        radiusReal, triangle, sumLess

-- Two balls whose common radius is half the distance between their centers
-- cannot share a point unless the centers coincide.
theorem openBall.half_radius_unique (X A B : Real)
  requires nearA : X ∈ openBall(A, half(dist(A, B)))
  requires nearB : X ∈ openBall(B, half(dist(A, B)))
  shows A = B
proof
  have distanceReal := dist.real at A, B with *
  have radiusReal := half.real with distanceReal
  have aNearX := openBall.symmetric.forward at
    X, A, half(dist(A, B)) with
      *{2}, radiusReal, nearA
  have path := openBall.triangle at
    A, X, B, half(dist(A, B)), half(dist(A, B)) with
      *{3}, radiusReal, radiusReal,
      aNearX, nearB
  have doubled := half.add_self with distanceReal
  rw doubled at path
  have pathData := openBall.membership.forward at
    B, dist(A, B), A with path
  rcases pathData with ⟨realA, impossible⟩
  exfalso
  exact IsOrderedField.irreflexive with reals.ordered_field, impossible

theorem dist.add_right (A B C : Real)
  shows dist(A + C, B + C) = dist(A, B)
proof
  have identity : (A + C) - (B + C) = A - B
    unfold realSubValue
    have negSum := realNegValue.add at B, C with *
    rw negSum
    have negBReal := realNegValue.real at B
    have negCReal := realNegValue.real at C
    have shuffle := realAddValue.four_shuffle at A, C, -B, -C with
      *{2}, negBReal, negCReal
    have inverse := realAddValue.neg_right at C
    have differenceReal := realAddValue.real at A, -B with
      assumption, negBReal
    have zero := realAddValue.zero_right with differenceReal
    cc
  simp [dist]

theorem dist.add_left (A B C : Real)
  shows dist(C + A, C + B) = dist(A, B)
proof
  have leftCommutative := realAddValue.commutative at C, A with
    *{2}
  have rightCommutative := realAddValue.commutative at C, B with
    *{2}
  rw [leftCommutative, rightCommutative]
  exact dist.add_right with *

theorem dist.neg (A B : Real)
  shows dist(-A, -B) = dist(A, B)
proof
  have differenceReal := realSubValue.real at A, B with *
  have identity : (-A) - (-B) = -(A - B)
    unfold realSubValue
    have negBReal := realNegValue.real at B
    have leftInvolutive := realNegValue.involutive at B
    have rightDistribution := realNegValue.add at A, -B with
      assumption, negBReal
    cc
  unfold dist
  rw identity
  exact abs.neg with differenceReal

-- Pointwise addition is Lipschitz in both arguments.
theorem dist.add_add (A B C D : Real)
  shows dist(A + B, C + D) ≤ dist(A, C) + dist(B, D)
proof
  have firstDifferenceReal := realSubValue.real at A, C with
    *{2}
  have secondDifferenceReal := realSubValue.real at B, D with
    *{2}
  have identity : (A + B) - (C + D) = (A - C) + (B - D)
    unfold realSubValue
    have negSum := realNegValue.add at C, D with *
    have negCReal := realNegValue.real at C
    have negDReal := realNegValue.real at D
    rw negSum
    exact realAddValue.four_shuffle with *{2}, negCReal, negDReal
  have triangle := abs.triangle with firstDifferenceReal, secondDifferenceReal
  unfold dist
  rwa identity

-- Adding points in two balls adds their radii.
theorem openBall.add (A B C D E F : Real)
  requires nearA : A ∈ openBall(C, E)
  requires nearB : B ∈ openBall(D, F)
  shows A + B ∈ openBall(C + D, E + F)
proof
  have dataA := openBall.membership.forward with nearA
  have dataB := openBall.membership.forward with nearB
  rcases dataA with ⟨realA, closeA⟩
  rcases dataB with ⟨realB, closeB⟩
  have distanceACReal := dist.real at A, C with *
  have distanceBDReal := dist.real at B, D with *
  have sumDistancesReal := realAddValue.real with distanceACReal, distanceBDReal
  have radiusReal := realAddValue.real at E, F with *
  have sumReal := realAddValue.real at A, B with *
  have centerReal := realAddValue.real at C, D with *
  have totalDistanceReal := dist.real with sumReal, centerReal
  have distanceBound := dist.add_add at A, B, C, D with
    *{4}
  have radiiBound := realLess.add at
    dist(A, C), E, dist(B, D), F with
      distanceACReal, assumption, distanceBDReal, assumption,
      closeA, closeB
  have within := realLe.transitive_less with
    totalDistanceReal, sumDistancesReal, radiusReal, distanceBound, radiiBound
  apply openBall.membership.backward
  constructor
    exact sumReal
  . exact within

-- A point near B has absolute value at most its distance from B plus |B|.
-- This is the standard local boundedness estimate used in limit proofs.
theorem abs.le_dist_add_abs (A B : Real)
  shows abs(A) ≤ dist(A, B) + abs(B)
proof
  have differenceReal := realSubValue.real at A, B with *
  have cancellation := realSubValue.add_right_cancel at A, B with
    *{2}
  have triangle := abs.triangle at A - B, B with differenceReal, assumption
  unfold dist
  rwa cancellation at triangle

-- The familiar reciprocal-difference identity, stated in the orientation
-- used by epsilon estimates.
theorem realSubValue.inv_inv (A B : Real)
  requires nonzeroA : A ≠ 0
  requires nonzeroB : B ≠ 0
  shows realInvValue(A) - realInvValue(B) =
    (B - A) * (realInvValue(A) * realInvValue(B))
proof
  have inverseAReal := realInvValue.real at A
  have inverseBReal := realInvValue.real at B
  have negAReal := realNegValue.real at A
  have inverseProductReal := realMulValue.real with inverseAReal, inverseBReal
  have inverseA := realInvValue.mul_right with nonzeroA
  have inverseB := realInvValue.mul_right with nonzeroB
  have distribute := realMulValue.distributive_right at
    B, -A, realInvValue(A) * realInvValue(B) with
      assumption, negAReal, inverseProductReal
  have negProduct := realMulValue.neg_left at
    A, realInvValue(A) * realInvValue(B) with
      assumption, inverseProductReal
  have commuteBInvA := realMulValue.commutative at B, realInvValue(A) with
    assumption, inverseAReal
  have assocB := realMulValue.associative at
    B, realInvValue(A), realInvValue(B) with
      assumption, inverseAReal, inverseBReal
  have assocInvAB := realMulValue.associative at
    realInvValue(A), B, realInvValue(B) with
      inverseAReal, assumption, inverseBReal
  have assocA := realMulValue.associative at
    A, realInvValue(A), realInvValue(B) with
      assumption, inverseAReal, inverseBReal
  have oneLeftInvA := realMulValue.one_left with inverseAReal
  have oneLeftInvB := realMulValue.one_left with inverseBReal
  have oneRightInvA := realMulValue.one_right with inverseAReal
  unfold realSubValue
  calc
    realInvValue(A) + -realInvValue(B) =
        realInvValue(A) * 1 + -(1 * realInvValue(B)) := by cc
    _ = realInvValue(A) * (B * realInvValue(B)) +
        -((A * realInvValue(A)) * realInvValue(B)) := by cc
    _ = B * (realInvValue(A) * realInvValue(B)) +
        -(A * (realInvValue(A) * realInvValue(B))) := by cc
    _ = (B + -A) * (realInvValue(A) * realInvValue(B)) := by cc

theorem dist.inv_inv (A B : Real)
  requires nonzeroA : A ≠ 0
  requires nonzeroB : B ≠ 0
  shows dist(realInvValue(A), realInvValue(B)) =
    dist(A, B) * (abs(realInvValue(A)) * abs(realInvValue(B)))
proof
  have inverseAReal := realInvValue.real at A
  have inverseBReal := realInvValue.real at B
  have difference := realSubValue.inv_inv with nonzeroA, nonzeroB
  have baReal := realSubValue.real at B, A with *
  have inverseProductReal := realMulValue.real with inverseAReal, inverseBReal
  have outerAbs := abs.mul with baReal, inverseProductReal
  have innerAbs := abs.mul with inverseAReal, inverseBReal
  have symmetric := dist.symmetric at B, A with *
  unfold dist
  unfold dist at symmetric
  rw [difference, outerAbs, innerAbs]
  have absSymmetric : abs(B - A) = abs(A - B) by exact symmetric
  calc
    abs(B - A) * (abs(realInvValue(A)) * abs(realInvValue(B))) =
        abs(A - B) * (abs(realInvValue(A)) * abs(realInvValue(B))) :=
      by cc

-- If A lies within half of |B| from a nonzero B, then A remains uniformly
-- away from zero.  This is the standard local lower bound for reciprocals.
theorem abs.half_lt_of_dist_lt_half (A B : Real)
  requires nonzeroB : B ≠ 0
  requires close : dist(A, B) < half(abs(B))
  shows half(abs(B)) < abs(A)
proof
  have absAReal := abs.real at A
  have absBReal := abs.real at B
  have halfAbsBReal := half.real with absBReal
  have distReal := dist.real at A, B with *
  have absBPositive := abs.positive_of_ne with nonzeroB
  have halfPositive := half.positive with absBPositive
  have cutHalf := Real.characterization.forward with halfAbsBReal
  have cutAbsA := Real.characterization.forward with absAReal
  have notAbsBelow : ¬(abs(A) ⊆ half(abs(B)))
    intro absABelow
    have absALeHalf := realLe.of_subset with absABelow
    have first := realLess.add_right with distReal, halfAbsBReal, absAReal, close
    have second := realLe.add_left with absAReal, halfAbsBReal, halfAbsBReal, absALeHalf
    have sumBelow := realLess.transitive_le with first, second
    have doubled := half.add_self with absBReal
    rw doubled at sumBelow
    have triangle := abs.le_dist_add_abs at B, A with
      *{2}
    have symmetric := dist.symmetric at B, A with *
    rw symmetric at triangle
    have cycle := realLe.transitive_less with triangle, sumBelow
    have irreflexive := realLess.irreflexive_on
    exact irreflexive with abs(B), cycle
  have comparable := DedekindCut.comparable with cutHalf, cutAbsA
  cases comparable with halfBelow | absABelow
  . apply realLess.characterization.backward at half(abs(B)), abs(A)
    unfold RealLess
    refine ⟨halfAbsBReal, absAReal, _⟩
    constructor
    . exact halfBelow
    . intro equal
      apply notAbsBelow
      rw ← equal
      exact Subset.reflexive
  . exfalso
    exact notAbsBelow with absABelow

-- The difference of two products, arranged in the form most useful for
-- analysis: AB - CD = A(B - D) + D(A - C).
theorem realSubValue.mul_mul (A B C D : Real)
  shows A * B - C * D = A * (B - D) + D * (A - C)
proof
  have negDReal := realNegValue.real at D
  have negCReal := realNegValue.real at C
  have abReal := realMulValue.real at A, B with *
  have adReal := realMulValue.real at A, D with *
  have cdReal := realMulValue.real at C, D with *
  have negADReal := realNegValue.real with adReal
  have negCDReal := realNegValue.real with cdReal
  have adPlusNegCDReal := realAddValue.real with adReal, negCDReal
  have distributeA := realMulValue.distributive at A, B, -D with
    *{2}, negDReal
  have distributeD := realMulValue.distributive at D, A, -C with
    *{2}, negCReal
  have negateAD := realMulValue.neg_right at A, D with *
  have negateDC := realMulValue.neg_right at D, C with *
  have commuteDA := realMulValue.commutative at D, A with *
  have commuteDC := realMulValue.commutative at D, C with *
  have cancelAD := realAddValue.neg_left with adReal
  have zeroNegCD := realAddValue.zero_left with negCDReal
  have middleAssoc := realAddValue.associative with negADReal, adReal, negCDReal
  have outerAssoc := realAddValue.associative with abReal, negADReal, adPlusNegCDReal
  unfold realSubValue
  calc
    A * B + -(C * D) = A * B + (0 + -(C * D)) := by cc
    _ = A * B + ((-(A * D) + A * D) + -(C * D)) := by cc
    _ = A * B + (-(A * D) + (A * D + -(C * D))) := by cc
    _ = A * (B + -D) + D * (A + -C) := by cc

-- Multiplication is locally Lipschitz in the familiar two-term form.
theorem dist.mul_mul (A B C D : Real)
  shows dist(A * B, C * D) ≤
    abs(A) * dist(B, D) + abs(D) * dist(A, C)
proof
  have bdReal := realSubValue.real at B, D with *
  have acReal := realSubValue.real at A, C with *
  have firstReal := realMulValue.real at A, B - D with assumption, bdReal
  have secondReal := realMulValue.real at D, A - C with assumption, acReal
  have decomposition := realSubValue.mul_mul at A, B, C, D with
    *{4}
  have triangle := abs.triangle with firstReal, secondReal
  have firstAbsolute := abs.mul at A, B - D with assumption, bdReal
  have secondAbsolute := abs.mul at D, A - C with assumption, acReal
  unfold dist
  rw decomposition
  rwa [firstAbsolute, secondAbsolute] at triangle

-- Cancel doubling without introducing a numeral-dependent arithmetic rule.
theorem realAddValue.double_cancel (A B : Real)
  requires doubled : A + A = B + B
  shows A = B
proof
  have halfDouble := half.add_self with realOne.real
  linear_combination half(realOne) * doubled - (A - B) * halfDouble

-- Keep the small scalar calculation reusable in vector and geometry proofs.
theorem realMulValue.square_of_double (A B : Real)
  requires doubled : A + A = B
  shows B * B = A * A + A * A + A * A + A * A
proof
  rw ← doubled
  ring

theorem realAddValue.two_nonzero
  shows (2:R) ≠ 0
proof
  intro zero
  have onePositive := realZero.lt_one
  linarith

-- Recover a value from its doubled equation without expanding its expression.
theorem realDiv.of_double_eq (A B : Real)
  requires doubled : A + A = B
  shows A = B / (2:R)
proof
  have two : Real((2:R)) by typecheck
  have quotient := realDiv.real at B, (2:R) with *
  have cancel := realDiv.mul_left at B, (2:R) with
    assumption, two, realAddValue.two_nonzero
  apply realAddValue.double_cancel with assumption, quotient
  linear_combination doubled - cancel

-- Halves as quotients by two.
theorem realHalf.add_self
  shows (1:R) / 2 + 1 / 2 = 1
proof
  have twoNonzero : (2:R) ≠ 0
    intro zero
    linarith
  have oneReal : (1:R) ∈ ℝ by typecheck
  have twoReal : (2:R) ∈ ℝ by typecheck
  have halfReal := realDiv.real at (1:R), (2:R) with *
  have half := realDiv.mul_right at (1:R), (2:R) with twoNonzero
  have twice : (1:R) / 2 + 1 / 2 = 1 / 2 * 2 by ring
  rw [twice, half]
  rfl

theorem realDiv.lt_half (A B : Real)
  requires positive : 0 < B
  requires below : 2 * A < B
  shows A / B < 1 / 2
proof
  have oneReal : (1:R) ∈ ℝ by typecheck
  have twoReal : (2:R) ∈ ℝ by typecheck
  have halfReal := realDiv.real at (1:R), (2:R) with *
  have twice := realHalf.add_self
  have split : 1 / 2 * B + 1 / 2 * B = (1 / 2 + 1 / 2) * B by ring
  rw twice at split
  have unit : (1:R) * B = B by ring
  have halfBelow : A < 1 / 2 * B by linarith
  exact realDiv.lt_of_lt_mul with positive, halfBelow

-- Division by three and cancellation of tripled real values.
theorem realAddValue.three_nonzero
  shows (3:R) ≠ 0
proof
  intro zero
  have onePositive := realZero.lt_one
  linarith

def third (A : Real) : Real := A / (3:R)

theorem third.real (A : Real)
  shows Real(third(A))
proof
  unfold third
  typecheck

theorem third.add_self (A : Real)
  shows third(A) + third(A) + third(A) = A
proof
  have cancel := realDiv.mul_left with realAddValue.three_nonzero
  unfold third
  linear_combination cancel

theorem realAddValue.triple_cancel (A B : Real)
  requires tripled : A + A + A = B + B + B
  shows A = B
proof
  have thirdTriple := third.add_self at realOne with *
  linear_combination third(realOne) * tripled - (A - B) * thirdTriple