From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 28 Oct 2008 22:23:47 +0000 (+0000)
Subject: even more polymorphic dualizer
X-Git-Tag: make_still_working~4621
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5322d66340d43e85b85e15dddcddeff3ae3a3552;p=helm.git

even more polymorphic dualizer
---

diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
index 5957235cc..1536476b0 100644
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -59,14 +59,6 @@ cases (wloss_prop (os_l C))(W W); unfold os_r; unfold dual_hos; simplify;rewrite
   rewrite <W in H1; simplify in H1; apply (H1 Hw);]
 qed. 
 
-alias symbol "upp" = "uppper".
-alias symbol "leq" = "Ordered set less or equal than".
-lemma cases_in_segment: 
-  ∀C:half_ordered_set.∀s:segment C.∀x. x ∈ s → seg_l C s (λl.l ≤≤ x) ∧ seg_u C s (λu.x ≤≤ u).
-intros; unfold in H; cases (wloss_prop C) (W W); rewrite<W in H; [cases H; split;assumption]
-cases H; split; assumption;
-qed. 
-
 lemma trans_under_upp:
  ∀O:ordered_set.∀s:‡O.∀x,y:O.
   x ≤ y → 𝕦_s (λu.y ≤ u) → 𝕦_s (λu.x ≤ u).
diff --git a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
index dfeaa6d35..9129cef9a 100644
--- a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
@@ -44,7 +44,7 @@ cases (nat_discriminable x z); [2: left; assumption] cases H1; clear H1;
 qed.
   
 lemma nat_ordered_set : ordered_set.
-letin hos ≝ (mk_half_ordered_set nat (λT:Type.λf:T→T→CProp.f) ? nat_excess ? nat_excess_cotransitive);
+letin hos ≝ (mk_half_ordered_set nat (λT,R:Type.λf:T→T→R.f) ? nat_excess ? nat_excess_cotransitive);
 [ intros; left; intros; reflexivity;
 | intro x; intro H; apply (not_le_Sn_n ? H);]
 constructor 1;  
diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma
index 2a1089fec..56b354859 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma
@@ -27,14 +27,14 @@ interpretation "" ' = ( (os_r _)).
 (* Definition 2.1 *)
 record half_ordered_set: Type ≝ {
   hos_carr:> Type;
-  wloss: ∀A:Type. (A → A → CProp) → A → A → CProp;
-  wloss_prop: (∀T,P,x,y.P x y = wloss T P x y) ∨ (∀T,P,x,y.P y x = wloss T P x y); 
+  wloss: ∀A,B:Type. (A → A → B) → A → A → B;
+  wloss_prop: (∀T,R,P,x,y.P x y = wloss T R P x y) ∨ (∀T,R,P,x,y.P y x = wloss T R P x y); 
   hos_excess_: hos_carr → hos_carr → CProp;
-  hos_coreflexive: coreflexive ? (wloss ? hos_excess_);
-  hos_cotransitive: cotransitive ? (wloss ? hos_excess_)
+  hos_coreflexive: coreflexive ? (wloss ?? hos_excess_);
+  hos_cotransitive: cotransitive ? (wloss ?? hos_excess_)
 }.
 
-definition hos_excess ≝ λO:half_ordered_set.wloss O ? (hos_excess_ O). 
+definition hos_excess ≝ λO:half_ordered_set.wloss O ?? (hos_excess_ O). 
 
 (*
 lemma find_leq : half_ordered_set → half_ordered_set.
@@ -55,7 +55,7 @@ qed.
 definition dual_hos : half_ordered_set → half_ordered_set.
 intro; constructor 1;
 [ apply (hos_carr h);
-| apply (λT,f,x,y.wloss h T f y x); 
+| apply (λT,R,f,x,y.wloss h T R f y x); 
 | intros; cases (wloss_prop h);[right|left]intros;apply H; 
 | apply (hos_excess_ h);
 | apply (hos_coreflexive h);
@@ -169,12 +169,12 @@ apply (mk_half_ordered_set (O × O));
 [1: apply (wloss O);
 |2: intros; cases (wloss_prop O); [left|right] intros; apply H;
 |3: apply (square_exc O); 
-|4: intro x; cases (wloss_prop O); rewrite < (H  ? (square_exc O) x x); clear H;
+|4: intro x; cases (wloss_prop O); rewrite < (H  ?? (square_exc O) x x); clear H;
     cases x; clear x; unfold square_exc; intro H; cases H; clear H; simplify in H1;
     [1,3: apply (hos_coreflexive O h H1);
     |*: apply (hos_coreflexive O h1 H1);]
 |5: intros 3 (x0 y0 z0); cases (wloss_prop O);
-    do 3 rewrite < (H  ? (square_exc O)); clear H; cases x0; cases y0; cases z0; clear x0 y0 z0;
+    do 3 rewrite < (H  ?? (square_exc O)); clear H; cases x0; cases y0; cases z0; clear x0 y0 z0;
     simplify; intro H; cases H; clear H;
     [1: cases (hos_cotransitive ? h h2 h4 H1); [left;left|right;left] assumption;
     |2: cases (hos_cotransitive ? h1 h3 h5 H1); [left;right|right;right] assumption;
diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
index 48551f85e..9788d4d35 100644
--- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
+++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
@@ -19,10 +19,10 @@ 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;
+      upper_bound ? ⌊n,\fst (a n)⌋ (seg_u C s). 
+intros 4; simplify; cases (a n); simplify; unfold in H;
+cases (wloss_prop C); rewrite < H1 in H; simplify; cases H; 
+assumption;
 qed.
 
 notation "'segment_upperbound'" non associative with precedence 90 for @{'segment_upperbound}.
@@ -68,12 +68,7 @@ definition exhaustive ≝
      (a is_increasing → a is_upper_located → a is_cauchy) ∧
      (b is_decreasing → b is_lower_located → b is_cauchy).
 
-lemma prove_in_segment: 
- ∀O:half_ordered_set.∀s:segment O.∀x:O.
-   seg_l O s (λl.l ≤≤ x) → seg_u O s (λu.x ≤≤ u) → x ∈ s.
-intros; unfold; cases (wloss_prop O); rewrite < H2;
-split; assumption;
-qed.
+STOP
 
 lemma h_uparrow_to_in_segment:
   ∀C:half_ordered_set.
@@ -83,7 +78,7 @@ lemma h_uparrow_to_in_segment:
        ∀x:C. uparrow C a x → 
          in_segment C s x.
 intros (C H a H1 x H2); unfold in H2; cases H2; clear H2;unfold in H3 H4; cases H4; clear H4; unfold in H2;
-cases (wloss_prop C) (W W); apply prove_in_segment; unfold; rewrite <W;simplify;
+cases (wloss_prop C) (W W); apply prove_in_segment; unfold; 
 [ apply (hle_transitive ??? x ? (H2 O)); lapply (H1 O) as K; unfold in K; rewrite <W in K;
   cases K; unfold in H4 H6; rewrite <W in H6 H4; simplify in H4 H6; assumption;
 | intro; cases (H5 ? H4); clear H5 H4;lapply(H1 w) as K; unfold in K; rewrite<W in K;
diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index bad35177b..e3a83a09a 100644
--- 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 45 for @{'upp $s}.
+notation "𝕦 \sub term 90 s" non associative with precedence 45 for @{'upp $s}. 
+notation > "𝕝_term 90 s" non associative with precedence 45 for @{'low $s}.
+notation "𝕝 \sub term 90 s" non associative with precedence 45 for @{'low $s}. 
  
 definition seg_u ≝
- λO:half_ordered_set.λs:segment O.λP: O → CProp.
-   wloss O ? (λl,u.P l) (seg_u_ ? s) (seg_l_ ? 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 l) (seg_l_ ? s) (seg_u_ ? 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_l ? s (λl.l ≤≤ x)) (seg_u ? s (λu.x ≤≤ u)).
+    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,7 +336,7 @@ 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.