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