include "nat/sqrt.ma".
include "nat/chebyshev_teta.ma".
include "nat/chebyshev.ma".
-include "list/list.ma".
+include "list/in.ma".
+include "list/sort.ma".
include "nat/o.ma".
let rec list_divides l n \def
| false => aux m1 (n-m1::acc)]]
in aux (pred n) [].
-let rec filter A l p on l \def
- match l with
- [ nil => nil A
- | cons (a:A) (tl:list A) => match (p a) with
- [ true => a::(filter A tl p)
- | false => filter A tl p ]].
-
-let rec length A (l:list A) on l \def
- match l with
- [ nil => O
- | cons (a:A) (tl:list A) => S (length A tl) ].
-
let rec list_n_aux n k \def
match n with
[ O => nil nat
definition sieve : nat \to list nat \def
\lambda m.sieve_aux [] (list_n m) m.
-definition ord_list \def
- \lambda l.
- \forall a,b,l1,l2.l = l1@(a::b::l2) \to b \leq a.
-
-definition in_list \def
- \lambda A.\lambda a:A.\lambda l:list A.
- \exists l1,l2.l = l1@(a::l2).
-
-lemma in_list_filter_to_p_true : \forall l,x,p.
-in_list nat x (filter nat l p) \to p x = true.
-intros;elim H;elim H1;clear H H1;generalize in match H2;generalize in match a;elim l 0
- [simplify;intro;elim l1
- [simplify in H;destruct H
- |simplify in H1;destruct H1]
- |intros;simplify in H1;apply (bool_elim ? (p t));intro;
- rewrite > H3 in H1;simplify in H1
- [generalize in match H1;elim l2
- [simplify in H4;destruct H4;assumption
- |simplify in H5;destruct H5;apply (H l3);assumption]
- |apply (H l2);assumption]]
-qed.
-
-lemma in_list_cons : \forall l,x,y.in_list nat x l \to in_list nat x (y::l).
-intros;unfold in H;unfold;elim H;elim H1;apply (ex_intro ? ? (y::a));
-apply (ex_intro ? ? a1);simplify;rewrite < H2;reflexivity.
-qed.
-
-lemma in_list_tail : \forall l,x,y.in_list nat x (y::l) \to x \neq y \to in_list nat x l.
-intros;elim H;elim H2;generalize in match H3;elim a
- [simplify in H4;destruct H4;elim H1;reflexivity
- |simplify in H5;destruct H5;apply (ex_intro ? ? l1);apply (ex_intro ? ? a1);
- reflexivity]
-qed.
-
-lemma in_list_filter : \forall l,p,x.in_list nat x (filter nat l p) \to in_list nat x l.
-intros;elim H;elim H1;generalize in match H2;generalize in match a;elim l 0
- [simplify;intro;elim l1
- [simplify in H3;destruct H3
- |simplify in H4;destruct H4]
- |intros;simplify in H4;apply (bool_elim ? (p t));intro
- [rewrite > H5 in H4;simplify in H4;generalize in match H4;elim l2
- [simplify in H6;destruct H6;apply (ex_intro ? ? []);apply (ex_intro ? ? l1);
- simplify;reflexivity
- |simplify in H7;destruct H7;apply in_list_cons;apply (H3 ? Hcut1);]
- |rewrite > H5 in H4;simplify in H4;apply in_list_cons;apply (H3 ? H4);]]
-qed.
-
-lemma in_list_filter_r : \forall l,p,x.in_list nat x l \to p x = true \to in_list nat x (filter nat l p).
-intros;elim H;elim H2;rewrite > H3;elim a
- [simplify;rewrite > H1;simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? (filter nat a1 p));
- reflexivity
- |simplify;elim (p t);simplify
- [apply in_list_cons;assumption
- |assumption]]
-qed.
-
-lemma in_list_head : \forall x,l.in_list nat x (x::l).
-intros;apply (ex_intro ? ? []);apply (ex_intro ? ? l);reflexivity;
-qed.
-
-lemma in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
- x = a \lor in_list A x l.
-intros;elim H;elim H1;clear H H1;generalize in match H2;elim a1
- [simplify in H;destruct H;left;reflexivity
- |simplify in H1;destruct H1;right;
- apply (ex_intro ? ? l1);
- apply (ex_intro ? ? a2);
- reflexivity]
-qed.
-
lemma divides_to_prime_divides : \forall n,m.1 < m \to m < n \to m \divides n \to
\exists p.p \leq m \land prime p \land p \divides n.
intros;apply (ex_intro ? ? (nth_prime (max_prime_factor m)));split
assumption]
qed.
-
-lemma le_length_filter : \forall A,l,p.length A (filter A l p) \leq length A l.
-intros;elim l
- [simplify;apply le_n
- |simplify;apply (bool_elim ? (p t));intro
- [simplify;apply le_S_S;assumption
- |simplify;apply le_S;assumption]]
-qed.
-
-inductive sorted (P:nat \to nat \to Prop): list nat \to Prop \def
-| sort_nil : sorted P []
-| sort_cons : \forall x,l.sorted P l \to (\forall y.in_list ? y l \to P x y)
- \to sorted P (x::l).
-
-definition sorted_lt : list nat \to Prop \def \lambda l.sorted lt l.
-
-definition sorted_gt : list nat \to Prop \def \lambda l.sorted gt l.
-
-lemma sorted_cons_to_sorted : \forall P,x,l.sorted P (x::l) \to sorted P l.
-intros;inversion H;intros
- [destruct H1
- |destruct H4;assumption]
-qed.
-
-lemma sorted_to_minimum : \forall P,x,l.sorted P (x::l) \to
- \forall y.in_list ? y l \to P x y.
-intros;inversion H;intros;
- [destruct H2
- |destruct H5;apply H4;assumption]
-qed.
-
-lemma not_in_list_nil : \forall A,a.\lnot in_list A a [].
-intros;intro;elim H;elim H1;generalize in match H2;elim a1
- [simplify in H3;destruct H3
- |simplify in H4;destruct H4]
-qed.
+definition sorted_lt \def sorted ? lt.
+definition sorted_gt \def sorted ? gt.
lemma sieve_prime : \forall t,k,l2,l1.
(\forall p.(in_list ? p l1 \to prime p \land p \leq k \land \forall x.in_list ? x l2 \to p < x) \land
|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;]
[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);
|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]]]
- |unfold;apply (ex_intro ? ? []);
- apply (ex_intro ? ? l);
- reflexivity]
- |elim (H3 t1);elim H11
+ |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]
|assumption]]
- |elim (H3 t1);elim H9
+ |elim (H3 a);elim H9
[elim H11;assumption
- |apply (ex_intro ? ? []);apply (ex_intro ? ? l);reflexivity]]
- |intros;elim (le_to_or_lt_eq t1 x)
+ |apply in_list_head]]
+ |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)]]
+ |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)
- [rewrite > H10;apply (ex_intro ? ? []);apply (ex_intro ? ? l1);
- reflexivity
+ |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 (ex_intro ? ? []);apply (ex_intro ? ? l);
- reflexivity]
+ |apply in_list_head]
|apply prime_to_lt_SO;elim (H2 p1);elim (H22 H18);
elim H24;assumption]]
|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)
[rewrite > H14;apply le_n
- |apply lt_to_le;apply (sorted_to_minimum ? ? ? H6);assumption]]]]
+ |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]]]
|elim (H3 x);split;intros;
[split
[elim H7
[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
|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]]]]
[assumption
|intros;unfold;elim (H2 y);elim (H8 H7);
apply H11;apply in_list_head]
- |generalize in match (sorted_cons_to_sorted ? ? ? H6);elim l
+ |generalize in match (sorted_cons_to_sorted ? ? ? ? H6);elim l
[simplify;assumption
- |simplify;elim (notb (divides_b t1 t2));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);
- |apply H7;apply (sorted_cons_to_sorted ? ? ? H8)]]]]]
-qed.
-
-lemma in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
-intros;elim H;elim H1;generalize in match H2;elim a
- [simplify in H3;destruct H3;reflexivity
- |simplify in H4;destruct H4;generalize in match Hcut1;elim l
- [simplify in H4;destruct H4
- |simplify in H5;destruct H5]]
+ |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);
+ |apply H7;apply (sorted_cons_to_sorted ? ? ? ? H8)]]]]]
qed.
lemma le_list_n_aux_k_k : \forall n,m,k.in_list ? n (list_n_aux m k) \to
k \leq n.
intros 2;elim m
[simplify in H;elim (not_in_list_nil ? ? H)
- |simplify in H1;elim H1;elim H2;generalize in match H3;elim a
- [simplify in H4;destruct H4;apply le_n
- |simplify in H5;destruct H5;apply lt_to_le;apply (H (S k));
- apply (ex_intro ? ? l);apply (ex_intro ? ? a1);assumption]]
+ |simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
+ [rewrite > H2;apply le_n
+ |apply lt_to_le;apply H;assumption]]
qed.
lemma in_list_SSO_list_n : \forall n.2 \leq n \to in_list ? 2 (list_n n).
-intros;elim H
- [simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? []);
- simplify;reflexivity
- |generalize in match H2;elim H1
- [simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? [3]);simplify;reflexivity
- |simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? (list_n_aux n2 3));
- simplify;reflexivity]]
+intros;elim H;simplify
+ [apply in_list_head
+ |generalize in match H2;elim H1;simplify;apply in_list_head]
qed.
lemma le_SSO_list_n : \forall m,n.in_list nat n (list_n m) \to 2 \leq n.
lemma le_list_n_aux : \forall n,m,k.in_list ? n (list_n_aux m k) \to n \leq k+m-1.
intros 2;elim m
[simplify in H;elim (not_in_list_nil ? ? H)
- |simplify in H1;elim H1;elim H2;generalize in match H3;elim a
- [simplify in H4;destruct H4;rewrite < plus_n_Sm;simplify;rewrite < minus_n_O;
+ |simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
+ [rewrite > H2;rewrite < plus_n_Sm;simplify;rewrite < minus_n_O;
rewrite > plus_n_O in \vdash (? % ?);apply le_plus_r;apply le_O_n
- |simplify in H5;destruct H5;rewrite < plus_n_Sm;apply (H (S k));
- apply (ex_intro ? ? l);apply (ex_intro ? ? a1);assumption]]
+ |rewrite < plus_n_Sm;apply (H (S k));assumption]]
qed.
lemma le_list_n : \forall n,m.in_list ? n (list_n m) \to n \leq m.
intros;elim (decidable_le 2 n)
[elim (sieve_sound1 ? H);assumption
|generalize in match (le_S_S_to_le ? ? (not_le_to_lt ? ? H));cases n
- [intro;apply sort_nil
+ [intro;simplify;apply sort_nil
|intros;lapply (le_S_S_to_le ? ? H1);rewrite < (le_n_O_to_eq ? Hletin);
- apply sort_nil]]
+ simplify;apply sort_nil]]
qed.
lemma in_list_sieve_to_prime : \forall n,p.2 \leq n \to in_list ? p (sieve n) \to
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.
|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
projects / helm.git / blobdiff