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 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.
  36 #a; #b; #c; //; nqed.
  37 naxiom Qle_refl: ∀q1. q1≤q1.
  38 naxiom Qle_trans: ∀x,y,z. x≤y → y≤z → x≤z.
  39 naxiom Qle_plus_compat: ∀x,y,z,t. x≤y → z≤t → x+z ≤ y+t.
  40
  41
  42 (* naxiom Ndivides_mult: ∀n:nat.∀q. (n * q) / n = q. *)
  43
  44 ntheorem lem1: ∀n:nat.∀q:Q. (n * q + q) = (S n) * q.
  45 #n; #q; ncut (plus n 1 = S n);##[//##]
  46 //; nqed.
  47
  48 (*ndefinition aaa ≝ Qtimes_distr.
  49 ndefinition bbb ≝ Qmult_one.
  50 ndefinition ccc ≝ Qdivides_mult.*)
  51
  52 naxiom disjoint: Q → Q → Q → Q → bool.
  53
  54 ncoinductive locate : Q → Q → Prop ≝
  55    L: ∀l,l',u',u. l≤l' → u'≤((2 * l + u) / 3) → locate l' u' → locate l u
  56  | H: ∀l,l',u',u. ((l + 2 * u) / 3)≤l' → u'≤ u → locate l' u' → locate l u.
  57
  58 ndefinition locate_inv_ind ≝
  59 λx1,x2:Q.λP:Q → Q → Prop.
  60  λH1: ∀l',u'.x1≤l' → u'≤((2 * x1 + x2) / 3) → locate l' u' → P x1 x2.
  61  λH2: ∀l',u'. ((x1 + 2 * x2) / 3)≤l' → u'≤ x2 → locate l' u' → P x1 x2.
  62  λHterm:locate x1 x2.
  63   (λHcut:x1=x1 → x2=x2 → P x1 x2. Hcut (refl Q x1) (refl Q x2))
  64    match Hterm return λy1,y2.λp:locate y1 y2.
  65     x1=y1 → x2=y2 →P x1 x2
  66    with
  67     [ L l l' u' u Hle1 Hle2 r ⇒ ?(*H1 l l' u' u ?*)
  68     | H l l' u' u Hle1 Hle2 r ⇒ ?(*H2 l l' u' u ?*)].
  69 #a; #b; ##[ napply (H2 … r …) ##| napply (H1 … r …) ##] //.
  70 nqed.
  71
  72 ndefinition R ≝ ∃l,u:Q. locate l u.
  73
  74 nlet corec Q_to_locate q : locate q q ≝ L q q q q ….
  75   //;
  76  ncut (q = (2*q+q)/3)
  77   [##2: #H; ncases H; //; (*NOT WORKING: nrewrite > H;*) napply Q_to_locate
  78   | nrewrite < (Qdivides_mult 3 q) in ⊢ (? ? % ?);//
  79   ]
  80 nqed.
  81
  82 ndefinition Q_to_R : Q → R.
  83  #q; @ q; @q; //.
  84 nqed.
  85
  86 nlet corec locate_add (l1,u1:?) (r1: locate l1 u1) (l2,u2:?) (r2: locate l2 u2) :
  87  locate (l1 + l2) (u1 + u2) ≝ ?.
  88  ninversion r1; ninversion r2; #l2'; #u2'; #leq2l; #leq2u; #r2;
  89  #l1'; #u1'; #leq1l; #leq1u; #r1
  90   [ ##1,4: ##[ @1 ? (l1'+l2') (u1'+u2') | @2 ? (l1'+l2') (u1'+u2') ]
  91     ##[ ##1,5: /2/ | napplyS (Qle_plus_compat …leq1u leq2u) |
  92         ##4: napplyS (Qle_plus_compat …leq1l leq2l)
  93       |##*: /2/ ]
  94  ##| ninversion r2; #l2''; #u2''; #leq2l'; #leq2u'; #r2';
  95      ninversion r1; #l1''; #u1''; #leq1l'; #leq1u'; #r1';
  96       ##[ @1 ? (l1''+l2'') (u1''+u2'');
  97       ##[ napply Qle_plus_compat; /3/;
  98         ##| ##3: /2/;
  99         ##| napplyS (Qle_plus_compat …leq1u' leq2u');
 100       .
 101
 102 nlet corec apart (l1,u1) (r1: locate l1 u1) (l2,u2) (r2: locate l2 u2) : CProp[0] ≝
 103  match disjoint l1 u1 l2 u2 with
 104   [ true ⇒ True
 105   | false ⇒
 106 *)