Library Streams.Eratosthene

Require Import Arith.
Require Import Peano_dec.
Require Import Euclid.

Definition div (b a : nat) : Prop := q : nat, a = q × b.

Lemma div_mod_O :
a b r q : nat, a = q × b + rdiv b ab > r → 0 = r.
simple induction 2; intros q' Hq'.
replace r with ((q' - q) × b); intros.
elim (mult_O_le b (q' - q)); intros.
rewrite H2; auto with v62.
absurd (b (q' - q) × b); auto with v62.
rewrite mult_minus_distr_r.
symmetry in |- *; apply plus_minus.
elim H; auto with v62.
Qed.

Lemma div_dec : p q : nat, 0 < p{div p q} + {¬ div p q}.
intros; elim modulo with p q; intros; auto with v62.
elim (eq_nat_dec 0 x); intro y0.
left; elim p0; intros q0 Hq0.
red in |- *; q0.
elim Hq0; intros.
rewrite H0.
elim y0; auto with v62.
right; red in |- *; intro; absurd (0 = x); trivial with v62.
elim p0; simple induction 1; intros.
apply div_mod_O with q p x0; auto with v62.
Qed.

Inductive divinf (p q : nat) : Prop :=
Bs : r : nat, 2 rr qdiv r pdivinf p q.

Inductive nondivinf (p : nat) : natProp :=
| Base : nondivinf p 1
| Step1 :
q : nat, nondivinf p q¬ div (S q) pnondivinf p (S q)
| Step2 :
q : nat, nondivinf p qdivinf (S q) qnondivinf p (S q).

Hint Resolve Base Step1 Step2.

Inductive natext (p n : nat) : Set :=
| Nondiv : nondivinf n pnatext p n
| Div : divinf n pnatext p n.

Hint Resolve Nondiv Div.

Definition Filtre (p n : nat) :=
C : Set,
( P : natSet,
( q : nat, P qnatext p q) →
( q : nat, P qP (S q)) → P nC) → C.

Lemma Filtrebuild :
(p n : nat) (P : natSet),
( q : nat, P qnatext p q) →
( q : nat, P qP (S q)) → P nFiltre p n.
intros.
red in |- ×.
intros.
apply (H2 P); trivial with v62.
Qed.

Lemma Filtrehd : p n : nat, Filtre p nnatext p n.
intros.
apply H.
auto with v62.
Qed.
Hint Immediate Filtrehd.

Lemma Filtretl : p n : nat, Filtre p nFiltre p (S n).
intros.
apply H.
intros.
apply Filtrebuild with P; auto with v62.
Qed.
Hint Resolve Filtretl.

Lemma lemme1 : q p : nat, divinf p qdivinf p (S q).
simple induction 1; intros.
apply Bs with r; auto with v62.
Qed.
Hint Resolve lemme1.

Lemma Sift : p n : nat, 1 pFiltre p nFiltre (S p) n.
intros.
apply Filtrebuild with (Filtre p); auto with v62.
intros; elim (Filtrehd p q); intros; auto with v62.
elim (div_dec (S p) q); auto with v62.
intros; apply Div.
apply Bs with (S p); auto with v62.
Qed.

Definition Eratosthene :=
C : Set,
( P : natSet,
( q : nat, P qnatext q (S q)) →
( q : nat, P qP (S q)) → P 1 → C) → C.

Lemma Eratobuild :
P : natSet,
( q : nat, P qnatext q (S q)) →
( q : nat, P qP (S q)) → P 1 → Eratosthene.
red in |- *; intros.
apply (H2 P); auto with v62.
Qed.

Lemma lemme2 :
q r : nat, divinf (S q) qnatext q rnatext (S q) r.
simple induction 2; auto with v62.
Qed.
Hint Resolve lemme2.

Inductive Pred (q : nat) : Set :=
Predintro : 1 qFiltre q (S q) → Pred q.
Hint Resolve Predintro.

Theorem Crible : Eratosthene.
apply Eratobuild with Pred. intros; apply Filtrehd.
elim H; trivial with v62.
intros; elim H; intros.
apply Predintro; auto with v62.
elim (Filtrehd q (S q) f); intro.
apply Filtretl.
apply Sift; auto with v62.
apply f; intros.
apply Filtrebuild with P; auto with v62.
apply Predintro; auto with v62.
apply Filtrebuild with (natext 1); auto with v62.
Qed.