1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/Z/times".
17 include "nat/lt_arith.ma".
19 include "higher_order_defs/functions.ma".
21 definition Ztimes :Z \to Z \to Z \def
28 | (pos n) \Rightarrow (pos (pred (times (S m) (S n))))
29 | (neg n) \Rightarrow (neg (pred (times (S m) (S n))))]
33 | (pos n) \Rightarrow (neg (pred (times (S m) (S n))))
34 | (neg n) \Rightarrow (pos (pred (times (S m) (S n))))]].
36 (*CSC: the URI must disappear: there is a bug now *)
37 interpretation "integer times" 'times x y = (cic:/matita/Z/times/Ztimes.con x y).
39 theorem Ztimes_z_OZ: \forall z:Z. z*OZ = OZ.
46 theorem Ztimes_neg_Zopp: \forall n:nat.\forall x:Z.
47 eq Z (Ztimes (neg n) x) (Zopp (Ztimes (pos n) x)).
53 theorem symmetric_Ztimes : symmetric Z Ztimes.
54 change with \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x).
55 intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
56 elim y.simplify.reflexivity.
57 change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
58 rewrite < sym_times.reflexivity.
59 change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
60 rewrite < sym_times.reflexivity.
61 elim y.simplify.reflexivity.
62 change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
63 rewrite < sym_times.reflexivity.
64 change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
65 rewrite < sym_times.reflexivity.
68 variant sym_Ztimes : \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x)
69 \def symmetric_Ztimes.
71 theorem associative_Ztimes: associative Z Ztimes.
72 change with \forall x,y,z:Z.eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)).
74 elim x.simplify.reflexivity.
75 elim y.simplify.reflexivity.
76 elim z.simplify.reflexivity.
78 eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
79 (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
80 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
84 eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
85 (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
86 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
87 apply lt_O_times_S_S.apply lt_O_times_S_S.
88 elim z.simplify.reflexivity.
90 eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
91 (pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
92 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
93 apply lt_O_times_S_S.apply lt_O_times_S_S.
95 eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
96 (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
97 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
100 elim y.simplify.reflexivity.
101 elim z.simplify.reflexivity.
103 eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
104 (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
105 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
106 apply lt_O_times_S_S.
107 apply lt_O_times_S_S.
109 eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
110 (neg (pred (times (S n) (S (pred (times (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 elim z.simplify.reflexivity.
115 eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
116 (neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
117 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
118 apply lt_O_times_S_S.apply lt_O_times_S_S.
120 eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
121 (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
122 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
123 apply lt_O_times_S_S.
124 apply lt_O_times_S_S.
127 variant assoc_Ztimes : \forall x,y,z:Z.
128 eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)) \def
131 lemma times_minus1: \forall n,p,q:nat. lt q p \to
132 eq nat (times (S n) (S (pred (minus (S p) (S q)))))
133 (minus (pred (times (S n) (S p)))
134 (pred (times (S n) (S q)))).
136 rewrite < S_pred ? ?.
137 rewrite > minus_pred_pred ? ? ? ?.
138 rewrite < distr_times_minus.
140 (* we now close all positivity conditions *)
141 apply lt_O_times_S_S.
142 apply lt_O_times_S_S.
144 apply le_SO_minus. exact H.
147 lemma Ztimes_Zplus_pos_neg_pos: \forall n,p,q:nat.
148 (pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q).
151 change in match (plus p (times n (S p))) with (pred (times (S n) (S p))).
152 change in match (plus q (times n (S q))) with (pred (times (S n) (S q))).
153 rewrite < nat_compare_pred_pred ? ? ? ?.
154 rewrite < nat_compare_times_l.
155 rewrite < nat_compare_S_S.
156 apply nat_compare_elim p q.
159 change with (eq Z (pos (pred (times (S n) (S (pred (minus (S q) (S p)))))))
160 (pos (pred (minus (pred (times (S n) (S q)))
161 (pred (times (S n) (S p))))))).
162 rewrite < times_minus1 n q p H.reflexivity.
163 intro.rewrite < H.simplify.reflexivity.
165 change with (eq Z (neg (pred (times (S n) (S (pred (minus (S p) (S q)))))))
166 (neg (pred (minus (pred (times (S n) (S p)))
167 (pred (times (S n) (S q))))))).
168 rewrite < times_minus1 n p q H.reflexivity.
169 (* two more positivity conditions from nat_compare_pred_pred *)
170 apply lt_O_times_S_S.
171 apply lt_O_times_S_S.
174 lemma Ztimes_Zplus_pos_pos_neg: \forall n,p,q:nat.
175 (pos n)*((pos p)+(neg q)) = (pos n)*(pos p)+ (pos n)*(neg q).
178 rewrite > Ztimes_Zplus_pos_neg_pos.
182 lemma distributive2_Ztimes_pos_Zplus:
183 distributive2 nat Z (\lambda n,z. Ztimes (pos n) z) Zplus.
184 change with \forall n,y,z.
185 eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)).
190 eq Z (neg (pred (times (S n) (plus (S n1) (S n2)))))
191 (neg (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
192 rewrite < distr_times_plus.reflexivity.
193 apply Ztimes_Zplus_pos_neg_pos.
195 apply Ztimes_Zplus_pos_pos_neg.
197 eq Z (pos (pred (times (S n) (plus (S n1) (S n2)))))
198 (pos (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
199 rewrite < distr_times_plus.
203 variant distr_Ztimes_Zplus_pos: \forall n,y,z.
204 eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)) \def
205 distributive2_Ztimes_pos_Zplus.
207 lemma distributive2_Ztimes_neg_Zplus :
208 distributive2 nat Z (\lambda n,z. Ztimes (neg n) z) Zplus.
209 change with \forall n,y,z.
210 eq Z (Ztimes (neg n) (Zplus y z)) (Zplus (Ztimes (neg n) y) (Ztimes (neg n) z)).
212 rewrite > Ztimes_neg_Zopp.
213 rewrite > distr_Ztimes_Zplus_pos.
214 rewrite > Zopp_Zplus.
215 rewrite < Ztimes_neg_Zopp. rewrite < Ztimes_neg_Zopp.
219 variant distr_Ztimes_Zplus_neg: \forall n,y,z.
220 eq Z (Ztimes (neg n) (Zplus y z)) (Zplus (Ztimes (neg n) y) (Ztimes (neg n) z)) \def
221 distributive2_Ztimes_neg_Zplus.
223 theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus.
224 change with \forall x,y,z:Z.
225 eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)).
228 simplify.reflexivity.
230 apply distr_Ztimes_Zplus_neg.
232 apply distr_Ztimes_Zplus_pos.
235 variant distr_Ztimes_Zplus: \forall x,y,z.
236 eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)) \def
237 distributive_Ztimes_Zplus.