]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/Q/Qaxioms.ma
notation factored, coercion commant taking terms and not only URI
[helm.git] / helm / software / matita / library / Q / Qaxioms.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/times.ma".
17 include "nat/iteration2.ma".
18
19 (* a fraction is a list of Z-coefficients for primes, in natural
20 order. The last coefficient must eventually be different from 0 *)
21
22 axiom Q:Type.
23 axiom Qopp:Q \to Q.
24 axiom Qinv:Q \to Q.
25 axiom Qplus:Q \to Q \to Q.
26 axiom Qtimes:Q \to Q \to Q.
27 axiom QO:Q.
28 axiom Q1:Q.
29 axiom Qlt:Q \to Q \to Prop.
30
31 axiom num: Q \to Z.
32 axiom denom: Q \to nat.
33 axiom frac: Z \to nat \to Q.
34
35 (* plus *)
36 axiom symmetric_Qplus: symmetric ? Qplus.
37 axiom associative_Qplus: associative ? Qplus.
38 axiom Qplus_QO: \forall q:Q.Qplus q QO = q.
39 axiom Qplus_Qopp: \forall q:Q.Qplus q (Qopp q) = QO.
40
41 (* times *)
42 axiom symmetric_Qtimes: symmetric ? Qtimes.
43 axiom associative_Qtimes: associative ? Qtimes.
44 axiom Qtimes_Q1: \forall q:Q.Qtimes q Q1 = q.
45 axiom Qtimes_Qinv: \forall q:Q.q \neq QO \to Qtimes q (Qinv q) = Q1.
46
47 (* plus times *)
48 axiom distributive_Qtimes_Qplus: distributive ? Qtimes Qplus.
49
50 axiom frac_num_denom: \forall q.frac (num q) (denom q) = q.
51 axiom frac_O: \forall n. frac O n = QO.
52 axiom frac_n: \forall n. n\neq O \to frac n n = Q1.
53 axiom Qtimes_frac : \forall a,b,c,d.Qtimes (frac a b) (frac c d) =
54 (frac (a * c) (b * d)). 
55 alias symbol "times" = "natural times".
56 axiom Qplus_frac:\forall a,b,c,d.Qplus (frac a b) (frac c d) =
57 (frac (a * d + b * c) (b * d)).
58 axiom Qlt_fracl:\forall a,b,c,d.Qlt (frac a b) (frac c d) \to
59 a*d \lt b*c. 
60 axiom Qlt_fracr:\forall a,b,c,d.a*d \lt b*c \to Qlt (frac a b) (frac c d).
61 axiom frac_Qopp: \forall a,b.Qopp(frac a b) = frac (Zopp a) b.
62 axiom frac_Qinv1: \forall a,b:nat.Qinv(frac a b) = frac b a.
63 axiom frac_Qinv2: \forall a,b:nat.Qinv(frac (Zopp a) b) = frac (Zopp b) a.
64
65 definition sigma_Q \def \lambda n,p,f.iter_p_gen n p Q f QO Qplus. 
66 (*
67 theorem geometric: \forall q.\exists k. 
68 Qlt q (sigma_Q k (\lambda x.true) (\lambda x. frac (S O) x)).
69 *)