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 interpretation "Rationals" 'Q = Q.
  25
  26 definition Qone ≝ Qpos one.
  27
  28 definition Qopp ≝
  29  λq.
  30   match q with
  31    [ OQ ⇒ OQ
  32    | Qpos r ⇒ Qneg r
  33    | Qneg r ⇒ Qpos r
  34    ].
  35
  36 definition nat_fact_all_to_Q \def
  37 \lambda n.
  38   match n with
  39   [nfa_zero \Rightarrow OQ
  40   |nfa_one \Rightarrow Qpos one
  41   |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction l))
  42   ].
  43
  44 definition nat_to_Q ≝ λn.nat_fact_all_to_Q (factorize n).
  45
  46 definition Z_to_Q ≝
  47  λz.
  48   match z with
  49    [ OZ ⇒ OQ
  50    | pos n ⇒ nat_to_Q (S n)
  51    | neg n ⇒ Qopp (nat_to_Q (S n))
  52    ].
  53
  54 definition numeratorQ \def
  55 \lambda q.match q with
  56   [OQ \Rightarrow nfa_zero
  57   |Qpos r \Rightarrow
  58     match r with
  59     [one \Rightarrow nfa_one
  60     |frac x \Rightarrow numerator x
  61     ]
  62   |Qneg r \Rightarrow
  63     match r with
  64     [one \Rightarrow nfa_one
  65     |frac x \Rightarrow numerator x
  66     ]
  67   ].
  68
  69 theorem numeratorQ_nat_fact_all_to_Q: \forall g.
  70 numeratorQ (nat_fact_all_to_Q g) = g.
  71 intro.cases g
  72   [reflexivity
  73   |reflexivity
  74   |apply numerator_nat_fact_to_fraction
  75   ]
  76 qed.