From: Claudio Sacerdoti Coen Date: Sun, 8 Jun 2008 17:56:36 +0000 (+0000) Subject: generalize no more required before elim X-Git-Tag: make_still_working~5056 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dc0aa21dae28cd07142cb7bcaf8e6a1bfd99018d;p=helm.git generalize no more required before elim --- diff --git a/helm/software/matita/library/nat/iteration2.ma b/helm/software/matita/library/nat/iteration2.ma index 752e89b9d..3a4128e70 100644 --- a/helm/software/matita/library/nat/iteration2.ma +++ b/helm/software/matita/library/nat/iteration2.ma @@ -286,17 +286,16 @@ theorem le_sigma_p: (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to sigma_p n p g1 \le sigma_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_sigma_p_Sn [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %) [apply le_plus - [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 ] @@ -304,9 +303,9 @@ elim n ] |rewrite > false_to_sigma_p_Sn [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %) - [apply H1. + [apply H. intros. - apply H2[apply le_S.assumption|assumption] + apply H1[apply le_S.assumption|assumption] |assumption ] |assumption @@ -322,25 +321,24 @@ theorem le_sigma_p1: bool_to_nat (p1 i)*(g1 i) \le bool_to_nat (p2 i)*g2 i) \to sigma_p n p1 g1 \le sigma_p n p2 g2. intros. -generalize in match H. -elim n +elim n in H ⊢ % [apply le_n. |apply (bool_elim ? (p1 n1));intros [apply (bool_elim ? (p2 n1));intros [rewrite > true_to_sigma_p_Sn [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %) [apply le_plus - [lapply (H2 n1) as H5 - [rewrite > H3 in H5. - rewrite > H4 in H5. + [lapply (H1 n1) as H5 + [rewrite > H2 in H5. + rewrite > H3 in H5. simplify in H5. rewrite < plus_n_O in H5. rewrite < plus_n_O in H5. assumption |apply le_S_S.apply le_n ] - |apply H1.intros. - apply H2.apply le_S.assumption + |apply H.intros. + apply H1.apply le_S.assumption ] |assumption ] @@ -350,16 +348,16 @@ elim n [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %) [change in ⊢ (? ? %) with (O + sigma_p n1 p2 g2). apply le_plus - [lapply (H2 n1) as H5 - [rewrite > H3 in H5. - rewrite > H4 in H5. + [lapply (H1 n1) as H5 + [rewrite > H2 in H5. + rewrite > H3 in H5. simplify in H5. rewrite < plus_n_O in H5. assumption |apply le_S_S.apply le_n ] - |apply H1.intros. - apply H2.apply le_S.assumption + |apply H.intros. + apply H1.apply le_S.assumption ] |assumption ] @@ -371,16 +369,16 @@ elim n [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %) [change in ⊢ (? % ?) with (O + sigma_p n1 p1 g1). apply le_plus - [lapply (H2 n1) as H5 - [rewrite > H3 in H5. - rewrite > H4 in H5. + [lapply (H1 n1) as H5 + [rewrite > H2 in H5. + rewrite > H3 in H5. simplify in H5. rewrite < plus_n_O in H5. assumption |apply le_S_S.apply le_n ] - |apply H1.intros. - apply H2.apply le_S.assumption + |apply H.intros. + apply H1.apply le_S.assumption ] |assumption ] @@ -388,8 +386,8 @@ elim n ] |rewrite > false_to_sigma_p_Sn [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %) - [apply H1.intros. - apply H2.apply le_S.assumption + [apply H.intros. + apply H1.apply le_S.assumption |assumption ] |assumption @@ -397,7 +395,7 @@ elim n ] ] ] -qed. +qed. theorem lt_sigma_p: \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat. diff --git a/helm/software/matita/library/nat/minimization.ma b/helm/software/matita/library/nat/minimization.ma index bc2cc7059..5b1552dc6 100644 --- a/helm/software/matita/library/nat/minimization.ma +++ b/helm/software/matita/library/nat/minimization.ma @@ -236,17 +236,16 @@ intros 2. elim n.absurd (le m O).assumption. cut (O < m).apply (lt_O_n_elim m Hcut).exact not_le_Sn_O. rewrite < (max_O_f f).assumption. -generalize in match H1. -elim (max_S_max f n1). -elim H3. +elim (max_S_max f n1) in H1 ⊢ %. +elim H1. absurd (m \le S n1).assumption. -apply lt_to_not_le.rewrite < H6.assumption. -elim H3. +apply lt_to_not_le.rewrite < H5.assumption. +elim H1. apply (le_n_Sm_elim m n1 H2). intro. -apply H.rewrite < H6.assumption. +apply H.rewrite < H5.assumption. apply le_S_S_to_le.assumption. -intro.rewrite > H7.assumption. +intro.rewrite > H6.assumption. qed. theorem f_false_to_le_max: \forall f,n,p. (∃i:nat.i≤n∧f i=true) \to @@ -385,7 +384,7 @@ qed. theorem lt_min_aux_to_false : \forall f:nat \to bool. \forall n,off,m:nat. n \leq m \to m < (min_aux off n f) \to f m = false. intros 3. -generalize in match n; clear n. +generalize in match n; clear n; elim off.absurd (le n1 m).assumption. apply lt_to_not_le.rewrite < (min_aux_O_f f n1).assumption. elim (le_to_or_lt_eq ? ? H1); @@ -422,8 +421,7 @@ qed. lemma le_min_aux : \forall f:nat \to bool. \forall n,off:nat. n \leq (min_aux off n f). intros 3. -generalize in match n. clear n. -elim off. +elim off in n ⊢ %. rewrite > (min_aux_O_f f n1).apply le_n. elim (min_aux_S f n n1). elim H1.rewrite > H3.apply le_n. @@ -437,8 +435,7 @@ qed. theorem le_min_aux_r : \forall f:nat \to bool. \forall n,off:nat. (min_aux off n f) \le n+off. intros. -generalize in match n. clear n. -elim off.simplify. +elim off in n ⊢ %.simplify. elim (f n1).simplify.rewrite < plus_n_O.apply le_n. simplify.rewrite < plus_n_O.apply le_n. simplify.elim (f n1).