(* *)
(**************************************************************************)
-include "nat/sqrt.ma".
+include "nat/primes.ma".
include "list/sort.ma".
-include "nat/factorization.ma".
let rec list_n_aux n k \def
match n with
(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
[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 a);elim H12
- [clear H13 H12;elim (H18 ? ? H14);elim (H2 a1);
- apply H13
- [assumption
- |elim H17;apply (trans_le ? ? ? ? H20);
- apply (trans_le ? ? ? H15);
- apply lt_to_le;assumption
- |intros;apply (trans_le ? (S m))
- [apply le_S_S;assumption
- |apply (trans_le ? ? ? H11);
- elim (in_list_cons_case ? ? ? ? H19)
- [rewrite > H20;apply le_n
- |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]]
- |apply in_list_head]
+ [cut (1 < a) as Lt1a; [2: apply (trans_lt ??? H10 H11)]
+ letin a1 ≝ (smallest_factor a);
+ lapply (divides_smallest_factor_n a) as H14;
+ [2: apply (trans_lt ? (S O) ? ? Lt1a);
+ apply lt_O_S
+ | fold unfold a1 a1 in H14;
+ lapply (prime_smallest_factor_n a Lt1a) as H16;
+ fold unfold a1 a1 in H16;
+ cut (a1 ≤ m) as H15;
+ [2: generalize in match (leb_to_Prop a1 m);
+ elim (leb a1 m); simplify in H12;
+ [ assumption
+ | elim (lt_smallest_factor_to_not_divides a m Lt1a H10 ? H9);
+ apply (not_le_to_lt ?? H12)]
+ | clearbody a1;
+ elim (H3 a);elim H12
+ [clear H13 H12;elim (H18 ? ? H14);elim (H2 a1);
+ apply H13
+ [assumption
+ |elim H17;apply (trans_le ? ? ? ? H20);
+ apply (trans_le ? ? ? H15);
+ apply lt_to_le;assumption
+ |intros;apply (trans_le ? (S m))
+ [apply le_S_S;assumption
+ |apply (trans_le ? ? ? H11);
+ elim (in_list_cons_case ? ? ? ? H19)
+ [rewrite > H20;apply le_n
+ |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]]
+ |apply in_list_head]]]
|elim (H3 a);elim H11
[elim H13;apply lt_to_le;assumption
|apply in_list_head]
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
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.
[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))