X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fproperty_sigma.ma;h=67209928116df8aec54e7a70e5304a0011d257e1;hb=ada8695ba51b2ecbd4a955f990e8d06f038aac6b;hp=c67dd1785297b96968870033dadca3df385053a1;hpb=9156537d75378d7a254e93b5a2d036d687cd79ee;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma
index c67dd1785..672099281 100644
--- a/helm/software/matita/contribs/dama/dama/property_sigma.ma
+++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "ordered_uniform.ma".
-
+include "russell_support.ma".
 
 (* Definition 3.5 *)
 alias num (instance 0) = "natural number".
@@ -22,7 +22,7 @@ definition property_sigma ≝
    ∀U.us_unifbase ? U → 
      ∃V:sequence (C square → Prop).
        (∀i.us_unifbase ? (V i)) ∧ 
-       ∀a:sequence C.∀x:C.a ↑ x → 
+       ∀a:sequence C.∀x:C.(a ↑ x ∨ a ↓ x) → 
          (∀n.∀i,j.n ≤ i → n ≤ j → V n 〈a i,a j〉) → U 〈a 0,x〉.
       
 definition max ≝
@@ -57,75 +57,61 @@ qed.
 lemma max_le_r: ∀n,m,z.max n m ≤ z → m ≤ z.
 intros; rewrite > sym_max in H; apply (max_le_l ??? H); 
 qed.
-
-
-definition hide ≝ λT:Type.λx:T.x.
-
-notation < "\blacksquare" non associative with precedence 50 for @{'hide}.
-interpretation "hide" 'hide =
- (cic:/matita/dama/property_sigma/hide.con _ _).
-interpretation "hide2" 'hide =
- (cic:/matita/dama/property_sigma/hide.con _ _ _).
-
-definition inject ≝ λP.λa:nat.λp:P a. ex_introT ? P ? p.
-coercion cic:/matita/dama/property_sigma/inject.con 0 1.
-definition eject ≝ λP.λc: ∃n:nat.P n. match c with [ ex_introT w _ ⇒ w].
-coercion cic:/matita/dama/property_sigma/eject.con.
-      
+    
 (* Lemma 3.6 *)   
 lemma sigma_cauchy:
   ∀C:ordered_uniform_space.property_sigma C →
-    ∀a:sequence C.∀l:C.a ↑ l → a is_cauchy → a uniform_converges l.
-intros 8; cases H1; cases H5; clear H5;
-cases (H ? H3); cases H5; clear H5;
+    ∀a:sequence C.∀l:C.(a ↑ l ∨ a ↓ l) → a is_cauchy → a uniform_converges l.
+intros 8; cases (H ? H3) (w H5); cases H5 (H8 H9); clear H5;
+alias symbol "pair" = "pair".
+letin spec ≝ (λz,k:nat.∀i,j,l:nat.k ≤ i → k ≤ j → l ≤ z → w l 〈a i,a j〉);
 letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
   match i with
   [ O ⇒ match H2 (w i) ? with [ ex_introT k _ ⇒ k ]
   | S i' ⇒ max (match H2 (w i) ? with [ ex_introT k _ ⇒ k ]) (S (aux i'))
   ] in aux
-  : 
-  ∀z:nat.∃k:nat.∀i,j,l.k ≤ i → k ≤ j → l ≤ z → w l 〈a i, a j〉));
+  : ∀z.∃k. spec z k)); unfold spec in aux ⊢ %;
   [1,2:apply H8;
   |3: intros 3; cases (H2 (w n) (H8 n)); simplify in ⊢ (? (? % ?) ?→?);
       simplify in ⊢ (?→? (? % ?) ?→?);
-      intros; lapply (H10 i j) as H14;
-        [2: apply (max_le_l ??? H11);|3:apply (max_le_l ??? H12);]
-      cases (le_to_or_lt_eq ?? H13); [2: destruct H15; destruct H5; assumption]
-      generalize in match H11; generalize in match H12;
-      cases (aux n1); simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
-      apply H16; [3: apply le_S_S_to_le; assumption]
+      intros; lapply (H5 i j) as H14;
+        [2: apply (max_le_l ??? H6);|3:apply (max_le_l ??? H7);]
+      cases (le_to_or_lt_eq ?? H10); [2: destruct H11; destruct H4; assumption]
+      cases (aux n1) in H6 H7 ⊢ %; simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
+      apply H6; [3: apply le_S_S_to_le; assumption]
       apply lt_to_le; apply (max_le_r w1); assumption;
-  |4: intros; clear H11; rewrite > H5 in H10; 
-      rewrite < (le_n_O_to_eq ? H14); apply H10; assumption;] 
-cut (((m : nat→nat) : sequence nat_ordered_set) is_strictly_increasing) as Hm; [2:
+  |4: intros; clear H6; rewrite > H4 in H5; 
+      rewrite < (le_n_O_to_eq ? H11); apply H5; assumption;] 
+cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_strictly_increasing) as Hm; [2:
   intro n; change with (S (m n) ≤ m (S n)); unfold m; 
   whd in ⊢ (? ? %); apply (le_max ? (S (m n)));]
-cut (((m : nat→nat) : sequence nat_ordered_set) is_increasing) as Hm1; [2:
+cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_increasing) as Hm1; [2:
   intro n; intro L; change in L with (m (S n) < m n);
   lapply (Hm n) as L1; change in L1 with (m n < m (S n));
   lapply (trans_lt ??? L L1) as L3; apply (not_le_Sn_n ? L3);] 
-clearbody m;
-lapply (selection ?? Hm a l H1) as H10; 
+clearbody m; unfold spec in m Hm Hm1; clear spec;
+cut (⌊x,a (m x)⌋ ↑ l ∨ ⌊x,a (m x)⌋ ↓ l) as H10; [2: 
+ cases H1;
+ [ left; apply (selection_uparrow ?? Hm a l H4);
+ | right; apply (selection_downarrow ?? Hm a l H4);]] 
 lapply (H9 ?? H10) as H11; [
   exists [apply (m 0:nat)] intros;
-  apply (ous_convex ?? H3 ? H11 (H6 (m 0)));
-  simplify; repeat split; [intro X; cases (os_coreflexive ?? X)|2,3:apply H6;]
-  change with (a (m O) ≤ a i);
-  apply (trans_increasing ?? H4); intro; whd in H12;
-  apply (not_le_Sn_n i);  apply (transitive_le ??? H12 H5)]
+  cases H1;
+    [cases H5; cases H7; apply (ous_convex ?? H3 ? H11 (H12 (m O)));
+    |cases H5; cases H7; cases (us_phi4 ?? H3 〈(a (m O)),l〉); 
+     lapply (H14 H11) as H11'; apply (ous_convex ?? H3 〈l,(a (m O))〉 H11' (H12 (m O)));]
+  simplify; repeat split; [1,6:intro X; cases (os_coreflexive ?? X)|*: try apply H12;]
+  [1:change with (a (m O) ≤ a i);
+     apply (trans_increasing ?? H6); intro; apply (le_to_not_lt ?? H4 H14);
+  |2:change with (a i ≤ a (m O));
+     apply (trans_decreasing ?? H6); intro; apply (le_to_not_lt ?? H4 H16);]]  
 clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
-generalize in match (refl_eq nat (m q)); 
-generalize in match (m q) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
-intros; simplify in H12:(? ? ? %); simplify in ⊢ (? ? (? ? ? % ?)); 
-generalize in match (refl_eq nat (m r)); 
-generalize in match (m r) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
-intros; simplify in H14:(? ? ? %); simplify in ⊢ (? ? (? ? ? ? %)); 
-generalize in match (refl_eq nat (m p));
-generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
-intros; simplify in H16:(? ? ? %);
-apply H15; [3: apply le_n] destruct H16; destruct H14; destruct H12; clear H11 H13 H15;
+generalize in match (refl_eq nat (m p)); 
+generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X; 
+intros (H16); simplify in H16:(? ? ? %); destruct H16;
+apply H15; [3: apply le_n]
 [1: lapply (trans_increasing ?? Hm1 p q) as T; [apply not_lt_to_le; apply T;]
-    apply (le_to_not_lt p q H5);
+    apply (le_to_not_lt p q H4);
 |2: lapply (trans_increasing ?? Hm1 p r) as T; [apply not_lt_to_le; apply T;]
-    apply (le_to_not_lt p r H10);]
-qed.
\ No newline at end of file
+    apply (le_to_not_lt p r H5);]
+qed.