X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fproperty_sigma.ma;h=691d21045957d285b230c08bb82ee45984fad487;hb=9eabe046c1182960de8cfdba96c5414224e3a61e;hp=7d35e086fcd88a7abae314e599d15d60c51f8f4e;hpb=5f5fa5c779fcef187edf08703ae8f56653481bd1;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 7d35e086f..691d21045 100644
--- a/helm/software/matita/contribs/dama/dama/property_sigma.ma
+++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma
@@ -30,31 +30,94 @@ definition max ≝
   
 lemma le_max: ∀n,m.m ≤ max n m.
 intros; unfold max; apply leb_elim; simplify; intros; [assumption] apply le_n;
-qed.   
+qed.
+
+lemma max_le_l: ∀n,m,z.max n m ≤ z → n ≤ z.
+intros 3; unfold max; apply leb_elim; simplify; intros; [assumption]
+apply lt_to_le; apply (lt_to_le_to_lt ???? H1);
+apply not_le_to_lt; assumption;
+qed.
+
+lemma sym_max: ∀n,m.max n m = max m n.
+intros; apply (nat_elim2 ???? n m); simplify; intros;
+[1: elim n1; [reflexivity] rewrite < H in ⊢ (? ? ? (? %));
+    simplify; rewrite > H; reflexivity;
+|2: reflexivity
+|3: apply leb_elim; apply leb_elim; simplify;
+    [1: intros; apply le_to_le_to_eq; apply le_S_S;assumption;
+    |2,3: intros; reflexivity;
+    |4: intros; unfold max in H; 
+        rewrite > (?:leb n1 m1 = false) in H; [2:
+          apply lt_to_leb_false; apply not_le_to_lt; assumption;]
+        rewrite > (?:leb m1 n1 = false) in H; [2:
+          apply lt_to_leb_false; apply not_le_to_lt; assumption;]
+        apply eq_f; assumption;]]
+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 "hide" 'hide = (hide _ _).
+interpretation "hide2" 'hide = (hide _ _ _).
+
+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:
-  ∀O:ordered_uniform_space.property_sigma O →
-    ∀a:sequence O.∀l:O.a ↑ l → a is_cauchy → a uniform_converges l.
+  ∀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;
-letin m ≝ (? : sequence nat_ordered_set); [
-  apply (hide (nat→nat)); intro i; elim i (i' Rec);
-    [1: apply (hide nat);cases (H2 ? (H8 0)) (k _); apply k;
-    |2: apply (max (hide nat ?) (S Rec)); cases (H2 ? (H8 (S i'))) (k Hk);apply k]]
-cut (m 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)));]    
-lapply (selection ?? Hm a l H1) as H10;
-lapply (H9 ?? H10) as H11;
-[1: exists [apply (m 0)] intros;
-    apply (ous_convex ?? H3 ? H11 (H6 (m 0)));
-    simplify; repeat split;
-        
-  
-  
\ No newline at end of file
+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〉));
+  [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]
+      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:
+  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:
+  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; 
+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)]
+clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
+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);
+|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.