From 37f225a76270658463fb28f9d2619efcecabdcd2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 8 Jun 2008 17:42:05 +0000 Subject: [PATCH] generalize no more required before elim --- helm/software/matita/library/nat/bertrand.ma | 6 ++-- .../matita/library/nat/factorization.ma | 33 +++++++++---------- 2 files changed, 18 insertions(+), 21 deletions(-) diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma index 7a0363a58..17f4c72e0 100644 --- 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. -intros 2;simplify;intro;generalize in match H;elim l +intros 2;simplify;intro;elim l in H ⊢ % [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 diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma index d649fbe14..6226f3b6d 100644 --- 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. -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 (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. -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 @@ -694,7 +692,7 @@ change with [ (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. @@ -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. -generalize in match H.elim g. +elim g in H ⊢ %. (* 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). -rewrite > H1 in \vdash (? ? %). +rewrite > H in \vdash (? ? %). 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. @@ -738,28 +735,28 @@ reflexivity. 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. -generalize in match H.elim g. +elim g in H ⊢ %. (* 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)). -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). -exact H1. +exact H. qed. theorem factorize_defactorize: -- 2.39.2