helm/software/matita/library/Q/nat_fact/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 "nat/factorization.ma".
  16
  17 let rec times_f h g \def
  18   match h with
  19   [nf_last a \Rightarrow
  20     match g with
  21     [nf_last b \Rightarrow nf_last (S (a+b))
  22     |nf_cons b g1 \Rightarrow nf_cons (S (a+b)) g1
  23     ]
  24   |nf_cons a h1 \Rightarrow
  25     match g with
  26     [nf_last b \Rightarrow nf_cons (S (a+b)) h1
  27     |nf_cons b g1 \Rightarrow nf_cons (a+b) (times_f h1 g1)
  28     ]].
  29
  30 theorem eq_times_f_times1:\forall g,h,m. defactorize_aux (times_f g h) m
  31 =defactorize_aux g m*defactorize_aux h m.
  32 intro.elim g
  33   [elim h;simplify;autobatch;
  34   |elim h
  35     [simplify;autobatch
  36     |simplify.rewrite > (H n3 (S m)).autobatch
  37     ]]
  38 qed.
  39
  40
  41 (******************* times_fa *********************)
  42
  43 definition times_fa \def
  44 \lambda f,g.
  45 match f with
  46 [nfa_zero \Rightarrow nfa_zero
  47 |nfa_one \Rightarrow g
  48 |nfa_proper f1 \Rightarrow match g with
  49   [nfa_zero \Rightarrow nfa_zero
  50   |nfa_one \Rightarrow nfa_proper f1
  51   |nfa_proper g1 \Rightarrow nfa_proper (times_f f1 g1)
  52   ]].
  53
  54 theorem eq_times_fa_times: \forall f,g.
  55 defactorize (times_fa f g) = defactorize f*defactorize g.
  56 intros.
  57 elim f
  58   [reflexivity
  59   |simplify.apply plus_n_O
  60   |elim g;simplify
  61     [apply times_n_O
  62     |apply times_n_SO
  63     |apply eq_times_f_times1
  64     ]]
  65 qed.
  66
  67 theorem eq_times_times_fa: \forall n,m.
  68 factorize (n*m) = times_fa (factorize n) (factorize m).
  69 intros.
  70 rewrite <(factorize_defactorize (times_fa (factorize n) (factorize m))).
  71 rewrite > eq_times_fa_times.
  72 rewrite > defactorize_factorize.
  73 rewrite > defactorize_factorize.
  74 reflexivity.
  75 qed.