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 naxiom Qle : Q → Q → Prop.
24 interpretation "Q plus" 'plus x y = (Qplus x y).
25 interpretation "Q times" 'times x y = (Qtimes x y).
26 interpretation "Q divides" 'divide x y = (Qdivides x y).
27 interpretation "Q le" 'leq x y = (Qle x y).
28 naxiom Qtimes_plus: ∀n,m:nat.∀q:Q. (n * q + m * q) = (plus n m) * q.
29 naxiom Qmult_one: ∀q:Q. 1 * q = q.
30 naxiom Qdivides_mult: ∀q1,q2. (q1 * q2) / q1 = q2.
31 naxiom Qtimes_distr: ∀q1,q2,q3:Q.(q3 * q1 + q3 * q2) = q3 * (q1 + q2).
32 naxiom Qdivides_distr: ∀q1,q2,q3:Q.(q1 / q3 + q2 / q3) = (q1 + q2) / q3.
33 naxiom Qplus_comm: ∀q1,q2. q1 + q2 = q2 + q1.
34 naxiom Qplus_assoc: ∀q1,q2,q3. q1 + q2 + q3 = q1 + (q2 + q3).
35 ntheorem Qplus_assoc1: ∀q1,q2,q3. q1 + q2 + q3 = q3 + q2 + q1.
37 naxiom Qle_refl: ∀q1. q1≤q1.
38 naxiom Qle_trans: transitive ? le.
40 (* naxiom Ndivides_mult: ∀n:nat.∀q. (n * q) / n = q. *)
42 ntheorem lem1: ∀n:nat.∀q:Q. (n * q + q) = (S n) * q.
43 #n; #q; ncut (plus n 1 = S n);##[//##]
46 (*ndefinition aaa ≝ Qtimes_distr.
47 ndefinition bbb ≝ Qmult_one.
48 ndefinition ccc ≝ Qdivides_mult.*)
50 naxiom disjoint: Q → Q → Q → Q → bool.
52 ncoinductive locate : Q → Q → Prop ≝
53 L: ∀l,l',u',u. l≤l' → u'≤((2 * l + u) / 3) → locate l' u' → locate l u
54 | H: ∀l,l',u',u. ((l + 2 * u) / 3)≤l' → u'≤ u → locate l' u' → locate l u.
56 ndefinition locate_inv_ind ≝
57 λx1,x2:Q.λP:Q → Q → Prop.
58 λH1: ∀l,l',u',u.l≤l' → u'≤((2 * l + u) / 3) → locate l' u' → P l u.
59 λH2: ∀l,l',u',u. ((l + 2 * u) / 3)≤l' → u'≤ u → locate l' u' → P l u.
61 (λHcut:x1=x1 → x2=x2 → P x1 x2. Hcut (refl Q x1) (refl Q x2))
62 match Hterm return λy1,y2.λp:locate y1 y2.
63 x1=y1 → x2=y2 → P y1 y2
65 [ L l l' u' u Hle1 Hle2 r ⇒ ?(*H1 l l' u' u ?*)
66 | H l l' u' u Hle1 Hle2 r ⇒ ?(*H2 l l' u' u ?*)].
67 ##[ #a; #b; /2/; napply H2; //; (* Qui non va auto! *)
69 napply (H2 … r …); //;
71 #h1; #h2; /2/; napply (H2 l l' u' u);
73 ndefinition R ≝ ∃l,u:Q. locate l u.
75 nlet corec Q_to_locate q : locate q q ≝ L q q ?.
77 [##2: #H; ncases H; (*NOT WORKING: nrewrite > H;*) napply Q_to_locate
78 | nrewrite < (Qdivides_mult 3 q) in ⊢ (? ? % ?);//
82 ndefinition Q_to_R : Q → R.
86 nlet corec locate_add (l1,u1:?) (r1: locate l1 u1) (l2,u2:?) (r2: locate l2 u2) :
87 locate (l1 + l2) (u1 + u2) ≝ ?.
88 ncases r1; ncases r2; #l2; #u2; #r2; #l1; #u1; #r1
89 [ ##1: @1; napplyS (locate_add … r1 …r2);
90 ##|##4: @2; napplyS (locate_add … r1 …r2);
91 ##| ninversion r2; #q; #q0; #H; #K;
92 ndestruct; #U; nrewrite < U in H ⊢ %; #r2';
93 ninversion r1;#q; #q0; #H; #K;
94 nrewrite < K in H ⊢ %; #H; #J; nrewrite < J in H;
96 ##[ @; nlapply (locate_add …r1'…r2'); #H;
100 nlet corec apart (l1,u1) (r1: locate l1 u1) (l2,u2) (r2: locate l2 u2) : CProp[0] ≝
101 match disjoint l1 u1 l2 u2 with