helm/software/matita/library/Q/q/qtimes.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/q/qinv.ma".
  16 include "Q/ratio/rtimes.ma".
  17
  18 definition Qtimes : Q \to Q \to Q \def
  19 \lambda p,q.
  20   match p with
  21   [OQ \Rightarrow OQ
  22   |Qpos p1 \Rightarrow
  23     match q with
  24     [OQ \Rightarrow OQ
  25     |Qpos q1 \Rightarrow Qpos (rtimes p1 q1)
  26     |Qneg q1 \Rightarrow Qneg (rtimes p1 q1)
  27     ]
  28   |Qneg p1 \Rightarrow
  29     match q with
  30     [OQ \Rightarrow OQ
  31     |Qpos q1 \Rightarrow Qneg (rtimes p1 q1)
  32     |Qneg q1 \Rightarrow Qpos (rtimes p1 q1)
  33     ]
  34   ].
  35
  36 interpretation "rational times" 'times x y = (cic:/matita/Q/q/qtimes/Qtimes.con x y).
  37
  38 theorem Qtimes_q_OQ: ∀q. q * OQ = OQ.
  39  intro;
  40  elim q;
  41  reflexivity.
  42 qed.
  43
  44 theorem symmetric_Qtimes: symmetric ? Qtimes.
  45  intros 2;
  46  elim x;
  47   [ rewrite > Qtimes_q_OQ; reflexivity
  48   |*:elim y;
  49      simplify;
  50      try rewrite > sym_rtimes;
  51      reflexivity
  52   ]
  53 qed.
  54
  55 theorem Qtimes_Qinv: ∀q. q ≠ OQ → q * (Qinv q) = Qpos one.
  56  intro;
  57  elim q;
  58   [ elim H; reflexivity
  59   |*:simplify;
  60      rewrite > rtimes_rinv;
  61      reflexivity
  62   ]
  63 qed.