From 59f65aaf6f8d23748e1294ecabffffaa903ae657 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 24 Jun 2008 18:48:31 +0000
Subject: [PATCH] removed <_,_> notation second interpretation for dependent
 pair, since it used to have an exponential slowdown on refinement of huge
 terms....

---
 .../contribs/dama/dama/cprop_connectives.ma   |  7 +++++-
 .../matita/contribs/dama/dama/lebesgue.ma     | 24 +++++++++----------
 .../contribs/dama/dama/models/q_function.ma   | 17 +++++--------
 .../contribs/dama/dama/ordered_uniform.ma     |  4 +---
 .../dama/dama/property_exhaustivity.ma        | 16 ++++++-------
 5 files changed, 33 insertions(+), 35 deletions(-)

diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
index b8b33f8e6..14e217000 100644
--- 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 c5a256a00..e1fbd0a5a 100644
--- 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]} (⌊n,〈a n,H n〉⌋) 〈x,h〉.
+       uniform_converge {[l,u]} (⌊n,≪a n,H n≫⌋) ≪x,h≫.
 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 ≝ (⌊n,〈xi n,Hxi n〉⌋);
-    letin Yi ≝ (⌊n,〈yi n,Hyi n〉⌋);
-    letin Ai ≝ (⌊n,〈a n,H1 n〉⌋);
-    apply (sandwich {[l,u]} 〈?,h〉 Xi Yi Ai); try assumption;
+    letin Xi ≝ (⌊n,≪xi n,Hxi n≫⌋);
+    letin Yi ≝ (⌊n,≪yi n,Hyi n≫⌋);
+    letin Ai ≝ (⌊n,≪a n,H1 n≫⌋);
+    apply (sandwich {[l,u]} ≪?,h≫ 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 〈?,h〉) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
+    |2: cases (H l u Xi ≪?,h≫) (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 〈?,h〉) (Ux Uy); apply Uy; cases Hy; split; [apply H3;]
+    |3: cases (H l u Yi ≪?,h≫) (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]} (⌊n,〈a n,H n〉⌋) 〈x,h〉.
+       uniform_converge {[l,u]} (⌊n,≪a n,H n≫⌋) ≪x,h≫.
 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 ≝ (⌊n,〈xi n,Hxi n〉⌋);
-    letin Yi ≝ (⌊n,〈yi n,Hyi n〉⌋);
-    letin Ai ≝ (⌊n,〈a n,H1 n〉⌋);
-    apply (sandwich {[l,u]} 〈x,h〉 Xi Yi Ai); try assumption;
+    letin Xi ≝ (⌊n,≪xi n,Hxi n≫⌋);
+    letin Yi ≝ (⌊n,≪yi n,Hyi n≫⌋);
+    letin Ai ≝ (⌊n,≪a n,H1 n≫⌋);
+    apply (sandwich {[l,u]} ≪x,h≫ 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 8f0f472a9..48d3012ec 100644
--- 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 7d80f7081..bf0260a51 100644
--- 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.〈〈\fst b,H1〉,〈\snd b,H2〉〉.
+  λb:(O:bishop_set) square.λH1,H2.〈≪\fst b,H1≫,≪\snd b,H2≫〉.
 
 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 d04ec1acc..f7250f9e2 100644
--- 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. 
-    ⌊n,\fst (a n)⌋ ↑ x → a ↑ 〈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;
@@ -42,7 +42,7 @@ qed.
 
 lemma segment_preserves_downarrow:
   ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.∀x,h. 
-    ⌊n,\fst (a n)⌋ ↓ x → a ↓ 〈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;
@@ -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∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges 〈x,h〉.
+      x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges ≪x,h≫.
 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 〈x,h〉) as Ha1;
+    lapply (uparrow_upperlocated ? a ≪x,h≫) as Ha1;
       [2: apply segment_preserves_uparrow;split; assumption;] 
-    lapply (segment_preserves_supremum ? l u a 〈?,h〉) as Ha2; 
+    lapply (segment_preserves_supremum ? l u a ≪?,h≫) 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∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges 〈x,h〉.
+      x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges ≪x,h≫.
 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 〈x,h〉) as Ha1;
+    lapply (downarrow_lowerlocated ? a ≪x,h≫) as Ha1;
       [2: apply segment_preserves_downarrow;split; assumption;] 
-    lapply (segment_preserves_infimum ?l u a 〈?,h〉) as Ha2; 
+    lapply (segment_preserves_infimum ?l u a ≪?,h≫) 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;
-- 
2.39.2