]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/Q/q.ma
51b66cacc8756f9b773f52bb95ec1edb621471a6
[helm.git] / 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 *)