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