From: Claudio Sacerdoti Coen Date: Wed, 24 Mar 2010 14:19:52 +0000 (+0000) Subject: Real numbers as co-inductive streams of digits (overlapping refining intervals). X-Git-Tag: make_still_working~2974 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f4d1feaa9cc24ef94f72fe32603a71f8d65acd01;p=helm.git Real numbers as co-inductive streams of digits (overlapping refining intervals). From: sacerdot --- diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma new file mode 100644 index 000000000..684514fcf --- /dev/null +++ b/helm/software/matita/nlibrary/arithmetics/R.ma @@ -0,0 +1,65 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "arithmetics/nat.ma". + +naxiom Q: Type[0]. +naxiom nat_to_Q: nat → Q. +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. +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 Qmult_one: ∀q:Q. 1 * q = q. +naxiom Qdivides_mult: ∀q1,q2. (q1 * q2) / q1 = q2. + +(*ndefinition aaa ≝ Qtimes_distr. +ndefinition bbb ≝ Qmult_one. +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. + +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/ ] +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; + +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