From: Enrico Tassi Date: Fri, 9 Nov 2007 13:37:05 +0000 (+0000) Subject: snapshot X-Git-Tag: 0.4.95@7852~30 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=8896b5179a1b8b0fa6f9b26bb3142fdaf863276f;p=helm.git snapshot --- diff --git a/matita/dama/constructive_connectives.ma b/matita/dama/constructive_connectives.ma index a0fb66ded..b7f15e500 100644 --- a/matita/dama/constructive_connectives.ma +++ b/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/matita/dama/constructive_pointfree/lebesgue.ma b/matita/dama/constructive_pointfree/lebesgue.ma index 583dc638c..a739ed715 100644 --- a/matita/dama/constructive_pointfree/lebesgue.ma +++ b/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;