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 + r → div b a → b > 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 ≤ r → r ≤ q → div r p → divinf p q.


Inductive nondivinf (p : nat) : nat → Prop :=
  | Base : nondivinf p 1
  | Step1 :
      ∀ q : nat, nondivinf p q → ¬ div (S q) p → nondivinf p (S q)
  | Step2 :
      ∀ q : nat, nondivinf p q → divinf (S q) q → nondivinf p (S q).

Hint Resolve Base Step1 Step2.


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

Hint Resolve Nondiv Div.

Definition Filtre (p n : nat) :=
  ∀ C : Set,
  (∀ P : nat → Set,
   (∀ q : nat, P q → natext p q) →
   (∀ q : nat, P q → P (S q)) → P n → C) → C.

Lemma Filtrebuild :
 ∀ (p n : nat) (P : nat → Set),
 (∀ q : nat, P q → natext p q) →
 (∀ q : nat, P q → P (S q)) → P n → Filtre p n.
intros.
red in |- ×.
intros.
apply (H2 P); trivial with v62.
Qed.

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

Lemma Filtretl : ∀ p n : nat, Filtre p n → Filtre 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 q → divinf p (S q).
simple induction 1; intros.
apply Bs with r; auto with v62.
Qed.
Hint Resolve lemme1.


Lemma Sift : ∀ p n : nat, 1 ≤ p → Filtre p n → Filtre (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 : nat → Set,
   (∀ q : nat, P q → natext q (S q)) →
   (∀ q : nat, P q → P (S q)) → P 1 → C) → C.

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


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

Inductive Pred (q : nat) : Set :=
    Predintro : 1 ≤ q → Filtre 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.