-- The discrete metric on any set: distinct points are at distance one, so
-- every subset is open, every subset is bounded, every map out of the
-- space is uniformly continuous, and the space is complete
-- 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.Discrete
import Line

def discreteDistance (X : Set) : Set :=
  { q ∈ (X × X) × ℝ | ∃ x ∈ X, ∃ y ∈ X,
    ((x = y ∧ q = ((x, y) ↦ (0:R))) ∨ (x ≠ y ∧ q = ((x, y) ↦ (1:R)))) }

theorem discreteDistance.relates_self (X x : Set)
  requires hx : x ∈ X
  shows relates(discreteDistance(X), (x, x), (0:R))
proof
  have zeroReal : (0:R) ∈ ℝ by typecheck
  have pair := product.pair at x, x, X, X with hx, hx
  have entry := product.pair at (x, x), (0:R), X × X, ℝ with pair, zeroReal
  unfold relates
  apply discreteDistance.membership.backward
  refine ⟨entry, x, hx, x, hx, ?_⟩
  left
  constructor
  . rfl
  . rfl

theorem discreteDistance.relates_distinct (X x y : Set)
  requires hx : x ∈ X
  requires hy : y ∈ X
  requires distinct : x ≠ y
  shows relates(discreteDistance(X), (x, y), (1:R))
proof
  have oneReal : (1:R) ∈ ℝ by typecheck
  have pair := product.pair at x, y, X, X with hx, hy
  have entry := product.pair at (x, y), (1:R), X × X, ℝ with pair, oneReal
  unfold relates
  apply discreteDistance.membership.backward
  refine ⟨entry, x, hx, y, hy, ?_⟩
  right
  constructor
  . exact distinct
  . rfl

theorem discreteDistance.relation (X : Set)
  shows RelationBetween(discreteDistance(X), X × X, ℝ)
proof
  intros q hq
  have parts := discreteDistance.membership.forward with hq
  exact parts.left

-- The value at a pair is determined by whether its coordinates coincide.
theorem discreteDistance.value_shape (X p v : Set)
  requires edge : relates(discreteDistance(X), p, v)
  shows
    ∃ x ∈ X, ∃ y ∈ X, p = (x, y) ∧ ((x = y ∧ v = (0:R)) ∨ (x ≠ y ∧ v = (1:R)))
proof
  unfold relates at edge
  obtain ⟨bound, x, hx, y, hy, split⟩ :=
    discreteDistance.membership.forward with edge
  refine ⟨x, hx, y, hy, ?_⟩
  cases split with same | different
  . obtain ⟨equal, shape⟩ := same
    obtain ⟨first, second⟩ := orderedPair.injective with shape
    refine ⟨first, ?_⟩
    left
    exact ⟨equal, second⟩
  . obtain ⟨unequal, shape⟩ := different
    obtain ⟨first, second⟩ := orderedPair.injective with shape
    refine ⟨first, ?_⟩
    right
    exact ⟨unequal, second⟩

theorem discreteDistance.functional (X : Set)
  shows Functional(discreteDistance(X))
proof
  intros p v first w second
  obtain ⟨x, hx, y, hy, shapeV, splitV⟩ :=
    discreteDistance.value_shape with first
  obtain ⟨a, ha, b, hb, shapeW, splitW⟩ :=
    discreteDistance.value_shape with second
  rw shapeV at shapeW
  obtain ⟨xa, yb⟩ := orderedPair.injective with shapeW
  rw [← xa, ← yb] at splitW
  cases splitV with sameV | differentV
  . cases splitW with sameW | differentW
    . rw [sameV.right, sameW.right]
      rfl
    . exfalso
      exact differentW.left with sameV.left
  . cases splitW with sameW | differentW
    . exfalso
      exact differentV.left with sameW.left
    . rw [differentV.right, differentW.right]
      rfl

theorem discreteDistance.total (X : Set)
  shows ∀ p ∈ X × X, ∃ v ∈ ℝ, relates(discreteDistance(X), p, v)
proof
  intros p hp
  obtain ⟨bound, x, hx, y, hy, rfl⟩ := product.membership.forward with hp
  have split : x = y ∨ x ≠ y by tauto
  cases split with same | different
  . have zeroReal : (0:R) ∈ ℝ by typecheck
    refine ⟨(0:R), zeroReal, ?_⟩
    rw same
    exact discreteDistance.relates_self with hy
  . have oneReal : (1:R) ∈ ℝ by typecheck
    refine ⟨(1:R), oneReal, ?_⟩
    exact discreteDistance.relates_distinct with hx, hy, different

theorem discreteDistance.function (X : Set)
  shows discreteDistance(X) : X × X → ℝ
proof
  constructor
  . exact discreteDistance.relation at X
  . constructor
    . exact discreteDistance.functional at X
    . exact discreteDistance.total at X

theorem discreteDistance.self (X x : Set)
  requires hx : x ∈ X
  shows discreteDistance(X)(x, x) = (0:R)
proof
  have function := discreteDistance.function at X
  have pair := product.pair at x, x, X, X with hx, hx
  have edge := discreteDistance.relates_self with hx
  unfold call2
  exact FunctionBetween.apply_value with function, pair, edge

theorem discreteDistance.distinct (X x y : Set)
  requires hx : x ∈ X
  requires hy : y ∈ X
  requires distinct : x ≠ y
  shows discreteDistance(X)(x, y) = (1:R)
proof
  have function := discreteDistance.function at X
  have pair := product.pair at x, y, X, X with hx, hy
  have edge := discreteDistance.relates_distinct with hx, hy, distinct
  unfold call2
  exact FunctionBetween.apply_value with function, pair, edge

theorem discreteDistance.le_one (X x y : Set)
  requires hx : x ∈ X
  requires hy : y ∈ X
  shows discreteDistance(X)(x, y) ≤ (1:R)
proof
  have split : x = y ∨ x ≠ y by tauto
  cases split with same | different
  . rw same
    have self := discreteDistance.self with hy
    rw self
    have one := realZero.lt_one
    linarith
  . have value := discreteDistance.distinct with hx, hy, different
    rw value
    exact realLe.reflexive

theorem discreteDistance.nonnegative (X x y : Set)
  requires hx : x ∈ X
  requires hy : y ∈ X
  shows (0:R) ≤ discreteDistance(X)(x, y)
proof
  have split : x = y ∨ x ≠ y by tauto
  cases split with same | different
  . rw same
    have self := discreteDistance.self with hy
    rw self
    exact realLe.reflexive
  . have value := discreteDistance.distinct with hx, hy, different
    rw value
    have one := realZero.lt_one
    linarith

theorem discreteDistance.real (X x y : Set)
  requires hx : x ∈ X
  requires hy : y ∈ X
  shows Real(discreteDistance(X)(x, y))
proof
  have function := discreteDistance.function at X
  have pair := product.pair at x, y, X, X with hx, hy
  unfold Real
  unfold call2
  exact FunctionBetween.apply_closed with function, pair

theorem discreteDistance.metric (X : Set)
  shows IsMetric(X, discreteDistance(X))
proof
  have one := realZero.lt_one
  constructor
  . exact discreteDistance.function at X
  . constructor
    . intros x hx y hy
      exact discreteDistance.nonnegative with hx, hy
    . constructor
      . intros x hx y hy
        constructor
        . intro zero
          by_contra
          have value := discreteDistance.distinct with hx, hy, this
          rw value at zero
          linarith
        . intro same
          rw same
          exact discreteDistance.self with hy
      . constructor
        . intros x hx y hy
          have split : x = y ∨ x ≠ y by tauto
          cases split with same | different
          . rw same
            rfl
          . have reversed : y ≠ x
              intro equal
              apply different
              symm at equal
              exact equal
            have valueXY := discreteDistance.distinct with hx, hy, different
            have valueYX := discreteDistance.distinct with hy, hx, reversed
            rw [valueXY, valueYX]
            rfl
        . intros x hx y hy z hz
          have nonnegativeXY := discreteDistance.nonnegative with hx, hy
          have nonnegativeYZ := discreteDistance.nonnegative with hy, hz
          have realXY := discreteDistance.real with hx, hy
          have realYZ := discreteDistance.real with hy, hz
          have realXZ := discreteDistance.real with hx, hz
          have splitXZ : x = z ∨ x ≠ z by tauto
          cases splitXZ with sameXZ | differentXZ
          . have self : discreteDistance(X)(x, z) = (0:R)
              rw sameXZ
              exact discreteDistance.self with hz
            rw self
            linarith
          . have valueXZ := discreteDistance.distinct with hx, hz, differentXZ
            rw valueXZ
            have splitXY : x = y ∨ x ≠ y by tauto
            cases splitXY with sameXY | differentXY
            . have differentYZ : y ≠ z
                intro equal
                apply differentXZ
                rw sameXY
                exact equal
              have valueYZ := discreteDistance.distinct with hy, hz, differentYZ
              rw valueYZ
              linarith
            . have valueXY := discreteDistance.distinct with hx, hy, differentXY
              rw valueXY
              linarith

-- Balls of radius at most one are singletons; larger balls are the space.
theorem discreteDistance.ball_small (X x : Set, r : Real)
  requires hx : x ∈ X
  requires positive : 0 < r
  requires small : r ≤ 1
  shows ball(X, discreteDistance(X), x, r) = {x}
proof
  ext y
  constructor
  . intro hy
    have hyX := ball.point with hy
    have near := ball.distance with hy
    have split : x = y ∨ x ≠ y by tauto
    cases split with same | different
    . rw ← same
      exact singleton.self at x
    . exfalso
      have value := discreteDistance.distinct with hx, hyX, different
      rw value at near
      linarith
  . intro hy
    have same := singleton.membership.forward with hy
    rw same
    apply ball.of_distance with hx
    have self := discreteDistance.self with hx
    rw self
    exact positive

theorem discreteDistance.ball_large (X x : Set, r : Real)
  requires hx : x ∈ X
  requires large : 1 < r
  shows ball(X, discreteDistance(X), x, r) = X
proof
  apply Subset.antisymmetric
  . exact ball.subset at X, discreteDistance(X), x, r
  . intros y hy
    have bound := discreteDistance.le_one with hx, hy
    have real := discreteDistance.real with hx, hy
    apply ball.of_distance with hy
    linarith

theorem discreteDistance.open (X U : Set)
  requires inside : U ⊆ X
  shows MetricOpen(X, discreteDistance(X), U)
proof
  constructor
  . exact inside
  . intros x hx
    have hxX := inside with x, hx
    have oneReal : (1:R) ∈ ℝ by typecheck
    have positive : (0:R) < 1 by linarith
    have reflexive : (1:R) ≤ 1 by linarith
    refine ⟨(1:R), oneReal, positive, ?_⟩
    have singleton := discreteDistance.ball_small at X, x, (1:R) with
      hxX, positive, reflexive
    rw singleton
    intros y hy
    have same := singleton.membership.forward with hy
    rw same
    exact hx

theorem discreteDistance.topology (X : Set)
  shows metricTopology(X, discreteDistance(X)) = 𝒫(X)
proof
  apply Subset.antisymmetric
  . exact metricTopology.subset_powerset at X, discreteDistance(X)
  . intros U hU
    have inside := powerset.membership_iff.forward with hU
    exact metricTopology.of_open with (discreteDistance.open with inside)

theorem discreteDistance.closed (X C : Set)
  requires inside : C ⊆ X
  shows MetricClosed(X, discreteDistance(X), C)
proof
  apply MetricClosed.of_complement_open with inside
  exact discreteDistance.open with (complement.subset at X, C)

theorem discreteDistance.bounded (X S : Set)
  requires inside : S ⊆ X
  shows IsBounded(X, discreteDistance(X), S)
proof
  apply IsBounded.of_bound at X, discreteDistance(X), S, (1:R) with inside
  intros x hx y hy
  exact discreteDistance.le_one with (inside with x, hx), (inside with y, hy)

-- Every map out of a discrete space is uniformly continuous.
theorem discreteDistance.uniformly_continuous (f X Y e : Set)
  requires metric : IsMetric(Y, e)
  requires function : f : X → Y
  shows IsUniformlyContinuous(f, X, discreteDistance(X), Y, e)
proof
  apply IsUniformlyContinuous.of_control with function
  intros ε hε positive
  have oneReal : (1:R) ∈ ℝ by typecheck
  have one : (0:R) < 1 by linarith
  refine ⟨(1:R), oneReal, one, ?_⟩
  intros x hx y hy near
  have split : x = y ∨ x ≠ y by tauto
  cases split with same | different
  . rw same
    have image := FunctionBetween.apply_closed with function, hy
    have self := IsMetric.self with metric, image
    rw self
    exact positive
  . exfalso
    have value := discreteDistance.distinct with hx, hy, different
    rw value at near
    linarith

theorem discreteDistance.continuous (f X Y e : Set)
  requires metric : IsMetric(Y, e)
  requires function : f : X → Y
  shows IsMetricContinuous(f, X, discreteDistance(X), Y, e)
proof
  have uniform := discreteDistance.uniformly_continuous with metric, function
  exact IsUniformlyContinuous.continuous with uniform

-- A Cauchy sequence in a discrete space is eventually constant.
theorem discreteDistance.cauchy_eventually_constant (X u : Set)
  requires cauchy : IsCauchy(X, discreteDistance(X), u)
  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, (N ≤ n → u(n) = u(N))
proof
  have sequence := IsCauchy.sequence with cauchy
  have one : (0:R) < 1 by linarith
  obtain ⟨N, hN, close⟩ := IsCauchy.eventually with cauchy, one
  have natN : Nat(N) by exact hN
  refine ⟨N, hN, ?_⟩
  intros n hn le
  have termN := SequenceIn.term_of_member with sequence, hN
  have termn := SequenceIn.term_of_member with sequence, hn
  have near := close with n, hn, N, hN, le, (LessEqual.reflexive at N)
  by_contra
  have value := discreteDistance.distinct with termn, termN, this
  rw value at near
  linarith

theorem discreteDistance.complete (X : Set)
  shows IsComplete(X, discreteDistance(X))
proof
  have metric := discreteDistance.metric at X
  apply IsComplete.of_limits with metric
  intros u cauchy
  have sequence := IsCauchy.sequence with cauchy
  obtain ⟨N, hN, constant⟩ :=
    discreteDistance.cauchy_eventually_constant with cauchy
  have termN := SequenceIn.term_of_member with sequence, hN
  refine ⟨u(N), termN, ?_⟩
  apply ConvergesIn.of_eventually with sequence, termN
  intros ε hε positive
  refine ⟨N, hN, ?_⟩
  intros n hn le
  have same := constant with n, hn, le
  rw same
  have self := discreteDistance.self with termN
  rw self
  exact positive