]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/times.ma
- oCic2NCic and nCic2OCic moved to ng_library
[helm.git] / helm / software / matita / library / nat / times.ma
1
2 (**************************************************************************)
3 (*       __                                                               *)
4 (*      ||M||                                                             *)
5 (*      ||A||       A project by Andrea Asperti                           *)
6 (*      ||T||                                                             *)
7 (*      ||I||       Developers:                                           *)
8 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
9 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
10 (*      \   /                                                             *)
11 (*       \ /        This file is distributed under the terms of the       *)
12 (*        v         GNU Lesser General Public License Version 2.1         *)
13 (*                                                                        *)
14 (**************************************************************************)
15
16 include "nat/plus.ma".
17
18 let rec times n m \def 
19  match n with 
20  [ O \Rightarrow O
21  | (S p) \Rightarrow m+(times p m) ].
22
23 interpretation "natural times" 'times x y = (times x y).
24
25 theorem times_Sn_m:
26 \forall n,m:nat. m+n*m = S n*m.
27 intros. reflexivity.
28 qed.
29
30 theorem times_n_O: \forall n:nat. O = n*O.
31 intros.elim n.
32 simplify.reflexivity.
33 simplify.assumption.
34 qed.
35
36 theorem times_n_Sm : 
37 \forall n,m:nat. n+(n*m) = n*(S m).
38 intros.elim n.
39 simplify.reflexivity.
40 simplify.
41 demodulate all.
42 (*
43 apply eq_f.rewrite < H.
44 transitivity ((n1+m)+n1*m).symmetry.apply assoc_plus.
45 transitivity ((m+n1)+n1*m).
46 apply eq_f2.
47 apply sym_plus.
48 reflexivity.
49 apply assoc_plus.
50 *)
51 qed.
52
53 theorem times_O_to_O: \forall n,m:nat.n*m = O \to n = O \lor m= O.
54 apply nat_elim2;intros
55   [left.reflexivity
56   |right.reflexivity
57   |apply False_ind.
58    simplify in H1.
59    apply (not_eq_O_S ? (sym_eq  ? ? ? H1))
60   ]
61 qed.
62
63 theorem times_n_SO : \forall n:nat. n = n * S O.
64 intros. demodulate. reflexivity. (*
65 rewrite < times_n_Sm.
66 rewrite < times_n_O.
67 rewrite < plus_n_O.
68 reflexivity.*)
69 qed.
70
71 theorem times_SSO_n : \forall n:nat. n + n = S (S O) * n.
72 intros.
73 simplify.
74 rewrite < plus_n_O.
75 reflexivity.
76 qed.
77
78 alias num (instance 0) = "natural number".
79 lemma times_SSO: \forall n.2*(S n) = S(S(2*n)).
80 intro.simplify.rewrite < plus_n_Sm.reflexivity.
81 qed.
82
83 theorem or_eq_eq_S: \forall n.\exists m. 
84 n = (S(S O))*m \lor n = S ((S(S O))*m).
85 intro.elim n
86   [apply (ex_intro ? ? O).
87    left.reflexivity
88   |elim H.elim H1
89     [apply (ex_intro ? ? a).
90      right.apply eq_f.assumption
91     |apply (ex_intro ? ? (S a)).
92      left.rewrite > H2.
93      apply sym_eq.
94      apply times_SSO
95     ]
96   ]
97 qed.
98
99 theorem symmetric_times : symmetric nat times. 
100 unfold symmetric.
101 intros.elim x;
102  [ simplify. apply times_n_O.
103  | demodulate. reflexivity. (*
104 (* applyS times_n_Sm. *) 
105 simplify.rewrite > H.apply times_n_Sm.*)]
106 qed.
107
108 variant sym_times : \forall n,m:nat. n*m = m*n \def
109 symmetric_times.
110
111 theorem distributive_times_plus : distributive nat times plus.
112 unfold distributive.
113 intros.elim x.
114 simplify.reflexivity.
115 simplify.
116 demodulate all.
117 (*
118 rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.
119 apply eq_f.rewrite < assoc_plus. rewrite < (sym_plus ? z).
120 rewrite > assoc_plus.reflexivity. *)
121 qed.
122
123 variant distr_times_plus: \forall n,m,p:nat. n*(m+p) = n*m + n*p
124 \def distributive_times_plus.
125
126 theorem associative_times: associative nat times.
127 unfold associative.
128 intros.
129 elim x. simplify.apply refl_eq. 
130 simplify.
131 demodulate all.
132 (*
133 rewrite < sym_times.
134 rewrite > distr_times_plus.
135 rewrite < sym_times.
136 rewrite < (sym_times (times n y) z).
137 rewrite < H.apply refl_eq.
138 *)
139 qed.
140
141 variant assoc_times: \forall n,m,p:nat. (n*m)*p = n*(m*p) \def
142 associative_times.
143
144 lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
145 intros. 
146 demodulate. reflexivity.
147 (* autobatch paramodulation. *)
148 qed.
149