helm/software/matita/library/Q/fraction/ftimes.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/finv.ma".
  17
  18 definition nat_frac_item_to_ratio: Z \to ratio \def
  19 \lambda x:Z. match x with
  20 [ OZ \Rightarrow one
  21 | (pos n) \Rightarrow frac (pp n)
  22 | (neg n) \Rightarrow frac (nn n)].
  23
  24 let rec ftimes f g \def
  25   match f with
  26   [ (pp n) \Rightarrow
  27     match g with
  28     [(pp m) \Rightarrow nat_frac_item_to_ratio (pos n + pos m)
  29     | (nn m) \Rightarrow nat_frac_item_to_ratio (pos n + neg m)
  30     | (cons y g1) \Rightarrow frac (cons (pos n + y) g1)]
  31   | (nn n) \Rightarrow
  32     match g with
  33     [(pp m) \Rightarrow nat_frac_item_to_ratio (neg n + pos m)
  34     | (nn m) \Rightarrow nat_frac_item_to_ratio (neg n + neg m)
  35     | (cons y g1) \Rightarrow frac (cons (neg n + y) g1)]
  36   | (cons x f1) \Rightarrow
  37     match g with
  38     [ (pp m) \Rightarrow frac (cons (x + pos m) f1)
  39     | (nn m) \Rightarrow frac (cons (x + neg m) f1)
  40     | (cons y g1) \Rightarrow
  41       match ftimes f1 g1 with
  42         [ one \Rightarrow nat_frac_item_to_ratio (x + y)
  43         | (frac h) \Rightarrow frac (cons (x + y) h)]]].
  44
  45 theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
  46 unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)).
  47   intros.elim g.
  48     change with (nat_frac_item_to_ratio (pos n + pos n1) = nat_frac_item_to_ratio (pos n1 + pos n)).
  49      apply eq_f.apply sym_Zplus.
  50     change with (nat_frac_item_to_ratio (pos n + neg n1) = nat_frac_item_to_ratio (neg n1 + pos n)).
  51      apply eq_f.apply sym_Zplus.
  52     change with (frac (cons (pos n + z) f) = frac (cons (z + pos n) f)).
  53      rewrite < sym_Zplus.reflexivity.
  54   intros.elim g.
  55     change with (nat_frac_item_to_ratio (neg n + pos n1) = nat_frac_item_to_ratio (pos n1 + neg n)).
  56      apply eq_f.apply sym_Zplus.
  57     change with (nat_frac_item_to_ratio (neg n + neg n1) = nat_frac_item_to_ratio (neg n1 + neg n)).
  58      apply eq_f.apply sym_Zplus.
  59     change with (frac (cons (neg n + z) f) = frac (cons (z + neg n) f)).
  60      rewrite < sym_Zplus.reflexivity.
  61   intros.change with (frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f)).
  62    rewrite < sym_Zplus.reflexivity.
  63   intros.change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)).
  64    rewrite < sym_Zplus.reflexivity.
  65   intros.
  66    (*CSC: simplify does something nasty here because of a redex in Zplus *)
  67    change with
  68    (match ftimes f g with
  69    [ one \Rightarrow nat_frac_item_to_ratio (x1 + y1)
  70    | (frac h) \Rightarrow frac (cons (x1 + y1) h)] =
  71    match ftimes g f with
  72    [ one \Rightarrow nat_frac_item_to_ratio (y1 + x1)
  73    | (frac h) \Rightarrow frac (cons (y1 + x1) h)]).
  74     rewrite < H.rewrite < sym_Zplus.reflexivity.
  75 qed.
  76
  77 theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one.
  78 intro.elim f.
  79   change with (nat_frac_item_to_ratio (pos n + - (pos n)) = one).
  80    rewrite > Zplus_Zopp.reflexivity.
  81   change with (nat_frac_item_to_ratio (neg n + - (neg n)) = one).
  82    rewrite > Zplus_Zopp.reflexivity.
  83    (*CSC: simplify does something nasty here because of a redex in Zplus *)
  84 (* again: we would need something to help finding the right change *)
  85   change with
  86   (match ftimes f1 (finv f1) with
  87   [ one \Rightarrow nat_frac_item_to_ratio (z + - z)
  88   | (frac h) \Rightarrow frac (cons (z + - z) h)] = one).
  89   rewrite > H.rewrite > Zplus_Zopp.reflexivity.
  90 qed.