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 *)