From: Matthias Puech <puech@cs.mcgill.ca>
Date: Thu, 25 Mar 2010 18:20:15 +0000 (+0000)
Subject: patched the definition of locate, advances in locate_add; still issues..
X-Git-Tag: make_still_working~2957
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a66dbbff290dd9b8e003e3694ec2cfbfa96e6d10;p=helm.git

patched the definition of locate, advances in locate_add; still issues..

From: puech <puech@c2b2084f-9a08-0410-b176-e24b037a169a>
---

diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma
index 5499311dc..5cbb571b6 100644
--- a/helm/software/matita/nlibrary/arithmetics/R.ma
+++ b/helm/software/matita/nlibrary/arithmetics/R.ma
@@ -35,7 +35,9 @@ naxiom Qplus_assoc: ∀q1,q2,q3. q1 + q2 + q3 = q1 + (q2 + q3).
 ntheorem Qplus_assoc1: ∀q1,q2,q3. q1 + q2 + q3 = q3 + q2 + q1.
 #a; #b; #c; //; nqed.
 naxiom Qle_refl: ∀q1. q1≤q1.
-naxiom Qle_trans: transitive ? le.
+naxiom Qle_trans: ∀x,y,z. x≤y → y≤z → x≤z.
+naxiom Qle_plus_compat: ∀x,y,z,t. x≤y → z≤t → x+z ≤ y+t.
+
 
 (* naxiom Ndivides_mult: ∀n:nat.∀q. (n * q) / n = q. *)
 
@@ -55,26 +57,24 @@ ncoinductive locate : Q → Q → Prop ≝
 
 ndefinition locate_inv_ind ≝ 
 λx1,x2:Q.λP:Q → Q → Prop.
- λH1: ∀l,l',u',u.l≤l' → u'≤((2 * l + u) / 3) → locate l' u' → P l u. 
- λH2: ∀l,l',u',u. ((l + 2 * u) / 3)≤l' → u'≤ u → locate l' u' → P l u.
+ λH1: ∀l',u'.x1≤l' → u'≤((2 * x1 + x2) / 3) → locate l' u' → P x1 x2. 
+ λH2: ∀l',u'. ((x1 + 2 * x2) / 3)≤l' → u'≤ x2 → locate l' u' → P x1 x2.
  λHterm:locate x1 x2.
   (λHcut:x1=x1 → x2=x2 → P x1 x2. Hcut (refl Q x1) (refl Q x2))
    match Hterm return λy1,y2.λp:locate y1 y2.
-    x1=y1 → x2=y2 → P y1 y2
+    x1=y1 → x2=y2 →P x1 x2
    with
     [ L l l' u' u Hle1 Hle2 r ⇒ ?(*H1 l l' u' u ?*)
     | H l l' u' u Hle1 Hle2 r ⇒ ?(*H2 l l' u' u ?*)].
-      ##[ #a; #b; /2/; napply H2; //; (* Qui non va auto! *)
-      
-      napply (H2 … r …); //;
-     /2/;
-    #h1; #h2; /2/; napply (H2 l l' u' u);
+#a; #b; ##[ napply (H2 … r …) ##| napply (H1 … r …) ##] //.
+nqed.
 
 ndefinition R ≝ ∃l,u:Q. locate l u.
 
-nlet corec Q_to_locate q : locate q q ≝ L q q ?.
+nlet corec Q_to_locate q : locate q q ≝ L q q q q ….
+  //;
  ncut (q = (2*q+q)/3)
-  [##2: #H; ncases H; (*NOT WORKING: nrewrite > H;*) napply Q_to_locate
+  [##2: #H; ncases H; //; (*NOT WORKING: nrewrite > H;*) napply Q_to_locate
   | nrewrite < (Qdivides_mult 3 q) in ⊢ (? ? % ?);//
   ]
 nqed.
@@ -85,17 +85,19 @@ nqed.
 
 nlet corec locate_add (l1,u1:?) (r1: locate l1 u1) (l2,u2:?) (r2: locate l2 u2) :
  locate (l1 + l2) (u1 + u2) ≝ ?.
- ncases r1; ncases r2; #l2; #u2; #r2; #l1; #u1; #r1
-  [ ##1: @1; napplyS (locate_add … r1 …r2);
-  ##|##4: @2; napplyS (locate_add … r1 …r2);
-  ##| ninversion r2; #q; #q0; #H; #K;
-      ndestruct; #U; nrewrite < U in H ⊢ %; #r2';
-      ninversion r1;#q;  #q0; #H; #K;
-      nrewrite < K in H ⊢ %; #H; #J; nrewrite < J in H;
-      #r1'; 
-      ##[ @; nlapply (locate_add …r1'…r2'); #H;
-      
-    .
+ ninversion r1; ninversion r2; #l2'; #u2'; #leq2l; #leq2u; #r2;
+ #l1'; #u1'; #leq1l; #leq1u; #r1
+  [ ##1,4: ##[ @1 ? (l1'+l2') (u1'+u2') | @2 ? (l1'+l2') (u1'+u2') ]
+    ##[ ##1,5: /2/ | napplyS (Qle_plus_compat …leq1u leq2u) |
+        ##4: napplyS (Qle_plus_compat …leq1l leq2l)
+      |##*: /2/ ]
+ ##| ninversion r2; #l2''; #u2''; #leq2l'; #leq2u'; #r2';
+     ninversion r1; #l1''; #u1''; #leq1l'; #leq1u'; #r1';
+      ##[ @1 ? (l1''+l2'') (u1''+u2''); 
+      ##[ napply Qle_plus_compat; /3/;
+        ##| ##3: /2/;
+        ##| napplyS (Qle_plus_compat …leq1u' leq2u');
+      .
  
 nlet corec apart (l1,u1) (r1: locate l1 u1) (l2,u2) (r2: locate l2 u2) : CProp[0] ≝
  match disjoint l1 u1 l2 u2 with