X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Ftimes.ma;h=e5e1cdb452fa38ce33a8ba73f95b6ca4a5d5f27d;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=1352988df32cd32d2dcf77699db265a8c4f4c523;hpb=c12d08acf947823bbfd5909618b042c65ff107de;p=helm.git diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma index 1352988df..e5e1cdb45 100644 --- a/helm/matita/library/Z/times.ma +++ b/helm/matita/library/Z/times.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* __ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) @@ -14,7 +14,8 @@ set "baseuri" "cic:/matita/Z/times". -include "Z/z.ma". +include "nat/lt_arith.ma". +include "Z/plus.ma". definition Ztimes :Z \to Z \to Z \def \lambda x,y. @@ -23,13 +24,13 @@ definition Ztimes :Z \to Z \to Z \def | (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). @@ -41,217 +42,194 @@ simplify.reflexivity. simplify.reflexivity. qed. -(*CSC: da qui in avanti niente notazione *) -(* +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 e1) (S e)))) (pos (pred (times (S e) (S e1)))). +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 e1) (S e2)))) (neg (pred (times (S e2) (S e1)))). +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 e2) (S e1)))) (neg (pred (times (S e1) (S e2)))). +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 e2) (S e)))) (pos (pred (times (S e) (S e2)))). +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)). -intros. -elim x.simplify.reflexivity. -elim y.simplify.reflexivity. -elim z.simplify.reflexivity. -change with -eq Z (neg (pred (times (S (pred (times (S e1) (S e)))) (S e2)))) - (neg (pred (times (S e1) (S (pred (times (S e) (S e2))))))). -rewrite < S_pred_S. - -theorem Zpred_Zplus_neg_O : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z). -intros.elim z. -simplify.reflexivity. -simplify.reflexivity. -elim e2.simplify.reflexivity. -simplify.reflexivity. -qed. - -theorem Zsucc_Zplus_pos_O : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z). -intros.elim z. -simplify.reflexivity. -elim e1.simplify.reflexivity. -simplify.reflexivity. -simplify.reflexivity. -qed. - -theorem Zplus_pos_pos: -\forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))). -intros. -elim n.elim m. -simplify.reflexivity. -simplify.reflexivity. -elim m. -simplify. -rewrite < plus_n_O.reflexivity. -simplify. -rewrite < plus_n_Sm.reflexivity. -qed. - -theorem Zplus_pos_neg: -\forall n,m. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))). -intros.reflexivity. -qed. - -theorem Zplus_neg_pos : -\forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (Zsucc (neg n)) (Zpred (pos m))). -intros. -elim n.elim m. -simplify.reflexivity. -simplify.reflexivity. -elim m. -simplify.reflexivity. -simplify.reflexivity. -qed. - -theorem Zplus_neg_neg: -\forall n,m. eq Z (Zplus (neg n) (neg m)) (Zplus (Zsucc (neg n)) (Zpred (neg m))). -intros. -elim n.elim m. -simplify.reflexivity. -simplify.reflexivity. -elim m. -simplify.rewrite < plus_n_Sm.reflexivity. -simplify.rewrite > plus_n_Sm.reflexivity. -qed. - -theorem Zplus_Zsucc_Zpred: -\forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)). -intros. -elim x. elim y. -simplify.reflexivity. -simplify.reflexivity. -rewrite < Zsucc_Zplus_pos_O. -rewrite > Zsucc_Zpred.reflexivity. -elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ). -rewrite < Zpred_Zplus_neg_O. -rewrite > Zpred_Zsucc. -simplify.reflexivity. -rewrite < Zplus_neg_neg.reflexivity. -apply Zplus_neg_pos. -elim y.simplify.reflexivity. -apply Zplus_pos_neg. -apply Zplus_pos_pos. -qed. - -theorem Zplus_Zsucc_pos_pos : -\forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))). -intros.reflexivity. -qed. - -theorem Zplus_Zsucc_pos_neg: -\forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))). -intros. -apply nat_elim2 -(\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro. -intros.elim n1. -simplify. reflexivity. -elim e1.simplify. reflexivity. -simplify. reflexivity. -intros. elim n1. -simplify. reflexivity. -simplify.reflexivity. -intros. -rewrite < (Zplus_pos_neg ? m1). -elim H.reflexivity. -qed. - -theorem Zplus_Zsucc_neg_neg : -\forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))). -intros. -apply nat_elim2 -(\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro. -intros.elim n1. -simplify. reflexivity. -elim e1.simplify. reflexivity. -simplify. reflexivity. -intros. elim n1. -simplify. reflexivity. -simplify.reflexivity. +change with (\forall x,y,z:Z. (x*y)*z = x*(y*z)). +intros.elim x. + simplify.reflexivity. + elim y. + simplify.reflexivity. + elim z. + simplify.reflexivity. + change with + (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 + (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 + (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 + (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 + (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 + (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 + (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 + (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. +(x * y) * z = x * (y * z) \def +associative_Ztimes. + +lemma times_minus1: \forall n,p,q:nat. lt q p \to +(S n) * (S (pred ((S p) - (S q)))) = +pred ((S n) * (S p)) - pred ((S n) * (S q)). intros. -rewrite < (Zplus_neg_neg ? m1). +rewrite < S_pred. +rewrite > minus_pred_pred. +rewrite < distr_times_minus. reflexivity. +(* we now close all positivity conditions *) +apply lt_O_times_S_S. +apply lt_O_times_S_S. +simplify.unfold lt. +apply le_SO_minus. exact H. qed. -theorem Zplus_Zsucc_neg_pos: -\forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))). +lemma Ztimes_Zplus_pos_neg_pos: \forall n,p,q:nat. +(pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q). intros. -apply nat_elim2 -(\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))). -intros.elim n1. -simplify. reflexivity. -elim e1.simplify. reflexivity. -simplify. reflexivity. -intros. elim n1. -simplify. reflexivity. -simplify.reflexivity. +simplify. +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). +intro. +(* uff *) +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 (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 Ztimes_Zplus_pos_pos_neg: \forall n,p,q:nat. +(pos n)*((pos p)+(neg q)) = (pos n)*(pos p)+ (pos n)*(neg q). intros. -rewrite < H. -rewrite < (Zplus_neg_pos ? (S m1)). -reflexivity. -qed. - -theorem Zplus_Zsucc : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)). -intros.elim x.elim y. -simplify. reflexivity. -rewrite < Zsucc_Zplus_pos_O.reflexivity. -simplify.reflexivity. -elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity. -apply Zplus_Zsucc_neg_neg. -apply Zplus_Zsucc_neg_pos. -elim y. -rewrite < sym_Zplus OZ.reflexivity. -apply Zplus_Zsucc_pos_neg. -apply Zplus_Zsucc_pos_pos. -qed. - -theorem Zplus_Zpred: \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)). +rewrite < sym_Zplus. +rewrite > Ztimes_Zplus_pos_neg_pos. +apply sym_Zplus. +qed. + +lemma distributive2_Ztimes_pos_Zplus: +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 + (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 + (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. +(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. (neg n) * z) Zplus. +change with (\forall n,y,z. +(neg n) * (y + z) = (neg n) * y + (neg n) * z). intros. -cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)). -rewrite > Hcut. -rewrite > Zplus_Zsucc. -rewrite > Zpred_Zsucc. -reflexivity. -rewrite > Zsucc_Zpred. +rewrite > Ztimes_neg_Zopp. +rewrite > distr_Ztimes_Zplus_pos. +rewrite > Zopp_Zplus. +rewrite < Ztimes_neg_Zopp. rewrite < Ztimes_neg_Zopp. reflexivity. qed. +variant distr_Ztimes_Zplus_neg: \forall n,y,z. +(neg n) * (y + z) = (neg n) * y + (neg n) * z \def +distributive2_Ztimes_neg_Zplus. -theorem associative_Zplus: associative Z Zplus. -change with \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)). - -intros.elim x.simplify.reflexivity. -elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)). -rewrite < (Zpred_Zplus_neg_O y). -rewrite < Zplus_Zpred. -reflexivity. -rewrite > Zplus_Zpred (neg e). -rewrite > Zplus_Zpred (neg e). -rewrite > Zplus_Zpred (Zplus (neg e) y). -apply eq_f.assumption. -elim e2.rewrite < Zsucc_Zplus_pos_O. -rewrite < Zsucc_Zplus_pos_O. -rewrite > Zplus_Zsucc. -reflexivity. -rewrite > Zplus_Zsucc (pos e1). -rewrite > Zplus_Zsucc (pos e1). -rewrite > Zplus_Zsucc (Zplus (pos e1) y). -apply eq_f.assumption. +theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus. +change with (\forall x,y,z:Z. x * (y + z) = x*y + x*z). +intros.elim x. +(* case x = OZ *) +simplify.reflexivity. +(* case x = pos n *) +apply distr_Ztimes_Zplus_pos. +(* case x = neg n *) +apply distr_Ztimes_Zplus_neg. qed. -variant assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)) -\def associative_Zplus. -*) +variant distr_Ztimes_Zplus: \forall x,y,z. +x * (y + z) = x*y + x*z \def +distributive_Ztimes_Zplus.