ordered_set simplified

[helm.git] / helm / software / matita / contribs / dama / dama / supremum.ma

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index 7a52e5f064260f1a9f04463a4414e8b0c7b6962a..ca422597d5a9c7a98c8b5b18d9080294ab5c1eb9 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -202,26 +202,26 @@ record segment (O : Type) : Type ≝ {
    seg_u_ : O
 }.
 
-notation > "𝕦_term 90 s p" non associative with precedence 45 for @{'upp $s $p}.
-notation "𝕦 \sub term 90 s p" non associative with precedence 45 for @{'upp $s $p}. 
-notation > "𝕝_term 90 s p" non associative with precedence 45 for @{'low $s $p}.
-notation "𝕝 \sub term 90 s p" non associative with precedence 45 for @{'low $s $p}. 
+notation > "𝕦_term 90 s" non associative with precedence 90 for @{'upp $s}.
+notation "𝕦 \sub term 90 s" non associative with precedence 90 for @{'upp $s}. 
+notation > "𝕝_term 90 s" non associative with precedence 90 for @{'low $s}.
+notation "𝕝 \sub term 90 s" non associative with precedence 90 for @{'low $s}. 
  
 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).
+ λO:half_ordered_set.λs:segment O.
+   wloss O ?? (λl,u.l) (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). 
+ λO:half_ordered_set.λs:segment O.
+   wloss O ?? (λl,u.l) (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).
-interpretation "uppper dual" 'upp s P = (seg_l (os_r _) s P).
-interpretation "lower dual" 'low s P = (seg_u (os_r _) s P).
+interpretation "uppper" 'upp s = (seg_u (os_l _) s).
+interpretation "lower" 'low s = (seg_l (os_l _) s).
+interpretation "uppper dual" 'upp s = (seg_l (os_r _) s).
+interpretation "lower dual" 'low s = (seg_u (os_r _) s).
  
 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 ≤≤ x) (x ≤≤ seg_u ? s).
 
 notation "‡O" non associative with precedence 90 for @{'segment $O}.
 interpretation "Ordered set sergment" 'segment x = (segment x).
@@ -234,19 +234,19 @@ definition segment_ordered_set_exc ≝
   λO:half_ordered_set.λs:‡O.
    λx,y:segment_ordered_set_carr O s.hos_excess_ O (\fst x) (\fst y).
 lemma segment_ordered_set_corefl:
- ∀O,s. coreflexive ? (wloss O ? (segment_ordered_set_exc O s)).
+ ∀O,s. coreflexive ? (wloss O ?? (segment_ordered_set_exc O s)).
 intros 3; cases x; cases (wloss_prop O);
 generalize in match (hos_coreflexive O w);
-rewrite < (H1 ? (segment_ordered_set_exc O s));
-rewrite < (H1 ? (hos_excess_ O)); intros; assumption;
+rewrite < (H1 ?? (segment_ordered_set_exc O s));
+rewrite < (H1 ?? (hos_excess_ O)); intros; assumption;
 qed.
 lemma segment_ordered_set_cotrans : 
-  ∀O,s. cotransitive ? (wloss O ? (segment_ordered_set_exc O s)).
+  ∀O,s. cotransitive ? (wloss O ?? (segment_ordered_set_exc O s)).
 intros 5 (O s x y z); cases x; cases y ; cases z; clear x y z;
 generalize in match (hos_cotransitive O w w1 w2);
 cases (wloss_prop O); 
-do 3 rewrite < (H3 ? (segment_ordered_set_exc O s));
-do 3 rewrite < (H3 ? (hos_excess_ O)); intros; apply H4; assumption;
+do 3 rewrite < (H3 ?? (segment_ordered_set_exc O s));
+do 3 rewrite < (H3 ?? (hos_excess_ O)); intros; apply H4; assumption;
 qed.  
   
 lemma half_segment_ordered_set: 
@@ -278,6 +278,19 @@ interpretation "Ordered set segment" 'segset s = (segment_ordered_set _ s).
 intros; try reflexivity;
 *)
 
+lemma prove_in_segment: 
+ ∀O:half_ordered_set.∀s:segment O.∀x:O.
+   (seg_l O s) ≤≤ x → x ≤≤ (seg_u O s) → x ∈ s.
+intros; unfold; cases (wloss_prop O); rewrite < H2;
+split; assumption;
+qed.
+
+lemma cases_in_segment: 
+  ∀C:half_ordered_set.∀s:segment C.∀x. x ∈ s → (seg_l C s) ≤≤ x ∧ x ≤≤ (seg_u C s).
+intros; unfold in H; cases (wloss_prop C) (W W); rewrite<W in H; [cases H; split;assumption]
+cases H; split; assumption;
+qed. 
+
 definition hint_sequence: 
   ∀C:ordered_set.
     sequence (hos_carr (os_l C)) → sequence (Type_of_ordered_set C).
@@ -314,7 +327,7 @@ lemma x2sx:
    ∀s:segment O.∀x,y:half_segment_ordered_set ? s.
     \fst x ≰≰ \fst y → x ≰≰ y.
 intros 4; cases x; cases y; clear x y; simplify; unfold hos_excess;
-whd in ⊢ (?→? (% ? ?) ? ? ? ?); simplify in ⊢ (?→%);
+whd in ⊢ (?→? (% ? ?)? ? ? ? ?); simplify in ⊢ (?→%);
 cases (wloss_prop O) (E E); do 2 rewrite < E; intros; assumption;
 qed.
 
@@ -323,10 +336,22 @@ lemma sx2x:
    ∀s:segment O.∀x,y:half_segment_ordered_set ? s.
     x ≰≰ y → \fst x ≰≰ \fst y.
 intros 4; cases x; cases y; clear x y; simplify; unfold hos_excess;
-whd in ⊢ (? (% ? ?) ? ? ? ? → ?); simplify in ⊢ (% → ?);
+whd in ⊢ (? (% ? ?) ?? ? ? ? → ?); simplify in ⊢ (% → ?);
 cases (wloss_prop O) (E E); do 2 rewrite < E; intros; assumption;
 qed.
 
+lemma l2sl:
+  ∀C,s.∀x,y:half_segment_ordered_set C s. \fst x ≤≤ \fst y → x ≤≤ y.
+intros; intro; apply H; apply sx2x; apply H1;
+qed.
+
+
+lemma sl2l:
+  ∀C,s.∀x,y:half_segment_ordered_set C s. x ≤≤ y → \fst x ≤≤ \fst y.
+intros; intro; apply H; apply x2sx; apply H1;
+qed.
+
+
 lemma h_segment_preserves_supremum:
   ∀O:half_ordered_set.∀s:segment O.
    ∀a:sequence (half_segment_ordered_set ? s).
@@ -350,26 +375,33 @@ notation "'segment_preserves_infimum'" non associative with precedence 90 for @{
 interpretation "segment_preserves_supremum" 'segment_preserves_supremum = (h_segment_preserves_supremum (os_l _)).
 interpretation "segment_preserves_infimum" 'segment_preserves_infimum = (h_segment_preserves_supremum (os_r _)).
 
-(* TEST, ma quanto godo! *)
-lemma segment_preserves_infimum2:
+(*
+test segment_preserves_infimum2:
   ∀O:ordered_set.∀s:‡O.∀a:sequence {[s]}.∀x:{[s]}. 
     ⌊n,\fst (a n)⌋ is_decreasing ∧ 
     (\fst x) is_infimum ⌊n,\fst (a n)⌋ → a ↓ x.
 intros; apply (segment_preserves_infimum s a x H);
 qed.
 *)
-           
+       
 (* Definition 2.10 *)
+
 alias symbol "pi2" = "pair pi2".
 alias symbol "pi1" = "pair pi1".
+(*
 definition square_segment ≝ 
-  λO:ordered_set.λa,b:O.λx: O squareO.
-    And4 (\fst x ≤ b) (a ≤ \fst x) (\snd x ≤ b) (a ≤ \snd x).
- 
+  λ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:ordered_set.λU:O squareO → Prop.
-    ∀p.U p → \fst p ≤ \snd p → ∀y. 
-      square_segment O (\fst p) (\snd p) y → U y.
+  λO:half_ordered_set.λU:square_half_ordered_set O → Prop.
+    ∀s.U s → le O (\fst s) (\snd s) → 
+     ∀y. 
+       le O (\fst y) (\snd s) → 
+       le O (\fst s) (\fst y) →
+       le O (\snd y) (\snd s) →
+       le O (\fst y) (\snd y) →
+       U y.
   
 (* Definition 2.11 *)  
 definition upper_located ≝
@@ -394,8 +426,8 @@ interpretation "Ordered set lower locatedness" 'lower_located s =
 lemma h_uparrow_upperlocated:
   ∀C:half_ordered_set.∀a:sequence C.∀u:C.uparrow ? a u → upper_located ? a.
 intros (C a u H); cases H (H2 H3); clear H; intros 3 (x y Hxy);
-cases H3 (H4 H5); clear H3; cases (hos_cotransitive ??? u Hxy) (W W);
-[2: cases (H5 ? W) (w Hw); left; exists [apply w] assumption;
+cases H3 (H4 H5); clear H3; cases (hos_cotransitive C y x u Hxy) (W W);
+[2: cases (H5 x W) (w Hw); left; exists [apply w] assumption;
 |1: right; exists [apply u]; split; [apply W|apply H4]]
 qed.