From 43d182ba201048ea8f2fc40e56338b67acf05a58 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 24 Mar 2010 17:56:32 +0000 Subject: [PATCH] Nice examples for automation (that fails). From: sacerdot --- helm/software/matita/nlibrary/arithmetics/R.ma | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma index 684514fcf..36fec0159 100644 --- 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 -- 2.39.2