From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 19 Nov 2008 18:38:27 +0000 (+0000)
Subject: x2sx declared as coercion and used when possible
X-Git-Tag: make_still_working~4533
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7a9277a3775b7150a22b2039548508e85751f85a;p=helm.git

x2sx declared as coercion and used when possible
---

diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
index 251352d1f..f81c5ce46 100644
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -74,15 +74,15 @@ split;
     letin Ai ≝ (⌊n,≪a n, H1 n≫⌋); 
     apply (sandwich {[s]} ≪x, h≫ Xi Yi Ai); [4: assumption;]
     [1: intro j; cases (Hxy j); cases H3; cases H4; split; clear H3 H4; simplify in H5 H7;
-        [apply (l2sl ? s (Xi j) (Ai j) (H5 0));|apply (l2sl ? s (Ai j) (Yi j) (H7 0))]
-    |2: cases (H s Xi ≪?,h≫) (Ux Uy); apply Ux; cases Hx; split; [intro i; apply (l2sl ? s (Xi i) (Xi (S i)) (H3 i));]
-        cases H4; split; [intro i; apply (l2sl ? s (Xi i) ≪x,h≫ (H5 i))] 
-        intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x ? s ? y Hy)]
-        exists [apply w] apply (x2sx ? s (Xi w) y H7); 
-    |3: cases (H s Yi ≪?,h≫) (Ux Uy); apply Uy; cases Hy; split; [intro i; apply (l2sl ? s (Yi (S i))  (Yi i) (H3 i));]
-        cases H4; split; [intro i; apply (l2sl ? s ≪x,h≫ (Yi i) (H5 i))]
-        intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x ? s y ≪x,h≫ Hy)]
-        exists [apply w] apply (x2sx ? s y (Yi w) H7);]]
+        [apply (l2sl_ ? s (Xi j) (Ai j) (H5 0));|apply (l2sl_ ? s (Ai j) (Yi j) (H7 0))]
+    |2: cases (H s Xi ≪?,h≫) (Ux Uy); apply Ux; cases Hx; split; [intro i; apply (l2sl_ ? s (Xi i) (Xi (S i)) (H3 i));]
+        cases H4; split; [intro i; apply (l2sl_ ? s (Xi i) ≪x,h≫ (H5 i))] 
+        intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x_ ? s ? y Hy)]
+        exists [apply w] apply (x2sx_ ? s (Xi w) y H7); 
+    |3: cases (H s Yi ≪?,h≫) (Ux Uy); apply Uy; cases Hy; split; [intro i; apply (l2sl_ ? s (Yi (S i))  (Yi i) (H3 i));]
+        cases H4; split; [intro i; apply (l2sl_ ? s ≪x,h≫ (Yi i) (H5 i))]
+        intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x_ ? s y ≪x,h≫ Hy)]
+        exists [apply w] apply (x2sx_ ? s y (Yi w) H7);]]
 qed.
  
 
@@ -118,7 +118,7 @@ lapply (downarrow_lowerlocated  yi x Hy)as Uy;
 letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
 apply (sandwich {[s]} ≪x, h≫ Xi Yi Ai); [4: assumption;|2:apply H3;|3:apply H5]
 intro j; cases (Hxy j); cases H7; cases H8; split;
-[apply (l2sl ? s (Xi j) (Ai j) (H9 0));|apply (l2sl ? s (Ai j) (Yi j) (H11 0))]
+[apply (l2sl_ ? s (Xi j) (Ai j) (H9 0));|apply (l2sl_ ? s (Ai j) (Yi j) (H11 0))]
 qed. 
 
 
diff --git a/helm/software/matita/contribs/dama/dama/models/increasing_supremum_stabilizes.ma b/helm/software/matita/contribs/dama/dama/models/increasing_supremum_stabilizes.ma
index 9a43d186d..58626ff15 100644
--- a/helm/software/matita/contribs/dama/dama/models/increasing_supremum_stabilizes.ma
+++ b/helm/software/matita/contribs/dama/dama/models/increasing_supremum_stabilizes.ma
@@ -59,7 +59,7 @@ letin m ≝ (hide ? (
         [2: cases Hx; lapply (os_le_to_nat_le ?? H1);
             apply (symmetric_eq nat O x ?).apply (le_n_O_to_eq x ?).apply (Hletin).
         |1: intros; unfold Type_of_ordered_set in sg;
-            lapply (H2 O) as K; lapply (sl2l ?? (a O) ≪x,Hx≫ K) as P;
+            lapply (H2 O) as K; lapply (sl2l_ ?? (a O) ≪x,Hx≫ K) as P;
             simplify in P:(???%); lapply (le_transitive ??? P H1) as W;
             lapply (os_le_to_nat_le ?? W) as R; apply (le_n_O_to_eq (\fst (a O)) R);]
     |2: right; cases Hx; rewrite > (sym_plus x O); split; [apply le_S_S; apply le_O_n];
diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
index 5d6559d1f..5a712f127 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -120,9 +120,19 @@ lemma a2sa :
  (\fst (bs2_of_bss2 (ordered_set_OF_ordered_uniform_space O) s x))
  ≈
  (\snd (bs2_of_bss2 (ordered_set_OF_ordered_uniform_space O) s x)).
-intros 3; cases x (a b); clear x; cases a (x Hx); cases b (y Hy); clear a b;
-simplify; intros 2 (K H); apply K; clear K; whd; whd in H; cases H;
-[left|right] apply x2sx; assumption;
+intros 3; cases x (a b); clear x; simplify in match (\fst ?);
+simplify in match (\snd ?); intros 2 (K H); apply K; clear K;
+cases H; 
+[ left; change in H1:(? ? % ?) with (\fst a); 
+        change in H1:(? ? ? %) with (\fst b); 
+        change in a with (hos_carr (half_segment_ordered_set ? s));
+        change in b with (hos_carr (half_segment_ordered_set ? s));
+        apply rule H1;
+| right; change in H1:(? ? % ?) with (\fst b); 
+        change in H1:(? ? ? %) with (\fst a); 
+        change in a with (hos_carr (half_segment_ordered_set ? s));
+        change in b with (hos_carr (half_segment_ordered_set ? s));
+        apply rule H1;]
 qed.
 
 
@@ -169,31 +179,31 @@ intros (O s); apply mk_ordered_uniform_space;
     (* TODO: x2sx is for ≰, we need one for ≤ *) 
     cases H (u HU); cases HU (Gu HuU); clear HU H;
     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);
+    [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;
-        apply (x2sx (os_l O) s (\fst y) h1 H);
+        apply (x2sx_ (os_l O) s (\fst y) h1 H);
     |5: change with (\fst h ≤ \fst (\fst y)); intro; apply H4;
-        apply (x2sx (os_l O) s h (\fst y) H);
+        apply (x2sx_ (os_l O) s h (\fst y) H);
     |6: change with (\fst (\snd y) ≤ \fst h1); intro; apply H5;
-        apply (x2sx (os_l O) s (\snd y) h1 H);
+        apply (x2sx_ (os_l O) s (\snd y) h1 H);
     |7: change with (\fst (\fst y) ≤ \fst (\snd y)); intro; apply H6;
-        apply (x2sx (os_l O) s (\fst y) (\snd y) H);
+        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);]
-|3: simplify; unfold convex; intros 3; cases s1; intros; (* TODO *)
+|3: simplify; unfold convex; intros 3; cases s1; intros;
     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);
+    [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);
+    |4: intro; apply H3;
+        apply (x2sx_ (os_r O) s (\fst y) h1 H);
+    |5: intro; apply H4;
+        apply (x2sx_ (os_r O) s h (\fst y) H);
+    |6: intro; apply H5;
+        apply (x2sx_ (os_r O) s (\snd y) h1 H);
+    |7: 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);]
 ]  
diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
index 7145b4288..deddf8804 100644
--- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
+++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
@@ -35,11 +35,11 @@ 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);
+[ intro n; intro H; apply (Ha n); apply rule 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);]]
+  [ intro n; intro H; apply (H1 n);apply rule H; 
+  | intros; cases (H2 (\fst y)); [2: apply rule H3;] 
+    exists [apply w] apply (x2sx_ ?? (a w) y H4);]]
 qed.
 
 notation "'segment_preserves_uparrow'" non associative with precedence 90 for @{'segment_preserves_uparrow}.
diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index ca422597d..0de61b292 100644
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -322,7 +322,7 @@ coercion hint_sequence3 nocomposites.
 
 (* Lemma 2.9 - non easily dualizable *)
 
-lemma x2sx:
+lemma x2sx_:
   ∀O:half_ordered_set.
    ∀s:segment O.∀x,y:half_segment_ordered_set ? s.
     \fst x ≰≰ \fst y → x ≰≰ y.
@@ -331,7 +331,7 @@ whd in ⊢ (?→? (% ? ?)? ? ? ? ?); simplify in ⊢ (?→%);
 cases (wloss_prop O) (E E); do 2 rewrite < E; intros; assumption;
 qed.
 
-lemma sx2x:
+lemma sx2x_:
   ∀O:half_ordered_set.
    ∀s:segment O.∀x,y:half_segment_ordered_set ? s.
     x ≰≰ y → \fst x ≰≰ \fst y.
@@ -340,17 +340,21 @@ whd in ⊢ (? (% ? ?) ?? ? ? ? → ?); simplify in ⊢ (% → ?);
 cases (wloss_prop O) (E E); do 2 rewrite < E; intros; assumption;
 qed.
 
-lemma l2sl:
+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;
+intros; intro; apply H; apply sx2x_; apply H1;
 qed.
 
 
-lemma sl2l:
+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;
+intros; intro; apply H; apply x2sx_; apply H1;
 qed.
 
+coercion x2sx_ nocomposites.
+coercion sx2x_ nocomposites.
+coercion l2sl_ nocomposites.
+coercion sl2l_ nocomposites.
 
 lemma h_segment_preserves_supremum:
   ∀O:half_ordered_set.∀s:segment O.
@@ -360,13 +364,13 @@ lemma h_segment_preserves_supremum:
       supremum ? ⌊n,\fst (a n)⌋ (\fst x) → uparrow ? a x.
 intros; split; cases H; clear H; 
 [1: intro n; lapply (H1 n) as K; clear H1 H2;
-    intro; apply K; clear K; apply (sx2x ???? H);
+    intro; apply K; clear K; apply rule H; 
 |2: cases H2; split; clear H2;
     [1: intro n; lapply (H n) as K; intro W; apply K;
-        apply (sx2x ???? W);
+        apply rule W;
     |2: clear H1 H; intros (y0 Hy0); cases (H3 (\fst y0));[exists[apply w]]
-        [1: change in H with (\fst (a w) ≰≰ \fst y0); apply (x2sx ???? H);
-        |2: apply (sx2x ???? Hy0);]]]
+        [1: change in H with (\fst (a w) ≰≰ \fst y0); apply rule H;
+        |2: apply rule Hy0;]]]
 qed.
 
 notation "'segment_preserves_supremum'" non associative with precedence 90 for @{'segment_preserves_supremum}.