From bccbeb1ec0ef3b55625e4434e693db3cce2e69be Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 8 Jun 2008 18:48:45 +0000 Subject: [PATCH] generalize no more required before elim --- helm/software/matita/library/nat/orders.ma | 4 +--- helm/software/matita/library/nat/pi_p.ma | 13 ++++++------ helm/software/matita/library/nat/sieve.ma | 24 +++++++++++----------- 3 files changed, 19 insertions(+), 22 deletions(-) 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)) -- 2.39.2