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.

diff --git a/helm/matita/library/Z.ma b/helm/matita/library/Z.ma
index 130fdff13b6e3f12cd69f07865d47ccd43b387fc..842b952b902ce2b57bf2f901e6331c6bc80a6aed 100644 (file)
--- 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) ?)).