From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 27 Oct 2008 10:19:21 +0000 (+0000)
Subject: seg_u/l were inverted, more work
X-Git-Tag: make_still_working~4631
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=62571dd402d272b1632b7739607d25df3552cc04;p=helm.git

seg_u/l were inverted, more work
---

diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
index 1f4f6f686..1dba15a7c 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -34,7 +34,8 @@ coercion ous_unifspace.
 
 record ordered_uniform_space : Type ≝ {
   ous_stuff :> ordered_uniform_space_;
-  ous_convex: ∀U.us_unifbase ous_stuff U → convex (os_l ous_stuff) U
+  ous_convex_l: ∀U.us_unifbase ous_stuff U → convex (os_l ous_stuff) U;
+  ous_convex_r: ∀U.us_unifbase ous_stuff U → convex (os_r ous_stuff) U
 }.   
 
 definition half_ordered_set_OF_ordered_uniform_space : ordered_uniform_space → half_ordered_set.
@@ -170,7 +171,7 @@ intros (O s); apply mk_ordered_uniform_space;
 |2: simplify; unfold convex; intros 3; cases s1; intros;
     (* TODO: x2sx is for ≰, we need one for ≤ *) 
     cases H (u HU); cases HU (Gu HuU); clear HU H;
-    lapply depth=0 (ous_convex ?? Gu 〈\fst h,\fst h1〉 ???????) as K3;
+    lapply depth=0 (ous_convex_l ?? Gu 〈\fst h,\fst h1〉 ???????) as K3;
     [2: intro; apply H2; apply (x2sx (os_l O) s h h1 H);
     |3: apply 〈\fst (\fst y),\fst (\snd y)〉;
     |4: intro; change in H with (\fst (\fst y) ≰ \fst h1); apply H3;
@@ -182,23 +183,39 @@ intros (O s); apply mk_ordered_uniform_space;
     |7: change with (\fst (\fst y) ≤ \fst (\snd y)); intro; apply H6;
         apply (x2sx (os_l O) s (\fst y) (\snd y) H);
     |8: apply (restrict O s U u y HuU K3);
-    |1: apply (unrestrict O s ?? 〈h,h1〉 HuU H1);]]  
+    |1: apply (unrestrict O s ?? 〈h,h1〉 HuU H1);]
+|3: simplify; unfold convex; intros 3; cases s1; intros; (* TODO *)
+    cases H (u HU); cases HU (Gu HuU); clear HU H;
+    lapply depth=0 (ous_convex_r ?? Gu 〈\fst h,\fst h1〉 ???????) as K3;
+    [2: intro; apply H2; apply (x2sx (os_r O) s h h1 H);
+    |3: apply 〈\fst (\fst y),\fst (\snd y)〉;
+    |4: intro; (*change in H with (\fst (\fst y) ≱ \fst h1);*) apply H3;
+        apply (x2sx (os_r O) s (\fst y) h1 H);
+    |5: (*change with (\fst h ≥ \fst (\fst y));*) intro; apply H4;
+        apply (x2sx (os_r O) s h (\fst y) H);
+    |6: (*change with (\fst (\snd y) ≤ \fst h1);*) intro; apply H5;
+        apply (x2sx (os_r O) s (\snd y) h1 H);
+    |7: (*change with (\fst (\fst y) ≤ \fst (\snd y));*) intro; apply H6;
+        apply (x2sx (os_r O) s (\fst y) (\snd y) H);
+    |8: apply (restrict O s U u y HuU K3);
+    |1: apply (unrestrict O s ?? 〈h,h1〉 HuU H1);]
+]  
 qed.
 
-interpretation "Ordered uniform space segment" 'segment_set a b = 
- (segment_ordered_uniform_space _ a b).
+interpretation "Ordered uniform space segment" 'segment_set a = 
+ (segment_ordered_uniform_space _ a).
 
 (* Lemma 3.2 *)
 alias symbol "pi1" = "exT \fst".
 lemma restric_uniform_convergence:
  ∀O:ordered_uniform_space.∀s:‡O.
   ∀x:{[s]}.
-   ∀a:sequence {[s]}.
+   ∀a:sequence (segment_ordered_uniform_space O s).
     (⌊n, \fst (a n)⌋ : sequence O) uniform_converges (\fst x) → 
       a uniform_converges x.
-intros 8; cases H1; cases H2; clear H2 H1;
+intros 7; cases H1; cases H2; clear H2 H1;
 cases (H ? H3) (m Hm); exists [apply m]; intros; 
-apply (restrict ? l u ??? H4); apply (Hm ? H1);
+apply (restrict ? s ??? H4); apply (Hm ? H1);
 qed.
 
 definition order_continuity ≝
diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
index 41674ec00..713588e70 100644
--- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
+++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
@@ -22,40 +22,59 @@ definition exhaustive ≝
      (a is_increasing → a is_upper_located → a is_cauchy) ∧
      (b is_decreasing → b is_lower_located → b is_cauchy).
 
-lemma segment_upperbound:
-  ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.u is_upper_bound ⌊n,\fst (a n)⌋.
-intros 5; change with (\fst (a n) ≤ u); cases (a n); cases H; assumption;
+lemma h_segment_upperbound:
+  ∀C:half_ordered_set.
+   ∀s:segment C.
+    ∀a:sequence (half_segment_ordered_set C s).
+     (seg_u C s) (upper_bound ? ⌊n,\fst (a n)⌋). 
+intros; cases (wloss_prop C); unfold; rewrite < H; simplify; intro n;
+cases (a n); simplify; unfold in H1; rewrite < H in H1; cases H1; 
+simplify in H2 H3; rewrite < H in H2 H3; assumption;
 qed.
 
-lemma segment_lowerbound:
-  ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.l is_lower_bound ⌊n,\fst (a n)⌋.
-intros 5; change with (l ≤ \fst (a n)); cases (a n); cases H; assumption;
-qed.
+notation "'segment_upperbound'" non associative with precedence 90 for @{'segment_upperbound}.
+notation "'segment_lowerbound'" non associative with precedence 90 for @{'segment_lowerbound}.
 
-lemma segment_preserves_uparrow:
-  ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.∀x,h. 
-    ⌊n,\fst (a n)⌋ ↑ x → a ↑ ≪x,h≫.
-intros; cases H (Ha Hx); split [apply Ha] cases Hx; 
-split; [apply H1] intros;
-cases (H2 (\fst y)); [2: apply H3;] exists [apply w] assumption;
-qed.
+interpretation "segment_upperbound" 'segment_upperbound = (h_segment_upperbound (os_l _)).
+interpretation "segment_lowerbound" 'segment_lowerbound = (h_segment_upperbound (os_r _)).
 
-lemma segment_preserves_downarrow:
-  ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.∀x,h. 
-    ⌊n,\fst (a n)⌋ ↓ x → a ↓ ≪x,h≫.
-intros; cases H (Ha Hx); split [apply Ha] cases Hx; 
-split; [apply H1] intros;
-cases (H2 (\fst y));[2:apply H3]; exists [apply w] assumption;
+lemma h_segment_preserves_uparrow:
+  ∀C:half_ordered_set.∀s:segment C.∀a:sequence (half_segment_ordered_set C s).
+   ∀x,h. uparrow C ⌊n,\fst (a n)⌋ x → uparrow (half_segment_ordered_set C s) a ≪x,h≫.
+intros; cases H (Ha Hx); split;
+[ intro n; intro H; apply (Ha n); apply (sx2x ???? H);
+| cases Hx; split; 
+  [ intro n; intro H; apply (H1 n);apply (sx2x ???? H); 
+  | intros; cases (H2 (\fst y)); [2: apply (sx2x ???? H3);] 
+    exists [apply w] apply (x2sx ?? (a w) y H4);]]
 qed.
-    
+
+notation "'segment_preserves_uparrow'" non associative with precedence 90 for @{'segment_preserves_uparrow}.
+notation "'segment_preserves_downarrow'" non associative with precedence 90 for @{'segment_preserves_downarrow}.
+
+interpretation "segment_preserves_uparrow" 'segment_preserves_uparrow = (h_segment_preserves_uparrow (os_l _)).
+interpretation "segment_preserves_downarrow" 'segment_preserves_downarrow = (h_segment_preserves_uparrow (os_r _)).
+
+lemma hint_pippo:
+ ∀C,s.
+  sequence
+   (Type_of_ordered_set
+    (segment_ordered_set
+     (ordered_set_OF_ordered_uniform_space C) s))
+ →  
+ sequence (Type_OF_uniform_space (segment_ordered_uniform_space C s)). intros; assumption;
+qed. 
+
+coercion hint_pippo nocomposites.
+ 
 (* Fact 2.18 *)
 lemma segment_cauchy:
-  ∀C:ordered_uniform_space.∀l,u:C.∀a:sequence {[l,u]}.
+  ∀C:ordered_uniform_space.∀s:‡C.∀a:sequence {[s]}.
     a is_cauchy → ⌊n,\fst (a n)⌋ is_cauchy.
-intros 7; 
+intros 6; 
 alias symbol "pi1" (instance 3) = "pair pi1".
 alias symbol "pi2" = "pair pi2".
-apply (H (λx:{[l,u]} squareB.U 〈\fst (\fst x),\fst (\snd x)〉));
+apply (H (λx:{[s]} squareB.U 〈\fst (\fst x),\fst (\snd x)〉));
 (unfold segment_ordered_uniform_space; simplify);
 exists [apply U] split; [assumption;]
 intro; cases b; intros; simplify; split; intros; assumption;
diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma
index 9d9485f9c..74f03de4c 100644
--- a/helm/software/matita/contribs/dama/dama/property_sigma.ma
+++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma
@@ -95,17 +95,19 @@ cut (⌊x,a (m x)⌋ ↑ l ∨ ⌊x,a (m x)⌋ ↓ l) as H10; [2:
  | right; apply (selection_downarrow ? Hm a l H4);]] 
 lapply (H9 ?? H10) as H11; [
   exists [apply (m 0:nat)] intros;
-  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: apply (le_reflexive l); 
-  |2,5: apply (H12 (\fst (m 0)));
-  |3,8: apply (H12 i);
-  |4:change with (a (m O) ≤ a i);
-     apply (trans_increasing a H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H14);
-  |7:change with (a i ≤ a (m O));
+  cases H1; cases H5; cases H7; cases (us_phi4 ?? H3 〈l,a i〉);
+  apply H15; change with (U 〈a i,l〉);
+    [apply (ous_convex_l C ? H3 ? H11 (H12 (m O)));
+    |apply (ous_convex_r C ? H3 ? H11 (H12 (m O)));]
+  [1:apply (H12 i);
+  |3: apply (le_reflexive l);
+  |4: apply (H12 i);
+  |2:change with (a (m O) ≤ a i);
+     apply (trans_increasing a H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);
+  |5:apply (H12 i);
+  |7:apply (ge_reflexive (l : hos_carr (os_r C)));
+  |8:apply (H12 i);
+  |6:change with (a i ≤ a (m O));
      apply (trans_decreasing ? H6 (\fst (m 0)) i); 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 p)); 
diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index 7bb684fd8..8ee17fc7d 100644
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -209,10 +209,10 @@ notation "𝕝 \sub term 90 s p" non associative with precedence 45 for @{'low $
  
 definition seg_u ≝
  λO:half_ordered_set.λs:segment O.λP: O → CProp.
-   wloss O ? (λl,u.P u) (seg_l_ ? s) (seg_u_ ? s).
+   wloss O ? (λl,u.P u) (seg_u_ ? s) (seg_l_ ? s).
 definition seg_l ≝
  λO:half_ordered_set.λs:segment O.λP: O → CProp.
-   wloss O ? (λl,u.P u) (seg_u_ ? s) (seg_l_ ? s). 
+   wloss O ? (λl,u.P u) (seg_l_ ? s) (seg_u_ ? s). 
  
 interpretation "uppper" 'upp s P = (seg_u (os_l _) s P).
 interpretation "lower" 'low s P = (seg_l (os_l _) s P).
@@ -221,7 +221,7 @@ interpretation "lower dual" 'low s P = (seg_u (os_r _) s P).
  
 definition in_segment ≝ 
   λO:half_ordered_set.λs:segment O.λx:O.
-    wloss O ? (λp1,p2.p1 ∧ p2) (seg_u ? s (λu.u ≤≤ x)) (seg_l ? s (λl.x ≤≤ l)).
+    wloss O ? (λp1,p2.p1 ∧ p2) (seg_l ? s (λl.l ≤≤ x)) (seg_u ? s (λu.x ≤≤ u)).
 
 notation "‡O" non associative with precedence 90 for @{'segment $O}.
 interpretation "Ordered set sergment" 'segment x = (segment x).
@@ -360,12 +360,14 @@ qed.
 *)
        
 (* Definition 2.10 *)
+
 alias symbol "pi2" = "pair pi2".
 alias symbol "pi1" = "pair pi1".
+(*
 definition square_segment ≝ 
   λO:half_ordered_set.λs:segment O.λx: square_half_ordered_set O.
     in_segment ? s (\fst x) ∧ in_segment ? s (\snd x).
- 
+*) 
 definition convex ≝
   λO:half_ordered_set.λU:square_half_ordered_set O → Prop.
     ∀s.U s → le O (\fst s) (\snd s) →