Automation problem

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 f1da6c4979b1a14983719883ecba43a4cda2b720..5499311dc1a0a9b0c5e45f0de4cb5b718445a15c 100644 (file)
--- a/helm/software/matita/nlibrary/arithmetics/R.ma
+++ b/helm/software/matita/nlibrary/arithmetics/R.ma
@@ -20,9 +20,11 @@ ncoercion nat_to_Q : ∀x:nat.Q ≝ nat_to_Q on _x:nat to Q.
 naxiom Qplus: Q → Q → Q.
 naxiom Qtimes: Q → Q → Q.
 naxiom Qdivides: Q → Q → Q.
+naxiom Qle : Q → Q → Prop.
 interpretation "Q plus" 'plus x y = (Qplus x y).
 interpretation "Q times" 'times x y = (Qtimes x y).
 interpretation "Q divides" 'divide x y = (Qdivides x y).
+interpretation "Q le" 'leq x y = (Qle x y).
 naxiom Qtimes_plus: ∀n,m:nat.∀q:Q. (n * q + m * q) = (plus n m) * q.
 naxiom Qmult_one: ∀q:Q. 1 * q = q.
 naxiom Qdivides_mult: ∀q1,q2. (q1 * q2) / q1 = q2.
@@ -32,6 +34,8 @@ naxiom Qplus_comm: ∀q1,q2. q1 + q2 = q2 + q1.
 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 Ndivides_mult: ∀n:nat.∀q. (n * q) / n = q. *)
 
@@ -46,15 +50,32 @@ ndefinition ccc ≝ Qdivides_mult.*)
 naxiom disjoint: Q → Q → Q → Q → bool.
 
 ncoinductive locate : Q → Q → Prop ≝
-   L: ∀l,u. locate l ((2 * l + u) / 3) → locate l u
- | H: ∀l,u. locate ((l + 2 * u) / 3) u → locate l u.
+   L: ∀l,l',u',u. l≤l' → u'≤((2 * l + u) / 3) → locate l' u' → locate l u
+ | H: ∀l,l',u',u. ((l + 2 * u) / 3)≤l' → u'≤ u → locate l' u' → locate l u.
+
+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.
+ λ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
+   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);
 
 ndefinition R ≝ ∃l,u:Q. locate l u.
 
 nlet corec Q_to_locate q : locate q q ≝ L q q ?.
  ncut (q = (2*q+q)/3)
   [##2: #H; ncases H; (*NOT WORKING: nrewrite > H;*) napply Q_to_locate
-  |nrewrite < (Qdivides_mult 3 q) in ⊢ (? ? % ?);//
+  | nrewrite < (Qdivides_mult 3 q) in ⊢ (? ? % ?);//
   ]
 nqed.
 
@@ -67,7 +88,13 @@ nlet corec locate_add (l1,u1:?) (r1: locate l1 u1) (l2,u2:?) (r2: locate l2 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);
-  ##| ncases r2; #l2'; #u2'; #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;
+      
     .
  
 nlet corec apart (l1,u1) (r1: locate l1 u1) (l2,u2) (r2: locate l2 u2) : CProp[0] ≝