helm/software/matita/library/Q/times.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/inv.ma".
  16
  17 definition Z_to_ratio: Z \to ratio \def
  18 \lambda x:Z. match x with
  19 [ OZ \Rightarrow one
  20 | (pos n) \Rightarrow frac (pp n)
  21 | (neg n) \Rightarrow frac (nn n)].
  22
  23 let rec ftimes f g \def
  24   match f with
  25   [ (pp n) \Rightarrow
  26     match g with
  27     [(pp m) \Rightarrow Z_to_ratio (pos n + pos m)
  28     | (nn m) \Rightarrow Z_to_ratio (pos n + neg m)
  29     | (cons y g1) \Rightarrow frac (cons (pos n + y) g1)]
  30   | (nn n) \Rightarrow
  31     match g with
  32     [(pp m) \Rightarrow Z_to_ratio (neg n + pos m)
  33     | (nn m) \Rightarrow Z_to_ratio (neg n + neg m)
  34     | (cons y g1) \Rightarrow frac (cons (neg n + y) g1)]
  35   | (cons x f1) \Rightarrow
  36     match g with
  37     [ (pp m) \Rightarrow frac (cons (x + pos m) f1)
  38     | (nn m) \Rightarrow frac (cons (x + neg m) f1)
  39     | (cons y g1) \Rightarrow
  40       match ftimes f1 g1 with
  41         [ one \Rightarrow Z_to_ratio (x + y)
  42         | (frac h) \Rightarrow frac (cons (x + y) h)]]].
  43
  44 theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
  45 unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)).
  46   intros.elim g.
  47     change with (Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n)).
  48      apply eq_f.apply sym_Zplus.
  49     change with (Z_to_ratio (pos n + neg n1) = Z_to_ratio (neg n1 + pos n)).
  50      apply eq_f.apply sym_Zplus.
  51     change with (frac (cons (pos n + z) f) = frac (cons (z + pos n) f)).
  52      rewrite < sym_Zplus.reflexivity.
  53   intros.elim g.
  54     change with (Z_to_ratio (neg n + pos n1) = Z_to_ratio (pos n1 + neg n)).
  55      apply eq_f.apply sym_Zplus.
  56     change with (Z_to_ratio (neg n + neg n1) = Z_to_ratio (neg n1 + neg n)).
  57      apply eq_f.apply sym_Zplus.
  58     change with (frac (cons (neg n + z) f) = frac (cons (z + neg n) f)).
  59      rewrite < sym_Zplus.reflexivity.
  60   intros.change with (frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f)).
  61    rewrite < sym_Zplus.reflexivity.
  62   intros.change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)).
  63    rewrite < sym_Zplus.reflexivity.
  64   intros.
  65    (*CSC: simplify does something nasty here because of a redex in Zplus *)
  66    change with
  67    (match ftimes f g with
  68    [ one \Rightarrow Z_to_ratio (x1 + y1)
  69    | (frac h) \Rightarrow frac (cons (x1 + y1) h)] =
  70    match ftimes g f with
  71    [ one \Rightarrow Z_to_ratio (y1 + x1)
  72    | (frac h) \Rightarrow frac (cons (y1 + x1) h)]).
  73     rewrite < H.rewrite < sym_Zplus.reflexivity.
  74 qed.
  75
  76 theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one.
  77 intro.elim f.
  78   change with (Z_to_ratio (pos n + - (pos n)) = one).
  79    rewrite > Zplus_Zopp.reflexivity.
  80   change with (Z_to_ratio (neg n + - (neg n)) = one).
  81    rewrite > Zplus_Zopp.reflexivity.
  82    (*CSC: simplify does something nasty here because of a redex in Zplus *)
  83 (* again: we would need something to help finding the right change *)
  84   change with
  85   (match ftimes f1 (finv f1) with
  86   [ one \Rightarrow Z_to_ratio (z + - z)
  87   | (frac h) \Rightarrow frac (cons (z + - z) h)] = one).
  88   rewrite > H.rewrite > Zplus_Zopp.reflexivity.
  89 qed.
  90
  91 definition rtimes : ratio \to ratio \to ratio \def
  92 \lambda r,s:ratio.
  93   match r with
  94   [one \Rightarrow s
  95   | (frac f) \Rightarrow
  96       match s with
  97       [one \Rightarrow frac f
  98       | (frac g) \Rightarrow ftimes f g]].
  99
 100 theorem rtimes_rinv: \forall r:ratio. rtimes r (rinv r) = one.
 101 intro.elim r.
 102 reflexivity.
 103 simplify.apply ftimes_finv.
 104 qed.
 105
 106 theorem symmetric_rtimes : symmetric ratio rtimes.
 107 change with (\forall r,s:ratio. rtimes r s = rtimes s r).
 108 intros.
 109 elim r. elim s.
 110 reflexivity.
 111 reflexivity.
 112 elim s.
 113 reflexivity.
 114 simplify.apply symmetric2_ftimes.
 115 qed.
 116
 117 variant sym_rtimes : ∀x,y:ratio. rtimes x y = rtimes y x ≝ symmetric_rtimes.
 118
 119 definition Qtimes : Q \to Q \to Q \def
 120 \lambda p,q.
 121   match p with
 122   [OQ \Rightarrow OQ
 123   |Qpos p1 \Rightarrow
 124     match q with
 125     [OQ \Rightarrow OQ
 126     |Qpos q1 \Rightarrow Qpos (rtimes p1 q1)
 127     |Qneg q1 \Rightarrow Qneg (rtimes p1 q1)
 128     ]
 129   |Qneg p1 \Rightarrow
 130     match q with
 131     [OQ \Rightarrow OQ
 132     |Qpos q1 \Rightarrow Qneg (rtimes p1 q1)
 133     |Qneg q1 \Rightarrow Qpos (rtimes p1 q1)
 134     ]
 135   ].
 136
 137 interpretation "rational times" 'times x y = (cic:/matita/Q/times/Qtimes.con x y).
 138
 139 theorem Qtimes_q_OQ: ∀q. q * OQ = OQ.
 140  intro;
 141  elim q;
 142  reflexivity.
 143 qed.
 144
 145 theorem symmetric_Qtimes: symmetric ? Qtimes.
 146  intros 2;
 147  elim x;
 148   [ rewrite > Qtimes_q_OQ; reflexivity
 149   |*:elim y;
 150      simplify;
 151      try rewrite > sym_rtimes;
 152      reflexivity
 153   ]
 154 qed.
 155
 156 theorem Qtimes_Qinv: ∀q. q ≠ OQ → q * (Qinv q) = Qpos one.
 157  intro;
 158  elim q;
 159   [ elim H; reflexivity
 160   |*:simplify;
 161      rewrite > rtimes_rinv;
 162      reflexivity
 163   ]
 164 qed.