CoRN.metric2.DistanceMetricSpace

Require NNUpperR.
Import NNUpperR.notations.
Import QnonNeg.notations.

Require Import Metric.

Open Scope NNUpperR_scope.

Record is_DistanceMetricSpace (X : RSetoid) (distance: X → X → NNUpperR) : Prop
  := Build_is_DistanceMetricSpace
  { dmsp_refl: ∀ x y, st_eq x y ↔ distance x y == 0%Qnn
  ; dmsp_sym: ∀ x y, distance x y == distance y x
  ; dmsp_triangle: ∀ x y z, distance x z ≤ distance x y + distance y z
  }.

Record DistanceMetricSpace: Type := Build_alt_MetricSpace
  { dmsp_is_setoid:> RSetoid;
    distance: dmsp_is_setoid → dmsp_is_setoid → NNUpperR.T;
    distance_wd: Proper (@st_eq _ ==> @st_eq _ ==> NNUpperR.eq) distance;
    dmsp : is_DistanceMetricSpace dmsp_is_setoid distance }.

Implicit Arguments distance [d].
Existing Instance distance_wd.

Section DistanceMetricSpace.
  Context {X: DistanceMetricSpace}.

  Lemma distance_refl (x y: X): st_eq x y ↔ distance x y == 0%Qnn.
  Proof. apply dmsp_refl, dmsp. Qed.

  Lemma distance_sym (x y: X): distance x y == distance y x.
  Proof. apply dmsp_sym, dmsp. Qed.

  Lemma distance_triangle (x y z: X):
    distance x z ≤ distance x y + distance y z.
  Proof. apply dmsp_triangle, dmsp. Qed.

End DistanceMetricSpace.


Section from_alt.

  Variable (X: DistanceMetricSpace).

  Definition ball (q: Qpos) (x y: X): Prop := distance x y ≤ q.

  Instance ball_wd: Proper (QposEq ==> @st_eq X ==> @st_eq X ==> iff) ball.
  Proof.
   intros ?? E ?? F ?? G. unfold ball.
   rewrite E, F, G. reflexivity.
  Qed.

  Lemma ball_refl e: Reflexive (ball e).
  Proof.
   unfold Reflexive, ball. intros.
   rewrite (proj1 (distance_refl x x)).
    apply NNUpperR.le_0.
   reflexivity.
  Qed.

  Lemma ball_sym e: Symmetric (ball e).
  Proof with auto.
   unfold Symmetric, ball. intros.
   rewrite distance_sym...
  Qed.

  Lemma ball_closed e x y: (∀ d, ball (e + d) x y) → ball e x y.
  Proof with auto.
   unfold ball. intros.
   apply NNUpperR.le_closed. intros.
   rewrite <- NNUpperR.plus_homo.
   rewrite <- QnonNeg.from_Qpos_plus_homo...
  Qed.

  Lemma ball_triangle e1 e2 a b c: ball e1 a b → ball e2 b c → ball (e1 + e2) a c.
  Proof with auto.
   unfold ball.
   intros.
   apply NNUpperR.le_trans with (distance a b + distance b c).
    apply distance_triangle.
   rewrite QnonNeg.from_Qpos_plus_homo.
   rewrite NNUpperR.plus_homo.
   apply NNUpperR.plus_le_compat...
  Qed.

  Lemma ball_eq x y: (∀ e, ball e x y) → st_eq x y.
  Proof with auto.
   unfold ball.
   intros.
   apply distance_refl.
   apply NNUpperR.le_0_eq.
   apply NNUpperR.le_closed.
   intros.
   rewrite NNUpperR.plus_0_l...
  Qed.

  Lemma is_MetricSpace: is_MetricSpace X ball.
  Proof with auto.
   constructor.
       apply ball_refl.
      apply ball_sym.
     apply ball_triangle.
    apply ball_closed.
   apply ball_eq.
  Qed.

  Definition ballSpace: MetricSpace.
   apply (@Build_MetricSpace X ball).
    apply ball_wd.
   apply is_MetricSpace.
  Defined.

End from_alt.