The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

There it is. You can skip prime_infinitude and prime_infinitude_0.

Require Import Omega ArithRing.

Ltac cut' H := cut H; [intro |]. 
Ltac omega' := abstract(omega).
Ltac ring' := abstract(ring).
Ltac congruence' := abstract(congruence).
Ltac tauto' := abstract(tauto).

Definition divide n m := exists k, n * k = m.

Theorem divisors_of_zero: forall n, divide n 0.
Proof. intros. exists 0. exact (mult_0_r n). Qed.

Theorem divider_gt m n: 0 < n -> n < m -> divide m n -> False.
Proof.
 intros. destruct H1.
 abstract( destruct x; [| rewrite mult_succ_r in H1; set (W := m * x); fold W 
in H1 ]; omega ).
Qed.

Definition divide_dec m n: { divide m n } + { divide m n -> False }.
 pattern n; apply lt_wf_rec; clear n; intros.
 destruct (lt_dec n m).
  destruct n.
   left. apply divisors_of_zero.
   right. abstract( apply (divider_gt m (S n)); omega; auto ).
  assert (n - m <= n) by omega'. pose proof (le_lt_eq_dec _ _ H0). destruct 
H1.
   destruct (H (n - m) l).
    left. destruct d. exists (S x). abstract( rewrite mult_succ_r, H1; omega 
).
    right. intro. apply f. destruct H1. exists (pred x).
     abstract( destruct x; [| simpl; rewrite <- H1, mult_succ_r; set (W := m 
* x)]; omega ).
   destruct n.
    left. apply divisors_of_zero.
    right. abstract( assert (m = 0) by omega; rewrite H1; intro; destruct H2; 
omega ).
Defined.

Theorem divide_of_succ m n: 1 < m -> divide m n -> divide m (S n) -> False.
Proof.
 intros. destruct H0, H1.
 abstract( assert (m * (x0 - x) = 1) by (rewrite <- H0 in H1; rewrite 
mult_minus_distr_l, H1; omega);
  apply mult_is_one in H2; omega ).
Qed.

Theorem divide_trans a b c: divide a b -> divide b c -> divide a c.
Proof.
 intros. destruct H, H0. exists (x * x0). abstract( rewrite <- H0, <- H; 
apply mult_assoc ).
Qed.

Fixpoint fact n :=
 match n with
 | O => 1
 | S m => fact m * S m
 end.

Theorem fact_neq_0 n: fact n <> 0.
 induction n; simpl.
  congruence'.
  abstract( apply NPeano.Nat.neq_mul_0; split; [ auto | congruence ] ).
Qed.

Theorem fact_thm_0 {k n}: 0 < k <= n -> divide k (fact n).
Proof.
 induction n. omega'.
  simpl. intro. assert (0 < k <= n \/ k = S n) by omega'. destruct H0.
   destruct (IHn H0). exists (x * S n). abstract( rewrite <- H1; apply 
mult_assoc ).
   exists (fact n). abstract( rewrite H0; apply mult_comm ).
Qed.

Theorem fact_thm_1 {k n}: k <= n -> divide (fact k) (fact n).
Proof.
 induction n; intros.
  inversion H. exists 1. auto.
  assert (k <= n \/ k = S n) by omega'. destruct H0.
   simpl. destruct (IHn H0). exists (S n * x). abstract( rewrite <- H1; ring' 
).
   exists 1. abstract( rewrite <- H0; ring ).
Qed.

Theorem fact_thm_2 n: n <= fact n.
Proof.
 induction n; simpl. auto. pose proof (fact_neq_0 n).
  abstract( assert (fact n = S (pred (fact n))) by omega'; rewrite H0; simpl;
   rewrite mult_succ_r; set (W := (pred (fact n)) * n); omega ).
Qed.

Definition is_prime n := 1 < n /\ (forall m, 1 < m -> divide m n -> m = n).

Theorem zero_not_prime: ~ is_prime 0. Proof. abstract( intro; destruct H; 
omega ). Qed.
Theorem one_not_prime: ~ is_prime 1. Proof. abstract( intro; destruct H; 
omega ). Qed.

(* For every N and X, either
   1) Forall M, such that 1 < M < X, M doesn't divide N,
OR 2) Exists M, such that 1 < M < X and M divides N. *)

Definition less_than_x_divides_dec n x:
  { exists m, 1 < m < x /\ divide m n } + { forall m, 1 < m < x -> divide m n 
-> False }.
Proof.
 induction x.
  right. abstract( intros; omega ).
  destruct IHx.
   left. destruct e. exists x0. abstract( destruct H; split; [ omega | auto ] 
).
   destruct x. right; abstract( intros; omega ). destruct x. right; abstract( 
intros; omega ). set (W := S (S x)).
   destruct (divide_dec W n).
    left. exists W. abstract( split; unfold W; [ omega | auto ] ).
    right. intros. assert (1 < m < W \/ m = W) by omega'. destruct H1.
     eauto. rewrite <- H1 in f0. auto.
Defined.

(* Forall N, bigger than 1: N is a prime IFF forall n, such that 1 < M < N, M 
doesn't divide N. *) 
Theorem prime_thm n:
  1 < n -> ((forall m, 1 < m < n -> divide m n -> False) <-> is_prime n).
Proof.
 split; intros.
  split; auto. intros. assert (1 < m < n \/ n <= m) by omega'. destruct H3.
   exfalso; eauto.
   assert (n < m \/ m = n) by omega'. destruct H4.
    exfalso. apply (divider_gt m n); auto; omega'.
    auto.
  destruct H0, H1. assert (m = n) by auto. omega'.
Qed.

(* Forall N, bigger than 1: N isn't a prime IFF exists such M, that 1 < M < N 
and M divides N. *)
Theorem not_prime_thm n:
  1 < n -> ((exists m, 1 < m < n /\ divide m n) <-> ~ is_prime n).
Proof.
 split; intros.
  intro. destruct H0, H0, H0, H1. assert (x = n) by auto. omega'.
  rewrite <- prime_thm in H0. destruct (less_than_x_divides_dec n n).
   destruct e. destruct H; eauto. elim (H0 f). auto.
Qed.

(* Every natural number is either a prime or not a prime. *)
Definition prime_dec n: { is_prime n } + { ~ is_prime n }.
Proof.
 destruct n. right; apply zero_not_prime. destruct n. right; apply 
one_not_prime.
 set (W := S (S n)). assert (1 < W) by abstract( unfold W; omega ).
 destruct (less_than_x_divides_dec W W).
  right. destruct e. apply not_prime_thm; eauto.
  left. apply prime_thm; auto.
Defined.

Theorem prime_divisor n: 1 < n -> exists p, is_prime p /\ divide p n.
 pattern n; apply lt_wf_ind; clear n; intros.
  destruct (prime_dec n).
   exists n. split. auto. exists 1. apply mult_1_r.
   apply not_prime_thm in n0; auto. destruct n0. destruct H1. destruct 
(prime_dec x).
    eauto.
    destruct H1. apply (H x) in H3; auto. destruct H3, H3. exists x0. split. 
auto. eapply divide_trans; eauto.
Qed.

(* Every list of natural numbers has the maximal element. *)
Theorem max_of_list (L: list nat): exists n, forall m, List.In m L -> m <= n.
Proof.
 induction L.
  exists 0. intros. inversion H.
  destruct IHL. simpl. destruct (lt_dec a x).
   exists x. intros. destruct H0. omega'. auto.
   exists a. intros. destruct H0. omega'. pose proof (H m H0). omega'.
Qed.

Theorem prime_infinitude: (exists L, forall n, is_prime n -> List.In n L) -> 
False.
Proof.
 intro. destruct H as [L H]. destruct (max_of_list L) as [max_prime H0].
 (* The list L contains are primes. *)
 assert (forall m, is_prime m -> 0 < m <= max_prime) by
  abstract( intros; split; [ destruct H1; omega | auto ] ).
 (* max_prime is the biggest prime. *)
 set (F := fact max_prime).
 (* F is factorial of max_prime *)
 assert (forall n, is_prime n -> divide n F).
  intros. apply fact_thm_0. auto.
 (* Every prime divides F. *)
 assert (forall n, is_prime n -> divide n (S F) -> False).
  intros. apply (divide_of_succ n F). destruct H3. auto. apply fact_thm_0. 
auto. auto.
 (* Therefore no prime divides S F. *)
 assert (F <> 0) by (apply fact_neq_0). assert (1 < S F) by omega.
 pose proof (prime_divisor (S F) H5). destruct H6, H6. eauto.
Qed.

Theorem prime_infinitude_0: (exists n, forall p, is_prime p -> p <= n) -> 
False.
 intro. destruct H. set (F := fact x).
 assert (forall n, is_prime n -> 0 < n <= x). intros. split. destruct H0. 
omega. auto.
 assert (forall n, is_prime n -> divide n F).
  intros. apply fact_thm_0. auto.
 assert (forall n, is_prime n -> divide n (S F) -> False).
  intros. apply (divide_of_succ n F). destruct H2. auto. apply fact_thm_0. 
auto. auto.
 assert (F <> 0) by (apply fact_neq_0). assert (1 < S F) by omega.
 pose proof (prime_divisor (S F) H4). destruct H5, H5. eauto.
Qed.

Theorem two_is_prime: is_prime 2.
 split. auto. intros. destruct H0.
 destruct x. omega. destruct x. omega. repeat rewrite mult_succ_r in H0.
 set (W := m * x) in H0. omega.
Qed.

Theorem prime_infinitude_1: forall n, exists p, is_prime p /\ p > n.
 intro. assert (n <= 1 \/ 1 < n) by omega. destruct H.
 exists 2. split. apply two_is_prime. omega.
 set (F := fact n).
 assert (forall m, is_prime m -> 1 < m -> m <= n -> divide m F).
  intros. apply fact_thm_0. omega'.
 assert (forall m, is_prime m -> m <= n -> divide m (S F) -> False).
  intros. apply (divide_of_succ m F). destruct H1. auto. apply H0. auto. 
destruct H1. auto. auto. auto.
 assert (F <> 0) by (apply fact_neq_0). assert (1 < S F) by omega.
 pose proof (prime_divisor (S F) H3). destruct H4. destruct H4.
 exists x. split. auto.
 assert (x <= n -> False). eauto. omega.
Qed.

Theorem prime_infinitude_2: forall L, exists p, is_prime p /\ ~ List.In p L.
 intro. destruct (max_of_list L) as [max_n H0]. destruct (prime_infinitude_1 
max_n) as [p H1].
 exists p. destruct H1. split; auto. intro. apply H0 in H2. omega'.
Qed.