(* Copyright © 1998-2006
 * Henk Barendregt
 * Luís Cruz-Filipe
 * Herman Geuvers
 * Mariusz Giero
 * Rik van Ginneken
 * Dimitri Hendriks
 * Sébastien Hinderer
 * Bart Kirkels
 * Pierre Letouzey
 * Iris Loeb
 * Lionel Mamane
 * Milad Niqui
 * Russell O’Connor
 * Randy Pollack
 * Nickolay V. Shmyrev
 * Bas Spitters
 * Dan Synek
 * Freek Wiedijk
 * Jan Zwanenburg
 *
 * This work is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * This work is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License along
 * with this work; if not, write to the Free Software Foundation, Inc.,
 * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
 *)

Require Export CoRN.reals.Intervals.

(**
* Metric Spaces (traditional)
*)

Section Relations.
(**
** Relations necessary for Pseudo Metric Spaces and Metric Spaces
%\begin{convention}%
Let [A : CSetoid], [d : (CSetoid_bin_fun A A IR)].
%\end{convention}%
*)
Variable A : CSetoid.

Variable d : CSetoid_bin_fun A A IR.

Set Implicit Arguments.
Unset Strict Implicit.

Definition com : Prop := forall x y : A, d x y[=]d y x.

Definition nneg : Prop := forall x y : A, [0][<=]d x y.

Definition pos_imp_ap : CProp := forall x y : A, [0][<]d x y -> x[#]y.

Definition tri_ineq : Prop := forall x y z : A, d x z[<=]d x y[+]d y z.

Set Strict Implicit.
Unset Implicit Arguments.

Definition diag_zero (X : CSetoid) (d : CSetoid_bin_fun X X IR) : Prop :=
  forall x : X, d x x[=][0].

Definition apdiag_imp_grzero (X : CSetoid) (d : CSetoid_bin_fun X X IR) :
  CProp := forall x y : X, x[#]y -> [0][<]d x y.

End Relations.

Section Definition_PsMS0.
(**
** Definition of Pseudo Metric Space
*)
(**
A pseudo metric space consists of a setoid and a %''pseudo metric''% #"pseudo metric"#, also called
%''distance''% #"distance"#, a binairy function that fulfils certain properties.
*)

Record is_CPsMetricSpace (A : CSetoid) (d : CSetoid_bin_fun A A IR) :
  Type :=
  {ax_d_com : com d;
   ax_d_nneg : nneg d;
   ax_d_pos_imp_ap : pos_imp_ap d;
   ax_d_tri_ineq : tri_ineq d}.

Record CPsMetricSpace : Type :=
  {cms_crr :> CSetoid;
   cms_d : CSetoid_bin_fun cms_crr cms_crr IR;
   cms_proof : is_CPsMetricSpace cms_crr cms_d}.

End Definition_PsMS0.

Arguments cms_d {c}.
Infix "[-d]" := cms_d (at level 68, left associativity).


Section PsMS_axioms.
(**
** Pseudo Metric Space axioms
%\begin{convention}%
Let [A] be a pseudo metric space.
%\end{convention}%
*)
Variable A : CPsMetricSpace.

Lemma CPsMetricSpace_is_CPsMetricSpace : is_CPsMetricSpace A cms_d.
Proof cms_proof A.

Lemma d_com : com (cms_d (c:=A)).
Proof.
 elim CPsMetricSpace_is_CPsMetricSpace.
 auto.
Qed.

Lemma d_nneg : nneg (cms_d (c:=A)).
Proof.
 elim CPsMetricSpace_is_CPsMetricSpace.
 auto.
Qed.

Lemma d_pos_imp_ap : pos_imp_ap (cms_d (c:=A)).
Proof.
 elim CPsMetricSpace_is_CPsMetricSpace.
 auto.
Qed.

Lemma d_tri_ineq : tri_ineq (cms_d (c:=A)).
Proof.
 elim CPsMetricSpace_is_CPsMetricSpace.
 auto.
Qed.

End PsMS_axioms.

Section PsMS_basics.
(**
** Pseudo Metric Space basics
%\begin{convention}%
Let [Y] be a pseudo metric space.
%\end{convention}%
*)

Variable Y : CPsMetricSpace.

Lemma rev_tri_ineq :
 forall a b c : cms_crr Y, AbsSmall (b[-d]c) ((a[-d]b)[-](a[-d]c)).
Proof.
 intros.
 unfold AbsSmall in |- *.
 split.
  apply shift_leEq_minus.
  apply shift_plus_leEq'.
  unfold cg_minus in |- *.
  cut ([--][--](b[-d]c)[=]b[-d]c).
   intros.
   apply leEq_wdr with ((a[-d]b)[+](b[-d]c)).
    apply ax_d_tri_ineq.
    apply CPsMetricSpace_is_CPsMetricSpace.
   apply eq_symmetric_unfolded.
   apply bin_op_wd_unfolded.
    apply eq_reflexive_unfolded.
   exact H.
  apply cg_inv_inv.
 astepr (c[-d]b).
  apply shift_minus_leEq.
  apply shift_leEq_plus'.
  apply shift_minus_leEq.
  apply ax_d_tri_ineq.
  apply CPsMetricSpace_is_CPsMetricSpace.
 apply ax_d_com.
 apply CPsMetricSpace_is_CPsMetricSpace.
Qed.

(**
Instead of taking [pos_imp_ap] as axiom,
we could as well have taken [diag_zero].
*)

Lemma diag_zero_imp_pos_imp_ap :
 forall (X : CSetoid) (d : CSetoid_bin_fun X X IR),
 diag_zero X d -> pos_imp_ap d.
Proof.
 intros X d.
 unfold diag_zero in |- *.
 unfold pos_imp_ap in |- *.
 intros H.
 intros x y H0.
 cut (x[#]x or x[#]y).
  intro H1.
  elim H1.
   cut (Not (x[#]x)).
    intros H3 H4.
    set (H5 := H3 H4) in *.
    intuition.
   apply ap_irreflexive_unfolded.
  intro H2.
  exact H2.
 apply (csbf_strext X X IR d).
 astepl ZeroR.
 apply less_imp_ap.
 exact H0.
Qed.

Lemma pos_imp_ap_imp_diag_zero :
 forall (X : CSetoid) (d : CSetoid_bin_fun X X IR),
 pos_imp_ap d -> nneg d -> diag_zero X d.
Proof.
 intros X d.
 unfold pos_imp_ap in |- *.
 unfold nneg in |- *.
 intros H H6.
 unfold diag_zero in |- *.
 intro x.
 apply not_ap_imp_eq.
 red in |- *.
 intro H0.
 set (H1 := less_conf_ap IR (d x x) [0]) in *.
 generalize H1.
 unfold Iff in |- *.
 intro H2.
 elim H2.
 intros H3 H4.
 set (H5 := H3 H0) in *.
 elim H5.
  generalize H6.
  intros H7 H8.
  set (H9 := H7 x x) in *.
  rewrite -> leEq_def in H9.
  set (H10 := H9 H8) in *.
  exact H10.
 intro H7.
 set (H8 := H x x) in *.
 set (H9 := H8 H7) in *.
 set (H10 := ap_irreflexive_unfolded X x H9) in *.
 exact H10.
Qed.

Lemma is_CPsMetricSpace_diag_zero :
 forall (X : CSetoid) (d : CSetoid_bin_fun X X IR),
 com d /\ tri_ineq d /\ nneg d /\ diag_zero X d -> is_CPsMetricSpace X d.
Proof.
 intros X d H.
 elim H.
 intros H1 H2.
 elim H2.
 intros H3 H4.
 elim H4.
 intros H5 H6.
 apply (Build_is_CPsMetricSpace X d H1 H5 (diag_zero_imp_pos_imp_ap X d H6) H3).
Qed.

End PsMS_basics.

Section Zerof.
(**
** Zero function
*)
(**
Every setoid forms with the binary function that always returns zero,
a pseudo metric space.
*)

Definition zero_fun (X : CSetoid) (x y : X) : IR := ZeroR.

Lemma zero_fun_strext :
 forall X : CSetoid, bin_fun_strext X X IR (zero_fun X).
Proof.
 intro X.
 unfold bin_fun_strext in |- *.
 unfold zero_fun in |- *.
 intros x1 x2 y1 y2 Z.
 set (H := ap_irreflexive_unfolded IR [0] Z) in *.
 intuition.
Qed.

Definition Zero_fun (X : CSetoid) :=
  Build_CSetoid_bin_fun X X IR (zero_fun X) (zero_fun_strext X).

Lemma zero_fun_com : forall X : CSetoid, com (Zero_fun X).
Proof.
 intro X.
 unfold com in |- *.
 intros x y.
 unfold Zero_fun in |- *.
 simpl in |- *.
 unfold zero_fun in |- *.
 intuition.
Qed.

Lemma zero_fun_nneg : forall X : CSetoid, nneg (Zero_fun X).
Proof.
 intro X.
 unfold nneg in |- *.
 intros x y.
 unfold Zero_fun in |- *.
 simpl in |- *.
 unfold zero_fun in |- *.
 apply eq_imp_leEq.
 intuition.
Qed.

Lemma zero_fun_pos_imp_ap : forall X : CSetoid, pos_imp_ap (Zero_fun X).
Proof.
 intro X.
 unfold pos_imp_ap in |- *.
 intros x y.
 unfold Zero_fun in |- *.
 simpl in |- *.
 unfold zero_fun in |- *.
 intro Z.
 set (H := less_irreflexive IR [0] Z) in *.
 intuition.
Qed.

Lemma zero_fun_tri_ineq : forall X : CSetoid, tri_ineq (Zero_fun X).
Proof.
 intro X.
 unfold tri_ineq in |- *.
 intros x y z.
 unfold Zero_fun in |- *.
 simpl in |- *.
 unfold zero_fun in |- *.
 apply eq_imp_leEq.
 rational.
Qed.

Definition zf_is_CPsMetricSpace (X : CSetoid) :=
  Build_is_CPsMetricSpace X (Zero_fun X) (zero_fun_com X) (
    zero_fun_nneg X) (zero_fun_pos_imp_ap X) (zero_fun_tri_ineq X).

Definition zf_as_CPsMetricSpace (X : CSetoid) :=
  Build_CPsMetricSpace X (Zero_fun X) (zf_is_CPsMetricSpace X).

End Zerof.