generalize no more required before elim

diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma
index 7a0363a58117f7455ef7ed127ef339542c151369..17f4c72e0078ded8e054dc4e750e26aa6b876ea5 100644 (file)
--- a/helm/software/matita/library/nat/bertrand.ma
+++ b/helm/software/matita/library/nat/bertrand.ma
@@ -42,10 +42,10 @@ let rec checker l \def
          | cons h2 t2 => (andb (checker t1) (leb h1 (2*h2))) ]].
 
 lemma checker_cons : \forall t,l.checker (t::l) = true \to checker l = true.
          | cons h2 t2 => (andb (checker t1) (leb h1 (2*h2))) ]].
 
 lemma checker_cons : \forall t,l.checker (t::l) = true \to checker l = true.

-intros 2;simplify;intro;generalize in match H;elim l
+intros 2;simplify;intro;elim l in H ⊢ %

   [reflexivity
   [reflexivity

-  |change in H2 with (andb (checker (a::l1)) (leb t (a+(a+O))) = true);
-   apply (andb_true_true ? ? H2)]
+  |change in H1 with (andb (checker (a::l1)) (leb t (a+(a+O))) = true);
+   apply (andb_true_true ? ? H1)]

 qed.
 
 theorem checker_sound : \forall l1,l2,l,x,y.l = l1@(x::y::l2) \to 
 qed.
 
 theorem checker_sound : \forall l1,l2,l,x,y.l = l1@(x::y::l2) \to 

diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma
index d649fbe145a4022e3f6a34115b87f9fae1f4ef9c..6226f3b6de81997ac3eefa61006d0c54205deafc 100644 (file)
--- a/helm/software/matita/library/nat/factorization.ma
+++ b/helm/software/matita/library/nat/factorization.ma
@@ -648,21 +648,19 @@ theorem eq_defactorize_aux_to_eq: \forall f,g:nat_fact.\forall i:nat.
 defactorize_aux f i = defactorize_aux g i \to f = g.
 intro.
 elim f.
 defactorize_aux f i = defactorize_aux g i \to f = g.
 intro.
 elim f.

-generalize in match H.
-elim g.
+elim g in H ⊢ %.

 apply eq_f.
 apply inj_S. apply (inj_exp_r (nth_prime i)).
 apply lt_SO_nth_prime_n.
 assumption.
 apply False_ind.
 apply eq_f.
 apply inj_S. apply (inj_exp_r (nth_prime i)).
 apply lt_SO_nth_prime_n.
 assumption.
 apply False_ind.

-apply (not_eq_nf_last_nf_cons n2 n n1 i H2).
-generalize in match H1.
-elim g.
+apply (not_eq_nf_last_nf_cons n2 n n1 i H1).
+elim g in H1 ⊢ %.

 apply False_ind.
 apply (not_eq_nf_last_nf_cons n1 n2 n i).
 apply sym_eq. assumption.
 apply False_ind.
 apply (not_eq_nf_last_nf_cons n1 n2 n i).
 apply sym_eq. assumption.

-simplify in H3.
-generalize in match H3.
+simplify in H2.
+generalize in match H2.

 apply (nat_elim2 (\lambda n,n2.
 ((nth_prime i) \sup n)*(defactorize_aux n1 (S i)) =
 ((nth_prime i) \sup n2)*(defactorize_aux n3 (S i)) \to
 apply (nat_elim2 (\lambda n,n2.
 ((nth_prime i) \sup n)*(defactorize_aux n1 (S i)) =
 ((nth_prime i) \sup n2)*(defactorize_aux n3 (S i)) \to


@@ -694,7 +692,7 @@ change with
 [ (nf_last m) \Rightarrow m
 | (nf_cons m g) \Rightarrow m ] = m).
 rewrite > Hcut.simplify.reflexivity.
 [ (nf_last m) \Rightarrow m
 | (nf_cons m g) \Rightarrow m ] = m).
 rewrite > Hcut.simplify.reflexivity.

-apply H4.simplify in H5.
+apply H3.simplify in H4.

 apply (inj_times_r1 (nth_prime i)).
 apply lt_O_nth_prime_n.
 rewrite < assoc_times.rewrite < assoc_times.assumption.
 apply (inj_times_r1 (nth_prime i)).
 apply lt_O_nth_prime_n.
 rewrite < assoc_times.rewrite < assoc_times.assumption.


@@ -712,22 +710,21 @@ injective nat_fact_all nat defactorize.
 unfold injective.
 change with (\forall f,g.defactorize f = defactorize g \to f=g).
 intro.elim f.
 unfold injective.
 change with (\forall f,g.defactorize f = defactorize g \to f=g).
 intro.elim f.

-generalize in match H.elim g.
+elim g in H ⊢ %.

 (* zero - zero *)
 reflexivity.
 (* zero - one *)
 simplify in H1.
 apply False_ind.
 (* zero - zero *)
 reflexivity.
 (* zero - one *)
 simplify in H1.
 apply False_ind.

-apply (not_eq_O_S O H1).
+apply (not_eq_O_S O H).

 (* zero - proper *)
 simplify in H1.
 apply False_ind.
 apply (not_le_Sn_n O).
 (* zero - proper *)
 simplify in H1.
 apply False_ind.
 apply (not_le_Sn_n O).

-rewrite > H1 in \vdash (? ? %).
+rewrite > H in \vdash (? ? %).

 change with (O < defactorize_aux n O).
 apply lt_O_defactorize_aux.
 change with (O < defactorize_aux n O).
 apply lt_O_defactorize_aux.

-generalize in match H.
-elim g.
+elim g in H ⊢ %.

 (* one - zero *)
 simplify in H1.
 apply False_ind.
 (* one - zero *)
 simplify in H1.
 apply False_ind.


@@ -738,28 +735,28 @@ reflexivity.
 simplify in H1.
 apply False_ind.
 apply (not_le_Sn_n (S O)).
 simplify in H1.
 apply False_ind.
 apply (not_le_Sn_n (S O)).

-rewrite > H1 in \vdash (? ? %).
+rewrite > H in \vdash (? ? %).

 change with ((S O) < defactorize_aux n O).
 apply lt_SO_defactorize_aux.
 change with ((S O) < defactorize_aux n O).
 apply lt_SO_defactorize_aux.

-generalize in match H.elim g.
+elim g in H ⊢ %.

 (* proper - zero *)
 simplify in H1.
 apply False_ind.
 apply (not_le_Sn_n O).
 (* proper - zero *)
 simplify in H1.
 apply False_ind.
 apply (not_le_Sn_n O).

-rewrite < H1 in \vdash (? ? %).
+rewrite < H in \vdash (? ? %).

 change with (O < defactorize_aux n O).
 apply lt_O_defactorize_aux.
 (* proper - one *)
 simplify in H1.
 apply False_ind.
 apply (not_le_Sn_n (S O)).
 change with (O < defactorize_aux n O).
 apply lt_O_defactorize_aux.
 (* proper - one *)
 simplify in H1.
 apply False_ind.
 apply (not_le_Sn_n (S O)).

-rewrite < H1 in \vdash (? ? %).
+rewrite < H in \vdash (? ? %).

 change with ((S O) < defactorize_aux n O).
 apply lt_SO_defactorize_aux.
 (* proper - proper *)
 apply eq_f.
 apply (injective_defactorize_aux O).
 change with ((S O) < defactorize_aux n O).
 apply lt_SO_defactorize_aux.
 (* proper - proper *)
 apply eq_f.
 apply (injective_defactorize_aux O).

-exact H1.
+exact H.

 qed.
 
 theorem factorize_defactorize: 
 qed.
 
 theorem factorize_defactorize: