/- Clara L"oh 2021 -/

import tactic          -- standard proof tactics
import data.real.basic -- standards on real numbers

open classical   -- we want to work in classical logic

/-
# Metric Spaces

This is an implementation of some very basic facts on metric 
spaces. A more comprehensive treatment can be found in the 
mathlib library topology.metric_space .
-/

class metric_space 
      (X : Type*)     -- underlying set
      (d : X → X → ℝ) -- the distance function
:= (d_nonneg :   ∀ x y : X,   d x y ≥ 0)
   (d_self :     ∀ x : X,     d x x = 0) 
   (d_definite : ∀ x y : X,   d x y = 0 → x = y)
   (d_symm :     ∀ x y : X,   d x y = d y x)
   (d_triangle : ∀ x y z : X, d x z ≤ d x y + d y z)

-- Isometric embeddings are maps between metric spaces 
-- that preserve the distance.
def is_isometric_embedding 
    (X : Type*)  (d : X → X → ℝ)    [metric_space X d]
    (X' : Type*) (d' : X' → X' → ℝ) [metric_space X' d']
    (f : X → X')
:= ∀ x y : X, d' (f x) (f y) = d x y  

-- The composition of isometric embeddings is an isometric embedding
lemma comp_of_isom_emb
    (X : Type*)  (d : X → X → ℝ)      [metric_space X d]
    (X' : Type*) (d' : X' → X' → ℝ)   [metric_space X' d']
    (X'': Type*) (d'': X'' → X'' → ℝ) [metric_space X'' d'']
    (f  : X → X')
    (f' : X' → X'')
    (isom_embd_f : is_isometric_embedding X d X' d' f)    
    (isom_embd_f': is_isometric_embedding X' d' X'' d'' f')
  : (is_isometric_embedding X d X'' d'' (f' ∘ f))
:=
begin
  assume x y : X,
  let f'' : X → X'' := f' ∘ f, 

  -- we prove the claim by direct computation
  show d'' (f'' x) (f'' y) = d x y, by
  calc d'' (f'' x) (f'' y) = d'' (f' (f x)) (f' (f y)) 
                           : by {refl} 
                             -- resolving def of f''
                       ... = d' (f x) (f y)
                           : by {exact isom_embd_f' (f x) (f y)} 
                             -- f' is an isom emb
                       ... = d x y
                           : by {exact isom_embd_f x y}, 
                             -- f is an isom embd        
end   

-- As an example metric space, we consider the real numbers 
-- with the standard metric:
noncomputable 
def d_real 
    (x : ℝ) 
    (y : ℝ)
:= abs (x - y)    

noncomputable
instance real_std_metric_space : metric_space ℝ d_real
:= metric_space.mk
   -- non-negativity 
   (assume x y : ℝ,
    show d_real x y ≥ 0, 
         by {unfold d_real, exact abs_nonneg (x - y)})
   -- distance from self
   (assume x : ℝ,
    show d_real x x = 0, 
         by {unfold d_real, ring, exact abs_zero})
   -- definiteness
   (assume x y : ℝ,
    assume dist_0 : d_real x y = 0,
    have abs_0 : abs (x - y) = 0,
         by {exact dist_0},
    show x = y, 
         by {exact eq_of_abs_sub_eq_zero abs_0})
   -- symmetry
   (assume x y : ℝ,
    show d_real x y = d_real y x, 
         by {unfold d_real, exact abs_sub x y})
   -- triangle inequality
   (assume x y z : ℝ,
    show d_real x z ≤ d_real x y + d_real y z,
         by {unfold d_real, exact abs_sub_le x y z})