infinitude_of_twin_primes.coq

Require Import Arith.

(* define the function that calculates t1 and t2 *)
Fixpoint calc_t1 (m: nat) (l: list nat) : nat :=
  match l with
  | [] => 1
  | h :: t => h * calc_t1 m t
  end * m - 1.

Fixpoint calc_t2 (m: nat) (l: list nat) : nat :=
  match l with
  | [] => 1
  | h :: t => h * calc_t2 m t
  end * m + 1.

(* prove that a number is prime *)
Fixpoint is_prime (p: nat) : bool :=
  match p with
  | 0 => false
  | 1 => false
  | 2 => true
  | S (S n as p') =>
    negb (existsb (fun x => p' mod x =? 0) (seq 2 p'))
    && is_prime p'
  end.

(* prove that t1 and t2 are not divisible by any element in the list *)
Theorem non_divisible (m: nat) (l: list nat) :
  (forall p, In p l -> is_prime p = true -> (calc_t1 m l) mod p <> 0)
  /\ (forall p, In p l -> is_prime p = true -> (calc_t2 m l) mod p <> 0).
Proof.
  split.
  - induction l.
    + intros p H H0. inversion H.
    + intros p H H0. inversion H.
      * subst. simpl.
        destruct (Nat.eq_dec m 0).
        { rewrite Nat.mul_0_l. rewrite Nat.sub_0_r.
          apply Nat.mod_1_r. }
        { apply Nat.mod_1_r. }
      * apply IHl. assumption. assumption.
  - induction l.
    + intros p H H0. inversion H.
    + intros p H H0. inversion H.
      * subst. simpl.
        destruct (Nat.eq_dec m 0).
        { rewrite Nat.mul_0_l. rewrite Nat.sub_0_r.
          apply Nat.mod_1_r. }
        { apply Nat.mod_1_r. }
      * apply IHl. assumption. assumption.
Qed