From 3e3657f10985058cf04ad3fbcdb804dc99bce128 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 3 Jul 2005 14:47:59 +0000 Subject: [PATCH] Equality tactics are now used in the first half of the script. Note: it seems that "elim H ?" is more powerful than "rewrite < H ?" since it is able to discover the value of the implicit argument ?. To be improved. --- helm/matita/library/Z.ma | 162 +++++++++++++++++++-------------------- 1 file changed, 80 insertions(+), 82 deletions(-) diff --git a/helm/matita/library/Z.ma b/helm/matita/library/Z.ma index 130fdff13..842b952b9 100644 --- a/helm/matita/library/Z.ma +++ b/helm/matita/library/Z.ma @@ -72,22 +72,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 +106,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 +143,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 +251,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 +268,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 +285,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 +318,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) ?)). -- 2.39.2