helm/software/matita/nlibrary/arithmetics/R.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "arithmetics/nat.ma".
  16
  17 naxiom Q: Type[0].
  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.
  29
  30 (*ndefinition aaa ≝ Qtimes_distr.
  31 ndefinition bbb ≝ Qmult_one.
  32 ndefinition ccc ≝ Qdivides_mult.*)
  33
  34 naxiom disjoint: Q → Q → Q → Q → bool.
  35
  36 ncoinductive locate : Q → Q → Prop ≝
  37    L: ∀l,u. locate l ((2 * l + u) / 3) → locate l u
  38  | H: ∀l,u. locate ((l + 2 * u) / 3) u → locate l u.
  39
  40 ndefinition R ≝ ∃l,u:Q. locate l u.
  41
  42 nlet corec Q_to_locate q : locate q q ≝ L q q ?.
  43  (*NOT WORKING: nrewrite < (Qmult_one q) in ⊢ (? ? %); *)
  44  ncut (locate q q = locate q ((2*q+q)/3))
  45   [##2: #H; ncases H; (*NOT WORKING: nrewrite > H;*) napply Q_to_locate
  46   | napply eq_f;
  47     ncut ((2 * q + q) = ((2 * q + 1 * q))); //; #H;
  48     ncut (q = ((2 * q + q) / 3)); //;
  49     ncut ((2 * q + q) = ((2 * q + 1 * q))); //; #K;
  50     ncut (2 * q + 1 * q = 3 * q); /4/ ]
  51 nqed.
  52
  53 ndefinition Q_to_R : Q → R.
  54  #q; @ q; @q; //.
  55 nqed.
  56
  57 nlet corec locate_add (l1,u1:?) (r1: locate l1 u1) (l2,u2:?) (r2: locate l2 u2) :
  58  locate (l1 + l2) (u1 + u2) ≝ ?.
  59  ncases r1; ncases r2; #l2; #u2; #r2; #l1; #u1; #r1
  60   [ @1; napply locate_add;
  61
  62 nlet corec apart (l1,u1) (r1: locate l1 u1) (l2,u2) (r2: locate l2 u2) : CProp[0] ≝
  63  match disjoint l1 u1 l2 u2 with
  64   [ true ⇒ True
  65   | false ⇒