-- Metric spaces: a distance function on a set with its defining laws and
-- their first consequences
-- 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.Metric.Space
import Real.Metric
import Topology.Subspace

-- A metric on X is a real-valued function on X × X, applied as d(x, y),
-- that is nonnegative, vanishes exactly on the diagonal, is symmetric, and
-- satisfies the triangle inequality. Points of X are arbitrary sets, so the
-- real order and addition are written through their graphs here; once a
-- distance is known to be real, proofs use the usual notation.
predicate IsMetric (X d : Set) :=
  FunctionBetween(d, X × X, ℝ) ∧
  (∀ x ∈ X, ∀ y ∈ X, relates(realLe, (0:R), d(x, y))) ∧
  (∀ x ∈ X, ∀ y ∈ X, d(x, y) = (0:R) ↔ x = y) ∧
  (∀ x ∈ X, ∀ y ∈ X, d(x, y) = d(y, x)) ∧
  (∀ x ∈ X, ∀ y ∈ X, ∀ z ∈ X,
    relates(realLe, d(x, z), realAdd(d(x, y), d(y, z))))

theorem IsMetric.function (X d : Set)
  requires metric : IsMetric(X, d)
  shows d : X × X → ℝ
proof
  exact metric.left

theorem Metric.apply_pair (d x y : Set)
  shows d((x, y)) = d(x, y)
proof
  unfold call2
  rfl

theorem IsMetric.real (X d x y : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  shows Real(d(x, y))
proof
  have function := IsMetric.function with metric
  have pair := product.pair_membership.backward at x, y, X, X with ⟨hx, hy⟩
  unfold Real
  unfold call2
  exact FunctionBetween.apply_closed with function, pair

theorem IsMetric.member_reals (X d x y : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  shows d(x, y) ∈ ℝ
proof
  exact IsMetric.real with metric, hx, hy

theorem IsMetric.nonnegative (X d x y : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  shows (0:R) ≤ d(x, y)
proof
  obtain ⟨function, nonnegative, zero, symmetric, triangle⟩ := metric
  exact nonnegative with x, hx, y, hy

theorem IsMetric.eq_zero_iff (X d x y : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  shows d(x, y) = (0:R) ↔ x = y
proof
  obtain ⟨function, nonnegative, zero, symmetric, triangle⟩ := metric
  exact zero with x, hx, y, hy

theorem IsMetric.self (X d x : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  shows d(x, x) = (0:R)
proof
  have characterization := IsMetric.eq_zero_iff with metric, hx, hx
  apply characterization.backward
  rfl

theorem IsMetric.eq_of_zero (X d x y : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  requires zero : d(x, y) = (0:R)
  shows x = y
proof
  have characterization := IsMetric.eq_zero_iff with metric, hx, hy
  exact characterization.forward with zero

theorem IsMetric.symmetric (X d x y : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  shows d(x, y) = d(y, x)
proof
  obtain ⟨function, nonnegative, zero, symmetric, triangle⟩ := metric
  exact symmetric with x, hx, y, hy

theorem IsMetric.triangle (X d x y z : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  requires hz : z ∈ X
  shows d(x, z) ≤ realAdd(d(x, y), d(y, z))
proof
  obtain ⟨function, nonnegative, zero, symmetric, triangle⟩ := metric
  exact triangle with x, hx, y, hy, z, hz

theorem IsMetric.positive_of_ne (X d x y : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  requires distinct : x ≠ y
  shows (0:R) < d(x, y)
proof
  have nonnegative := IsMetric.nonnegative with metric, hx, hy
  have real := IsMetric.real with metric, hx, hy
  have nonzero : d(x, y) ≠ 0
    intro zero
    exact distinct with (IsMetric.eq_of_zero with metric, hx, hy, zero)
  have order := realLess.trichotomy at (0:R), d(x, y)
  rcases order with positive | zero | negative
  . exact positive
  . exfalso
    symm at zero
    exact nonzero with zero
  . exfalso
    linarith

theorem IsMetric.ne_of_positive (X d x y : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  requires positive : (0:R) < d(x, y)
  shows x ≠ y
proof
  intro same
  have zero : d(x, y) = (0:R)
    rw same
    exact IsMetric.self with metric, hy
  rw zero at positive
  exact realLess.not_self with positive

theorem IsMetric.zero_or_positive (X d x y : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  shows x = y ∨ (0:R) < d(x, y)
proof
  have split : x = y ∨ x ≠ y by tauto
  cases split with same | distinct
  . left
    exact same
  . right
    exact IsMetric.positive_of_ne with metric, hx, hy, distinct

theorem IsMetric.positive_iff_ne (X d x y : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  shows (0:R) < d(x, y) ↔ x ≠ y
proof
  constructor
  . intro positive
    exact IsMetric.ne_of_positive with metric, hx, hy, positive
  . intro distinct
    exact IsMetric.positive_of_ne with metric, hx, hy, distinct

-- The triangle inequality with the middle point measured from the same
-- side, in the forms the ball lemmas use.
theorem IsMetric.triangle_from (X d x y z : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  requires hz : z ∈ X
  shows d(y, z) ≤ realAdd(d(x, y), d(x, z))
proof
  have triangle := IsMetric.triangle with metric, hy, hx, hz
  have symmetric := IsMetric.symmetric with metric, hy, hx
  rwa symmetric at triangle

theorem IsMetric.triangle_to (X d x y z : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  requires hz : z ∈ X
  shows d(x, y) ≤ realAdd(d(x, z), d(y, z))
proof
  have triangle := IsMetric.triangle with metric, hx, hz, hy
  have symmetric := IsMetric.symmetric with metric, hz, hy
  rwa symmetric at triangle

theorem IsMetric.sub_le (X d x y z : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  requires hz : z ∈ X
  shows realSubValue(d(x, z), d(y, z)) ≤ d(x, y)
proof
  have triangle := IsMetric.triangle with metric, hx, hy, hz
  have dxz := IsMetric.real with metric, hx, hz
  have dyz := IsMetric.real with metric, hy, hz
  have dxy := IsMetric.real with metric, hx, hy
  linarith

-- The reverse triangle inequality: distances to a third point differ by at
-- most the distance between the two points.
theorem IsMetric.abs_sub_le (X d x y z : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  requires hz : z ∈ X
  shows abs(realSubValue(d(x, z), d(y, z))) ≤ d(x, y)
proof
  have dxz := IsMetric.real with metric, hx, hz
  have dyz := IsMetric.real with metric, hy, hz
  have dxy := IsMetric.real with metric, hx, hy
  have dyx := IsMetric.real with metric, hy, hx
  have forward := IsMetric.sub_le with metric, hx, hy, hz
  have backward := IsMetric.sub_le with metric, hy, hx, hz
  have symmetric := IsMetric.symmetric with metric, hx, hy
  have differenceReal : Real(d(x, z) - d(y, z)) by typecheck
  have sign := realLess.trichotomy at (0:R), d(x, z) - d(y, z)
  rcases sign with positive | zero | negative
  . have nonnegative : 0 ≤ d(x, z) - d(y, z) by linarith
    have unfolded := abs.of_nonnegative with nonnegative
    rw unfolded
    exact forward
  . have nonnegative : 0 ≤ d(x, z) - d(y, z) by linarith
    have unfolded := abs.of_nonnegative with nonnegative
    rw unfolded
    exact forward
  . have nonpositive : d(x, z) - d(y, z) ≤ 0 by linarith
    have unfolded := abs.of_nonpositive with nonpositive
    rw unfolded
    linarith

theorem IsMetric.abs_sub_le_from (X d x y z : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  requires hz : z ∈ X
  shows abs(realSubValue(d(x, y), d(x, z))) ≤ d(y, z)
proof
  have bound := IsMetric.abs_sub_le with metric, hy, hz, hx
  have symmetricY := IsMetric.symmetric with metric, hy, hx
  have symmetricZ := IsMetric.symmetric with metric, hz, hx
  rwa [symmetricY, symmetricZ] at bound

-- A path through two intermediate points.
theorem IsMetric.four_points (X d x y z w : Set)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  requires hz : z ∈ X
  requires hw : w ∈ X
  shows d(x, y) ≤ realAdd(realAdd(d(x, z), d(z, w)), d(w, y))
proof
  have first := IsMetric.triangle with metric, hx, hz, hy
  have second := IsMetric.triangle with metric, hz, hw, hy
  have dxy := IsMetric.real with metric, hx, hy
  have dxz := IsMetric.real with metric, hx, hz
  have dzy := IsMetric.real with metric, hz, hy
  have dzw := IsMetric.real with metric, hz, hw
  have dwy := IsMetric.real with metric, hw, hy
  linarith

theorem IsMetric.le_add_of_le (X d x y z : Set) (A B : Real)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  requires hz : z ∈ X
  requires first : d(x, y) ≤ A
  requires second : d(y, z) ≤ B
  shows d(x, z) ≤ A + B
proof
  have triangle := IsMetric.triangle with metric, hx, hy, hz
  have dxy := IsMetric.real with metric, hx, hy
  have dyz := IsMetric.real with metric, hy, hz
  have dxz := IsMetric.real with metric, hx, hz
  linarith

theorem IsMetric.lt_add_of_lt (X d x y z : Set) (A B : Real)
  requires metric : IsMetric(X, d)
  requires hx : x ∈ X
  requires hy : y ∈ X
  requires hz : z ∈ X
  requires first : d(x, y) < A
  requires second : d(y, z) < B
  shows d(x, z) < A + B
proof
  have triangle := IsMetric.triangle with metric, hx, hy, hz
  have dxy := IsMetric.real with metric, hx, hy
  have dyz := IsMetric.real with metric, hy, hz
  have dxz := IsMetric.real with metric, hx, hz
  linarith

-- Two metrics on the same set agreeing at every pair of points coincide.
theorem IsMetric.ext (X d e : Set)
  requires metricD : IsMetric(X, d)
  requires metricE : IsMetric(X, e)
  requires same : ∀ x ∈ X, ∀ y ∈ X, d(x, y) = e(x, y)
  shows d = e
proof
  have functionD := IsMetric.function with metricD
  have functionE := IsMetric.function with metricE
  apply FunctionBetween.ext with functionD, functionE
  intros p hp
  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with hp
  rw shape
  have pairD := Metric.apply_pair at d, x, y
  have pairE := Metric.apply_pair at e, x, y
  rw [pairD, pairE]
  exact same with x, hx, y, hy

-- The empty set carries the empty metric.
theorem IsMetric.empty
  shows IsMetric(∅, ∅)
proof
  have product := product.left_empty at ∅
  constructor
  . rw product
    exact FunctionBetween.empty at ℝ
  . constructor
    . intros x hx
      exfalso
      exact empty.membership with hx
    . constructor
      . intros x hx
        exfalso
        exact empty.membership with hx
      . constructor
        . intros x hx
          exfalso
          exact empty.membership with hx
        . intros x hx
          exfalso
          exact empty.membership with hx