From 2d406b0e91788ab83ddad04be1d9532a23bb9e59 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 9 Nov 2007 13:37:05 +0000
Subject: [PATCH] snapshot

---
 .../matita/dama/constructive_connectives.ma   |   6 +
 .../dama/constructive_pointfree/lebesgue.ma   | 107 ++++++++++++------
 2 files changed, 76 insertions(+), 37 deletions(-)

diff --git a/helm/software/matita/dama/constructive_connectives.ma b/helm/software/matita/dama/constructive_connectives.ma
index a0fb66ded..b7f15e500 100644
--- a/helm/software/matita/dama/constructive_connectives.ma
+++ b/helm/software/matita/dama/constructive_connectives.ma
@@ -32,3 +32,9 @@ for @{ 'sigma ${default
 
 interpretation "constructive exists" 'sigma \eta.x =
   (cic:/matita/constructive_connectives/ex.ind#xpointer(1/1) _ x).
+
+alias id "False" = "cic:/matita/logic/connectives/False.ind#xpointer(1/1)".
+definition Not ≝ λx:Type.False.
+
+interpretation "constructive not" 'not x = 
+  (cic:/matita/constructive_connectives/Not.con x).
\ No newline at end of file
diff --git a/helm/software/matita/dama/constructive_pointfree/lebesgue.ma b/helm/software/matita/dama/constructive_pointfree/lebesgue.ma
index 583dc638c..a739ed715 100644
--- a/helm/software/matita/dama/constructive_pointfree/lebesgue.ma
+++ b/helm/software/matita/dama/constructive_pointfree/lebesgue.ma
@@ -17,59 +17,92 @@ set "baseuri" "cic:/matita/lebesgue/".
 include "reals.ma".
 include "lattices.ma".
 
-record measured_set (R : real) : Type ≝ {
+axiom ltT : ∀R:real.∀a,b:R.Type.  
+  
+   
+alias symbol "or" = "constructive or".
+definition rapart ≝ λR:real.λa,b:R.a < b ∨ b < a. 
+
+notation "a # b" non associative with precedence 50 for
+ @{ 'apart $a $b}.
+notation "a \approx b" non associative with precedence 50 for
+ @{ 'napart $a $b}.    
+interpretation "real apartness" 'apart a b =
+ (cic:/matita/lebesgue/rapart.con _ a b). 
+interpretation "real non apartness" 'napart a b =
+ (cic:/matita/constructive_connectives/Not.con
+   (cic:/matita/lebesgue/rapart.con _ a b)). 
+
+record is_semi_metric (R : real) (T : Type) (d : T → T → R): Prop ≝ {
+ sm_positive: ∀a,b:T. d a b ≤ 0; 
+ sm_reflexive: ∀a. d a a ≈ 0;
+ sm_symmetric: ∀a,b. d a b ≈ d b a;
+ sm_tri_ineq: ∀a,b,c:T. d a b ≤ d a c + d c b
+}.
+
+record semimetric_set (R : real) : Type ≝ {
   ms_carr :> Type;
-  ms_measure: ms_carr → ms_carr → R
+  ms_semimetric: ms_carr → ms_carr → R;
+  ms_properties:> is_semi_metric R ms_carr ms_semimetric
 }.
 
-notation "\delta" non associative with precedence 90 for @{ 'delta }.
-interpretation "measure" 'delta = (cic:/matita/lebesgue/ms_measure.con _ _).
+notation < "\nbsp \delta a \nbsp b" non associative with precedence 80 for @{ 'delta2 $a $b}.
+interpretation "semimetric" 'delta2 a b = (cic:/matita/lebesgue/ms_semimetric.con _ _ a b).
+notation "\delta" non associative with precedence 80 for @{ 'delta }.
+interpretation "semimetric" 'delta = (cic:/matita/lebesgue/ms_semimetric.con _ _).
 
-record pre_measured_lattice (R : real) : Type ≝ {
+record pre_semimetric_lattice (R : real) : Type ≝ {
   ml_lattice :> lattice;
-  ml_measured_set_ : measured_set R;
-  with_ml_lattice_eq_ml_measured_set_: ms_carr ? ml_measured_set_ = ml_lattice
+  ml_semimetric_set_ : semimetric_set R;
+  with_ml_lattice_eq_ml_semimetric_set_: ms_carr ? ml_semimetric_set_ = ml_lattice
 }.
 
-lemma ml_measured_set : ∀R.∀ms:pre_measured_lattice R. measured_set R.
-intros (R ml); constructor 1; [1:apply (ml : Type);] cases ml; 
-rewrite < H; clear H; cases ml_measured_set_; simplify; exact f;
-qed.  
+lemma ml_semimetric_set : ∀R.∀ms:pre_semimetric_lattice R. semimetric_set R.
+intros (R ml); constructor 1; [apply (ml : Type);]
+cases ml (l ms with_); clear ml; simplify;
+[1: rewrite < with_; apply (ms_semimetric ? ms);  
+|2: cases with_; simplify; apply (ms_properties ? ms);]
+qed.
 
-coercion cic:/matita/lebesgue/ml_measured_set.con.
+coercion cic:/matita/lebesgue/ml_semimetric_set.con.
 
-record is_measured_lattice (R : real) (ml : pre_measured_lattice R) : Prop ≝ {
-  prop1a: ∀a : ml.δ (a ∧ a) a = 0;
-  prop1b: ∀a : ml.δ (a ∨ a) a = 0;
-  prop2a: ∀a,b: ml. δ (a ∨ b) (b ∨ a) = 0;
-  prop2b: ∀a,b: ml. δ (a ∧ b) (b ∧ a) = 0;
-  prop3a: ∀a,b,c: ml. δ (a ∨ (b ∨ c)) ((a ∨ b) ∨ c) = 0;
-  prop3b: ∀a,b,c: ml. δ (a ∧ (b ∧ c)) ((a ∧ b) ∧ c) = 0;
-  prop4a: ∀a,b: ml. δ (a ∨ (a ∧ b)) a = 0;
-  prop4b: ∀a,b: ml. δ (a ∧ (a ∨ b)) a = 0;
+record is_semimetric_lattice (R : real) (ml : pre_semimetric_lattice R) : Prop ≝ {
+  prop1a: ∀a : ml.δ (a ∧ a) a ≈ 0;
+  prop1b: ∀a : ml.δ (a ∨ a) a ≈ 0;
+  prop2a: ∀a,b: ml. δ (a ∨ b) (b ∨ a) ≈ 0;
+  prop2b: ∀a,b: ml. δ (a ∧ b) (b ∧ a) ≈ 0;
+  prop3a: ∀a,b,c: ml. δ (a ∨ (b ∨ c)) ((a ∨ b) ∨ c) ≈ 0;
+  prop3b: ∀a,b,c: ml. δ (a ∧ (b ∧ c)) ((a ∧ b) ∧ c) ≈ 0;
+  prop4a: ∀a,b: ml. δ (a ∨ (a ∧ b)) a ≈ 0;
+  prop4b: ∀a,b: ml. δ (a ∧ (a ∨ b)) a ≈ 0;
   prop5: ∀a,b,c: ml. δ (a ∨ b) (a ∨ c) + δ (a ∧ b) (a ∧ c) ≤ δ b c
 }. 
   
-record measured_lattice (R : real) : Type ≝ {
-  ml_pre_measured_lattice:> pre_measured_lattice R;
-  ml_measured_lattice_properties: is_measured_lattice R ml_pre_measured_lattice
+record semimetric_lattice (R : real) : Type ≝ {
+  ml_pre_semimetric_lattice:> pre_semimetric_lattice R;
+  ml_semimetric_lattice_properties: is_semimetric_lattice R ml_pre_semimetric_lattice
 }.
-  
+
 definition apart:= 
- λR: real. λml: measured_lattice R. λa,b: ml. 0 < δ a b.
+ λR: real. λml: semimetric_lattice R. λa,b: ml. 
+ (* 0 < δ a b *) ltT ? 0 (δ a b).
  (* < scazzato, ma CSC dice che poi si cambia dopo  *)    
 
-notation "a # b" non associative with precedence 50 for
- @{ 'apart $a $b}.
-interpretation "measured lattice apartness" 'apart a b =
+interpretation "semimetric lattice apartness" 'apart a b =
  (cic:/matita/lebesgue/apart.con _ _ a b). 
-notation "a \approx b" non associative with precedence 50 for
- @{ 'napart $a $b}.
-interpretation "measured lattice non apartness" 'napart a b =
- (cic:/matita/logic/connectives/Not.con
-   (cic:/matita/lebesgue/apart.con _ _ a b)). 
+interpretation "semimetric lattice non apartness" 'napart a b =
+ (cic:/matita/constructive_connectives/Not.con
+   (cic:/matita/lebesgue/apart.con _ _ a b)).
+  
+
+lemma triangular_inequality : ∀R: real. ∀ms: semimetric_set R.∀a,b,c:ms.
+ δ a b ≤ δ a c + δ c b.
+intros (R ms a b c); exact (sm_tri_ineq R ms (ms_semimetric R ms) ms a b c);
+qed. 
 
-lemma foo : ∀R: real. ∀ml: measured_lattice R.∀a,b,a1,b1: ml. 
-  a ≈ a1 → b ≈ b1 → δ a b = δ a1 b1. 
-     (* =R scazzato *)  
+lemma foo : ∀R: real. ∀ml: semimetric_lattice R.∀a,b,a1,b1: ml. 
+  a ≈ a1 → b ≈ b1 → (δ a b ≈ δ a1 b1).  
 intros;
+lapply (triangular_inequality ? ? a b a1) as H1;
+lapply (triangular_inequality ? ? a1 b b1) as H2;
+lapply (og_ordered_abelian_group_properties R ? ? (δ a a1) H2) as H3;
-- 
2.39.2