Nice examples for automation (that fails).

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

diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma
index 684514fcf135902276902bbc4cf638f5ccd5d7a4..36fec015971743d1a78e5ae7bda2b9e208f7c0a6 100644 (file)
--- a/helm/software/matita/nlibrary/arithmetics/R.ma
+++ b/helm/software/matita/nlibrary/arithmetics/R.ma
@@ -40,20 +40,21 @@ ncoinductive locate : Q → Q → Prop ≝
 ndefinition R ≝ ∃l,u:Q. locate l u.
 
 nlet corec Q_to_locate q : locate q q ≝ L q q ?.
- (*NOT WORKING: nrewrite < (Qmult_one q) in ⊢ (? ? %); *)
  ncut (locate q q = locate q ((2*q+q)/3))
   [##2: #H; ncases H; (*NOT WORKING: nrewrite > H;*) napply Q_to_locate
   | napply eq_f;
     ncut ((2 * q + q) = ((2 * q + 1 * q))); //; #H;    
     ncut (q = ((2 * q + q) / 3)); //;
-    ncut ((2 * q + q) = ((2 * q + 1 * q))); //; #K;
-    ncut (2 * q + 1 * q = 3 * q); /4/ ]
+    ncut (2 * q + 1 * q = 3 * q); //;
+    /4/ (*CSC: basta applicare la distributivita' a meno di riduzione, altro
+               che 4!*) ]
 nqed.
 
 ndefinition Q_to_R : Q → R.
  #q; @ q; @q; //.
 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
@@ -62,4 +63,5 @@ nlet corec locate_add (l1,u1:?) (r1: locate l1 u1) (l2,u2:?) (r2: locate l2 u2)
 nlet corec apart (l1,u1) (r1: locate l1 u1) (l2,u2) (r2: locate l2 u2) : CProp[0] ≝
  match disjoint l1 u1 l2 u2 with
   [ true ⇒ True
-  | false ⇒ 
\ No newline at end of file
+  | false ⇒ 
+*) 
\ No newline at end of file