helm/software/matita/dama/metric_space.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 include "ordered_divisible_group.ma".
  18
  19 record metric_space (R : todgroup) : Type ≝ {
  20   ms_carr :> Type;
  21   metric: ms_carr → ms_carr → R;
  22   mpositive: ∀a,b:ms_carr. 0 ≤ metric a b;
  23   mreflexive: ∀a. metric a a ≈ 0;
  24   msymmetric: ∀a,b. metric a b ≈ metric b a;
  25   mtineq: ∀a,b,c:ms_carr. metric a b ≤ metric a c + metric c b
  26 }.
  27
  28 notation < "\nbsp \delta a \nbsp b" non associative with precedence 80 for @{ 'delta2 $a $b}.
  29 interpretation "metric" 'delta2 a b = (cic:/matita/metric_space/metric.con _ _ a b).
  30 notation "\delta" non associative with precedence 80 for @{ 'delta }.
  31 interpretation "metric" 'delta = (cic:/matita/metric_space/metric.con _ _).
  32
  33 definition apart_metric:=
  34   λR.λms:metric_space R.λa,b:ms.0 < δ a b.
  35
  36 lemma apart_of_metric_space: ∀R:todgroup.metric_space R → apartness.
  37 intros (R ms); apply (mk_apartness ? (apart_metric ? ms)); unfold apart_metric; unfold;
  38 [1: intros 2 (x H); cases H (H1 H2);
  39     lapply (ap_rewr ???? (eq_sym ??? (mreflexive ??x)) H2);
  40     apply (ap_coreflexive R 0); assumption;
  41 |2: intros (x y H); cases H; split;
  42     [1: apply (le_rewr ???? (msymmetric ????)); assumption
  43     |2: apply (ap_rewr ???? (msymmetric ????)); assumption]
  44 |3: simplify; intros (x y z H); cases H (LExy Axy);
  45     lapply (mtineq ?? x y z) as H1; whd in Axy; cases Axy (H2 H2); [cases (LExy H2)]
  46     clear LExy; lapply (lt_le_transitive ???? H H1) as LT0;
  47     apply (lt0plus_orlt ????? LT0); apply mpositive;]
  48 qed.
  49
  50 (* coercion cic:/matita/metric_space/apart_of_metric_space.con. *)
  51
  52 lemma ap2delta: ∀R.∀m:metric_space R.∀x,y:m.ap_apart (apart_of_metric_space ? m) x y → 0 < δ x y.
  53 intros 2 (R m); cases m 0; simplify; intros; assumption; qed.