X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Fplus.ma;h=976f6cfb3ce01d379244fc66ec964a99563917d3;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=d2e6ec2b0d2dbe7357814a810d649761b44a4194;hpb=92140306286b05521c7cc49e75c4dae194ccbb52;p=helm.git diff --git a/helm/matita/library/Z/plus.ma b/helm/matita/library/Z/plus.ma index d2e6ec2b0..976f6cfb3 100644 --- a/helm/matita/library/Z/plus.ma +++ b/helm/matita/library/Z/plus.ma @@ -15,7 +15,6 @@ set "baseuri" "cic:/matita/Z/plus". include "Z/z.ma". -include "nat/compare.ma". include "nat/minus.ma". definition Zplus :Z \to Z \to Z \def @@ -30,7 +29,7 @@ definition Zplus :Z \to Z \to Z \def match nat_compare m n with [ LT \Rightarrow (neg (pred (n-m))) | EQ \Rightarrow OZ - | GT \Rightarrow (pos (pred (m-n)))]] + | GT \Rightarrow (pos (pred (m-n)))] ] | (neg m) \Rightarrow match y with [ OZ \Rightarrow x @@ -39,7 +38,7 @@ definition Zplus :Z \to Z \to Z \def [ LT \Rightarrow (pos (pred (n-m))) | EQ \Rightarrow OZ | GT \Rightarrow (neg (pred (m-n)))] - | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))]]. + | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))] ]. (*CSC: the URI must disappear: there is a bug now *) interpretation "integer plus" 'plus x y = (cic:/matita/Z/plus/Zplus.con x y). @@ -60,12 +59,12 @@ simplify. rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity. simplify. rewrite > nat_compare_n_m_m_n. -simplify.elim nat_compare ? ?.simplify.reflexivity. +simplify.elim nat_compare.simplify.reflexivity. simplify. reflexivity. simplify. reflexivity. elim y.simplify.reflexivity. simplify.rewrite > nat_compare_n_m_m_n. -simplify.elim nat_compare ? ?.simplify.reflexivity. +simplify.elim nat_compare.simplify.reflexivity. simplify. reflexivity. simplify. reflexivity. simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity. @@ -73,18 +72,20 @@ qed. theorem Zpred_Zplus_neg_O : \forall z:Z. Zpred z = (neg O)+z. intros.elim z. -simplify.reflexivity. -simplify.reflexivity. -elim n.simplify.reflexivity. -simplify.reflexivity. + simplify.reflexivity. + elim n. + simplify.reflexivity. + simplify.reflexivity. + simplify.reflexivity. qed. theorem Zsucc_Zplus_pos_O : \forall z:Z. Zsucc z = (pos O)+z. intros.elim z. -simplify.reflexivity. -elim n.simplify.reflexivity. -simplify.reflexivity. -simplify.reflexivity. + simplify.reflexivity. + simplify.reflexivity. + elim n. + simplify.reflexivity. + simplify.reflexivity. qed. theorem Zplus_pos_pos: @@ -129,21 +130,20 @@ qed. theorem Zplus_Zsucc_Zpred: \forall x,y. x+y = (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. +intros.elim x. + elim y. + simplify.reflexivity. + rewrite < Zsucc_Zplus_pos_O.rewrite > Zsucc_Zpred.reflexivity. + simplify.reflexivity. + elim y. + simplify.reflexivity. + apply Zplus_pos_pos. + apply Zplus_pos_neg. + elim y. + rewrite < sym_Zplus.rewrite < (sym_Zplus (Zpred OZ)). + rewrite < Zpred_Zplus_neg_O.rewrite > Zpred_Zsucc.simplify.reflexivity. + apply Zplus_neg_pos. + rewrite < Zplus_neg_neg.reflexivity. qed. theorem Zplus_Zsucc_pos_pos : @@ -154,8 +154,8 @@ qed. theorem Zplus_Zsucc_pos_neg: \forall n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))). intros. -apply nat_elim2 -(\lambda n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))).intro. +apply (nat_elim2 +(\lambda n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))))).intro. intros.elim n1. simplify. reflexivity. elim n2.simplify. reflexivity. @@ -169,10 +169,10 @@ elim H.reflexivity. qed. theorem Zplus_Zsucc_neg_neg : -\forall n,m. (Zsucc (neg n))+(neg m) = Zsucc ((neg n)+(neg m)). +\forall n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m). intros. -apply nat_elim2 -(\lambda n,m. ((Zsucc (neg n))+(neg m)) = Zsucc ((neg n)+(neg m))).intro. +apply (nat_elim2 +(\lambda n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m))).intro. intros.elim n1. simplify. reflexivity. elim n2.simplify. reflexivity. @@ -188,8 +188,8 @@ qed. theorem Zplus_Zsucc_neg_pos: \forall n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)). intros. -apply nat_elim2 -(\lambda n,m. (Zsucc (neg n))+(pos m) = Zsucc ((neg n)+(pos m))). +apply (nat_elim2 +(\lambda n,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m))). intros.elim n1. simplify. reflexivity. elim n2.simplify. reflexivity. @@ -204,22 +204,24 @@ reflexivity. qed. theorem Zplus_Zsucc : \forall x,y:Z. (Zsucc x)+y = Zsucc (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. +intros.elim x. + elim y. + simplify. reflexivity. + simplify.reflexivity. + rewrite < Zsucc_Zplus_pos_O.reflexivity. + elim y. + rewrite < (sym_Zplus OZ).reflexivity. + apply Zplus_Zsucc_pos_pos. + apply Zplus_Zsucc_pos_neg. + elim y. + rewrite < sym_Zplus.rewrite < (sym_Zplus OZ).simplify.reflexivity. + apply Zplus_Zsucc_neg_pos. + apply Zplus_Zsucc_neg_neg. qed. theorem Zplus_Zpred: \forall x,y:Z. (Zpred x)+y = Zpred (x+y). intros. -cut Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y). +cut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y)). rewrite > Hcut. rewrite > Zplus_Zsucc. rewrite > Zpred_Zsucc. @@ -230,25 +232,20 @@ qed. theorem associative_Zplus: associative Z Zplus. -change with \forall x,y,z:Z. (x + y) + z = x + (y + z). +change with (\forall x,y,z:Z. (x + y) + z = x + (y + z)). (* simplify. *) -intros.elim x.simplify.reflexivity. -elim n.rewrite < (Zpred_Zplus_neg_O (y+z)). -rewrite < (Zpred_Zplus_neg_O y). -rewrite < Zplus_Zpred. -reflexivity. -rewrite > Zplus_Zpred (neg n1). -rewrite > Zplus_Zpred (neg n1). -rewrite > Zplus_Zpred ((neg n1)+y). -apply eq_f.assumption. -elim n.rewrite < Zsucc_Zplus_pos_O. -rewrite < Zsucc_Zplus_pos_O. -rewrite > Zplus_Zsucc. -reflexivity. -rewrite > Zplus_Zsucc (pos n1). -rewrite > Zplus_Zsucc (pos n1). -rewrite > Zplus_Zsucc ((pos n1)+y). -apply eq_f.assumption. +intros.elim x. + simplify.reflexivity. + elim n. + rewrite < Zsucc_Zplus_pos_O.rewrite < Zsucc_Zplus_pos_O. + rewrite > Zplus_Zsucc.reflexivity. + rewrite > (Zplus_Zsucc (pos n1)).rewrite > (Zplus_Zsucc (pos n1)). + rewrite > (Zplus_Zsucc ((pos n1)+y)).apply eq_f.assumption. + elim n. + rewrite < (Zpred_Zplus_neg_O (y+z)).rewrite < (Zpred_Zplus_neg_O y). + rewrite < Zplus_Zpred.reflexivity. + rewrite > (Zplus_Zpred (neg n1)).rewrite > (Zplus_Zpred (neg n1)). + rewrite > (Zplus_Zpred ((neg n1)+y)).apply eq_f.assumption. qed. variant assoc_Zplus : \forall x,y,z:Z. (x+y)+z = x+(y+z)