Let's see what it takes to trust an F* proof by walking through this proof that 733929337 is the largest truncatable palindromic prime.
Like in any other proof assistant, it requires trusting that the meta-theory of F* is sound. Unlike more mature systems like Coq that have small trusted kernels and independent proof checkers, in the case of F* this entails trusting a larger code base. Mistakes can be made (it has happened in LCF, Coq and F*), but if the author of a proof is well-intended, it's unlikely that they have exploited any unsound corner case to complete a proof. I'm well-intended :)
Starting from the main statement, we'll walk backwards identifying all definitions involved.
In this case, the statement reads:
val largest_prime_pyramid: n:prime_pyramid -> Lemma (n <= 733929337)
This says that 733929337 is the largest value of type prime_pyramid.
Assuming the author hasn't tampered with the pre-defined meaning of Lemma and <= (easy to check, but for another time), this statement only depends on the definition of prime_pyramid below.
val is_prime_pyramid: nat -> bool
let rec is_prime_pyramid n =
if n <= 9 then is_prime n
else is_prime n && is_palindrome n && no_zero n && is_prime_pyramid (truncate n)
type prime_pyramid = n:nat{is_prime_pyramid n}
The type prime_pyramid refines the pre-defined nat type (itself a refinement of the built-in int type). It is the type of natural numbers that satisfy the is_prime_pyramid predicate. is_prime_pyramid is recusively defined. For an integer n, it holds when either:
nis a single prime digit, ornis a palindromic prime without zeros andis_prime_pyramid (truncate n)holds.
This matches closely the definition one would expect. Everything checks out so far, but we still need to validate the definitions of is_prime, is_palindrome, no_zero and truncate.
Let's start with is_prime:
val is_prime: nat -> bool
let is_prime a = 1 < a && greatest_divisor a 2 1 = 1
It depends on greatest_divisor a b d, a recursive function that finds the largest divisor greater than or equal to b of a positive integer a , returning d if there is none. It does so by dumbly trying every number between b and the square root of a. This is schoolbook trial division.
val divides: pos -> nat -> bool
let divides b a = a % b = 0
val greatest_divisor: a:pos -> b:pos -> d:pos{d < b} -> Tot pos (decreases (a - b))
let rec greatest_divisor a b d =
if a < b * b then d
else greatest_divisor a (b + 1) (if b `divides` a then b else d)
When sqrt(a) < b, the function returns d. Otherwise, it continues from b + 1, updating the largest divisor d when b divides a. It is not hard to see that greatest_divisor a 2 1 computes the greatest divisor of a, and hence is_prime is correct.
In F*, by default all defintions are proven terminating. The decreases (a - b) clause says that the quantity a - b decreases in every recursive call (and is non-negative), so greatest_divisor terminates.
Let's have a look at is_palindrome now:
val is_palindrome: nat -> bool
let is_palindrome n = (n = reverse n)
type palindrome = n:nat{is_palindrome n}
A number is a palindrome if it equals its reverse. Fair enough.
The definition of reverse is short but slightly convoluted:
val reverse_acc: nat -> nat -> nat
let rec reverse_acc n m =
if n <= 9 then m + n else reverse_acc (n / 10) (10 * (m + n % 10))
val reverse: nat -> nat
let reverse n = reverse_acc n 0
To reverse a decimal number n, we successively divide it by 10 to remove
the last digit (n % 10), computing its reverse in an accumulator. So,
reverse (10^n * dn + ... + 10 * d1 + d0) = 10^n * d0 + ... + dn
No complications here. A number n has no zeros if it is a single non-zero digit, or it has more than one digit, its last digit is not 0 and n / 10 has no zeros.
val no_zero: nat -> bool
let rec no_zero n =
if n <= 9 then 0 < n % 10
else 0 < n % 10 && no_zero (n / 10)
Lastly, to truncate a palindromic number we
- remove its last digit by dividing it by 10;
- reverse the result;
- remove the last digit of this reverse (which is the first digit of the original number).
Note that if the number wasn't palindromic, we would need to reverse the result once more.
val truncate: palindrome -> nat
let truncate n = reverse (n / 10) / 10
That was it. To convince ourselves that the proof is correct we did not have to look at definitions used in proofs, or at intermediate lemmas. Surely, these are essential to complete the proof, but looking at them is unnecessary because F* checked the proof.
One last thing though; I'm well-intended, but I'm also lazy, so I left one lemma unproved. Such assumptions are easy to identify by the assume keyword:
val add: n:nat{n <= 9} -> nat -> nat
let add d n = 10 * reverse (10 * n + d) + d
assume val add_truncate: n:prime_pyramid{9 < n} ->
Lemma (n = add (n % 10) (truncate n))
This is more or less obvious: adding the truncated digits back to a prime pyramid with more than one digit gives the original number. This crucially relies on the number having no zeros. For instance, 10001 is a palindrome, but truncating it yields 0, and adding the last digit back results in 11, not 10001. I have tested this property in F* for all integers up to 6 digits long, but I think that proving it is not easy without a roundtrip converting numbers to strings (list of digits) and back. I may get back to this when I have more time to spare.
F* checks the proof in about 2 minutes on a modest laptop. The expensive part is to construct the list of all prime pyramids of length 9, and check that none can be extended. As expected, the bottleneck is the primality test. It can be improved by not checking even divisors, or only prime divisors with a full sieve.
Let's recap to see the parts of the proof we had to inspect, stripping everything else.
val divides: pos -> nat -> bool
let divides b a = a % b = 0
val greatest_divisor: a:pos -> b:pos -> d:pos{d < b} -> Tot pos (decreases (a - b))
let rec greatest_divisor a b d =
if a < b * b then d
else greatest_divisor a (b + 1) (if b `divides` a then b else d)
val is_prime: nat -> bool
let is_prime a = 1 < a && greatest_divisor a 2 1 = 1
val reverse_acc: nat -> nat -> nat
let rec reverse_acc n m =
if n <= 9 then m + n else reverse_acc (n / 10) (10 * (m + n % 10))
val reverse: nat -> nat
let reverse n = reverse_acc n 0
val is_palindrome: nat -> bool
let is_palindrome n = (n = reverse n)
type palindrome = n:nat{is_palindrome n}
val truncate: palindrome -> nat
let truncate n = reverse (n / 10) / 10
val no_zero: nat -> bool
let rec no_zero n =
if n <= 9 then 0 < n % 10
else 0 < n % 10 && no_zero (n / 10)
val is_prime_pyramid: nat -> bool
let rec is_prime_pyramid n =
if n <= 9 then is_prime n
else is_prime n && is_palindrome n && no_zero n && is_prime_pyramid (truncate n)
type prime_pyramid = n:nat{is_prime_pyramid n}
val add: n:nat{n <= 9} -> nat -> nat
let add d n = 10 * reverse (10 * n + d) + d
assume val add_truncate: n:prime_pyramid{9 < n} ->
Lemma (n = add (n % 10) (truncate n))
val largest_prime_pyramid: n:prime_pyramid -> Lemma (n <= 733929337)
Only 45 lines, not bad!
For the sake of readability, I haven't attempted to minimize this. Type definitions could be inlined, val declarations could be omitted, etc. Had there been good library support for reasoning about prime numbers in F* (there is such thing in Coq), I would also have saved a couple of definitions.
Assuming a trusted definition of is_prime, proving add_truncate, and inlining type definitions and val annotations, would result in a core proof of just 15 lines, 5 of which are empty. Now that's not bad at all: auditing these 10 lines of code is all it would take:
let rec reverse_acc (n:nat) (m:nat) : nat =
if n <= 9 then m + n else reverse_acc (n / 10) (10 * (m + n % 10))
let reverse (n:nat) = reverse_acc n 0
let truncate (n:nat{n = reverse n}) : nat = reverse (n / 10) / 10
let rec no_zero (n:nat) =
if n <= 9 then 0 < n % 10 else 0 < n % 10 && no_zero (n / 10)
let rec is_prime_pyramid (n:nat) =
if n <= 9 then is_prime n
else is_prime n && n = reverse n && no_zero n && is_prime_pyramid (truncate n)
val largest_prime_pyramid: (n:nat{is_prime_pyramid n}) -> Lemma (n <= 733929337)