From: Claudio Sacerdoti Coen Date: Sun, 18 May 2008 19:30:44 +0000 (+0000) Subject: Dummy dependent types are no longer cleaned in inductive type arities. X-Git-Tag: make_still_working~5156 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=097e94fd9b070378d68dbfe8e7cba18b14ed8518;p=helm.git Dummy dependent types are no longer cleaned in inductive type arities. --- diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma index d1ad9e12e..4d8596b6e 100644 --- a/helm/software/matita/library/nat/bertrand.ma +++ b/helm/software/matita/library/nat/bertrand.ma @@ -94,7 +94,7 @@ intro.elim t 0 |intro;elim (H1 p);split;intros [elim (H6 H8);assumption |apply (H7 H8 H9);intros;elim (not_in_list_nil ? ? H10)]] - |simplify;elim (H k (filter ? l (\lambda x.notb (divides_b t1 x))) (t1::l1)) + |simplify;elim (H k (filter ? l (\lambda x.notb (divides_b a x))) (a::l1)) [split; [assumption |intro;apply H8;] @@ -103,13 +103,13 @@ intro.elim t 0 [rewrite > H8;split [split [unfold;intros;split - [elim (H3 t1);elim H9 + [elim (H3 a);elim H9 [elim H11;assumption |apply in_list_head] |intros;elim (le_to_or_lt_eq ? ? (divides_to_le ? ? ? H9)) [elim (divides_to_prime_divides ? ? H10 H11 H9);elim H12; - elim H13;clear H13 H12;elim (H3 t1);elim H12 - [clear H13 H12;elim (H18 ? ? H14);elim (H2 a); + elim H13;clear H13 H12;elim (H3 a);elim H12 + [clear H13 H12;elim (H18 ? ? H14);elim (H2 a1); apply H13 [assumption |elim H17;apply (trans_le ? ? ? ? H20); @@ -122,48 +122,48 @@ intro.elim t 0 [rewrite > H20;apply le_n |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]] |apply in_list_head] - |elim (H3 t1);elim H11 + |elim (H3 a);elim H11 [elim H13;apply lt_to_le;assumption |apply in_list_head] |assumption]] - |elim (H3 t1);elim H9 + |elim (H3 a);elim H9 [elim H11;assumption |apply in_list_head]] - |intros;elim (le_to_or_lt_eq t1 x) + |intros;elim (le_to_or_lt_eq a x) [assumption |rewrite > H10 in H9;lapply (in_list_filter_to_p_true ? ? ? H9); lapply (divides_n_n x); rewrite > (divides_to_divides_b_true ? ? ? Hletin1) in Hletin [simplify in Hletin;destruct Hletin - |rewrite < H10;elim (H3 t1);elim H11 + |rewrite < H10;elim (H3 a);elim H11 [elim H13;apply lt_to_le;assumption |apply in_list_head]] |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);apply (in_list_filter ? ? ? H9)]] |elim (H2 p);elim (H9 H8);split [assumption |intros;apply H12;apply in_list_cons;apply (in_list_filter ? ? ? H13)]] - |elim (decidable_eq_nat p t1) + |elim (decidable_eq_nat p a) [rewrite > H10;apply in_list_head |apply in_list_cons;elim (H2 p);apply (H12 H7 H8);intros; - apply (trans_le ? t1) - [elim (decidable_lt p t1) + apply (trans_le ? a) + [elim (decidable_lt p a) [assumption |lapply (not_lt_to_le ? ? H14); - lapply (decidable_divides t1 p) + lapply (decidable_divides a p) [elim Hletin1 [elim H7;lapply (H17 ? H15) [elim H10;symmetry;assumption - |elim (H3 t1);elim H18 + |elim (H3 a);elim H18 [elim H20;assumption |apply in_list_head]] |elim (Not_lt_n_n p);apply H9;apply in_list_filter_r - [elim (H3 p);apply (in_list_tail ? ? t1) + [elim (H3 p);apply (in_list_tail ? ? a) [apply H17 [apply prime_to_lt_SO;assumption |assumption |intros;elim H7;intro;lapply (H20 ? H21) [rewrite > Hletin2 in H18;elim (H11 H18); - lapply (H23 t1) + lapply (H23 a) [elim (lt_to_not_le ? ? Hletin3 Hletin) |apply in_list_head] |apply prime_to_lt_SO;elim (H2 p1);elim (H22 H18); @@ -171,10 +171,10 @@ intro.elim t 0 |unfold;intro;apply H15;rewrite > H18;apply divides_n_n] |rewrite > (not_divides_to_divides_b_false ? ? ? H15); [reflexivity - |elim (H3 t1);elim H16 + |elim (H3 a);elim H16 [elim H18;apply lt_to_le;assumption |apply in_list_head]]]] - |elim (H3 t1);elim H15 + |elim (H3 a);elim H15 [elim H17;apply lt_to_le;assumption |apply in_list_head]]] |elim (in_list_cons_case ? ? ? ? H13) @@ -189,7 +189,7 @@ intro.elim t 0 [rewrite > H11;intro;lapply (in_list_filter_to_p_true ? ? ? H9); rewrite > (divides_to_divides_b_true ? ? ? H12) in Hletin [simplify in Hletin;destruct Hletin - |elim (H3 t1);elim H13 + |elim (H3 a);elim H13 [elim H15;apply lt_to_le;assumption |apply in_list_head]] |elim H7 @@ -204,10 +204,10 @@ intro.elim t 0 |intros;apply H11;apply in_list_cons;assumption |apply in_list_filter_r; [assumption - |lapply (H11 t1) + |lapply (H11 a) [rewrite > (not_divides_to_divides_b_false ? ? ? Hletin); [reflexivity - |elim (H3 t1);elim H13 + |elim (H3 a);elim H13 [elim H15;apply lt_to_le;assumption |apply in_list_head]] |apply in_list_head]]]] @@ -219,7 +219,7 @@ intro.elim t 0 apply H11;apply in_list_head] |generalize in match (sorted_cons_to_sorted ? ? ? ? H6);elim l [simplify;assumption - |simplify;elim (notb (divides_b t1 t2));simplify + |simplify;elim (notb (divides_b a a1));simplify [lapply (sorted_cons_to_sorted ? ? ? ? H8);lapply (H7 Hletin); apply (sort_cons ? ? ? ? Hletin1);intros; apply (sorted_to_minimum ? ? ? ? H8);apply (in_list_filter ? ? ? H9); @@ -396,7 +396,7 @@ let rec checker l \def lemma checker_cons : \forall t,l.checker (t::l) = true \to checker l = true. intros 2;simplify;intro;generalize in match H;elim l [reflexivity - |change in H2 with (andb (checker (t1::l1)) (leb t (t1+(t1+O))) = true); + |change in H2 with (andb (checker (a::l1)) (leb t (a+(a+O))) = true); apply (andb_true_true ? ? H2)] qed. @@ -561,7 +561,7 @@ intro.elim l 2 |rewrite > H1.assumption ] |elim (H H6 p H1 H3).clear H. - apply (ex_intro ? ? a). + apply (ex_intro ? ? a1). elim H8.clear H8. elim H.clear H. split