1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "arithmetics/nat.ma".
18 naxiom nat_to_Q: nat → Q.
19 ncoercion nat_to_Q : ∀x:nat.Q ≝ nat_to_Q on _x:nat to Q.
20 naxiom Qplus: Q → Q → Q.
21 naxiom Qtimes: Q → Q → Q.
22 naxiom Qdivides: Q → Q → Q.
23 interpretation "Q plus" 'plus x y = (Qplus x y).
24 interpretation "Q times" 'times x y = (Qtimes x y).
25 interpretation "Q divides" 'divide x y = (Qdivides x y).
26 naxiom Qtimes_distr: ∀n,m:nat.∀q:Q. (n * q + m * q) = (plus n m) * q.
27 naxiom Qmult_one: ∀q:Q. 1 * q = q.
28 naxiom Qdivides_mult: ∀q1,q2. (q1 * q2) / q1 = q2.
30 (* naxiom Ndivides_mult: ∀n:nat.∀q. (n * q) / n = q. *)
32 ntheorem lem1: ∀n:nat.∀q:Q. (n * q + q) = (S n) * q.
33 #n; #q; ncut (plus n 1 = S n);##[//##]
36 (*ndefinition aaa ≝ Qtimes_distr.
37 ndefinition bbb ≝ Qmult_one.
38 ndefinition ccc ≝ Qdivides_mult.*)
40 naxiom disjoint: Q → Q → Q → Q → bool.
42 ncoinductive locate : Q → Q → Prop ≝
43 L: ∀l,u. locate l ((2 * l + u) / 3) → locate l u
44 | H: ∀l,u. locate ((l + 2 * u) / 3) u → locate l u.
46 ndefinition R ≝ ∃l,u:Q. locate l u.
48 nlet corec Q_to_locate q : locate q q ≝ L q q ?.
49 ncut (locate q q = locate q ((2*q+q)/3))
50 [##2: #H; ncases H; (*NOT WORKING: nrewrite > H;*) napply Q_to_locate
55 ndefinition Q_to_R : Q → R.
60 nlet corec locate_add (l1,u1:?) (r1: locate l1 u1) (l2,u2:?) (r2: locate l2 u2) :
61 locate (l1 + l2) (u1 + u2) ≝ ?.
62 ncases r1; ncases r2; #l2; #u2; #r2; #l1; #u1; #r1
63 [ @1; napply locate_add;
65 nlet corec apart (l1,u1) (r1: locate l1 u1) (l2,u2) (r2: locate l2 u2) : CProp[0] ≝
66 match disjoint l1 u1 l2 u2 with