helm/software/matita/library/Q/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 "Q/ratio/ratio.ma".
  16 include "Q/fraction/numerator_denominator.ma".
  17
  18 (* a rational number is either O or a ratio with a sign *)
  19 inductive Q : Set \def
  20     OQ : Q
  21   | Qpos : ratio  \to Q
  22   | Qneg : ratio  \to Q.
  23
  24 definition Qone ≝ Qpos one.
  25
  26 definition Qopp ≝
  27  λq.
  28   match q with
  29    [ OQ ⇒ OQ
  30    | Qpos r ⇒ Qneg r
  31    | Qneg r ⇒ Qpos r
  32    ].
  33
  34 definition nat_fact_all_to_Q \def
  35 \lambda n.
  36   match n with
  37   [nfa_zero \Rightarrow OQ
  38   |nfa_one \Rightarrow Qpos one
  39   |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction l))
  40   ].
  41
  42 definition nat_to_Q ≝ λn.nat_fact_all_to_Q (factorize n).
  43
  44 definition Z_to_Q ≝
  45  λz.
  46   match z with
  47    [ OZ ⇒ OQ
  48    | pos n ⇒ nat_to_Q (S n)
  49    | neg n ⇒ Qopp (nat_to_Q (S n))
  50    ].
  51
  52 definition numeratorQ \def
  53 \lambda q.match q with
  54   [OQ \Rightarrow nfa_zero
  55   |Qpos r \Rightarrow
  56     match r with
  57     [one \Rightarrow nfa_one
  58     |frac x \Rightarrow numerator x
  59     ]
  60   |Qneg r \Rightarrow
  61     match r with
  62     [one \Rightarrow nfa_one
  63     |frac x \Rightarrow numerator x
  64     ]
  65   ].
  66
  67 theorem numeratorQ_nat_fact_all_to_Q: \forall g.
  68 numeratorQ (nat_fact_all_to_Q g) = g.
  69 intro.cases g
  70   [reflexivity
  71   |reflexivity
  72   |apply numerator_nat_fact_to_fraction
  73   ]
  74 qed.