From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 8 Jun 2008 18:48:45 +0000 (+0000)
Subject: generalize no more required before elim
X-Git-Tag: make_still_working~5054
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bccbeb1ec0ef3b55625e4434e693db3cce2e69be;p=helm.git

generalize no more required before elim
---

diff --git a/helm/software/matita/library/nat/orders.ma b/helm/software/matita/library/nat/orders.ma
index 6336a5e9b..6dd8773f8 100644
--- a/helm/software/matita/library/nat/orders.ma
+++ b/helm/software/matita/library/nat/orders.ma
@@ -154,9 +154,7 @@ elim n;
 [ simplify;
   apply le_O_n
 | simplify;
-  generalize in match H1;
-  clear H1;
-  elim m;
+  elim m in H1 ⊢ %;
   [ elim (not_le_Sn_O ? H1)
   | simplify;
     apply le_S_S_to_le;
diff --git a/helm/software/matita/library/nat/pi_p.ma b/helm/software/matita/library/nat/pi_p.ma
index 93f127372..0c5e0d701 100644
--- a/helm/software/matita/library/nat/pi_p.ma
+++ b/helm/software/matita/library/nat/pi_p.ma
@@ -198,17 +198,16 @@ theorem le_pi_p:
 (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to 
 pi_p n p g1 \le pi_p n p g2.
 intros.
-generalize in match H.
-elim n
+elim n in H ⊢ %
   [apply le_n.
   |apply (bool_elim ? (p n1));intros
     [rewrite > true_to_pi_p_Sn
       [rewrite > true_to_pi_p_Sn in ⊢ (? ? %)
         [apply le_times
-          [apply H2[apply le_n|assumption]
-          |apply H1.
+          [apply H1[apply le_n|assumption]
+          |apply H.
            intros.
-           apply H2[apply le_S.assumption|assumption]
+           apply H1[apply le_S.assumption|assumption]
           ]
         |assumption
         ]
@@ -216,9 +215,9 @@ elim n
       ]
     |rewrite > false_to_pi_p_Sn
       [rewrite > false_to_pi_p_Sn in ⊢ (? ? %)
-        [apply H1.
+        [apply H.
          intros.
-         apply H2[apply le_S.assumption|assumption]
+         apply H1[apply le_S.assumption|assumption]
         |assumption
         ]
       |assumption
diff --git a/helm/software/matita/library/nat/sieve.ma b/helm/software/matita/library/nat/sieve.ma
index 3525bc0b2..3f6775f60 100644
--- a/helm/software/matita/library/nat/sieve.ma
+++ b/helm/software/matita/library/nat/sieve.ma
@@ -50,9 +50,9 @@ lemma sieve_prime : \forall t,k,l2,l1.
             (prime p \to p \leq k \to in_list ? p (sieve_aux l1 l2 t)).
 intro.elim t 0
   [intros;cut (l2 = [])
-     [|generalize in match H2;elim l2
+     [|elim l2 in H2 ⊢ %
         [reflexivity
-        |simplify in H6;elim (not_le_Sn_O ? H6)]]
+        |simplify in H5;elim (not_le_Sn_O ? H5)]]
    simplify;split
      [assumption
      |intro;elim (H p);split;intros
@@ -216,7 +216,7 @@ definition list_of_primes \def \lambda n.\lambda l.
 lemma in_list_SSO_list_n : \forall n.2 \leq n \to in_list ? 2 (list_n n).
 intros;elim H;simplify
   [apply in_list_head
-  |generalize in match H2;elim H1;simplify;apply in_list_head]
+  |elim H1 in H2 ⊢ %;simplify;apply in_list_head]
 qed.
 
 lemma le_list_n_aux_k_k : \forall n,m,k.in_list ? n (list_n_aux m k) \to
@@ -243,9 +243,9 @@ qed.
 
 lemma le_list_n : \forall n,m.in_list ? n (list_n m) \to n \leq m.
 intros;unfold list_n in H;lapply (le_list_n_aux ? ? ? H);
-simplify in Hletin;generalize in match H;generalize in match Hletin;elim m
-   [simplify in H2;elim (not_in_list_nil ? ? H2)
-   |simplify in H2;assumption]
+simplify in Hletin;elim m in H Hletin ⊢ %
+   [simplify in H;elim (not_in_list_nil ? ? H)
+   |simplify in H;assumption]
 qed.
 
 
@@ -254,23 +254,23 @@ intros 3;elim H 0
   [intros;simplify;rewrite < plus_n_Sm in H2;simplify in H2;
    rewrite < plus_n_O in H2;rewrite < minus_n_O in H2;
    rewrite > (antisymmetric_le k n H1 H2);apply in_list_head
-  |intros 5;simplify;generalize in match H2;elim H3
+  |intros 5;simplify;elim H3 in H2 ⊢ %
      [apply in_list_head
-     |apply in_list_cons;apply H6
+     |apply in_list_cons;apply H5
         [apply le_S_S;assumption
-        |rewrite < plus_n_Sm in H7;apply H7]]]
+        |rewrite < plus_n_Sm in H6;apply H6]]]
 qed.
 
 lemma le_list_n_r : \forall n,m.S O < m \to 2 \leq n \to n \leq m \to in_list ? n (list_n m).
 intros;unfold list_n;apply le_list_n_aux_r
   [elim H;simplify
      [apply lt_O_S
-     |generalize in match H4;elim H3;
+     |elim H3 in H4 ⊢ %;
         [apply lt_O_S
         |simplify in H7;apply le_S;assumption]]
   |assumption
-  |simplify;generalize in match H2;elim H;simplify;assumption]
-qed.  
+  |simplify;elim H in H2 ⊢ %;simplify;assumption]
+qed.
 
 lemma le_length_list_n : \forall n. length ? (list_n n) \leq n.
 intro;cut (\forall n,k.length ? (list_n_aux n k) \leq (S n))