CoRN.metrics.CPseudoMSpaces

Require Export Intervals.

Metric Spaces (traditional)

Section Relations.

Relations necessary for Pseudo Metric Spaces and Metric Spaces

Let A : CSetoid, d : (CSetoid_bin_fun A A IR).

Variable A : CSetoid.

Variable d : CSetoid_bin_fun A A IR.

Set Implicit Arguments.
Unset Strict Implicit.

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

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

Definition pos_imp_ap : CProp := ∀ x y : A, [0][<]d x y → x [#]y.

Definition tri_ineq : Prop := ∀ 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 :=
∀ x : X, d x x [=][0].

Definition apdiag_imp_grzero (X : CSetoid) (d : CSetoid_bin_fun X X IR) :
CProp := ∀ 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", also called "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.

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

Section PsMS_axioms.

Pseudo Metric Space axioms

Let A be a pseudo metric space.

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

Let Y be a pseudo metric space.

Variable Y : CPsMetricSpace.

Lemma rev_tri_ineq :
∀ 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 :
∀ (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 :
∀ (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 :
∀ (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 :
∀ 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 : ∀ 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 : ∀ 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 : ∀ 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 : ∀ 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.