X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Ftimes.ma;h=e5e1cdb452fa38ce33a8ba73f95b6ca4a5d5f27d;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=7e4b10e0028428b64f7809329eb430f9123ac37e;hpb=7bbce6bc163892cfd99cfcda65db42001b86789f;p=helm.git diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma index 7e4b10e00..e5e1cdb45 100644 --- a/helm/matita/library/Z/times.ma +++ b/helm/matita/library/Z/times.ma @@ -15,7 +15,7 @@ set "baseuri" "cic:/matita/Z/times". include "nat/lt_arith.ma". -include "Z/z.ma". +include "Z/plus.ma". definition Ztimes :Z \to Z \to Z \def \lambda x,y. @@ -24,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). @@ -42,186 +42,194 @@ simplify.reflexivity. simplify.reflexivity. qed. +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)). -intros. -elim x.simplify.reflexivity. -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. -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. -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. -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. -apply lt_O_times_S_S. -apply lt_O_times_S_S. -elim y.simplify.reflexivity. -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. -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. -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. -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. -apply lt_O_times_S_S. -apply lt_O_times_S_S. +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. -eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)) \def +(x * y) * z = x * (y * z) \def associative_Ztimes. - -theorem distributive_Ztimes: 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)). -intros.elim x. -simplify.reflexivity. -(* case x = neg n *) -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))))). -rewrite < times_plus_distr.reflexivity. -simplify. (* problemi di naming su n *) -(* sintassi della change ??? *) -cut \forall n,m:nat.eq nat (plus m (times n (S m))) (pred (times (S n) (S m))). -rewrite > Hcut. -rewrite > Hcut. -rewrite < nat_compare_pred_pred ? ? ? ?. -rewrite < nat_compare_times_l. -rewrite < nat_compare_S_S. -apply nat_compare_elim n1 n2. -intro. -(* per ricavare questo change ci ho messo un'ora; -LA GESTIONE DELLA RIDUZIONE NON VA *) -change with (eq Z (neg (pred (times (S n) (S (pred (minus (S n2) (S n1))))))) - (neg (pred (minus (pred (times (S n) (S n2))) - (pred (times (S n) (S n1))))))). -rewrite < S_pred ? ?. -rewrite > minus_pred_pred ? ? ? ?. -rewrite < distr_times_minus. -reflexivity. -(* we start closing stupid positivity conditions *) -apply lt_O_times_S_S. -apply lt_O_times_S_S. -simplify. -apply le_SO_minus. exact H. -intro.rewrite < H.simplify.reflexivity. -intro. -change with (eq Z (pos (pred (times (S n) (S (pred (minus (S n1) (S n2))))))) - (pos (pred (minus (pred (times (S n) (S n1))) - (pred (times (S n) (S n2))))))). -rewrite < S_pred ? ?. -rewrite > minus_pred_pred ? ? ? ?. +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 < S_pred. +rewrite > minus_pred_pred. rewrite < distr_times_minus. -reflexivity. -(* we start closing stupid positivity conditions *) +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. -(* questi non so neppure da dove vengano *) -apply lt_O_times_S_S. -apply lt_O_times_S_S. -(* adesso chiudo il cut stupido *) -intros.reflexivity. -elim z.reflexivity. -simplify. -cut \forall n,m:nat.eq nat (plus m (times n (S m))) (pred (times (S n) (S m))). -rewrite > Hcut. -rewrite > Hcut. -rewrite < nat_compare_pred_pred ? ? ? ?. +qed. + +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. +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 n1 n2. +apply (nat_compare_elim p q). intro. -(* per ricavare questo change ci ho messo un'ora; -LA GESTIONE DELLA RIDUZIONE NON VA *) -change with (eq Z (pos (pred (times (S n) (S (pred (minus (S n2) (S n1))))))) - (pos (pred (minus (pred (times (S n) (S n2))) - (pred (times (S n) (S n1))))))). -rewrite < S_pred ? ?. -rewrite > minus_pred_pred ? ? ? ?. -rewrite < distr_times_minus. -reflexivity. -(* we start closing stupid positivity conditions *) -apply lt_O_times_S_S. -apply lt_O_times_S_S. -simplify. -apply le_SO_minus. exact H. +(* 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 (eq Z (neg (pred (times (S n) (S (pred (minus (S n1) (S n2))))))) - (neg (pred (minus (pred (times (S n) (S n1))) - (pred (times (S n) (S n2))))))). -rewrite < S_pred ? ?. -rewrite > minus_pred_pred ? ? ? ?. -rewrite < distr_times_minus. -reflexivity. -(* we start closing stupid positivity conditions *) -apply lt_O_times_S_S. -apply lt_O_times_S_S. -simplify. -apply le_SO_minus. exact H. -(* questi non so neppure da dove vengano *) -apply lt_O_times_S_S. +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. -(* adesso chiudo il cut stupido *) -intros.reflexivity. -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))))). -rewrite < times_plus_distr. +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 < 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. +rewrite > Ztimes_neg_Zopp. +rewrite > distr_Ztimes_Zplus_pos. +rewrite > Zopp_Zplus. +rewrite < Ztimes_neg_Zopp. rewrite < Ztimes_neg_Zopp. reflexivity. -(* and now the case x = pos n *) +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 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 distr_Ztimes_Zplus: \forall x,y,z. +x * (y + z) = x*y + x*z \def +distributive_Ztimes_Zplus.