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