Real numbers as co-inductive streams of digits (overlapping refining intervals).

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
new file mode 100644 (file)
index 0000000..684514f
--- /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