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".
20 definition Ztimes :Z \to Z \to Z \def
27 | (pos n) \Rightarrow (pos (pred (times (S m) (S n))))
28 | (neg n) \Rightarrow (neg (pred (times (S m) (S n))))]
32 | (pos n) \Rightarrow (neg (pred (times (S m) (S n))))
33 | (neg n) \Rightarrow (pos (pred (times (S m) (S n))))]].
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).
38 theorem Ztimes_z_OZ: \forall z:Z. z*OZ = OZ.
45 theorem symmetric_Ztimes : symmetric Z Ztimes.
46 change with \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x).
47 intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
48 elim y.simplify.reflexivity.
49 change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
50 rewrite < sym_times.reflexivity.
51 change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
52 rewrite < sym_times.reflexivity.
53 elim y.simplify.reflexivity.
54 change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
55 rewrite < sym_times.reflexivity.
56 change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
57 rewrite < sym_times.reflexivity.
60 variant sym_Ztimes : \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x)
61 \def symmetric_Ztimes.
63 theorem associative_Ztimes: associative Z Ztimes.
64 change with \forall x,y,z:Z.eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)).
66 elim x.simplify.reflexivity.
67 elim y.simplify.reflexivity.
68 elim z.simplify.reflexivity.
70 eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
71 (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
72 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
76 eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
77 (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
78 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
79 apply lt_O_times_S_S.apply lt_O_times_S_S.
80 elim z.simplify.reflexivity.
82 eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
83 (pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
84 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
85 apply lt_O_times_S_S.apply lt_O_times_S_S.
87 eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
88 (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
89 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
92 elim y.simplify.reflexivity.
93 elim z.simplify.reflexivity.
95 eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
96 (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
97 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
101 eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
102 (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
103 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
104 apply lt_O_times_S_S.apply lt_O_times_S_S.
105 elim z.simplify.reflexivity.
107 eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
108 (neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
109 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
110 apply lt_O_times_S_S.apply lt_O_times_S_S.
112 eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
113 (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
114 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
115 apply lt_O_times_S_S.
116 apply lt_O_times_S_S.
119 variant assoc_Ztimes : \forall x,y,z:Z.
120 eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)) \def
124 theorem distributive_Ztimes: distributive Z Ztimes Zplus.
125 change with \forall x,y,z:Z.
126 eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)).
128 simplify.reflexivity.
133 eq Z (pos (pred (times (S n) (plus (S n1) (S n2)))))
134 (pos (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
135 rewrite < times_plus_distr.reflexivity.
136 simplify. (* problemi di naming su n *)
137 (* sintassi della change ??? *)
138 cut \forall n,m:nat.eq nat (plus m (times n (S m))) (pred (times (S n) (S m))).
141 rewrite < nat_compare_pred_pred ? ? ? ?.
142 rewrite < nat_compare_times_l.
143 rewrite < nat_compare_S_S.
144 apply nat_compare_elim n1 n2.
146 (* per ricavare questo change ci ho messo un'ora;
147 LA GESTIONE DELLA RIDUZIONE NON VA *)
148 change with (eq Z (neg (pred (times (S n) (S (pred (minus (S n2) (S n1)))))))
149 (neg (pred (minus (pred (times (S n) (S n2)))
150 (pred (times (S n) (S n1))))))).
151 rewrite < S_pred ? ?.
152 rewrite > minus_pred_pred ? ? ? ?.
153 rewrite < distr_times_minus.
155 (* we start closing stupid positivity conditions *)
156 apply lt_O_times_S_S.
157 apply lt_O_times_S_S.
159 apply le_SO_minus. exact H.
160 intro.rewrite < H.simplify.reflexivity.
162 change with (eq Z (pos (pred (times (S n) (S (pred (minus (S n1) (S n2)))))))
163 (pos (pred (minus (pred (times (S n) (S n1)))
164 (pred (times (S n) (S n2))))))).
165 rewrite < S_pred ? ?.
166 rewrite > minus_pred_pred ? ? ? ?.
167 rewrite < distr_times_minus.
169 (* we start closing stupid positivity conditions *)
170 apply lt_O_times_S_S.
171 apply lt_O_times_S_S.
173 apply le_SO_minus. exact H.
174 (* questi non so neppure da dove vengano *)
175 apply lt_O_times_S_S.
176 apply lt_O_times_S_S.
177 (* adesso chiudo il cut stupido *)
181 cut \forall n,m:nat.eq nat (plus m (times n (S m))) (pred (times (S n) (S m))).
184 rewrite < nat_compare_pred_pred ? ? ? ?.
185 rewrite < nat_compare_times_l.
186 rewrite < nat_compare_S_S.
187 apply nat_compare_elim n1 n2.
189 (* per ricavare questo change ci ho messo un'ora;
190 LA GESTIONE DELLA RIDUZIONE NON VA *)
191 change with (eq Z (pos (pred (times (S n) (S (pred (minus (S n2) (S n1)))))))
192 (pos (pred (minus (pred (times (S n) (S n2)))
193 (pred (times (S n) (S n1))))))).
194 rewrite < S_pred ? ?.
195 rewrite > minus_pred_pred ? ? ? ?.
196 rewrite < distr_times_minus.
198 (* we start closing stupid positivity conditions *)
199 apply lt_O_times_S_S.
200 apply lt_O_times_S_S.
202 apply le_SO_minus. exact H.
203 intro.rewrite < H.simplify.reflexivity.
205 change with (eq Z (neg (pred (times (S n) (S (pred (minus (S n1) (S n2)))))))
206 (neg (pred (minus (pred (times (S n) (S n1)))
207 (pred (times (S n) (S n2))))))).
208 rewrite < S_pred ? ?.
209 rewrite > minus_pred_pred ? ? ? ?.
210 rewrite < distr_times_minus.
212 (* we start closing stupid positivity conditions *)
213 apply lt_O_times_S_S.
214 apply lt_O_times_S_S.
216 apply le_SO_minus. exact H.
217 (* questi non so neppure da dove vengano *)
218 apply lt_O_times_S_S.
219 apply lt_O_times_S_S.
220 (* adesso chiudo il cut stupido *)
223 eq Z (neg (pred (times (S n) (plus (S n1) (S n2)))))
224 (neg (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
225 rewrite < times_plus_distr.
227 (* and now the case x = pos n *)