Proving primes in Coq

Question

I have a Coq function that classifies prime numbers. I exported it to Haskell and tested it; it works fine. I want to rigorously prove it indeed classifies primes, so I tried to prove the following theorem isPrimeCorrect:

(************)
(* helper'' *)
(************)
Fixpoint helper' (p m n : nat) : bool :=
  match m with
  | 0 => false
  | 1 => false
  | S m' => (orb ((mult m n) =? p) (helper' p m' n))
  end.

(**********)
(* helper *)
(**********)
Fixpoint helper (p m : nat) : bool :=
  match m with
  | 0 => false
  | S m' => (orb ((mult m m) =? p) (orb (helper' p m' m) (helper p m')))
  end.

(***********)
(* isPrime *)
(***********)
Fixpoint isPrime (p : nat) : bool :=
  match p with
  | 0 => false
  | 1 => false
  | S p' => (negb (helper p p'))
  end.

(***********)
(* divides *)
(***********)
Definition divides (n p : nat) : Prop :=
  exists (m : nat), ((mult m n) = p).

(*********)
(* prime *)
(*********)
Definition prime (p : nat) : Prop :=
  (p > 1) /\ (forall (n : nat), ((divides n p) -> ((n = 1) \/ (n = p)))).

(*****************************)
(* isPrime correctness proof *)
(*****************************)
Theorem isPrimeCorrect: forall (p : nat),
  ((isPrime p) = true) <-> (prime p).

I spent a good few hours on this theorem today with no actual progress. Actually, I was a bit surprised how difficult it is since I previously managed to prove pretty similar stuff. Any hints/clues how to proceed?

A few remarks : isPrime does not need to be declared as a Fixpoint; some of your definitions exist in the standard library (Nat.divide, ZArith.Znumtheory.prime). But maybe you want to experiment with your own definitions. — eponier

Yves Yves · Accepted Answer · 2019-04-09T08:01:59

You must explicitely write lemmas for each of the helping functions, which state exactly what you think this function does for you. For instance, I tried to do this for your helper' function and I came up with the following lemma:

Require Import Arith Psatz.

(************)
(* helper'' *)
(************)
Fixpoint helper' (p m n : nat) : bool :=
  match m with
  | 0 => false
  | 1 => false
  | S m' => (orb ((mult m n) =? p) (helper' p m' n))
  end.


Lemma helper'_correct :
  forall p m n,
    helper' p m n = true <-> exists k, (1 < k <= m /\ p = k * n).
Proof.
intros p; induction m as [ | m' IH]; intros n.
  split;[discriminate | ].
  intros [k [abs _]].
  lia.  (* Here the hypothesis abs has statement  1 <= k < 0 
            and lia recognizes that it is absurd. *)
destruct m' as [ | m''] eqn: E.
  split;[discriminate | intros [k [abs _]]; lia].
change (helper' p (S (S m'')) n) with (orb ((mult (S (S m'')) n) =? p)
                                    (helper' p (S m'') n)).
rewrite Bool.orb_true_iff.
split.
  intros [it | later].
    now exists (S (S m'')); split;[lia | symmetry; apply beq_nat_true ].
  rewrite IH in later; destruct later as [k [k1 k2]].
  exists k.
  (* here hypothesis k1 states 1 < k <= S m''
                     k2 states p = k * n
     and we need to prove 1 < k <= S (S m'') /\ p = k * n
     lia can do that automatically. *)
  lia.
intros [k [[k1 km] k2]].
apply le_lt_or_eq in km; rewrite or_comm in km; destruct km as [km | km].
  now left; rewrite <- km; rewrite Nat.eqb_eq, k2.
right; apply lt_n_Sm_le in km.
change (helper' p (S m'') n = true); rewrite IH.
exists k.
lia.
Qed.

Obviously there should also be a way to link the helper function wih the divides predicate.

Proving primes in Coq

1 Answers