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

generalize no more required before elim
---

diff --git a/helm/software/matita/library/demo/propositional_sequent_calculus.ma b/helm/software/matita/library/demo/propositional_sequent_calculus.ma
index d647830bf..fb5278d6b 100644
--- a/helm/software/matita/library/demo/propositional_sequent_calculus.ma
+++ b/helm/software/matita/library/demo/propositional_sequent_calculus.ma
@@ -422,8 +422,7 @@ lemma same_atom_to_eq: ∀f1,f2. same_atom f1 f2 = true → f1=f2.
   [1,2:
     simplify in H;
     destruct H
-  | generalize in match H; clear H;
-    elim f2;
+  | elim f2 in H ⊢ %;
      [1,2:
        simplify in H;
        destruct H
@@ -588,16 +587,10 @@ lemma sizel_0_no_axiom_is_tautology:
  intros;
  lapply (H1 (λn.mem ? same_atom (FAtom n) l1)); clear H1;
  simplify in Hletin;  
- generalize in match Hletin; clear Hletin;
- generalize in match H2; clear H2;
- generalize in match H; clear H;
- elim l1 0;
+ elim l1 in Hletin H2 H ⊢ % 0;
   [ intros;
     simplify in H2;
-    generalize in match H2; clear H2;
-    generalize in match H1; clear H1;
-    generalize in match H; clear H;
-    elim l2 0;
+    elim l2 in H2 H1 H ⊢ % 0;
      [ intros;
        simplify in H2;
        destruct H2
@@ -677,8 +670,7 @@ lemma sizel_0_no_axiom_is_tautology:
         | assumption
         | lapply (H2 n1); clear H2;
           simplify in Hletin;
-          generalize in match Hletin; clear Hletin;
-          elim (eqb n1 n);
+          elim (eqb n1 n) in Hletin ⊢ %;
            [ simplify in H2;
              rewrite > H2;
              autobatch
@@ -693,10 +685,7 @@ lemma sizel_0_no_axiom_is_tautology:
           rewrite > eqb_n_n in H3;
           simplify in H3;
 (*
-          generalize in match H3;
-          generalize in match H1; clear H1;
-          generalize in match H; clear H;
-          elim l 0;
+          elim l in H3 H1 H ⊢ % 0;
            [ elim l2 0;
               [ intros;
                 simplify in H2;
@@ -714,9 +703,7 @@ lemma sizel_0_no_axiom_is_tautology:
                  ]
                     
                  [ autobatch
-                 | generalize in match H4; clear H4;
-                   generalize in match H2; clear H2;
-                   elim t1;
+                 | elim t1 in H4 H2 ⊢ %;
                     [
                     |
                     |
diff --git a/helm/software/matita/library/demo/realisability.ma b/helm/software/matita/library/demo/realisability.ma
index 0cd58c63d..0de10940a 100644
--- a/helm/software/matita/library/demo/realisability.ma
+++ b/helm/software/matita/library/demo/realisability.ma
@@ -116,9 +116,8 @@ theorem correct: ∀F:SP.∀r:type_OF_SP F.modr F r → Prop_OF_SP F.
        | apply (proj2 ? ? H2)
        ]
      ]
-  | generalize in match H2; clear H2;
-    change in r with (type_OF_SP s + type_OF_SP s1);
-    elim r; simplify in H2;
+  | change in r with (type_OF_SP s + type_OF_SP s1);
+    elim r in H2 ⊢ %; simplify in H2;
      [ left; apply H; assumption
      | right; apply H1; assumption
      ]
@@ -131,8 +130,7 @@ theorem correct: ∀F:SP.∀r:type_OF_SP F.modr F r → Prop_OF_SP F.
     | skip
     ]
   | simplify in r;
-    generalize in match H1; clear H1;
-    elim r;
+    elim r in H1 ⊢ %;
     apply (ex_intro ? ? a);
     apply H;
     assumption