How to prove that a number is prime using Znumtheory in Coq

Link:: https://stackoverflow.com/q/49282773

Display all goals and responses

Question

I'm trying to prove that a number is prime using the Znumtheory library.

In Znumtheory primes are defined in terms of relative primes:

Inductive prime (p : Z) : Prop :=
  prime_intro :
    1 < p -> (forall n : Z, 1 <= n < p -> rel_prime n p) -> prime p.

So to prove that 3 is prime I should apply prime_intro to the goal. Here is my try:

Require Import Lia.
Theorem prime3 : prime 3.prime 3
Proof.prime 3
  apply prime_intro.1 < 3
forall n : Z, 1 <= n < 3 -> rel_prime n 3
  -1 < 3 lia.
  -forall n : Z, 1 <= n < 3 -> rel_prime n 3 intros.n: Z
H: 1 <= n < 3
rel_prime n 3 unfold rel_prime.n: Z
H: 1 <= n < 3
Zis_gcd n 3 1 apply Zis_gcd_intro.n: Z
H: 1 <= n < 3
(1 | n)
n: Z
H: 1 <= n < 3
(1 | 3)
n: Z
H: 1 <= n < 3
forall x : Z, (x | n) -> (x | 3) -> (x | 1)
    +n: Z
H: 1 <= n < 3
(1 | n) apply Z.divide_1_l.
    +n: Z
H: 1 <= n < 3
(1 | 3) apply Z.divide_1_l.
    +n: Z
H: 1 <= n < 3
forall x : Z, (x | n) -> (x | 3) -> (x | 1) intros.n: Z
H: 1 <= n < 3
x: Z
H0: (x | n)
H1: (x | 3)
(x | 1) Abort.

I don't know how to use the hypothesis H : 1 <= n < 3 which says that n is 1 or 2. I could destruct it, apply lt_eq_cases and destruct it again, but I would be stuck with a useless 1 < n in the first case.

I wasn't expecting to have a hard time with something that looks so simple.

Answer (larsr)

Here is a proof that I think is quite understandable as one steps through it. It stays at the level of number theory and doesn't unfold definitions that much. I put in some comments, don't know if it makes it more or less readable. But try to step through it in the IDE, if you care for it...

Require Import ZArith.
Require Import Znumtheory.

Inductive prime (p : Z) : Prop :=
  prime_intro :
    1 < p -> (forall n : Z, 1 <= n < p -> rel_prime n p) -> prime p.

Require Import Lia.

Theorem prime3 : prime 3.prime 3
Proof.prime 3
  constructor.1 < 3
forall n : Z, 1 <= n < 3 -> rel_prime n 3
  -1 < 3 lia.                        (* prove 1 < 3 *)
  -forall n : Z, 1 <= n < 3 -> rel_prime n 3 intros.n: Z
H: 1 <= n < 3
rel_prime n 3 constructor.        (* prove rel_prime n 3 *)n: Z
H: 1 <= n < 3
(1 | n)
n: Z
H: 1 <= n < 3
(1 | 3)
n: Z
H: 1 <= n < 3
forall x : Z, (x | n) -> (x | 3) -> (x | 1)
    +n: Z
H: 1 <= n < 3
(1 | n) exists n.n: Z
H: 1 <= n < 3
n = n * 1 lia.            (* prove (1 | n) *)
    +n: Z
H: 1 <= n < 3
(1 | 3) exists 3.n: Z
H: 1 <= n < 3
3 = 3 * 1 lia.            (* prove (1 | 3) *)

      (* our goal is now (x | 1), and we know (x | n) and (x | 3) *)
    +n: Z
H: 1 <= n < 3
forall x : Z, (x | n) -> (x | 3) -> (x | 1) assert (Hn : n = 1 \/ n = 2) by lia.n: Z
H: 1 <= n < 3
Hn: n = 1 \/ n = 2
forall x : Z, (x | n) -> (x | 3) -> (x | 1) clear H. (* because 1 <= n < 3 *)n: Z
Hn: n = 1 \/ n = 2
forall x : Z, (x | n) -> (x | 3) -> (x | 1)
      case Hn.                  (* consider cases n=1 and n=2 *)n: Z
Hn: n = 1 \/ n = 2
n = 1 -> forall x : Z, (x | n) -> (x | 3) -> (x | 1)
n: Z
Hn: n = 1 \/ n = 2
n = 2 -> forall x : Z, (x | n) -> (x | 3) -> (x | 1)
      *n: Z
Hn: n = 1 \/ n = 2
n = 1 -> forall x : Z, (x | n) -> (x | 3) -> (x | 1) intros.n: Z
Hn: n = 1 \/ n = 2
H: n = 1
x: Z
H0: (x | n)
H1: (x | 3)
(x | 1) subst.Hn: 1 = 1 \/ 1 = 2
x: Z
H0: (x | 1)
H1: (x | 3)
(x | 1)
        (* case n = 1: proves (x | 1) because we know (x | n) *)
        trivial.
      *n: Z
Hn: n = 1 \/ n = 2
n = 2 -> forall x : Z, (x | n) -> (x | 3) -> (x | 1) intros.n: Z
Hn: n = 1 \/ n = 2
H: n = 2
x: Z
H0: (x | n)
H1: (x | 3)
(x | 1) subst.   (* case n = 2: we know (x | n) and (x | 3) *)Hn: 2 = 1 \/ 2 = 2
x: Z
H0: (x | 2)
H1: (x | 3)
(x | 1)
        assert (Hgcd: (x | Z.gcd 2 3)) by (apply Z.gcd_greatest; trivial).Hn: 2 = 1 \/ 2 = 2
x: Z
H0: (x | 2)
H1: (x | 3)
Hgcd: (x | Z.gcd 2 3)
(x | 1)
        (* Z.gcd_greatest: (x | 2) -> x | 3) -> (x | Z.gcd 2 3) *)
        apply Hgcd.         (* prove (x | 1), because Z.gcd 2 3 = 1 *)
Qed.

Answer (Arthur Azevedo De Amorim)

The lemma you mentioned is actually proved in that library, under the name prime_3. You can look up its proof on GitHub.

You mentioned how strange it is to have such a hard time to prove something so simple. Indeed, the proof in the standard library is quite complicated. Luckily, there are much better ways to work out this result. The Mathematical Components library advocates for a different style of development based on boolean properties. There, prime is not an inductively defined predicate, but a function nat -> bool that checks whether its argument is prime. Because of this, we can prove such simple facts by computation:

From Coq Require Import ssreflect ssrbool.
From mathcomp Require Import ssrnat prime.

Lemma prime_3 : prime 3.prime 3 Proof.prime 3 reflexivity. Qed.

There is a bit of magic going on here: the library declares a coercion is_true : bool -> Prop that is automatically inserted whenever a boolean is used in a place where a proposition is expected. It is defined as follows:

Definition is_true (b : bool) : Prop := b = true.

Thus, what prime_3 really is proving above is prime 3 = true, which is what makes that simple proof possible.

The library allows you to connect this boolean notion of what a prime number is to a more conventional one via a reflection lemma:

From mathcomp Require Import div eqtype.

Lemma primeP p :
  reflect (p > 1 /\ forall d, d %| p -> xpred2 1 p d) (prime p).p: nat
reflect
  (1 < p /\ (forall d : nat, d %| p -> xpred2 1 p d))
  (prime p)

Unpacking notations and definitions, what this statement says is that prime p equals true if and only if p > 1 and every d that divides p is equal to 1 or p. I am afraid it would be a lengthy detour to explain how this reflection lemma works exactly, but if you find this interesting I strongly encourage you to look up more about Mathematical Components.

Answer (epoiner)

I have a variant of @larsr's proof.

Require Import ZArith.
Require Import Znumtheory.
Require Import Lia.

Theorem prime3 : prime 3.prime 3
Proof.prime 3
  constructor.1 < 3
forall n : Z, 1 <= n < 3 -> rel_prime n 3
  -1 < 3 lia.
  -forall n : Z, 1 <= n < 3 -> rel_prime n 3 intros.n: Z
H: 1 <= n < 3
rel_prime n 3 assert (n = 1 \/ n = 2) as Ha by lia.n: Z
H: 1 <= n < 3
Ha: n = 1 \/ n = 2
rel_prime n 3
    destruct Ha; subst n; apply Zgcd_is_gcd.
Qed.

Like @larsr's proof, we prove that 1 < 3 using lia and then prove that either n = 1 or n = 2 using lia again.

To prove rel_prime 1 3 and rel_prime 2 3 which are defined in terms of Zis_gcd, we apply Zgcd_is_gcd. This lemma states that computing the gcd is enough. This is trivial on concrete inputs like (1, 3) and (2, 3).

EDIT: We can generalize this result, using only Gallina. We define a boolean function is_prime that we prove correct w.r.t. the inductive specification prime. I guess this can be done in a more elegant way, but I am confused with all the lemmas related to Z. Moreover, some of the definitions are opaque and cannot be used (at least directly) to define a computable function.

Require Import ZArith.
Require Import Znumtheory.
Require Import Lia.
Require Import Bool.
Require Import Recdef.

(** [for_all] checks that [f] is true for any integer between 1 and [n] *)
Function for_all (f : Z -> bool) n {measure Z.to_nat n} :=
  if n <=? 1 then true
  else f (n - 1) && for_all f (n - 1).(Z -> bool) ->
forall n : Z,
(n <=? 1) = false ->
(Z.to_nat (n - 1) < Z.to_nat n)%nat
Proof.(Z -> bool) ->
forall n : Z,
(n <=? 1) = false ->
(Z.to_nat (n - 1) < Z.to_nat n)%nat
  intros.f: Z -> bool
n: Z
teq: (n <=? 1) = false
(Z.to_nat (n - 1) < Z.to_nat n)%nat apply Z.leb_nle in teq.f: Z -> bool
n: Z
teq: ~ n <= 1
(Z.to_nat (n - 1) < Z.to_nat n)%nat apply Z2Nat.inj_lt; lia.
Defined.

Lemma for_all_spec : forall f n,
    for_all f n = true -> forall k, 1 <= k < n -> f k = true.forall (f : Z -> bool) (n : Z),
for_all f n = true ->
forall k : Z, 1 <= k < n -> f k = true
Proof.forall (f : Z -> bool) (n : Z),
for_all f n = true ->
forall k : Z, 1 <= k < n -> f k = true
  intros.f: Z -> bool
n: Z
H: for_all f n = true
k: Z
H0: 1 <= k < n
f k = true assert (0 <= n) by lia.f: Z -> bool
n: Z
H: for_all f n = true
k: Z
H0: 1 <= k < n
H1: 0 <= n
f k = true revert n H1 k H0 H.f: Z -> bool
forall n : Z,
0 <= n ->
forall k : Z,
1 <= k < n -> for_all f n = true -> f k = true
  apply (natlike_ind
           (fun n => forall k : Z,
                1 <= k < n -> for_all f n = true -> f k = true)); intros.f: Z -> bool
k: Z
H: 1 <= k < 0
H0: for_all f 0 = true
f k = true
f: Z -> bool
x: Z
H: 0 <= x
H0: forall k : Z,
1 <= k < x -> for_all f x = true -> f k = true
k: Z
H1: 1 <= k < Z.succ x
H2: for_all f (Z.succ x) = true
f k = true
  -f: Z -> bool
k: Z
H: 1 <= k < 0
H0: for_all f 0 = true
f k = true lia.
  -f: Z -> bool
x: Z
H: 0 <= x
H0: forall k : Z,
1 <= k < x -> for_all f x = true -> f k = true
k: Z
H1: 1 <= k < Z.succ x
H2: for_all f (Z.succ x) = true
f k = true rewrite for_all_equation in H2.f: Z -> bool
x: Z
H: 0 <= x
H0: forall k : Z,
1 <= k < x -> for_all f x = true -> f k = true
k: Z
H1: 1 <= k < Z.succ x
H2: (if Z.succ x <=? 1
 then true
 else
  f (Z.succ x - 1) && for_all f (Z.succ x - 1)) =
true
f k = true
    destruct (Z.leb_spec0 (Z.succ x) 1).f: Z -> bool
x: Z
H: 0 <= x
H0: forall k : Z,
1 <= k < x -> for_all f x = true -> f k = true
k: Z
H1: 1 <= k < Z.succ x
H2: true = true
l: Z.succ x <= 1
f k = true
f: Z -> bool
x: Z
H: 0 <= x
H0: forall k : Z,
1 <= k < x -> for_all f x = true -> f k = true
k: Z
H1: 1 <= k < Z.succ x
H2: f (Z.succ x - 1) && for_all f (Z.succ x - 1) =
true
n: ~ Z.succ x <= 1
f k = true
    +f: Z -> bool
x: Z
H: 0 <= x
H0: forall k : Z,
1 <= k < x -> for_all f x = true -> f k = true
k: Z
H1: 1 <= k < Z.succ x
H2: true = true
l: Z.succ x <= 1
f k = true lia.
    +f: Z -> bool
x: Z
H: 0 <= x
H0: forall k : Z,
1 <= k < x -> for_all f x = true -> f k = true
k: Z
H1: 1 <= k < Z.succ x
H2: f (Z.succ x - 1) && for_all f (Z.succ x - 1) =
true
n: ~ Z.succ x <= 1
f k = true replace (Z.succ x - 1) with x in H2 by lia.f: Z -> bool
x: Z
H: 0 <= x
H0: forall k : Z,
1 <= k < x -> for_all f x = true -> f k = true
k: Z
H1: 1 <= k < Z.succ x
H2: f x && for_all f x = true
n: ~ Z.succ x <= 1
f k = true apply andb_true_iff in H2.f: Z -> bool
x: Z
H: 0 <= x
H0: forall k : Z,
1 <= k < x -> for_all f x = true -> f k = true
k: Z
H1: 1 <= k < Z.succ x
H2: f x = true /\ for_all f x = true
n: ~ Z.succ x <= 1
f k = true
      assert (k < x \/ k = x) by lia.f: Z -> bool
x: Z
H: 0 <= x
H0: forall k : Z,
1 <= k < x -> for_all f x = true -> f k = true
k: Z
H1: 1 <= k < Z.succ x
H2: f x = true /\ for_all f x = true
n: ~ Z.succ x <= 1
H3: k < x \/ k = x
f k = true destruct H3.f: Z -> bool
x: Z
H: 0 <= x
H0: forall k : Z,
1 <= k < x -> for_all f x = true -> f k = true
k: Z
H1: 1 <= k < Z.succ x
H2: f x = true /\ for_all f x = true
n: ~ Z.succ x <= 1
H3: k < x
f k = true
f: Z -> bool
x: Z
H: 0 <= x
H0: forall k : Z,
1 <= k < x -> for_all f x = true -> f k = true
k: Z
H1: 1 <= k < Z.succ x
H2: f x = true /\ for_all f x = true
n: ~ Z.succ x <= 1
H3: k = x
f k = true
      *f: Z -> bool
x: Z
H: 0 <= x
H0: forall k : Z,
1 <= k < x -> for_all f x = true -> f k = true
k: Z
H1: 1 <= k < Z.succ x
H2: f x = true /\ for_all f x = true
n: ~ Z.succ x <= 1
H3: k < x
f k = true apply H0; [lia | apply H2].
      *f: Z -> bool
x: Z
H: 0 <= x
H0: forall k : Z,
1 <= k < x -> for_all f x = true -> f k = true
k: Z
H1: 1 <= k < Z.succ x
H2: f x = true /\ for_all f x = true
n: ~ Z.succ x <= 1
H3: k = x
f k = true subst k.f: Z -> bool
x: Z
H: 0 <= x
H0: forall k : Z,
1 <= k < x -> for_all f x = true -> f k = true
H1: 1 <= x < Z.succ x
H2: f x = true /\ for_all f x = true
n: ~ Z.succ x <= 1
f x = true apply H2.
Qed.

Definition is_prime (p : Z) :=
  (1 <? p) && for_all (fun k => Z.gcd k p =? 1) p.

Theorem is_prime_correct : forall z, is_prime z = true -> prime z.forall z : Z, is_prime z = true -> prime z
Proof.forall z : Z, is_prime z = true -> prime z
  intros.z: Z
H: is_prime z = true
prime z unfold is_prime in H.z: Z
H: (1 <? z) &&
for_all (fun k : Z => Z.gcd k z =? 1) z = true
prime z apply andb_true_iff in H.z: Z
H: (1 <? z) = true /\
for_all (fun k : Z => Z.gcd k z =? 1) z = true
prime z
  destruct H as (H & H0).z: Z
H: (1 <? z) = true
H0: for_all (fun k : Z => Z.gcd k z =? 1) z = true
prime z constructor.z: Z
H: (1 <? z) = true
H0: for_all (fun k : Z => Z.gcd k z =? 1) z = true
1 < z
z: Z
H: (1 <? z) = true
H0: for_all (fun k : Z => Z.gcd k z =? 1) z = true
forall n : Z, 1 <= n < z -> rel_prime n z
  -z: Z
H: (1 <? z) = true
H0: for_all (fun k : Z => Z.gcd k z =? 1) z = true
1 < z apply Z.ltb_lt.z: Z
H: (1 <? z) = true
H0: for_all (fun k : Z => Z.gcd k z =? 1) z = true
(1 <? z) = true assumption.
  -z: Z
H: (1 <? z) = true
H0: for_all (fun k : Z => Z.gcd k z =? 1) z = true
forall n : Z, 1 <= n < z -> rel_prime n z intros.z: Z
H: (1 <? z) = true
H0: for_all (fun k : Z => Z.gcd k z =? 1) z = true
n: Z
H1: 1 <= n < z
rel_prime n z apply for_all_spec with (k := n) in H0; try assumption.z: Z
H: (1 <? z) = true
n: Z
H0: (Z.gcd n z =? 1) = true
H1: 1 <= n < z
rel_prime n z
    unfold rel_prime.z: Z
H: (1 <? z) = true
n: Z
H0: (Z.gcd n z =? 1) = true
H1: 1 <= n < z
Zis_gcd n z 1 apply Z.eqb_eq in H0.z: Z
H: (1 <? z) = true
n: Z
H0: Z.gcd n z = 1
H1: 1 <= n < z
Zis_gcd n z 1 rewrite <- H0.z: Z
H: (1 <? z) = true
n: Z
H0: Z.gcd n z = 1
H1: 1 <= n < z
Zis_gcd n z (Z.gcd n z)
    apply Zgcd_is_gcd.
Qed.

The proof becomes nearly as simple as @Arthur's one.

Theorem prime113 : prime 113.prime 113
Proof.prime 113
  apply is_prime_correct; reflexivity.
Qed.

Answer (larsr)

Fun fact: @epoiner's answer can be used together with Ltac in a proof script for any prime number.

Theorem prime113 : prime 113.prime 113
Proof.prime 113
  constructor.1 < 113
forall n : Z, 1 <= n < 113 -> rel_prime n 113
  -1 < 113 lia.
  -forall n : Z, 1 <= n < 113 -> rel_prime n 113 intros n H;
      repeat match goal with
             | H : 1 <= ?n < ?a  |- _ =>
               assert (Hn: n = a - 1 \/ 1 <= n < a - 1) by lia;
                 clear H; destruct Hn as [Hn | H];
                   [subst n; apply Zgcd_is_gcd | simpl in H; try lia]
             end.
Qed.

However, the proof term gets unwieldy, and checking becomes slower and slower. This is why it small scale reflection (ssreflect) where computation is moved into the type checking probably is preferrable in the long run. It's hard to beat @Arthur Azevedo De Amorim's proof: Proof. reflexivity. Qed. :-) Both in terms of computation time, and memory-wise.