X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ.ma;h=d0049187a6a2510ef6b463156689491455ccdf50;hb=b05dceab1903f9d15f214a9ddeaf791cd594e215;hp=130fdff13b6e3f12cd69f07865d47ccd43b387fc;hpb=109ddb8c437013d6d86e1564d5df3f8b089b9700;p=helm.git diff --git a/helm/matita/library/Z.ma b/helm/matita/library/Z.ma index 130fdff13..d0049187a 100644 --- a/helm/matita/library/Z.ma +++ b/helm/matita/library/Z.ma @@ -14,30 +14,7 @@ set "baseuri" "cic:/matita/Z/". -alias id "nat" = "cic:/matita/nat/nat.ind#xpointer(1/1)". -alias id "O" = "cic:/matita/nat/nat.ind#xpointer(1/1/1)". -alias id "false" = "cic:/matita/bool/bool.ind#xpointer(1/1/2)". -alias id "true" = "cic:/matita/bool/bool.ind#xpointer(1/1/1)". -alias id "Not" = "cic:/matita/logic/Not.con". -alias id "eq" = "cic:/matita/equality/eq.ind#xpointer(1/1)". -alias id "if_then_else" = "cic:/matita/bool/if_then_else.con". -alias id "refl_equal" = "cic:/matita/equality/eq.ind#xpointer(1/1/1)". -alias id "False" = "cic:/matita/logic/False.ind#xpointer(1/1)". -alias id "True" = "cic:/matita/logic/True.ind#xpointer(1/1)". -alias id "sym_eq" = "cic:/matita/equality/sym_eq.con". -alias id "I" = "cic:/matita/logic/True.ind#xpointer(1/1/1)". -alias id "S" = "cic:/matita/nat/nat.ind#xpointer(1/1/2)". -alias id "LT" = "cic:/matita/compare/compare.ind#xpointer(1/1/1)". -alias id "minus" = "cic:/matita/nat/minus.con". -alias id "nat_compare" = "cic:/matita/nat/nat_compare.con". -alias id "plus" = "cic:/matita/nat/plus.con". -alias id "pred" = "cic:/matita/nat/pred.con". -alias id "sym_plus" = "cic:/matita/nat/sym_plus.con". -alias id "nat_compare_invert" = "cic:/matita/nat/nat_compare_invert.con". -alias id "plus_n_O" = "cic:/matita/nat/plus_n_O.con". -alias id "plus_n_Sm" = "cic:/matita/nat/plus_n_Sm.con". -alias id "nat_double_ind" = "cic:/matita/nat/nat_double_ind.con". -alias id "f_equal" = "cic:/matita/equality/f_equal.con". +include "nat.ma". inductive Z : Set \def OZ : Z @@ -72,22 +49,19 @@ match z with theorem OZ_discr : \forall z. if_then_else (OZ_testb z) (eq Z z OZ) (Not (eq Z z OZ)). -intros.elim z.simplify. -apply refl_equal. +intros.elim z.simplify.reflexivity. simplify.intros. cut match neg e with [ OZ \Rightarrow True | (pos n) \Rightarrow False | (neg n) \Rightarrow False]. -apply Hcut. - elim (sym_eq ? ? ? H).simplify. -exact I. +apply Hcut.rewrite > H.simplify.exact I. simplify.intros. cut match pos e with [ OZ \Rightarrow True | (pos n) \Rightarrow False | (neg n) \Rightarrow False]. -apply Hcut. elim (sym_eq ? ? ? H).simplify.exact I. +apply Hcut. rewrite > H.simplify.exact I. qed. definition Zsucc \def @@ -109,17 +83,17 @@ definition Zpred \def | (neg n) \Rightarrow neg (S n)]. theorem Zpred_succ: \forall z:Z. eq Z (Zpred (Zsucc z)) z. -intros.elim z.apply refl_equal. -elim e.apply refl_equal. -apply refl_equal. -apply refl_equal. +intros.elim z.reflexivity. +elim e.reflexivity. +reflexivity. +reflexivity. qed. theorem Zsucc_pred: \forall z:Z. eq Z (Zsucc (Zpred z)) z. -intros.elim z.apply refl_equal. -apply refl_equal. -elim e.apply refl_equal. -apply refl_equal. +intros.elim z.reflexivity. +reflexivity. +elim e.reflexivity. +reflexivity. qed. let rec Zplus x y : Z \def @@ -146,105 +120,106 @@ let rec Zplus x y : Z \def theorem Zplus_z_O: \forall z:Z. eq Z (Zplus z OZ) z. intro.elim z. -simplify.apply refl_equal. -simplify.apply refl_equal. -simplify.apply refl_equal. +simplify.reflexivity. +simplify.reflexivity. +simplify.reflexivity. qed. theorem sym_Zplus : \forall x,y:Z. eq Z (Zplus x y) (Zplus y x). -intros.elim x.simplify.elim (sym_eq ? ? ? (Zplus_z_O y)).apply refl_equal. +intros.elim x.simplify.rewrite > Zplus_z_O y.reflexivity. elim y.simplify.reflexivity. simplify. -elim (sym_plus e e1).apply refl_equal. +rewrite < (sym_plus e e1).reflexivity. simplify. -elim (sym_eq ? ? ?(nat_compare_invert e e1)). -simplify.elim nat_compare e1 e.simplify.apply refl_equal. -simplify. apply refl_equal. -simplify. apply refl_equal. +rewrite > nat_compare_invert e e1. +simplify.elim nat_compare e1 e.simplify.reflexivity. +simplify. reflexivity. +simplify. reflexivity. elim y.simplify.reflexivity. -simplify.elim (sym_eq ? ? ?(nat_compare_invert e e1)). -simplify.elim nat_compare e1 e.simplify.apply refl_equal. -simplify. apply refl_equal. -simplify. apply refl_equal. -simplify.elim (sym_plus e1 e).apply refl_equal. +simplify.rewrite > nat_compare_invert e e1. +simplify.elim nat_compare e1 e.simplify.reflexivity. +simplify. reflexivity. +simplify. reflexivity. +simplify.elim (sym_plus e1 e).reflexivity. qed. theorem Zpred_neg : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z). intros.elim z. -simplify.apply refl_equal. -simplify.apply refl_equal. -elim e.simplify.apply refl_equal. -simplify.apply refl_equal. +simplify.reflexivity. +simplify.reflexivity. +elim e.simplify.reflexivity. +simplify.reflexivity. qed. theorem Zsucc_pos : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z). intros.elim z. -simplify.apply refl_equal. -elim e.simplify.apply refl_equal. -simplify.apply refl_equal. -simplify.apply refl_equal. +simplify.reflexivity. +elim e.simplify.reflexivity. +simplify.reflexivity. +simplify.reflexivity. qed. theorem Zplus_succ_pred_pp : \forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))). intros. elim n.elim m. -simplify.apply refl_equal. -simplify.apply refl_equal. +simplify.reflexivity. +simplify.reflexivity. elim m. simplify. -elim (plus_n_O ?).apply refl_equal. +rewrite < plus_n_O e.reflexivity. simplify. -elim (plus_n_Sm ? ?).apply refl_equal. +rewrite < plus_n_Sm e e1.reflexivity. qed. theorem Zplus_succ_pred_pn : \forall n,m. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))). -intros.apply refl_equal. +intros.reflexivity. qed. theorem Zplus_succ_pred_np : \forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (Zsucc (neg n)) (Zpred (pos m))). intros. elim n.elim m. -simplify.apply refl_equal. -simplify.apply refl_equal. +simplify.reflexivity. +simplify.reflexivity. elim m. -simplify.apply refl_equal. -simplify.apply refl_equal. +simplify.reflexivity. +simplify.reflexivity. qed. theorem Zplus_succ_pred_nn: \forall n,m. eq Z (Zplus (neg n) (neg m)) (Zplus (Zsucc (neg n)) (Zpred (neg m))). intros. elim n.elim m. -simplify.apply refl_equal. -simplify.apply refl_equal. +simplify.reflexivity. +simplify.reflexivity. elim m. -simplify.elim (plus_n_Sm ? ?).apply refl_equal. -simplify.elim (sym_eq ? ? ? (plus_n_Sm ? ?)).apply refl_equal. +simplify.rewrite < plus_n_Sm e O.reflexivity. +simplify.rewrite > plus_n_Sm e (S e1).reflexivity. qed. +(*CSC: da qui in avanti rewrite ancora non utilizzata *) theorem Zplus_succ_pred: \forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)). intros. elim x. elim y. -simplify.apply refl_equal. -simplify.apply refl_equal. -elim (Zsucc_pos ?).elim (sym_eq ? ? ? (Zsucc_pred ?)).apply refl_equal. +simplify.reflexivity. +simplify.reflexivity. +elim (Zsucc_pos ?).elim (sym_eq ? ? ? (Zsucc_pred ?)).reflexivity. elim y.elim sym_Zplus ? ?.elim sym_Zplus (Zpred OZ) ?. elim (Zpred_neg ?).elim (sym_eq ? ? ? (Zpred_succ ?)). -simplify.apply refl_equal. +simplify.reflexivity. apply Zplus_succ_pred_nn. apply Zplus_succ_pred_np. -elim y.simplify.apply refl_equal. +elim y.simplify.reflexivity. apply Zplus_succ_pred_pn. apply Zplus_succ_pred_pp. qed. theorem Zsucc_plus_pp : \forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))). -intros.apply refl_equal. +intros.reflexivity. qed. theorem Zsucc_plus_pn : @@ -253,15 +228,15 @@ intros. apply nat_double_ind (\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro. intros.elim n1. -simplify. apply refl_equal. -elim e.simplify. apply refl_equal. -simplify. apply refl_equal. +simplify. reflexivity. +elim e.simplify. reflexivity. +simplify. reflexivity. intros. elim n1. -simplify. apply refl_equal. -simplify.apply refl_equal. +simplify. reflexivity. +simplify.reflexivity. intros. elim (Zplus_succ_pred_pn ? m1). -elim H.apply refl_equal. +elim H.reflexivity. qed. theorem Zsucc_plus_nn : @@ -270,15 +245,15 @@ intros. apply nat_double_ind (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro. intros.elim n1. -simplify. apply refl_equal. -elim e.simplify. apply refl_equal. -simplify. apply refl_equal. +simplify. reflexivity. +elim e.simplify. reflexivity. +simplify. reflexivity. intros. elim n1. -simplify. apply refl_equal. -simplify.apply refl_equal. +simplify. reflexivity. +simplify.reflexivity. intros. elim (Zplus_succ_pred_nn ? m1). -apply refl_equal. +reflexivity. qed. theorem Zsucc_plus_np : @@ -287,29 +262,29 @@ intros. apply nat_double_ind (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))). intros.elim n1. -simplify. apply refl_equal. -elim e.simplify. apply refl_equal. -simplify. apply refl_equal. +simplify. reflexivity. +elim e.simplify. reflexivity. +simplify. reflexivity. intros. elim n1. -simplify. apply refl_equal. -simplify.apply refl_equal. +simplify. reflexivity. +simplify.reflexivity. intros. elim H. elim (Zplus_succ_pred_np ? (S m1)). -apply refl_equal. +reflexivity. qed. theorem Zsucc_plus : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)). intros.elim x.elim y. -simplify. apply refl_equal. -elim (Zsucc_pos ?).apply refl_equal. -simplify.apply refl_equal. -elim y.elim sym_Zplus ? ?.elim sym_Zplus OZ ?.simplify.apply refl_equal. +simplify. reflexivity. +elim (Zsucc_pos ?).reflexivity. +simplify.reflexivity. +elim y.elim sym_Zplus ? ?.elim sym_Zplus OZ ?.simplify.reflexivity. apply Zsucc_plus_nn. apply Zsucc_plus_np. elim y. -elim (sym_Zplus OZ ?).apply refl_equal. +elim (sym_Zplus OZ ?).reflexivity. apply Zsucc_plus_pn. apply Zsucc_plus_pp. qed. @@ -320,18 +295,18 @@ cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)). elim (sym_eq ? ? ? Hcut). elim (sym_eq ? ? ? (Zsucc_plus ? ?)). elim (sym_eq ? ? ? (Zpred_succ ?)). -apply refl_equal. +reflexivity. elim (sym_eq ? ? ? (Zsucc_pred ?)). -apply refl_equal. +reflexivity. qed. theorem assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus x (Zplus y z)) (Zplus (Zplus x y) z). -intros.elim x.simplify.apply refl_equal. +intros.elim x.simplify.reflexivity. elim e.elim (Zpred_neg (Zplus y z)). elim (Zpred_neg y). elim (Zpred_plus ? ?). -apply refl_equal. +reflexivity. elim (sym_eq ? ? ? (Zpred_plus (neg e1) ?)). elim (sym_eq ? ? ? (Zpred_plus (neg e1) ?)). elim (sym_eq ? ? ? (Zpred_plus (Zplus (neg e1) y) ?)).