]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/times.ma
Dummy dependent products in inductive types arities are no longer cleaned.
[helm.git] / helm / software / matita / library / nat / 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/plus.ma".
16
17 let rec times n m \def 
18  match n with 
19  [ O \Rightarrow O
20  | (S p) \Rightarrow m+(times p m) ].
21
22 interpretation "natural times" 'times x y = (cic:/matita/nat/times/times.con x y).
23
24 theorem times_n_O: \forall n:nat. O = n*O.
25 intros.elim n.
26 simplify.reflexivity.
27 simplify.assumption.
28 qed.
29
30 theorem times_n_Sm : 
31 \forall n,m:nat. n+(n*m) = n*(S m).
32 intros.elim n.
33 simplify.reflexivity.
34 simplify.apply eq_f.rewrite < H.
35 transitivity ((n1+m)+n1*m).symmetry.apply assoc_plus.
36 transitivity ((m+n1)+n1*m).
37 apply eq_f2.
38 apply sym_plus.
39 reflexivity.
40 apply assoc_plus.
41 qed.
42
43 theorem times_O_to_O: \forall n,m:nat.n*m = O \to n = O \lor m= O.
44 apply nat_elim2;intros
45   [left.reflexivity
46   |right.reflexivity
47   |apply False_ind.
48    simplify in H1.
49    apply (not_eq_O_S ? (sym_eq  ? ? ? H1))
50   ]
51 qed.
52
53 theorem times_n_SO : \forall n:nat. n = n * S O.
54 intros.
55 rewrite < times_n_Sm.
56 rewrite < times_n_O.
57 rewrite < plus_n_O.
58 reflexivity.
59 qed.
60
61 theorem times_SSO_n : \forall n:nat. n + n = S (S O) * n.
62 intros.
63 simplify.
64 rewrite < plus_n_O.
65 reflexivity.
66 qed.
67
68 alias num (instance 0) = "natural number".
69 lemma times_SSO: \forall n.2*(S n) = S(S(2*n)).
70 intro.simplify.rewrite < plus_n_Sm.reflexivity.
71 qed.
72
73 theorem or_eq_eq_S: \forall n.\exists m. 
74 n = (S(S O))*m \lor n = S ((S(S O))*m).
75 intro.elim n
76   [apply (ex_intro ? ? O).
77    left.reflexivity
78   |elim H.elim H1
79     [apply (ex_intro ? ? a).
80      right.apply eq_f.assumption
81     |apply (ex_intro ? ? (S a)).
82      left.rewrite > H2.
83      apply sym_eq.
84      apply times_SSO
85     ]
86   ]
87 qed.
88
89 theorem symmetric_times : symmetric nat times. 
90 unfold symmetric.
91 intros.elim x.
92 simplify.apply times_n_O.
93 simplify.rewrite > H.apply times_n_Sm.
94 qed.
95
96 variant sym_times : \forall n,m:nat. n*m = m*n \def
97 symmetric_times.
98
99 theorem distributive_times_plus : distributive nat times plus.
100 unfold distributive.
101 intros.elim x.
102 simplify.reflexivity.
103 simplify.rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.
104 apply eq_f.rewrite < assoc_plus. rewrite < (sym_plus ? z).
105 rewrite > assoc_plus.reflexivity.
106 qed.
107
108 variant distr_times_plus: \forall n,m,p:nat. n*(m+p) = n*m + n*p
109 \def distributive_times_plus.
110
111 theorem associative_times: associative nat times.
112 unfold associative.intros.
113 elim x.simplify.apply refl_eq.
114 simplify.rewrite < sym_times.
115 rewrite > distr_times_plus.
116 rewrite < sym_times.
117 rewrite < (sym_times (times n y) z).
118 rewrite < H.apply refl_eq.
119 qed.
120
121 variant assoc_times: \forall n,m,p:nat. (n*m)*p = n*(m*p) \def
122 associative_times.