helm/software/matita/library/Q/q.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "Z/compare.ma".
  16 include "Z/plus.ma".
  17 include "nat/factorization.ma".
  18 include "Q/fraction/fraction.ma".
  19
  20 let rec enumerator_integral_fraction l ≝
  21  match l with
  22   [ pp n ⇒ Some ? l
  23   | nn _ ⇒ None ?
  24   | cons z r ⇒
  25      match enumerator_integral_fraction r with
  26       [ None ⇒
  27          match z with
  28           [ pos n ⇒ Some ? (pp n)
  29           | _ ⇒ None ?
  30           ]
  31       | Some r' ⇒
  32          Some ?
  33           match z with
  34            [ neg _ ⇒ cons OZ r'
  35            | _ ⇒ cons z r'
  36            ]
  37        ]
  38   ].
  39
  40 let rec denominator_integral_fraction l ≝
  41  match l with
  42   [ pp _ ⇒ None ?
  43   | nn n ⇒ Some ? (pp n)
  44   | cons z r ⇒
  45      match denominator_integral_fraction r with
  46       [ None ⇒
  47          match z with
  48           [ neg n ⇒ Some ? (pp n)
  49           | _ ⇒ None ?
  50           ]
  51       | Some r' ⇒
  52          Some ?
  53           match z with
  54            [ pos _ ⇒ cons OZ r'
  55            | neg m ⇒ cons (pos m) r'
  56            | OZ ⇒ cons OZ r'
  57            ]
  58        ]
  59   ].
  60
  61 (*
  62 definition enumerator_of_fraction ≝
  63  λq.
  64   match q with
  65    [ one ⇒ S O
  66    | frac f ⇒
  67       match enumerator_integral_fraction f with
  68        [ None ⇒ S O
  69        | Some l ⇒ defactorize_aux (nat_fact_of_integral_fraction l) O
  70        ]
  71    ].
  72
  73 definition denominator_of_fraction ≝
  74  λq.
  75   match q with
  76    [ one ⇒ S O
  77    | frac f ⇒
  78       match denominator_integral_fraction f with
  79        [ None ⇒ S O
  80        | Some l ⇒ defactorize_aux (nat_fact_of_integral_fraction l) O
  81        ]
  82    ].
  83
  84 definition enumerator ≝
  85  λq.
  86   match q with
  87    [ OQ ⇒ OZ
  88    | Qpos r ⇒ (enumerator_of_fraction r : Z)
  89    | Qneg r ⇒ neg(pred (enumerator_of_fraction r))
  90    ].
  91
  92 definition denominator ≝
  93  λq.
  94   match q with
  95    [ OQ ⇒ S O
  96    | Qpos r ⇒ denominator_of_fraction r
  97    | Qneg r ⇒ denominator_of_fraction r
  98    ].
  99 *)