| (pos m) \Rightarrow
match y with
[ OZ \Rightarrow OZ
- | (pos n) \Rightarrow (pos (pred (times (S m) (S n))))
- | (neg n) \Rightarrow (neg (pred (times (S m) (S n))))]
+ | (pos n) \Rightarrow (pos (pred ((S m) * (S n))))
+ | (neg n) \Rightarrow (neg (pred ((S m) * (S n))))]
| (neg m) \Rightarrow
match y with
[ OZ \Rightarrow OZ
- | (pos n) \Rightarrow (neg (pred (times (S m) (S n))))
- | (neg n) \Rightarrow (pos (pred (times (S m) (S n))))]].
+ | (pos n) \Rightarrow (neg (pred ((S m) * (S n))))
+ | (neg n) \Rightarrow (pos (pred ((S m) * (S n))))]].
(*CSC: the URI must disappear: there is a bug now *)
interpretation "integer times" 'times x y = (cic:/matita/Z/times/Ztimes.con x y).
simplify.reflexivity.
qed.
-theorem Ztimes_neg_Zopp: \forall n:nat.\forall x:Z.
-eq Z (Ztimes (neg n) x) (Zopp (Ztimes (pos n) x)).
+theorem Ztimes_neg_Zopp: \forall n:nat.\forall x:Z.
+neg n * x = - (pos n * x).
intros.elim x.
simplify.reflexivity.
simplify.reflexivity.
simplify.reflexivity.
qed.
theorem symmetric_Ztimes : symmetric Z Ztimes.
-change with \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x).
+change with (\forall x,y:Z. x*y = y*x).
intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
elim y.simplify.reflexivity.
-change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
+change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
rewrite < sym_times.reflexivity.
-change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
+change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
rewrite < sym_times.reflexivity.
elim y.simplify.reflexivity.
-change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
+change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
rewrite < sym_times.reflexivity.
-change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
+change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
rewrite < sym_times.reflexivity.
qed.
-variant sym_Ztimes : \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x)
+variant sym_Ztimes : \forall x,y:Z. x*y = y*x
\def symmetric_Ztimes.
theorem associative_Ztimes: associative Z Ztimes.
-change with \forall x,y,z:Z.eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)).
+change with (\forall x,y,z:Z. (x*y)*z = x*(y*z)).
intros.elim x.
simplify.reflexivity.
elim y.
elim z.
simplify.reflexivity.
change with
- eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
- rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
change with
- eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
- rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
elim z.
simplify.reflexivity.
change with
- eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
- rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
change with
- eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
- rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ pos(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
elim y.
simplify.reflexivity.
elim z.
simplify.reflexivity.
change with
- eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
- rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
change with
- eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
- rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
elim z.
simplify.reflexivity.
change with
- eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
- rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
change with
- eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
- rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ neg(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
qed.
variant assoc_Ztimes : \forall x,y,z:Z.
-eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)) \def
+(x * y) * z = x * (y * z) \def
associative_Ztimes.
lemma times_minus1: \forall n,p,q:nat. lt q p \to
-eq nat (times (S n) (S (pred (minus (S p) (S q)))))
- (minus (pred (times (S n) (S p)))
- (pred (times (S n) (S q)))).
+(S n) * (S (pred ((S p) - (S q)))) =
+pred ((S n) * (S p)) - pred ((S n) * (S q)).
intros.
-rewrite < S_pred ? ?.
-rewrite > minus_pred_pred ? ? ? ?.
+rewrite < S_pred.
+rewrite > minus_pred_pred.
rewrite < distr_times_minus.
-reflexivity.
+reflexivity.
(* we now close all positivity conditions *)
apply lt_O_times_S_S.
apply lt_O_times_S_S.
-simplify.
+simplify.unfold lt.
apply le_SO_minus. exact H.
qed.
(pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q).
intros.
simplify.
-change in match (plus p (times n (S p))) with (pred (times (S n) (S p))).
-change in match (plus q (times n (S q))) with (pred (times (S n) (S q))).
-rewrite < nat_compare_pred_pred ? ? ? ?.
+change in match (p + n * (S p)) with (pred ((S n) * (S p))).
+change in match (q + n * (S q)) with (pred ((S n) * (S q))).
+rewrite < nat_compare_pred_pred.
rewrite < nat_compare_times_l.
rewrite < nat_compare_S_S.
-apply nat_compare_elim p q.
+apply (nat_compare_elim p q).
intro.
(* uff *)
-change with (eq Z (pos (pred (times (S n) (S (pred (minus (S q) (S p)))))))
- (pos (pred (minus (pred (times (S n) (S q)))
- (pred (times (S n) (S p))))))).
-rewrite < times_minus1 n q p H.reflexivity.
+change with (pos (pred ((S n) * (S (pred ((S q) - (S p)))))) =
+ pos (pred ((pred ((S n) * (S q))) - (pred ((S n) * (S p)))))).
+rewrite < (times_minus1 n q p H).reflexivity.
intro.rewrite < H.simplify.reflexivity.
intro.
-change with (eq Z (neg (pred (times (S n) (S (pred (minus (S p) (S q)))))))
- (neg (pred (minus (pred (times (S n) (S p)))
- (pred (times (S n) (S q))))))).
-rewrite < times_minus1 n p q H.reflexivity.
+change with (neg (pred ((S n) * (S (pred ((S p) - (S q)))))) =
+ neg (pred ((pred ((S n) * (S p))) - (pred ((S n) * (S q)))))).
+rewrite < (times_minus1 n p q H).reflexivity.
(* two more positivity conditions from nat_compare_pred_pred *)
apply lt_O_times_S_S.
apply lt_O_times_S_S.
qed.
lemma distributive2_Ztimes_pos_Zplus:
-distributive2 nat Z (\lambda n,z. Ztimes (pos n) z) Zplus.
-change with \forall n,y,z.
-eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)).
+distributive2 nat Z (\lambda n,z. (pos n) * z) Zplus.
+change with (\forall n,y,z.
+(pos n) * (y + z) = (pos n) * y + (pos n) * z).
intros.elim y.
reflexivity.
elim z.
reflexivity.
change with
- eq Z (pos (pred (times (S n) (plus (S n1) (S n2)))))
- (pos (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
+ (pos (pred ((S n) * ((S n1) + (S n2)))) =
+ pos (pred ((S n) * (S n1) + (S n) * (S n2)))).
rewrite < distr_times_plus.reflexivity.
apply Ztimes_Zplus_pos_pos_neg.
elim z.
reflexivity.
apply Ztimes_Zplus_pos_neg_pos.
change with
- eq Z (neg (pred (times (S n) (plus (S n1) (S n2)))))
- (neg (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
+ (neg (pred ((S n) * ((S n1) + (S n2)))) =
+ neg (pred ((S n) * (S n1) + (S n) * (S n2)))).
rewrite < distr_times_plus.reflexivity.
qed.
variant distr_Ztimes_Zplus_pos: \forall n,y,z.
-eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)) \def
+(pos n) * (y + z) = ((pos n) * y + (pos n) * z) \def
distributive2_Ztimes_pos_Zplus.
lemma distributive2_Ztimes_neg_Zplus :
-distributive2 nat Z (\lambda n,z. Ztimes (neg n) z) Zplus.
-change with \forall n,y,z.
-eq Z (Ztimes (neg n) (Zplus y z)) (Zplus (Ztimes (neg n) y) (Ztimes (neg n) z)).
+distributive2 nat Z (\lambda n,z. (neg n) * z) Zplus.
+change with (\forall n,y,z.
+(neg n) * (y + z) = (neg n) * y + (neg n) * z).
intros.
rewrite > Ztimes_neg_Zopp.
rewrite > distr_Ztimes_Zplus_pos.
qed.
variant distr_Ztimes_Zplus_neg: \forall n,y,z.
-eq Z (Ztimes (neg n) (Zplus y z)) (Zplus (Ztimes (neg n) y) (Ztimes (neg n) z)) \def
+(neg n) * (y + z) = (neg n) * y + (neg n) * z \def
distributive2_Ztimes_neg_Zplus.
theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus.
-change with \forall x,y,z:Z.
-eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)).
+change with (\forall x,y,z:Z. x * (y + z) = x*y + x*z).
intros.elim x.
(* case x = OZ *)
simplify.reflexivity.
qed.
variant distr_Ztimes_Zplus: \forall x,y,z.
-eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)) \def
-distributive_Ztimes_Zplus.
\ No newline at end of file
+x * (y + z) = x*y + x*z \def
+distributive_Ztimes_Zplus.