Coq formalization of the infinitude of primes

primes_infinite.v

Require Import Arith Decidable Euclid Psatz Wf_nat.

Definition divides a b := exists k, b = k * a.
Definition prime p := 2 <= p /\ forall k, divides k p -> (k = 1 \/ k = p).

Lemma dec_divides k n: decidable (divides k n).
Proof with intuition.
  case (le_gt_dec k 0)...
  - case (le_gt_dec n 0).
    + left; exists 0...
    + right... destruct H.
      absurd (n = 0); nia.
  - pose proof modulo k g n.
    destruct H, e, H, x.
    + left; exists x0...
    + right... destruct H1.
      absurd ((x1 * k) = (x0 * k + (S x))); try congruence.
      case (le_dec x1 x0); nia.
Qed.

Lemma has_prime_divisor {n}: (n > 1) -> exists k, divides k n /\ prime k.
Proof with intuition.
  intros.
  assert (has_unique_least_element le (fun k => divides k n /\ 2 <= k)).
  - apply dec_inh_nat_subset_has_unique_least_element...
    + refine (dec_and _ _ (dec_divides _ _) (dec_le _ _)).
    + exists n...
  - do 4 destruct H0.
    unfold prime; exists x...
    case (le_gt_dec 2 k); destruct H4.
    + right; apply eq_sym, (H1 k)...
      * clear - H0 H4; destruct H0.
        exists (x0 * x1); nia.
      * pose proof (H2 x' (conj H6 H7)).
        enough (k <= x); transitivity x...
        clear - H3 H4.
        assert (x0 > 0); nia.
    + left; clear - H3 H4 g; nia.
Qed.

Lemma divides_fact {n x}: (x <= n /\ x > 1) -> divides x (fact n).
Proof with intuition.
  intro H; destruct H; induction H.
  - case_eq x...
    + absurd (x > 1)...
    + exists (fact n).
      simpl fact at 1; ring.
  - destruct IHle.
    exists ((S m) * x0).
    cbn [fact]; rewrite H1; ring.
Qed.

Theorem primes_infinite : forall n, exists p, p > n /\ prime p.
Proof with intuition.
  intro n.
  pose (z := 1 + (fact n)).
  assert (HZ: z > 1) by (pose proof (lt_O_fact n); intuition).
  enough ((exists x, prime x /\ x > 1 /\ divides x z) /\
          (forall x, x > n \/ ~ x > n) /\
          (forall x, ~(x > 1 /\ divides x z /\ ~ x > n))) by firstorder.
  repeat split...
  - decompose [ex and] (has_prime_divisor HZ).
    exists x...
    destruct H1...
  - apply dec_gt...
  - destruct H.
    assert (H3: exists m, m > 0 /\ z = 1 + (m*x)).
    + apply not_gt in H2.
      pose proof (divides_fact (conj H2 H0)).
      destruct H1 as [m]; clear - H1; exists m...
      pose proof (lt_O_fact n); nia.
    + decompose [ex and] H3.
      absurd (x0 * x = 1 + x1 * x); try congruence.
      clear - H0; case (le_dec x0 x1); nia.
Qed.

Check primes_infinite.