removed <_,_> notation second interpretation for dependent pair, since it used

to have an exponential slowdown on refinement of huge terms....

diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
index b8b33f8e6425bdf8c5aec7f525cdd5ee0f53b906..14e21700011917fd53902f5e19eae5cf548d5b72 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
+++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
@@ -44,7 +44,12 @@ inductive exT (A:Type) (P:A→CProp) : CProp ≝
   ex_introT: ∀w:A. P w → exT A P.
 
 interpretation "CProp exists" 'exists \eta.x = (exT _ x).
-interpretation "dependent pair" 'pair a b = (ex_introT _ _ a b).
+
+notation "\ll term 19 a, break term 19 b \gg" 
+with precedence 90 for @{'dependent_pair $a $b}.
+interpretation "dependent pair" 'dependent_pair a b = 
+  (ex_introT _ _ a b).
+
 
 definition pi1exT ≝ λA,P.λx:exT A P.match x with [ex_introT x _ ⇒ x].
 definition pi2exT ≝ 

diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
index c5a256a0061a1a22105e7b3a1e0d526cefaf4e3a..e1fbd0a5a75cac9f840d207833e3319214680224 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -47,7 +47,7 @@ theorem lebesgue_oc:
      ∀x:C.a order_converges x → 
       x ∈ [l,u] ∧ 
       ∀h:x ∈ [l,u].
-       uniform_converge {[l,u]} (â\8c\8an,â\8c©a n,H nâ\8cªâ\8c\8b) â\8c©x,hâ\8cª.
+       uniform_converge {[l,u]} (â\8c\8an,â\89ªa n,H nâ\89«â\8c\8b) â\89ªx,hâ\89«.
 intros;
 generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2);
 generalize in match (order_converges_smaller_upsegment ???? H1 ? H2);
@@ -65,16 +65,16 @@ split;
     [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption
     |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption]
 |2: intros 3 (h);
-    letin Xi â\89\9d (â\8c\8an,â\8c©xi n,Hxi nâ\8cª⌋);
-    letin Yi â\89\9d (â\8c\8an,â\8c©yi n,Hyi nâ\8cª⌋);
-    letin Ai â\89\9d (â\8c\8an,â\8c©a n,H1 nâ\8cª⌋);
-    apply (sandwich {[l,u]} â\8c©?,hâ\8cª Xi Yi Ai); try assumption;
+    letin Xi â\89\9d (â\8c\8an,â\89ªxi n,Hxi nâ\89«⌋);
+    letin Yi â\89\9d (â\8c\8an,â\89ªyi n,Hyi nâ\89«⌋);
+    letin Ai â\89\9d (â\8c\8an,â\89ªa n,H1 nâ\89«⌋);
+    apply (sandwich {[l,u]} â\89ª?,hâ\89« Xi Yi Ai); try assumption;
     [1: intro j; cases (Hxy j); cases H3; cases H4; split;
         [apply (H5 0);|apply (H7 0)]
-    |2: cases (H l u Xi â\8c©?,hâ\8cª) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
+    |2: cases (H l u Xi â\89ª?,hâ\89«) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
         cases H4; split; [apply H5] intros (y Hy);cases (H6 (\fst y));[2:apply Hy];
         exists [apply w] apply H7; 
-    |3: cases (H l u Yi â\8c©?,hâ\8cª) (Ux Uy); apply Uy; cases Hy; split; [apply H3;]
+    |3: cases (H l u Yi â\89ª?,hâ\89«) (Ux Uy); apply Uy; cases Hy; split; [apply H3;]
         cases H4; split; [apply H5] intros (y Hy);cases (H6 (\fst y));[2:apply Hy];
         exists [apply w] apply H7;]]
 qed.
@@ -88,7 +88,7 @@ theorem lebesgue_se:
      ∀x:C.a order_converges x → 
       x ∈ [l,u] ∧ 
       ∀h:x ∈ [l,u].
-       uniform_converge {[l,u]} (â\8c\8an,â\8c©a n,H nâ\8cªâ\8c\8b) â\8c©x,hâ\8cª.
+       uniform_converge {[l,u]} (â\8c\8an,â\89ªa n,H nâ\89«â\8c\8b) â\89ªx,hâ\89«.
 intros (C S);
 generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2);
 generalize in match (order_converges_smaller_upsegment ???? H1 ? H2);
@@ -108,10 +108,10 @@ split;
 |2: intros 3;
     lapply (uparrow_upperlocated ? xi x Hx)as Ux;
     lapply (downarrow_lowerlocated ? yi x Hy)as Uy;
-    letin Xi â\89\9d (â\8c\8an,â\8c©xi n,Hxi nâ\8cª⌋);
-    letin Yi â\89\9d (â\8c\8an,â\8c©yi n,Hyi nâ\8cª⌋);
-    letin Ai â\89\9d (â\8c\8an,â\8c©a n,H1 nâ\8cª⌋);
-    apply (sandwich {[l,u]} â\8c©x,hâ\8cª Xi Yi Ai); try assumption;
+    letin Xi â\89\9d (â\8c\8an,â\89ªxi n,Hxi nâ\89«⌋);
+    letin Yi â\89\9d (â\8c\8an,â\89ªyi n,Hyi nâ\89«⌋);
+    letin Ai â\89\9d (â\8c\8an,â\89ªa n,H1 nâ\89«⌋);
+    apply (sandwich {[l,u]} â\89ªx,hâ\89« Xi Yi Ai); try assumption;
     [1: intro j; cases (Hxy j); cases H3; cases H4; split;
         [apply (H5 0);|apply (H7 0)]
     |2: cases (restrict_uniform_convergence_uparrow ? S ?? (H l u) Xi x Hx);

diff --git a/helm/software/matita/contribs/dama/dama/models/q_function.ma b/helm/software/matita/contribs/dama/dama/models/q_function.ma
index 8f0f472a9a48b5658595f26da4a598234afa09b4..48d3012ec66974d8c8993e5db02bd72e3b488229 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_function.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma
@@ -16,6 +16,7 @@ include "Q/q/q.ma".
 include "list/list.ma".
 include "cprop_connectives.ma". 
 
+
 notation "\rationals" non associative with precedence 99 for @{'q}.
 interpretation "Q" 'q = Q. 
 
@@ -58,7 +59,7 @@ interpretation "Q x Q" 'q2 = (Prod Q Q).
 
 let rec make_list (A:Type) (def:nat→A) (n:nat) on n ≝
   match n with
-  [ O ⇒ []
+  [ O ⇒ nil ?
   | S m ⇒ def m :: make_list A def m].
 
 notation "'mk_list'" with precedence 90 for @{'mk_list}.
@@ -104,8 +105,8 @@ letin spec ≝ (λl1,l2:list (ℚ × ℚ).λm:nat.λz:(list (ℚ × ℚ)) × (li
 letin aux ≝ ( 
 let rec aux (l1,l2:list (ℚ × ℚ)) (n:nat) on n : (list (ℚ × ℚ)) × (list (ℚ × ℚ)) ≝
 match n with
-[ O ⇒ 〈[],[]〉
-| S m ⇒
+[ O ⇒ 〈 nil ? , nil ? 〉
+| S m ⇒ 
   match l1 with
   [ nil ⇒ 〈cb0h l2, l2〉
   | cons he1 tl1 ⇒
@@ -129,11 +130,5 @@ match n with
              let rc ≝ aux (〈rest,height1〉 :: tl1) tl2 m in
              〈〈base2,height1〉 :: \fst rc,〈base2,height2〉 :: \snd rc〉
 ]]]]
-in aux); : ∀l1,l2,m.∃z.spec l1 l2 m z); 
-  
-cases (q_cmp s1 s2);
-[1: apply (mk_q_f s1);
-|2: apply (mk_q_f s1); cases l2;
-    [1: letin l2' ≝ (
-[1: (* offset: the smallest one *)
-    cases 
+in aux : ∀l1,l2,m.∃z.spec l1 l2 m z); 
+qed.
\ No newline at end of file

diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
index 7d80f70812ec0e69a7f4257f793616ad8802e825..bf0260a510ac775fede207a1760f26e371e36daf 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -100,13 +100,11 @@ notation < "x \sub \neq" with precedence 91 for @{'bsss $x}.
 interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x).
 
 alias symbol "square" (instance 7) = "ordered set square".
-alias symbol "pair" (instance 4) = "dependent pair".
-alias symbol "pair" (instance 2) = "dependent pair".
 lemma ss_of_bs: 
  ∀O:ordered_set.∀u,v:O.
   ∀b:O square.\fst b ∈ [u,v] → \snd b ∈ [u,v] → {[u,v]} square ≝ 
  λO:ordered_set.λu,v:O.
-  λb:(O:bishop_set) square.λH1,H2.â\8c©â\8c©\fst b,H1â\8cª,â\8c©\snd b,H2â\8cª〉.
+  λb:(O:bishop_set) square.λH1,H2.â\8c©â\89ª\fst b,H1â\89«,â\89ª\snd b,H2â\89«〉.
 
 notation < "x \sub \nleq" with precedence 91 for @{'ssbs $x}.
 interpretation "ss_of_bs" 'ssbs x = (ss_of_bs _ _ _ x _ _).

diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
index d04ec1acca886c457ae4370f3a5fcdc722120a9d..f7250f9e2e167a7a428b1d604c14638142580772 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
+++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
@@ -34,7 +34,7 @@ qed.
 
 lemma segment_preserves_uparrow:
   ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.∀x,h. 
-    â\8c\8an,\fst (a n)â\8c\8b â\86\91 x â\86\92 a â\86\91 â\8c©x,hâ\8cª.
+    â\8c\8an,\fst (a n)â\8c\8b â\86\91 x â\86\92 a â\86\91 â\89ªx,hâ\89«.
 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;
@@ -42,7 +42,7 @@ qed.
 
 lemma segment_preserves_downarrow:
   ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.∀x,h. 
-    â\8c\8an,\fst (a n)â\8c\8b â\86\93 x â\86\92 a â\86\93 â\8c©x,hâ\8cª.
+    â\8c\8an,\fst (a n)â\8c\8b â\86\93 x â\86\92 a â\86\93 â\89ªx,hâ\89«.
 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;
@@ -66,7 +66,7 @@ lemma restrict_uniform_convergence_uparrow:
   ∀C:ordered_uniform_space.property_sigma C →
     ∀l,u:C.exhaustive {[l,u]} →
      ∀a:sequence {[l,u]}.∀x:C. ⌊n,\fst (a n)⌋ ↑ x → 
-      xâ\88\88[l,u] â\88§ â\88\80h:x â\88\88 [l,u].a uniform_converges â\8c©x,hâ\8cª.
+      xâ\88\88[l,u] â\88§ â\88\80h:x â\88\88 [l,u].a uniform_converges â\89ªx,hâ\89«.
 intros; cases H2 (Ha Hx); clear H2; cases Hx; split;
 [1: split;
     [1: apply (supremum_is_upper_bound C ?? Hx u); 
@@ -74,9 +74,9 @@ intros; cases H2 (Ha Hx); clear H2; cases Hx; split;
     |2: apply (le_transitive ? ??? ? (H2 O));
         apply (segment_lowerbound ?l u);]
 |2: intros;
-    lapply (uparrow_upperlocated ? a â\8c©x,hâ\8cª) as Ha1;
+    lapply (uparrow_upperlocated ? a â\89ªx,hâ\89«) as Ha1;
       [2: apply segment_preserves_uparrow;split; assumption;] 
-    lapply (segment_preserves_supremum ? l u a â\8c©?,hâ\8cª) as Ha2; 
+    lapply (segment_preserves_supremum ? l u a â\89ª?,hâ\89«) as Ha2; 
       [2:split; assumption]; cases Ha2; clear Ha2;
     cases (H1 a a); lapply (H6 H4 Ha1) as HaC;
     lapply (segment_cauchy ? l u ? HaC) as Ha;
@@ -88,7 +88,7 @@ lemma restrict_uniform_convergence_downarrow:
   ∀C:ordered_uniform_space.property_sigma C →
     ∀l,u:C.exhaustive {[l,u]} →
      ∀a:sequence {[l,u]}.∀x:C. ⌊n,\fst (a n)⌋ ↓ x → 
-      xâ\88\88[l,u] â\88§ â\88\80h:x â\88\88 [l,u].a uniform_converges â\8c©x,hâ\8cª.
+      xâ\88\88[l,u] â\88§ â\88\80h:x â\88\88 [l,u].a uniform_converges â\89ªx,hâ\89«.
 intros; cases H2 (Ha Hx); clear H2; cases Hx; split;
 [1: split;
     [2: apply (infimum_is_lower_bound C ?? Hx l); 
@@ -96,9 +96,9 @@ intros; cases H2 (Ha Hx); clear H2; cases Hx; split;
     |1: apply (le_transitive ???? (H2 O));
         apply (segment_upperbound ? l u);]
 |2: intros;
-    lapply (downarrow_lowerlocated ? a â\8c©x,hâ\8cª) as Ha1;
+    lapply (downarrow_lowerlocated ? a â\89ªx,hâ\89«) as Ha1;
       [2: apply segment_preserves_downarrow;split; assumption;] 
-    lapply (segment_preserves_infimum ?l u a â\8c©?,hâ\8cª) as Ha2; 
+    lapply (segment_preserves_infimum ?l u a â\89ª?,hâ\89«) as Ha2; 
       [2:split; assumption]; cases Ha2; clear Ha2;
     cases (H1 a a); lapply (H7 H4 Ha1) as HaC;
     lapply (segment_cauchy ? l u ? HaC) as Ha;