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
  19 let rec enumerator_integral_fraction l ≝
  20  match l with
  21   [ pp n ⇒ Some ? l
  22   | nn _ ⇒ None ?
  23   | cons z r ⇒
  24      match enumerator_integral_fraction r with
  25       [ None ⇒
  26          match z with
  27           [ pos n ⇒ Some ? (pp n)
  28           | _ ⇒ None ?
  29           ]
  30       | Some r' ⇒
  31          Some ?
  32           match z with
  33            [ neg _ ⇒ cons OZ r'
  34            | _ ⇒ cons z r'
  35            ]
  36        ]
  37   ].
  38
  39 let rec denominator_integral_fraction l ≝
  40  match l with
  41   [ pp _ ⇒ None ?
  42   | nn n ⇒ Some ? (pp n)
  43   | cons z r ⇒
  44      match denominator_integral_fraction r with
  45       [ None ⇒
  46          match z with
  47           [ neg n ⇒ Some ? (pp n)
  48           | _ ⇒ None ?
  49           ]
  50       | Some r' ⇒
  51          Some ?
  52           match z with
  53            [ pos _ ⇒ cons OZ r'
  54            | neg m ⇒ cons (pos m) r'
  55            | OZ ⇒ cons OZ r'
  56            ]
  57        ]
  58   ].
  59
  60 definition enumerator_of_fraction ≝
  61  λq.
  62   match q with
  63    [ one ⇒ S O
  64    | frac f ⇒
  65       match enumerator_integral_fraction f with
  66        [ None ⇒ S O
  67        | Some l ⇒ defactorize_aux (nat_fact_of_integral_fraction l) O
  68        ]
  69    ].
  70
  71 definition denominator_of_fraction ≝
  72  λq.
  73   match q with
  74    [ one ⇒ S O
  75    | frac f ⇒
  76       match denominator_integral_fraction f with
  77        [ None ⇒ S O
  78        | Some l ⇒ defactorize_aux (nat_fact_of_integral_fraction l) O
  79        ]
  80    ].
  81
  82 definition enumerator ≝
  83  λq.
  84   match q with
  85    [ OQ ⇒ OZ
  86    | Qpos r ⇒ (enumerator_of_fraction r : Z)
  87    | Qneg r ⇒ neg(pred (enumerator_of_fraction r))
  88    ].
  89
  90 definition denominator ≝
  91  λq.
  92   match q with
  93    [ OQ ⇒ S O
  94    | Qpos r ⇒ denominator_of_fraction r
  95    | Qneg r ⇒ denominator_of_fraction r
  96    ].