some work on uniformity

diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends
index 5e4ec73cba21c3a89f3eb144b8029bb551db52e4..ea9ec7bff8c9283a52aa03b626709a3d113bbdd7 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/depends
+++ b/helm/software/matita/contribs/dama/dama/depends
@@ -4,8 +4,10 @@ ordered_set.ma cprop_connectives.ma
 cprop_connectives.ma logic/equality.ma
 bishop_set_rewrite.ma bishop_set.ma
 sequence.ma nat/nat.ma
-supremum.ma bishop_set.ma cprop_connectives.ma nat_ordered_set.ma ordered_set.ma sequence.ma
+uniform.ma supremum.ma
+supremum.ma bishop_set.ma cprop_connectives.ma nat/plus.ma nat_ordered_set.ma ordered_set.ma sequence.ma
 nat_ordered_set.ma cprop_connectives.ma nat/compare.ma ordered_set.ma
 logic/equality.ma 
 nat/compare.ma 
 nat/nat.ma 
+nat/plus.ma 

diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
new file mode 100644 (file)
index 0000000..9744052
--- /dev/null
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -0,0 +1,62 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "uniform.ma".
+
+record ordered_uniform_space_ : Type ≝ {
+  ous_os:> ordered_set;
+  ous_us_: uniform_space;
+  with_ : us_carr ous_us_ = bishop_set_of_ordered_set ous_os
+}.
+
+lemma ous_unifspace: ordered_uniform_space_ → uniform_space.
+intro X; apply (mk_uniform_space (bishop_set_of_ordered_set X));
+unfold bishop_set_OF_ordered_uniform_space_;
+[1: rewrite < (with_ X); simplify; apply (us_unifbase (ous_us_ X));
+|2: cases (with_ X); simplify; apply (us_phi1 (ous_us_ X));
+|3: cases (with_ X); simplify; apply (us_phi2 (ous_us_ X));
+|4: cases (with_ X); simplify; apply (us_phi3 (ous_us_ X));
+|5: cases (with_ X); simplify; apply (us_phi4 (ous_us_ X))]
+qed.
+
+coercion cic:/matita/dama/ordered_uniform/ous_unifspace.con.
+
+record ordered_uniform_space : Type ≝ {
+  ous_stuff :> ordered_uniform_space_;
+  ous_prop1: ∀U.us_unifbase ous_stuff U → convex ous_stuff U
+}.
+
+
+lemma segment_ordered_uniform_space: 
+  ∀O:ordered_uniform_space.∀u,v:O.ordered_uniform_space.
+intros (O u v); apply mk_ordered_uniform_space;
+[1: apply mk_ordered_uniform_space_;
+    [1: apply (mk_ordered_set (sigma ? (λx.x ∈ [u,v])));
+        [1: intros (x y); apply (fst x ≰ fst y);
+        |2: intros 1; cases x; simplify; apply os_coreflexive;
+        |3: intros 3; cases x; cases y; cases z; simplify; apply os_cotransitive]
+    |2: apply (mk_uniform_space (bishop_set_of_ordered_set (mk_ordered_set (sigma ? (λx.x ∈ [u,v])) ???)));
+    |3: apply refl_eq;
+qed.
+
+
+(* Lemma 3.2 *)
+lemma foo:
+ ∀O:ordered_uniform_space.∀l,u:O.
+  ∀x:(segment_ordered_uniform_space O l u).
+   ∀a:sequence (segment_ordered_uniform_space O l u).
+     (* (λn.fst (a n)) uniform_converges (fst x) → *) 
+      a uniform_converges x.
+     
+      
\ No newline at end of file

diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma
new file mode 100644 (file)
index 0000000..2b5ed2c
--- /dev/null
+++ b/helm/software/matita/contribs/dama/dama/uniform.ma
@@ -0,0 +1,128 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "supremum.ma".
+
+(* Definition 2.13 *)
+definition square_bishop_set : bishop_set → bishop_set.
+intro S; apply (mk_bishop_set (pair S S));
+[1: intros (x y); apply ((fst x # fst y) ∨ (snd x # snd y));
+|2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X);   
+|3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X); 
+|4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H;
+    [1: cases (bs_cotransitive ??? (fst z) X); [left;left|right;left]assumption;
+    |2: cases (bs_cotransitive ??? (snd z) X); [left;right|right;right]assumption;]]
+qed.
+
+definition subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x.
+
+notation "a \subseteq u" left associative with precedence 70 
+  for @{ 'subset $a $u }.
+interpretation "Bishop subset" 'subset a b =
+  (cic:/matita/dama/uniform/subset.con _ a b). 
+
+notation "{ ident x : t | p }" non associative with precedence 50
+  for @{ 'explicitset (\lambda ${ident x} : $t . $p) }.  
+definition mk_set ≝ λT:bishop_set.λx:T→Prop.x.
+interpretation "explicit set" 'explicitset t =
+  (cic:/matita/dama/uniform/mk_set.con _ t).
+
+notation < "s \sup 2" non associative with precedence 90
+  for @{ 'square $s }.
+notation > "s 'square'" non associative with precedence 90
+  for @{ 'square $s }.
+interpretation "bishop suqare set" 'square x =
+  (cic:/matita/dama/uniform/square_bishop_set.con x).    
+
+alias symbol "exists" = "exists".
+alias symbol "and" = "logical and".
+definition compose_relations ≝
+  λC:bishop_set.λU,V:C square → Prop.
+   λx:C square.∃y:C. U (prod ?? (fst x) y) ∧ V (prod ?? y (snd x)).
+   
+notation "a \circ b"  left associative with precedence 60
+  for @{'compose $a $b}.
+interpretation "relations composition" 'compose a b = 
+ (cic:/matita/dama/uniform/compose_relations.con _ a b).
+
+definition invert_relation ≝
+  λC:bishop_set.λU:C square → Prop.
+    λx:C square. U (prod ?? (snd x) (fst x)).
+    
+notation < "s \sup (-1)"  non associative with precedence 90
+  for @{ 'invert $s }.
+notation > "'inv' s" non associative with precedence 90
+  for @{ 'invert $s }.
+interpretation "relation invertion" 'invert a = 
+ (cic:/matita/dama/uniform/invert_relation.con _ a).
+
+record uniform_space : Type ≝ {
+  us_carr:> bishop_set;
+  us_unifbase: (us_carr square → Prop) → CProp;
+  us_phi1: ∀U:us_carr square → Prop. us_unifbase U → 
+    {x:us_carr square|fst x ≈ snd x} ⊆ U;
+  us_phi2: ∀U,V:us_carr square → Prop. us_unifbase U → us_unifbase V →
+    ∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ {x:?|U x ∧ V x});
+  us_phi3: ∀U:us_carr square → Prop. us_unifbase U → 
+    ∃W:us_carr square → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U;
+  us_phi4: ∀U:us_carr square → Prop. us_unifbase U → U = inv U (* I should use double inclusion ... *)
+}.
+
+(* Definition 2.14 *)  
+alias symbol "leq" = "natural 'less or equal to'".
+definition cauchy ≝
+  λC:uniform_space.λa:sequence C.∀U.us_unifbase C U → 
+   ∃n. ∀i,j. n ≤ i → n ≤ j → U (prod ?? (a i) (a j)).
+   
+notation < "a \nbsp 'is_cauchy'" non associative with precedence 50 
+  for @{'cauchy $a}.
+notation > "a 'is_cauchy'" non associative with precedence 50 
+  for @{'cauchy $a}.
+interpretation "Cauchy sequence" 'cauchy s =
+ (cic:/matita/dama/uniform/cauchy.con _ s).  
+   
+(* Definition 2.15 *)  
+definition uniform_converge ≝
+  λC:uniform_space.λa:sequence C.λu:C.
+    ∀U.us_unifbase C U →  ∃n. ∀i. n ≤ i → U (prod ?? u (a i)).
+    
+notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50 
+  for @{'uniform_converge $a $x}.
+notation > "a 'uniform_converges' x" non associative with precedence 50 
+  for @{'uniform_converge $a $x}.
+interpretation "Uniform convergence" 'uniform_converge s u =
+ (cic:/matita/dama/uniform/uniform_converge.con _ s u).
+ 
+(* Lemma 2.16 *)
+lemma uniform_converge_is_cauchy : 
+  ∀C:uniform_space.∀a:sequence C.∀x:C.
+   a uniform_converges x → a is_cauchy. 
+intros (C a x Ha); intros 2 (u Hu);
+cases (us_phi3 ?? Hu) (v Hv0); cases Hv0 (Hv H); clear Hv0;
+cases (Ha ? Hv) (n Hn); exists [apply n]; intros;
+apply H; unfold; exists [apply x]; split [2: apply (Hn ? H2)]
+rewrite > (us_phi4 ?? Hv); simplify; apply (Hn ? H1);
+qed.
+
+(* Definition 2.17 *)
+definition mk_big_set ≝
+  λP:CProp.λF:P→CProp.F.
+interpretation "explicit big set" 'explicitset t =
+  (cic:/matita/dama/uniform/mk_big_set.con _ t).
+    
+definition restrict_uniformity ≝
+  λC:uniform_space.λX:C→Prop.
+   {U:C square → Prop| (U ⊆ {x:C square|X (fst x) ∧ X(snd x)}) ∧ us_unifbase C U}.
+
+