isPrime function with TLA+

Question

This question is about TLA+ using toolbox (https://github.com/tlaplus/tlaplus/releases) I haven't been able to find any tag about it. Sorry about that. This is why I only tagged with Primes. If I am missing something please be kind to add better tags or create the missing ones.

Here is the issue

There is a well known function and algorithm for GCD. Here it is.

------------------ MODULE Euclid -------------------------------
EXTENDS Naturals, TLC
CONSTANT K
Divides(i,j) == \E k \in 0..j: j = i * k
IsGCD(i,j,k) ==
    Divides(i,j)
    /\ Divides(i,k)
    /\ \A r \in 0..j \cup 0..k :
        (Divides(r,j ) /\ Divides(r,k)) => Divides(r,i)
    (* --algorithm EuclidSedgewick
    {
        variables m \in 1..K, n \in 1..m, u = m, v = n;
        {
            L1: while (u # 0) {
            if (u < v) { u := v || v := u };
            L2: u := u - v
            };
            assert IsGCD(v, m, n)
        }
    }
    *)

This is a well known solution which is working.

I'm now trying to write a isPrime function using this one. But I think what I'm doing is wrong. I would like to know if you have an idea.

isPrime(nb) ==
        \E k \in 2..nb: isGCD(nb,k,1) \/ isGCD(nb,k,nb)

Thanks

Answer 1

There are many way to express the notion that an integer is prime, however your attempt says that an integer N is prime if there exists some integer k in 2..N for which the gcd(k,n) = 1 or gcd(k,n) = n. This is easily seen to be incorrect, as 4 is clearly composite but gcd(3,4) = 1. And, of course, for every N prime or not, gcd(N, N) = N.

I'm not sure about the rules for TLA+, but I had a quick read of some documentation and here's my try at IsPrime

isPrime(nb) == \A k in 2..nb-1: ~Divides(k, nb)

or

isPrime(nb) == \A k in 1..nb: Divides(k, nb) => ( (k = 1) \/ (k=nb) )

or, if you really want to work IsGCD in there for some reason

isPrime(nb) == \A k in 1..nb: IsGCD(k, nb, d) => ( (d = 1) \/ (d = nb) )

or

isPrime(nb) == \A k in 2..nb-1: IsGCD(k, nb, d) => (d = 1)