]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/library/Q/q.ma
ground: some arithmetical properties added
[helm.git] / matita / 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 *)