]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/Q/nat_fact/times.ma
Sambin's & Valentini's toolbox (???)
[helm.git] / 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.