From: Andrea Asperti Date: Thu, 25 Mar 2010 14:22:31 +0000 (+0000) Subject: More work X-Git-Tag: make_still_working~2960 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bbd6917343dc01d5c5ae7fd905e17d84abe8f212;p=helm.git More work From: asperti --- diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma index 6d9360362..f1da6c497 100644 --- a/helm/software/matita/nlibrary/arithmetics/R.ma +++ b/helm/software/matita/nlibrary/arithmetics/R.ma @@ -23,9 +23,15 @@ naxiom Qdivides: Q → Q → Q. 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). -naxiom Qtimes_distr: ∀n,m:nat.∀q:Q. (n * q + m * q) = (plus n m) * q. +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. +naxiom Qtimes_distr: ∀q1,q2,q3:Q.(q3 * q1 + q3 * q2) = q3 * (q1 + q2). +naxiom Qdivides_distr: ∀q1,q2,q3:Q.(q1 / q3 + q2 / q3) = (q1 + q2) / q3. +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 Ndivides_mult: ∀n:nat.∀q. (n * q) / n = q. *) @@ -46,21 +52,23 @@ 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 ?. - ncut (locate q q = locate q ((2*q+q)/3)) + ncut (q = (2*q+q)/3) [##2: #H; ncases H; (*NOT WORKING: nrewrite > H;*) napply Q_to_locate - | //; - ##] + |nrewrite < (Qdivides_mult 3 q) in ⊢ (? ? % ?);// + ] 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 - [ @1; napply locate_add; + [ ##1: @1; napplyS (locate_add … r1 …r2); + ##|##4: @2; napplyS (locate_add … r1 …r2); + ##| ncases r2; #l2'; #u2'; #r2'; + . nlet corec apart (l1,u1) (r1: locate l1 u1) (l2,u2) (r2: locate l2 u2) : CProp[0] ≝ match disjoint l1 u1 l2 u2 with