]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/Z/times.ma
Dummy dependent types are no longer cleaned in inductive type arities.
[helm.git] / helm / software / matita / library / Z / 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 set "baseuri" "cic:/matita/Z/times".
16
17 include "nat/lt_arith.ma".
18 include "Z/plus.ma".
19
20 definition Ztimes :Z \to Z \to Z \def
21 \lambda x,y.
22   match x with
23     [ OZ \Rightarrow OZ
24     | (pos m) \Rightarrow
25         match y with
26          [ OZ \Rightarrow OZ
27          | (pos n) \Rightarrow (pos (pred ((S m) * (S n))))
28          | (neg n) \Rightarrow (neg (pred ((S m) * (S n))))]
29     | (neg m) \Rightarrow
30         match y with
31          [ OZ \Rightarrow OZ
32          | (pos n) \Rightarrow (neg (pred ((S m) * (S n))))
33          | (neg n) \Rightarrow (pos (pred ((S m) * (S n))))]].
34          
35 (*CSC: the URI must disappear: there is a bug now *)
36 interpretation "integer times" 'times x y = (cic:/matita/Z/times/Ztimes.con x y).
37
38 theorem Ztimes_z_OZ:  \forall z:Z. z*OZ = OZ.
39 intro.elim z.
40 simplify.reflexivity.
41 simplify.reflexivity.
42 simplify.reflexivity.
43 qed.
44
45 definition Zone \def pos O.
46
47 theorem Ztimes_neg_Zopp: \forall n:nat.\forall x:Z.
48 neg n * x = - (pos n * x).
49 intros.elim x.
50 simplify.reflexivity.
51 simplify.reflexivity.
52 simplify.reflexivity.
53 qed.
54
55 theorem symmetric_Ztimes : symmetric Z Ztimes.
56 change with (\forall x,y:Z. x*y = y*x).
57 intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
58 elim y.simplify.reflexivity. 
59 change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
60 rewrite < sym_times.reflexivity.
61 change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
62 rewrite < sym_times.reflexivity.
63 elim y.simplify.reflexivity.
64 change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
65 rewrite < sym_times.reflexivity.
66 change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
67 rewrite < sym_times.reflexivity.
68 qed.
69
70 variant sym_Ztimes : \forall x,y:Z. x*y = y*x
71 \def symmetric_Ztimes.
72
73 theorem Ztimes_Zone_l: \forall z:Z. Ztimes Zone z = z.
74 intro.unfold Zone.simplify.
75 elim z;simplify
76   [reflexivity
77   |rewrite < plus_n_O.reflexivity
78   |rewrite < plus_n_O.reflexivity
79   ]
80 qed.
81
82 theorem Ztimes_Zone_r: \forall z:Z. Ztimes z Zone = z.
83 intro.
84 rewrite < sym_Ztimes.
85 apply Ztimes_Zone_l.
86 qed.
87
88 theorem associative_Ztimes: associative Z Ztimes.
89 unfold associative.
90 intros.elim x.
91   simplify.reflexivity. 
92   elim y.
93     simplify.reflexivity.
94     elim z.
95       simplify.reflexivity.
96       change with 
97        (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
98        pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
99         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
100          apply lt_O_times_S_S.apply lt_O_times_S_S.
101       change with 
102        (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
103        neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
104         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
105          apply lt_O_times_S_S.apply lt_O_times_S_S.
106     elim z.
107       simplify.reflexivity.
108       change with 
109        (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
110        neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
111         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
112          apply lt_O_times_S_S.apply lt_O_times_S_S.
113       change with 
114        (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
115        pos(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
116         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
117         apply lt_O_times_S_S.apply lt_O_times_S_S.
118   elim y.
119     simplify.reflexivity.
120     elim z.
121       simplify.reflexivity.
122       change with 
123        (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
124        neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
125         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
126          apply lt_O_times_S_S.apply lt_O_times_S_S.
127       change with 
128        (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
129        pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
130         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
131          apply lt_O_times_S_S.apply lt_O_times_S_S.
132     elim z.
133       simplify.reflexivity.
134       change with 
135        (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
136        pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
137         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
138          apply lt_O_times_S_S.apply lt_O_times_S_S.
139       change with 
140        (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
141        neg(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
142         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
143          apply lt_O_times_S_S.apply lt_O_times_S_S.
144 qed.
145
146 variant assoc_Ztimes : \forall x,y,z:Z. 
147 (x * y) * z = x * (y * z) \def 
148 associative_Ztimes.
149
150 lemma times_minus1: \forall n,p,q:nat. lt q p \to
151 (S n) * (S (pred ((S p) - (S q)))) =
152 pred ((S n) * (S p)) - pred ((S n) * (S q)).
153 intros.
154 rewrite < S_pred.  
155 rewrite > minus_pred_pred.
156 rewrite < distr_times_minus. 
157 reflexivity.
158 (* we now close all positivity conditions *)
159 apply lt_O_times_S_S.                    
160 apply lt_O_times_S_S.
161 simplify.unfold lt.
162 apply le_SO_minus.  exact H.
163 qed.
164
165 lemma Ztimes_Zplus_pos_neg_pos: \forall n,p,q:nat.
166 (pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q). 
167 intros.
168 simplify. 
169 change in match (p + n * (S p)) with (pred ((S n) * (S p))).
170 change in match (q + n * (S q)) with (pred ((S n) * (S q))).
171 rewrite < nat_compare_pred_pred.
172 rewrite < nat_compare_times_l.
173 rewrite < nat_compare_S_S.
174 apply (nat_compare_elim p q).
175 intro.
176 (* uff *)
177 change with (pos (pred ((S n) * (S (pred ((S q) - (S p)))))) =
178             pos (pred ((pred ((S n) * (S q))) - (pred ((S n) * (S p)))))).
179 rewrite < (times_minus1 n q p H).reflexivity.
180 intro.rewrite < H.simplify.reflexivity.
181 intro.
182 change with (neg (pred ((S n) * (S (pred ((S p) - (S q)))))) =
183             neg (pred ((pred ((S n) * (S p))) - (pred ((S n) * (S q)))))). 
184 rewrite < (times_minus1 n p q H).reflexivity.                                 
185 (* two more positivity conditions from nat_compare_pred_pred *)   
186 apply lt_O_times_S_S.  
187 apply lt_O_times_S_S. 
188 qed. 
189
190 lemma Ztimes_Zplus_pos_pos_neg: \forall n,p,q:nat.
191 (pos n)*((pos p)+(neg q)) = (pos n)*(pos p)+ (pos n)*(neg q).
192 intros.
193 rewrite < sym_Zplus.
194 rewrite > Ztimes_Zplus_pos_neg_pos.
195 apply sym_Zplus.
196 qed.
197
198 lemma distributive2_Ztimes_pos_Zplus: 
199 distributive2 nat Z (\lambda n,z. (pos n) * z) Zplus.
200 change with (\forall n,y,z.
201 (pos n) * (y + z) = (pos n) * y + (pos n) * z).  
202 intros.elim y.
203   reflexivity.
204   elim z.
205     reflexivity.
206     change with
207      (pos (pred ((S n) * ((S n1) + (S n2)))) =
208      pos (pred ((S n) * (S n1) + (S n) * (S n2)))).
209       rewrite < distr_times_plus.reflexivity.
210     apply Ztimes_Zplus_pos_pos_neg.
211   elim z.
212     reflexivity.
213     apply Ztimes_Zplus_pos_neg_pos.
214     change with
215      (neg (pred ((S n) * ((S n1) + (S n2)))) =
216      neg (pred ((S n) * (S n1) + (S n) * (S n2)))).
217     rewrite < distr_times_plus.reflexivity.
218 qed.
219
220 variant distr_Ztimes_Zplus_pos: \forall n,y,z.
221 (pos n) * (y + z) = ((pos n) * y + (pos n) * z) \def
222 distributive2_Ztimes_pos_Zplus.
223
224 lemma distributive2_Ztimes_neg_Zplus : 
225 distributive2 nat Z (\lambda n,z. (neg n) * z) Zplus.
226 change with (\forall n,y,z.
227 (neg n) * (y + z) = (neg n) * y + (neg n) * z).  
228 intros.
229 rewrite > Ztimes_neg_Zopp. 
230 rewrite > distr_Ztimes_Zplus_pos.
231 rewrite > Zopp_Zplus.
232 rewrite < Ztimes_neg_Zopp. rewrite < Ztimes_neg_Zopp.
233 reflexivity.
234 qed.
235
236 variant distr_Ztimes_Zplus_neg: \forall n,y,z.
237 (neg n) * (y + z) = (neg n) * y + (neg n) * z \def
238 distributive2_Ztimes_neg_Zplus.
239
240 theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus.
241 change with (\forall x,y,z:Z. x * (y + z) = x*y + x*z).
242 intros.elim x.
243 (* case x = OZ *)
244 simplify.reflexivity.
245 (* case x = pos n *)
246 apply distr_Ztimes_Zplus_pos.
247 (* case x = neg n *)
248 apply distr_Ztimes_Zplus_neg.
249 qed.
250
251 variant distr_Ztimes_Zplus: \forall x,y,z.
252 x * (y + z) = x*y + x*z \def
253 distributive_Ztimes_Zplus.