From f4d1feaa9cc24ef94f72fe32603a71f8d65acd01 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it> Date: Wed, 24 Mar 2010 14:19:52 +0000 Subject: [PATCH] Real numbers as co-inductive streams of digits (overlapping refining intervals). From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a> --- .../software/matita/nlibrary/arithmetics/R.ma | 65 +++++++++++++++++++ 1 file changed, 65 insertions(+) create mode 100644 helm/software/matita/nlibrary/arithmetics/R.ma 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 -- 2.39.5