X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Fz.ma;h=cdc0e44d7c28f29fb01681a6d2b52a139a2955d0;hb=f981a524748846acc29b76b6e616af110b4ee13d;hp=11dd836f667b6ed884753f80ec88ac86e731e8d7;hpb=2b061073ed17c537a6ea969960e5a3038ed30d05;p=helm.git diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma index 11dd836f6..cdc0e44d7 100644 --- a/helm/matita/library/Z/z.ma +++ b/helm/matita/library/Z/z.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/Z/". +set "baseuri" "cic:/matita/Z/z". include "nat/compare.ma". include "nat/minus.ma". @@ -51,18 +51,18 @@ match z with theorem OZ_test_to_Prop :\forall z:Z. match OZ_test z with -[true \Rightarrow eq Z z OZ -|false \Rightarrow Not (eq Z z OZ)]. +[true \Rightarrow z=OZ +|false \Rightarrow \lnot (z=OZ)]. intros.elim z. simplify.reflexivity. simplify.intros. -cut match neg e1 with +cut match neg n with [ OZ \Rightarrow True | (pos n) \Rightarrow False | (neg n) \Rightarrow False]. apply Hcut.rewrite > H.simplify.exact I. simplify.intros. -cut match pos e2 with +cut match pos n with [ OZ \Rightarrow True | (pos n) \Rightarrow False | (neg n) \Rightarrow False]. @@ -87,17 +87,17 @@ definition Zpred \def | (S p) \Rightarrow pos p] | (neg n) \Rightarrow neg (S n)]. -theorem Zpred_Zsucc: \forall z:Z. eq Z (Zpred (Zsucc z)) z. +theorem Zpred_Zsucc: \forall z:Z. Zpred (Zsucc z) = z. intros.elim z.reflexivity. -elim e1.reflexivity. +elim n.reflexivity. reflexivity. reflexivity. qed. -theorem Zsucc_Zpred: \forall z:Z. eq Z (Zsucc (Zpred z)) z. +theorem Zsucc_Zpred: \forall z:Z. Zsucc (Zpred z) = z. intros.elim z.reflexivity. reflexivity. -elim e2.reflexivity. +elim n.reflexivity. reflexivity. qed. @@ -108,23 +108,26 @@ definition Zplus :Z \to Z \to Z \def | (pos m) \Rightarrow match y with [ OZ \Rightarrow x - | (pos n) \Rightarrow (pos (S (plus m n))) + | (pos n) \Rightarrow (pos (pred ((S m)+(S n)))) | (neg n) \Rightarrow match nat_compare m n with - [ LT \Rightarrow (neg (pred (minus n m))) + [ LT \Rightarrow (neg (pred (n-m))) | EQ \Rightarrow OZ - | GT \Rightarrow (pos (pred (minus m n)))]] + | GT \Rightarrow (pos (pred (m-n)))]] | (neg m) \Rightarrow match y with [ OZ \Rightarrow x | (pos n) \Rightarrow match nat_compare m n with - [ LT \Rightarrow (pos (pred (minus n m))) + [ LT \Rightarrow (pos (pred (n-m))) | EQ \Rightarrow OZ - | GT \Rightarrow (neg (pred (minus m n)))] - | (neg n) \Rightarrow (neg (S (plus m n)))]]. + | GT \Rightarrow (neg (pred (m-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/z/Zplus.con x y). -theorem Zplus_z_OZ: \forall z:Z. eq Z (Zplus z OZ) z. +theorem Zplus_z_OZ: \forall z:Z. z+OZ = z. intro.elim z. simplify.reflexivity. simplify.reflexivity. @@ -133,11 +136,11 @@ qed. (* theorem symmetric_Zplus: symmetric Z Zplus. *) -theorem sym_Zplus : \forall x,y:Z. eq Z (Zplus x y) (Zplus y x). +theorem sym_Zplus : \forall x,y:Z. x+y = y+x. intros.elim x.rewrite > Zplus_z_OZ.reflexivity. elim y.simplify.reflexivity. simplify. -rewrite < sym_plus.reflexivity. +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. @@ -148,45 +151,45 @@ simplify.rewrite > nat_compare_n_m_m_n. simplify.elim nat_compare ? ?.simplify.reflexivity. simplify. reflexivity. simplify. reflexivity. -simplify.rewrite < sym_plus.reflexivity. +simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity. qed. -theorem Zpred_Zplus_neg_O : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z). +theorem Zpred_Zplus_neg_O : \forall z:Z. Zpred z = (neg O)+z. intros.elim z. simplify.reflexivity. simplify.reflexivity. -elim e2.simplify.reflexivity. +elim n.simplify.reflexivity. simplify.reflexivity. qed. -theorem Zsucc_Zplus_pos_O : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z). +theorem Zsucc_Zplus_pos_O : \forall z:Z. Zsucc z = (pos O)+z. intros.elim z. simplify.reflexivity. -elim e1.simplify.reflexivity. +elim n.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))). +\forall n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)). intros. elim n.elim m. simplify.reflexivity. simplify.reflexivity. elim m. -simplify. +simplify.rewrite < plus_n_Sm. rewrite < plus_n_O.reflexivity. -simplify. +simplify.rewrite < plus_n_Sm. 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))). +\forall n,m. (pos n)+(neg m) = (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))). +\forall n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)). intros. elim n.elim m. simplify.reflexivity. @@ -197,18 +200,18 @@ simplify.reflexivity. qed. theorem Zplus_neg_neg: -\forall n,m. eq Z (Zplus (neg n) (neg m)) (Zplus (Zsucc (neg n)) (Zpred (neg m))). +\forall n,m. (neg n)+(neg m) = (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. simplify.rewrite > plus_n_Sm.reflexivity. qed. theorem Zplus_Zsucc_Zpred: -\forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)). +\forall x,y. x+y = (Zsucc x)+(Zpred y). intros. elim x. elim y. simplify.reflexivity. @@ -227,18 +230,18 @@ 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))). +\forall n,m. (Zsucc (pos n))+(pos m) = Zsucc ((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))). +\forall n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((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. +(\lambda n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))).intro. intros.elim n1. simplify. reflexivity. -elim e1.simplify. reflexivity. +elim n2.simplify. reflexivity. simplify. reflexivity. intros. elim n1. simplify. reflexivity. @@ -249,13 +252,13 @@ 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))). +\forall n,m. (Zsucc (neg n))+(neg m) = Zsucc ((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. +(\lambda n,m. ((Zsucc (neg n))+(neg m)) = Zsucc ((neg n)+(neg m))).intro. intros.elim n1. simplify. reflexivity. -elim e1.simplify. reflexivity. +elim n2.simplify. reflexivity. simplify. reflexivity. intros. elim n1. simplify. reflexivity. @@ -266,13 +269,13 @@ reflexivity. qed. theorem Zplus_Zsucc_neg_pos: -\forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))). +\forall n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)). intros. apply nat_elim2 -(\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))). +(\lambda n,m. (Zsucc (neg n))+(pos m) = Zsucc ((neg n)+(pos m))). intros.elim n1. simplify. reflexivity. -elim e1.simplify. reflexivity. +elim n2.simplify. reflexivity. simplify. reflexivity. intros. elim n1. simplify. reflexivity. @@ -283,7 +286,7 @@ 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)). +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. @@ -297,9 +300,9 @@ 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)). +theorem Zplus_Zpred: \forall x,y:Z. (Zpred x)+y = Zpred (x+y). intros. -cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)). +cut Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y). rewrite > Hcut. rewrite > Zplus_Zsucc. rewrite > Zpred_Zsucc. @@ -310,28 +313,48 @@ qed. theorem associative_Zplus: associative Z Zplus. -change with (\forall x,y,z. eq ?(Zplus (Zplus x y) z) (Zplus x (Zplus y z))). -(* simplify. *) +change with \forall x,y,z:Z. (x + y) + z = x + (y + z). +(* simplify. *) intros.elim x.simplify.reflexivity. -elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)). +elim n.rewrite < (Zpred_Zplus_neg_O (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). +rewrite > Zplus_Zpred (neg n1). +rewrite > Zplus_Zpred (neg n1). +rewrite > Zplus_Zpred ((neg n1)+y). apply eq_f.assumption. -elim e2.rewrite < Zsucc_Zplus_pos_O. +elim n.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). +rewrite > Zplus_Zsucc (pos n1). +rewrite > Zplus_Zsucc (pos n1). +rewrite > Zplus_Zsucc ((pos n1)+y). apply eq_f.assumption. qed. -variant assoc_Zplus : -\forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)) +variant assoc_Zplus : \forall x,y,z:Z. (x+y)+z = x+(y+z) \def associative_Zplus. +(* Zopp *) +definition Zopp : Z \to Z \def +\lambda x:Z. match x with +[ OZ \Rightarrow OZ +| (pos n) \Rightarrow (neg n) +| (neg n) \Rightarrow (pos n) ]. + +(*CSC: the URI must disappear: there is a bug now *) +interpretation "integer unary minus" 'uminus x = (cic:/matita/Z/z/Zopp.con x). + +theorem Zplus_Zopp: \forall x:Z. x+ -x = OZ. +intro.elim x. +apply refl_eq. +simplify. +rewrite > nat_compare_n_n. +simplify.apply refl_eq. +simplify. +rewrite > nat_compare_n_n. +simplify.apply refl_eq. +qed. +