\import Algebra.Group
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.Pointed
\import Arith.Rat
\import Arith.Real
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Operations
\import Order.Lattice
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Set.Filter
\import Set.Subset
\import Topology.CoverSpace
\import Topology.CoverSpace.Complete
\import Topology.RatherBelow
\import Topology.TopSpace
\import Topology.UniformSpace
\import Topology.UniformSpace.Complete
\import Topology.UniformSpace.Product
\open Bounded(top)
\open RealAbGroup \hiding (+, join, meet, negative, zro<ide)
\open PseudoMetricSpace \hiding (NFilter, isUniform)

\class PseudoMetricSpace \extends StronglyRegularUniformSpace {
  | dist : E -> E -> Real
  | dist-refl {x : E} : dist x x = zro
  | dist-symm {x y : E} : dist x y = dist y x
  | dist-triang {x y z : E} : dist x z <= dist x y + dist y z
  | dist-uniform {C : Set (Set E)} : isUniform C <-> ∃ (eps : Real) ( < eps) ∀ x ∃ (U : C) ∀ {y} (dist x y < eps -> U y)

  | uniform-cover Cu x => \case dist-uniform. Cu \with {
    | inP (eps,eps>0,h) => \case h x \with {
      | inP (U,CU,g) => inP (U, CU, g $ rewrite dist-refl eps>0)
    }
  }
  | uniform-top => dist-uniform. $ inP (, RealAbGroup.zro<ide, \lam x => inP (top, idp, \lam _ => ()))
  | uniform-refine Cu e => \case dist-uniform. Cu \with {
    | inP (eps,eps>0,h) => dist-uniform. $ inP (eps, eps>0, \lam x => \case h x \with {
      | inP (U,CU,g) => \case e CU \with {
        | inP (V,DV,U<=V) => inP (V, DV, \lam d => U<=V $ g d)
      }
    })
  }
  | uniform-inter Cu C'u => \case dist-uniform. Cu, dist-uniform. C'u \with {
    | inP (eps,eps>0,h), inP (eps',eps'>0,h') => dist-uniform. $ inP (eps ∧ eps', LinearOrder.<_meet-univ eps>0 eps'>0, \lam x => \case h x, h' x \with {
      | inP (U,CU,g), inP (U',DU',g') => inP (U ∧ U', inP $ later (U, CU, U', DU', idp), \lam d => (g $ d <∘l meet-left, g' $ d <∘l meet-right))
    })
  }
  | uniform-star Cu => \case dist-uniform. Cu \with {
    | inP (eps,eps>0,h) => inP (\lam V => \Sigma (∃ V) (∀ {x y : V} (dist x y < half eps)), dist-uniform. $ inP (half (half eps), half>0 (half>0 eps>0), \lam x => inP (\lam y => dist x y < half (half eps), later (inP (x, rewrite dist-refl (half>0 (half>0 eps>0))), \lam {z} p q => dist-triang {_} {z} {x} <∘r rewrite dist-symm (OrderedAddMonoid.<_+ p q <∘l Preorder.=_<= (half+half {half eps}))), \lam c => c)), \case __ \with {
      | (inP (x,Vx),g) => \case h x \with {
        | inP (U,CU,f) => inP (U, CU, \case __ \with {
          | (inP (y,V'y),g') => \lam (z,(Vz,V'z)) => \lam {w} V'w => f $ dist-triang <∘r OrderedAddMonoid.<_+ (g Vx Vz) (g' V'z V'w) <∘l Preorder.=_<= half+half
        })
      }
    })
  }
  | isStronglyRegularUniform Cu => \case dist-uniform. Cu \with {
    | inP (eps,eps>0,h) => dist-uniform. $ inP $ later (half (half eps), half>0 (half>0 eps>0), \lam x => \case h x \with {
      | inP (U,CU,f) => inP (\lam y => dist x y < half (half eps), inP (U, CU, uniform-refine {_} {\lam U => ∃ (x : E) (U = \lam y => dist x y < half (half eps))} (dist-uniform. $ inP (half (half eps), half>0 (half>0 eps>0), \lam x => inP $ later (_, inP (x, idp), \lam r => r))) \lam {W} => \case __ \with {
          | inP (y,p) => rewrite p \case real-located {dist x y} {half eps} {half eps + half (half eps)} (transport (`< _) zro-right $ <_+-right _ $ half>0 $ half>0 eps>0) \with {
            | byLeft xy>1/2 => inP (_, byLeft idp, \lam {z} yz<1/4 => \lam xz<1/4 => <-irreflexive $ xy>1/2 <∘ (rewrite (half+half {half eps}) in dist-triang <∘r OrderedAddMonoid.<_+ xz<1/4 (rewrite dist-symm in yz<1/4)))
            | byRight xy<3/4 => inP (_, byRight idp, \lam {z} yz<1/4 => f $ dist-triang <∘r OrderedAddMonoid.<_+ xy<3/4 yz<1/4 <∘l Preorder.=_<= (+-assoc *> pmap (_ +) (half+half {half eps}) *> half+half))
          }
        }), \lam r => r)
    })
  }

  \default isUniform C : \Prop => ∃ (eps : Real) ( < eps) ∀ x ∃ (U : C) ∀ {y} (dist x y < eps -> U y)
  \default dist-uniform \as dist-uniform-impl {C} : isUniform C <-> _ => <->refl

  \lemma properUniform : IsProperUniform
    => \lam Cu => \case dist-uniform. Cu \with {
      | inP (eps,eps>0,h) => dist-uniform. $ inP (eps, eps>0, \lam x => \case h x \with {
        | inP (U,CU,g) => inP (U, later (CU, inP (x, g $ rewrite dist-refl eps>0)), g)
      })
    }

  \lemma halving {z x y : E} {eps : Real} (d1 : dist z x < half eps) (d2 : dist z y < half eps) : dist x y < eps
    => dist-triang <∘r OrderedAddMonoid.<_+ (rewrite dist-symm in d1) d2 <∘l Preorder.=_<= half+half

  \lemma makeUniform {eps : Real} (eps>0 :  < eps) : UniformSpace.isUniform \lam U => ∃ (x : E) (U = \lam y => dist x y < eps)
    => dist-uniform. $ inP $ later (eps, eps>0, \lam x => inP (_, inP (x, idp), \lam r => r))

  \func NFilter (x : E) : SetFilter E \cowith
    | F U => ∃ (eps : Real) ( < eps) (OBall eps x ⊆ U)
    | filter-mono p (inP (eps,eps>0,q)) => inP (eps, eps>0, q <=∘ p)
    | filter-top => inP (, RealAbGroup.zro<ide, \lam _ => ())
    | filter-meet (inP (eps,eps>0,p)) (inP (eps',eps'>0,p')) => inP (eps ∧ eps', LinearOrder.<_meet-univ eps>0 eps'>0, \lam d => (p $ d <∘l meet-left, p' $ d <∘l meet-right))

  \lemma dist-uniform-rat {C : Set (Set E)} : UniformSpace.isUniform C <-> ∃ (eps : Rat) ( < eps) ∀ x ∃ (U : C) ∀ {y} (dist x y < eps -> U y)
    => (\lam Cu => \case dist-uniform. Cu \with {
          | inP (eps,eps>0,h) => \case real_<-rat-char. eps>0 \with {
            | inP (eps',eps'>0,eps'<eps) => inP (eps', eps'>0, \lam x => \case h x \with {
              | inP (U,CU,g) => inP (U, CU, \lam d => g $ d <∘ real_<_L. eps'<eps)
            })
          }
    }, \lam (inP (eps,eps>0,h)) => dist-uniform. $ inP (eps, real_<_L. eps>0, h))
}

\lemma dist>=0 {X : PseudoMetricSpace} {x y : X} :  <= dist x y
  => \have t => rewrite (dist-refl,dist-symm) in dist-triang {_} {y} {x} {y}
     \in \lam d => t $ OrderedAddMonoid.<_+ d d <∘l Preorder.=_<= zro-left

\func OBall {X : PseudoMetricSpace} (eps : Real) (x : X) : Set X =>
  \lam y => dist x y < eps

\lemma OBall-center {X : PseudoMetricSpace} {eps : Real} (eps>0 :  < eps) {x : X} : OBall eps x x =>
  transportInv (`< _) dist-refl eps>0

\lemma OBall-open {X : PseudoMetricSpace} {eps : Real} {x : X} : isOpen (OBall eps x)
  => cauchy-open. \lam {y} xy<eps => X.makeCauchy $ uniform-refine (X.makeUniform $ half>0 {eps - dist x y} $ transport (`< _) negative-right $ <_+-left (negative (dist x y)) xy<eps) \lam {_} (inP (z,idp)) => inP (_, later \lam d {w} e => dist-triang <∘r <_+-right (dist x y) (X.halving d e) <∘l Preorder.=_<= (+-comm *> +-assoc *> pmap (eps +) negative-left *> zro-right), <=-refl)

\lemma OBall-center_<=< {X : PseudoMetricSpace} {eps : Real} (eps>0 :  < eps) {x : X} : single x <=< OBall eps x
  => X.open-char. OBall-open (OBall-center eps>0)

\lemma dist_open {X : PseudoMetricSpace} {U : Set X} : isOpen U <-> ∀ {x : U} ∃ (eps : Real) ( < eps) (OBall eps x ⊆ U)
  => (\lam Uo {x} Ux => \case cauchy-ball (cauchy-open. Uo Ux) x \with {
    | inP (eps,eps>0,V,h,p) => inP (eps, eps>0, p <=∘ h (p $ OBall-center eps>0))
  }, \lam f => X.cover-open \lam Ux => \case f Ux \with {
    | inP (eps,eps>0,h) => inP (_, OBall-open, OBall-center eps>0, h)
  })

\lemma cauchy-ball {X : PseudoMetricSpace} {C : Set (Set X)} (Cc : isCauchy C) (x : X) : ∃ (eps : Real) ( < eps) (U : C) (OBall eps x ⊆ U)
  => \case ClosurePrecoverSpace.closure-filter (X.NFilter x) (\lam {D} Du => \case dist-uniform. Du \with {
    | inP (eps,eps>0,h) => \case h x \with {
      | inP (U,DU,p) => inP (U, DU, inP (eps, eps>0, p __))
    }
  }) (uniform-cauchy. Cc) \with {
    | inP (U, CU, inP (eps,eps>0,p)) => inP (eps, eps>0, U, CU, p)
  }

\lemma <=<-ball {X : PseudoMetricSpace} {x : X} {U : Set X} (x<=<U : single x <=< U) : ∃ (eps : Real) ( < eps) (OBall eps x ⊆ U)
  => \case cauchy-ball (unfolds in x<=<U) x \with {
    | inP (eps,eps>0,V,h,p) => inP (eps, eps>0, p <=∘ h (x, (idp, p $ OBall-center eps>0)))
  }

\lemma OBall_<=* {X : PseudoMetricSpace} {x : X} {eps delta : Real} (delta<eps : delta < eps) : OBall delta x <=* OBall eps x
  => inP (_, makeUniform $ half>0 $ transport (`< _) negative-right $ <_+-left (negative delta) delta<eps,
          \lam {y} (inP (_, (inP (z,idp), (w,(xw<delta,zw<eps-delta))), zy<eps-delta)) => transport (_ <) (+-comm *> +-assoc *> pmap (eps +) negative-left *> zro-right) $ dist-triang <∘r OrderedAddMonoid.<_+ xw<delta (halving zw<eps-delta zy<eps-delta))

\func IsBoundedSet {X : PseudoMetricSpace} (S : Set X) : \Prop
  => ∃ (B : Real) ( < B) ∀ {x y : S} (dist x y < B)

\class MetricSpace \extends PseudoMetricSpace, SeparatedCoverSpace
  | dist-ext {x y : E} : dist x y = zro -> x = y
  | isSeparatedCoverSpace {x} {y} f => dist-ext $ <=-antisymmetric (\lam d>0 => \case f (makeCauchy $ makeUniform (half>0 d>0)) \with {
    | inP (U, inP (z,p), (Ux,Uy)) =>
      \have | U'x => rewrite p Ux
            | U'y => rewrite p Uy
      \in <-irreflexive (halving U'x U'y)
  }) dist>=0

\record LocallyUniformMetricMap \extends LocallyUniformMap {
  \override Dom : PseudoMetricSpace
  \override Cod : PseudoMetricSpace

  | func-dist-locally-uniform : ∀ {eps : Real} ( < eps) ∃ (delta : Real) ( < delta) ∀ (x0 : Dom) ∃ (gamma : Real) ( < gamma) ∀ {x x' : Dom} (dist x0 x < delta -> dist x x' < gamma -> dist (func x) (func x') < eps)
  | func-locally-uniform Eu => \case dist-uniform. Eu \with {
    | inP (eps,eps>0,h) => \case func-dist-locally-uniform eps>0 \with {
      | inP (delta,delta>0,g) => inP (_, makeUniform delta>0, \lam (inP (x0,p)) => \case g x0 \with {
        | inP (gamma,gamma>0,g') => dist-uniform. $ inP (gamma, gamma>0, \lam x => \case h (func x) \with {
          | inP (W,EW,e) => inP (\lam x' => dist x x' < gamma, inP $ later (W, EW, \lam {x'} c => e $ rewrite dist-symm $ g' (rewrite p in c.) $ rewrite dist-symm c.), \lam d => d)
        })
      })
    }
  }
} \where {
  \lemma fromLocallyUniformMap {X Y : PseudoMetricSpace} (f : LocallyUniformMap X Y) : LocallyUniformMetricMap X Y f \cowith
    | func-dist-locally-uniform eps>0 => \case f.func-locally-uniform (makeUniform $ half>0 eps>0) \with {
      | inP (C,Cu,h) => \case dist-uniform. Cu \with {
        | inP (delta,delta>0,g) => inP (half delta, half>0 delta>0, \lam x0 => \case g x0 \with {
          | inP (U,CU,e) => \case dist-uniform. (h CU) \with {
            | inP (gamma,gamma>0,g') => inP (gamma ∧ half delta, LinearOrder.<_meet-univ gamma>0 (half>0 delta>0), \lam {x} {x'} d1 d2 => \case g' x \with {
              | inP (V, inP (W, inP (y, q), p), r) => rewrite q at p $ halving (p (e $ d1 <∘ half<id delta>0, r $ rewrite dist-refl gamma>0)) (p (e $ halving (rewrite dist-symm in d1) $ d2 <∘l meet-right, r $ d2 <∘l meet-left))
            })
          }
        })
      }
    }

  \lemma makeLocallyUniformMap2 {X Y Z : PseudoMetricSpace} (f : X -> Y -> Z) (fc : ∀ {eps : Real} ( < eps) ∃ (delta : Real) ( < delta) ∀ x0 y0 ∃ (gamma : Real) ( < gamma) ∀ {x x'} {y y'} (dist x0 x < delta -> dist y0 y < delta -> dist x x' < gamma -> dist y y' < gamma -> dist (f x y) (f x' y') < eps))
    : LocallyUniformMap (X ⨯ Y) Z (\lam s => f s. s.) \cowith
    | func-locally-uniform Eu => \case dist-uniform. Eu \with {
      | inP (eps,eps>0,h) => \case fc eps>0 \with {
        | inP (delta,delta>0,g) => inP (_, ProductUniformSpace.prodCover (makeUniform delta>0) (makeUniform delta>0), \lam {_} (inP (_, inP (x0,idp), _, inP (y0,idp), idp)) => \case g x0 y0 \with {
          | inP (gamma,gamma>0,g') => inP (_, makeUniform gamma>0, _, makeUniform gamma>0, \lam {_} (inP (_, inP (x,idp), _, inP (y,idp), idp)) => \case h (f x y) \with {
            | inP (W,EW,e) => inP (\lam s => \Sigma (dist x s. < gamma) (dist y s. < gamma), inP (W, EW, \lam {s} (c,d) => e $ rewrite dist-symm $ g' c. c. (rewrite dist-symm d.) (rewrite dist-symm d.)), \lam d => d)
          })
        })
      }
    }
}

\record UniformMetricMap \extends LocallyUniformMetricMap, UniformMap {
  \override Dom : PseudoMetricSpace
  \override Cod : PseudoMetricSpace

  | func-dist-uniform : ∀ {eps : Real} ( < eps) ∃ (delta : Real) ( < delta) ∀ {x x' : Dom} (dist x x' < delta -> dist (func x) (func x') < eps)
  | func-dist-locally-uniform eps>0 => \case func-dist-uniform eps>0 \with {
    | inP (delta,delta>0,h) => inP (delta, delta>0, \lam x0 => inP (delta, delta>0, \lam _ => h))
  }
  | func-uniform Eu => \case dist-uniform. Eu \with {
    | inP (eps,eps>0,h) => \case func-dist-uniform eps>0 \with {
      | inP (delta,delta>0,g) => dist-uniform. $ inP (delta, delta>0, \lam x => \case h (func x) \with {
        | inP (U,EU,e) => inP (_, inP $ later (U, EU, idp), \lam d => e (g d))
      })
    }
  }
} \where {
  \lemma fromUniformMap {X Y : PseudoMetricSpace} (f : UniformMap X Y) : UniformMetricMap X Y f \cowith
    | func-dist-uniform eps>0 => \case dist-uniform. $ f.func-uniform (makeUniform $ half>0 eps>0) \with {
      | inP (delta,delta>0,h) => inP (delta, delta>0, \lam {x} d => \case h x \with {
        | inP (U, inP (V, inP (y, q), p), g) => rewrite (p,q) at g $ halving (g $ rewrite dist-refl delta>0) (g d)
      })
    }
}

\record MetricMap \extends UniformMetricMap
  | func-dist {x y : Dom} : dist (func x) (func y) <= dist x y
  | func-dist-uniform {eps} eps>0 => inP (eps, eps>0, \lam d => func-dist <∘r d)
  | func-cont {U} => defaultImpl PrecoverMap func-cont {_} {U}

\record IsometricMap \extends MetricMap {
  | func-isometry {x y : Dom} : dist (func x) (func y) = dist x y
  | func-dist => Preorder.=_<= func-isometry

  \lemma dense->uniformEmbedding (d : IsDense) : UniformMap.IsDenseEmbedding
    => (d, \lam Cu => \case dist-uniform. Cu \with {
      | inP (eps,eps>0,h) => dist-uniform. $ inP (half eps, half>0 eps>0, \lam y => \case d {y} OBall-open (OBall-center (half>0 eps>0)) \with {
        | inP (_, inP (x,idp), yfx<eps/2) => \case h x \with {
          | inP (U,CU,g) => inP (OBall (half eps) y, inP $ later (U, CU, \lam {x'} yfx'<eps/2 => g $ rewrite func-isometry in halving yfx<eps/2 yfx'<eps/2), \lam d => d)
        }
      })
    })
}

\class CompleteMetricSpace \extends MetricSpace, CompleteUniformSpace

\lemma cauchyFilter-metric-char {X : PseudoMetricSpace} {F : SetFilter X} : ∀ {C : isCauchy} ∃ (U : C) (F U) <->
  (\Pi {eps : Real} ->  < eps -> ∃ (x : X) (F (OBall eps x)))
  => <->trans cauchyFilter-uniform-char $ later (\lam f eps>0 => \case f $ makeUniform eps>0 \with {
    | inP (_, inP (x, idp), FB) => inP (x, FB)
  }, \lam f Cu => \case dist-uniform. Cu \with {
    | inP (eps,eps>0,h) => \case f eps>0 \with {
      | inP (x,FB) => \case h x \with {
        | inP (U,CU,g) => inP (U, CU, filter-mono (g __) FB)
      }
    }
  })