sbv-13.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.TP.Primes

Description

Prove that there are an infinite number of primes. Along the way we formalize and prove a number of properties about divisibility as well. Our proof is inspired by the ACL2 proof in https://github.com/acl2/acl2/blob/master/books/projects/numbers/euclid.lisp.

Synopsis

Divisibility

dvd :: SInteger -> SInteger -> SBool Source #

Divides relation. By definition 0 only divides 0. (But every number divides 0).

dividesProduct :: TP (Proof (Forall "x" Integer -> Forall "y" Integer -> Forall "z" Integer -> SBool)) Source #

\(x \mid y \implies x \mid y * z\)

Proof

Expand
>>> runTP dividesProduct
Lemma: dividesProduct
  Step: 1 (2 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2.1                         Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.2.3                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] dividesProduct :: Ɐx ∷ Integer → Ɐy ∷ Integer → Ɐz ∷ Integer → Bool

dividesTransitive :: TP (Proof (Forall "x" Integer -> Forall "y" Integer -> Forall "z" Integer -> SBool)) Source #

\(x \mid y \land y \mid z \implies x \mid z\)

Proof

Expand
>>> runTP dividesTransitive
Lemma: dividesProduct                   Q.E.D.
Lemma: dividesTransitive
  Step: 1 (2 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2.1                         Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.2.3 (hard)                  Q.E.D.
    Step: 1.2.4                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] dividesTransitive :: Ɐx ∷ Integer → Ɐy ∷ Integer → Ɐz ∷ Integer → Bool

The least divisor

ld :: SInteger -> SInteger -> SInteger Source #

The definition of primality will depend on the notion of least divisor. Given k and n, the least-divisor of n that is at least k is the number that is at least k and divides n evenly. The idea is that a number is prime if the least divisor starting from 2 is itself.

leastDivisorDivides :: TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)) Source #

\(1 < k \leq n \implies \mathit{ld}\,k\,n \mid n \land k \leq \mathit{ld}\,k\,n \leq n\)

Proof

Expand
>>> runTP leastDivisorDivides
Inductive lemma (strong): leastDivisorDivides
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2                           Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] leastDivisorDivides :: Ɐk ∷ Integer → Ɐn ∷ Integer → Bool

leastDivisorIsLeast :: TP (Proof (Forall "k" Integer -> Forall "n" Integer -> Forall "d" Integer -> SBool)) Source #

\(1 < k \leq n \land d \mid n \land k \leq d \implies \mathit{ld}\,k\,n \leq d\)

Proof

Expand
>>> runTP leastDivisorIsLeast
Inductive lemma (strong): leastDivisorisLeast
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2                           Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] leastDivisorisLeast :: Ɐk ∷ Integer → Ɐn ∷ Integer → Ɐd ∷ Integer → Bool

leastDivisorTwice :: TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool)) Source #

\(n \geq k \geq 2 \implies \mathit{ld}\,k\,(\mathit{ld}\,k\,n) = \mathit{ld}\,k\,n\)

Proof

Expand
>>> runTP leastDivisorTwice
Lemma: dividesTransitive                Q.E.D.
Lemma: leastDivisorDivides              Q.E.D.
Lemma: leastDivisorIsLeast              Q.E.D.
Lemma: helper1                          Q.E.D.
Lemma: helper2                          Q.E.D.
Lemma: helper3                          Q.E.D.
Lemma: helper4                          Q.E.D.
Lemma: helper5
  Step: 1                               Q.E.D.
  Result:                               Q.E.D.
Lemma: leastDivisorTwice                Q.E.D.
[Proven] leastDivisorTwice :: Ɐk ∷ Integer → Ɐn ∷ Integer → Bool

Primality

isPrime :: SInteger -> SBool Source #

A number is prime if its least divisor greater than or equal to 2 is itself.

primeAtLeast2 :: TP (Proof (Forall "p" Integer -> SBool)) Source #

\(\mathit{isPrime}\,p \implies p \geq 2\)

Proof

Expand
>>> runTP primeAtLeast2
Lemma: primeAtLeast2                    Q.E.D.
[Proven] primeAtLeast2 :: Ɐp ∷ Integer → Bool

leastDivisorIsPrime :: TP (Proof (Forall "n" Integer -> SBool)) Source #

\(n \geq 2 \implies \mathit{isPrime}\,(\mathit{ld}\,2\,n)\)

Proof

Expand
>>> runTP leastDivisorIsPrime
Lemma: leastDivisorTwice                Q.E.D.
Lemma: leastDivisorDivides              Q.E.D.
Lemma: leastDivisorIsPrime
  Step: 1                               Q.E.D.
  Result:                               Q.E.D.
[Proven] leastDivisorIsPrime :: Ɐn ∷ Integer → Bool

leastPrimeDivisor :: SInteger -> SInteger Source #

The least prime divisor is the least divisor of it starting from 2. By leastDivisorIsPrime, this number is guaranteed to be prime.

Formalizing factorial

fact :: SInteger -> SInteger Source #

The factorial function.

factAtLeast1 :: TP (Proof (Forall "n" Integer -> SBool)) Source #

\(n! \geq 1\)

Proof

Expand
>>> runTP factAtLeast1
Inductive lemma: factAtLeast1
  Step: Base                            Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2.1                         Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] factAtLeast1 :: Ɐn ∷ Integer → Bool

dividesFact :: TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool)) Source #

\(1 \leq k \land k \leq n \implies k \mid n!\)

Proof

Expand
>>> runTP dividesFact
Lemma: dividesProduct                   Q.E.D.
Inductive lemma: dividesFact
  Step: Base                            Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2 (2 way case split)
    Step: 2.1.1                         Q.E.D.
    Step: 2.1.2                         Q.E.D.
    Step: 2.2.1                         Q.E.D.
    Step: 2.2.2                         Q.E.D.
    Step: 2.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] dividesFact :: Ɐn ∷ Integer → Ɐk ∷ Integer → Bool

notDividesFactP1 :: TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool)) Source #

\(1 \leq k \land k \leq n \implies \neg (k \mid n! + 1)\)

Proof

Expand
>>> runTP notDividesFactP1
Lemma: dividesFact                      Q.E.D.
Lemma: notDividesFactP1
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Result:                               Q.E.D.
[Proven] notDividesFactP1 :: Ɐn ∷ Integer → Ɐk ∷ Integer → Bool

Finding a greater prime

greaterPrime :: SInteger -> SInteger Source #

Given a number, return another number which is both prime and is larger than the input. Note that we don't claim to return the closest prime to the input. Just some prime that is larger, as we shall prove.

greaterPrimeDivides :: TP (Proof (Forall "n" Integer -> SBool)) Source #

\(\mathit{greaterPrime}\, n \mid n! + 1\)

Proof

Expand
>>> runTP greaterPrimeDivides
Lemma: leastDivisorDivides              Q.E.D.
Lemma: factAtLeast1                     Q.E.D.
Lemma: greaterPrimeDivides
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Result:                               Q.E.D.
[Proven] greaterPrimeDivides :: Ɐn ∷ Integer → Bool

greaterPrimeGreater :: TP (Proof (Forall "n" Integer -> SBool)) Source #

\(\mathit{greaterPrime}\, n > n\)

Proof

Expand
>>> runTP greaterPrimeGreater
Lemma: notDividesFactP1                 Q.E.D.
Lemma: greaterPrimeDivides              Q.E.D.
Lemma: leastDivisorIsPrime              Q.E.D.
Lemma: factAtLeast1                     Q.E.D.
Lemma: primeAtLeast2                    Q.E.D.
Lemma: greaterPrimeGreater
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: 6                               Q.E.D.
  Result:                               Q.E.D.
[Proven] greaterPrimeGreater :: Ɐn ∷ Integer → Bool

Infinitude of primes

infinitudeOfPrimes :: TP (Proof (Forall "n" Integer -> SBool)) Source #

\(\mathit{isPrime}\,(\mathit{greaterPrime}\,n) \land \mathit{greaterPrime}\,n > n\)

We can finally prove our goal: For each given number, there is a larger number that is prime. This establishes that we have an infinite number of primes.

Proof

Expand
>>> runTP infinitudeOfPrimes
Lemma: leastDivisorIsPrime              Q.E.D.
Lemma: factAtLeast1                     Q.E.D.
Lemma: greaterPrimeGreater              Q.E.D.
Lemma: infinitudeOfPrimes
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Result:                               Q.E.D.
[Proven] infinitudeOfPrimes :: Ɐn ∷ Integer → Bool

noLargestPrime :: TP (Proof (Forall "n" Integer -> SBool)) Source #

\(\forall n. \exists p. \mathit{isPrime}\,p \land p > n\)

Another expression of the fact that there are infinitely many primes. One might prefer this version as it only refers to the isPrime predicate only.

Proof

Expand
>>> runTP noLargestPrime
Lemma: infinitudeOfPrimes               Q.E.D.
Lemma: noLargestPrime
  Step: 1                               Q.E.D.
  Result:                               Q.E.D.
[Proven] noLargestPrime :: Ɐn ∷ Integer → Bool