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 include "Q/nat_fact/times.ma".
  18 include "Z/times.ma".
  19
  20 definition nat_frac_item_to_ratio: Z \to ratio \def
  21 \lambda x:Z. match x with
  22 [ OZ \Rightarrow one
  23 | (pos n) \Rightarrow frac (pp n)
  24 | (neg n) \Rightarrow frac (nn n)].
  25
  26 let rec ftimes f g \def
  27   match f with
  28   [ (pp n) \Rightarrow
  29     match g with
  30     [(pp m) \Rightarrow nat_frac_item_to_ratio (pos n + pos m)
  31     | (nn m) \Rightarrow nat_frac_item_to_ratio (pos n + neg m)
  32     | (cons y g1) \Rightarrow frac (cons (pos n + y) g1)]
  33   | (nn n) \Rightarrow
  34     match g with
  35     [(pp m) \Rightarrow nat_frac_item_to_ratio (neg n + pos m)
  36     | (nn m) \Rightarrow nat_frac_item_to_ratio (neg n + neg m)
  37     | (cons y g1) \Rightarrow frac (cons (neg n + y) g1)]
  38   | (cons x f1) \Rightarrow
  39     match g with
  40     [ (pp m) \Rightarrow frac (cons (x + pos m) f1)
  41     | (nn m) \Rightarrow frac (cons (x + neg m) f1)
  42     | (cons y g1) \Rightarrow
  43       match ftimes f1 g1 with
  44         [ one \Rightarrow nat_frac_item_to_ratio (x + y)
  45         | (frac h) \Rightarrow frac (cons (x + y) h)]]].
  46
  47 theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
  48 unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)).
  49   intros.elim g.
  50     change with (nat_frac_item_to_ratio (pos n + pos n1) = nat_frac_item_to_ratio (pos n1 + pos n)).
  51      apply eq_f.apply sym_Zplus.
  52     change with (nat_frac_item_to_ratio (pos n + neg n1) = nat_frac_item_to_ratio (neg n1 + pos n)).
  53      apply eq_f.apply sym_Zplus.
  54     change with (frac (cons (pos n + z) f) = frac (cons (z + pos n) f)).
  55      rewrite < sym_Zplus.reflexivity.
  56   intros.elim g.
  57     change with (nat_frac_item_to_ratio (neg n + pos n1) = nat_frac_item_to_ratio (pos n1 + neg n)).
  58      apply eq_f.apply sym_Zplus.
  59     change with (nat_frac_item_to_ratio (neg n + neg n1) = nat_frac_item_to_ratio (neg n1 + neg n)).
  60      apply eq_f.apply sym_Zplus.
  61     change with (frac (cons (neg n + z) f) = frac (cons (z + neg n) f)).
  62      rewrite < sym_Zplus.reflexivity.
  63   intros.change with (frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f)).
  64    rewrite < sym_Zplus.reflexivity.
  65   intros.change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)).
  66    rewrite < sym_Zplus.reflexivity.
  67   intros.
  68    (*CSC: simplify does something nasty here because of a redex in Zplus *)
  69    change with
  70    (match ftimes f g with
  71    [ one \Rightarrow nat_frac_item_to_ratio (x1 + y1)
  72    | (frac h) \Rightarrow frac (cons (x1 + y1) h)] =
  73    match ftimes g f with
  74    [ one \Rightarrow nat_frac_item_to_ratio (y1 + x1)
  75    | (frac h) \Rightarrow frac (cons (y1 + x1) h)]).
  76     rewrite < H.rewrite < sym_Zplus.reflexivity.
  77 qed.
  78
  79 theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one.
  80 intro.elim f.
  81   change with (nat_frac_item_to_ratio (pos n + - (pos n)) = one).
  82    rewrite > Zplus_Zopp.reflexivity.
  83   change with (nat_frac_item_to_ratio (neg n + - (neg n)) = one).
  84    rewrite > Zplus_Zopp.reflexivity.
  85    (*CSC: simplify does something nasty here because of a redex in Zplus *)
  86 (* again: we would need something to help finding the right change *)
  87   change with
  88   (match ftimes f1 (finv f1) with
  89   [ one \Rightarrow nat_frac_item_to_ratio (z + - z)
  90   | (frac h) \Rightarrow frac (cons (z + - z) h)] = one).
  91   rewrite > H.rewrite > Zplus_Zopp.reflexivity.
  92 qed.
  93
  94 theorem times_f_ftimes: \forall n,m.
  95 frac (nat_fact_to_fraction (times_f n m))
  96 = ftimes (nat_fact_to_fraction n) (nat_fact_to_fraction m).
  97 intro.
  98 elim n
  99   [elim m
 100     [simplify.
 101      rewrite < plus_n_Sm.reflexivity
 102     |elim n2
 103       [simplify.rewrite < plus_n_O.reflexivity
 104       |simplify.reflexivity.
 105       ]
 106     ]
 107   |elim m
 108     [elim n1
 109       [simplify.reflexivity
 110       |simplify.rewrite < plus_n_Sm.reflexivity
 111       ]
 112     |simplify.
 113      cut (\exist h.ftimes (nat_fact_to_fraction n2) (nat_fact_to_fraction n4) = frac h)
 114       [elim Hcut.
 115        rewrite > H2.
 116        simplify.apply eq_f.
 117        apply eq_f2
 118         [apply eq_plus_Zplus
 119         |apply injective_frac.
 120          rewrite < H2.
 121          apply H
 122         ]
 123       |generalize in match n4.
 124        elim n2
 125         [cases n6;simplify;
 126           [ exists; [2: autobatch;]
 127           | exists; [2:autobatch;]
 128           ]
 129         |cases n7;simplify
 130           [exists;[2:autobatch]
 131           |elim (H2 n9).
 132            rewrite > H3.
 133            simplify.
 134            exists;[2:autobatch]
 135           ]]]]]
 136 qed.