sbv-13.1: 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.GCD

Description

We define three different versions of the GCD algorithm: (1) Regular version using the modulus operator, (2) the more basic version using subtraction, and (3) the so called binary GCD. We prove that the modulus based algorithm correct, i.e., that it calculates the greatest-common-divisor of its arguments. We then prove that the other two variants are equivalent to this version, thus establishing their correctness as well.

Synopsis

Calculating GCD

nGCD :: SInteger -> SInteger -> SInteger Source #

nGCD is the version of GCD that works on non-negative integers.

Ideally, we should make this function local to gcd, but then we can't refer to it explicitly in our proofs.

Note on maximality: Note that, by definition gcd 0 0 = 0. Since any number divides 0, there is no greatest common divisor for the pair (0, 0). So, maximality here is meant to be in terms of divisibility. That is, any divisor of a and b will also divide their gcd.

gcd :: SInteger -> SInteger -> SInteger Source #

Generalized GCD, working for all integers. We simply call nGCD with the absolute value of the arguments.

Basic properties

gcdNonNegative :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)) Source #

\(\gcd\, a\ b \geq 0\)

Proof

Expand
>>> runTP gcdNonNegative
Inductive lemma (strong): nonNegativeNGCD
  Step: Measure is non-negative         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.
Lemma: nonNegative                      Q.E.D.
[Proven] nonNegative :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool

gcdZero :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)) Source #

\(\gcd\, a\ b=0\implies a=0\land b=0\)

Proof

Expand
>>> runTP gcdZero
Inductive lemma (strong): nGCDZero
  Step: Measure is non-negative         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.
Lemma: gcdZero                          Q.E.D.
[Proven] gcdZero :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool

commutative :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)) Source #

\(\gcd\, a\ b=\gcd\, b\ a\)

Proof

Expand
>>> runTP commutative
Lemma: nGCDCommutative
  Step: 1                               Q.E.D.
  Result:                               Q.E.D.
Lemma: commutative
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Result:                               Q.E.D.
[Proven] commutative :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool

negGCD :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)) Source #

\(\gcd\,(-a)\,b = \gcd\,a\,b = \gcd\,a\,(-b)\)

Proof

Expand
>>> runTP negGCD
Lemma: negGCD                           Q.E.D.
[Proven] negGCD :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool

zeroGCD :: TP (Proof (Forall "a" Integer -> SBool)) Source #

\( \gcd\,a\,0 = \gcd\,0\,a = |a| \land \gcd\,0\,0 = 0\)

Proof

Expand
>>> runTP zeroGCD
Lemma: negGCD                           Q.E.D.
[Proven] negGCD :: Ɐa ∷ Integer → Bool

Even and odd

isEven :: SInteger -> SBool Source #

Is the given integer even?

isOdd :: SInteger -> SBool Source #

Is the given integer odd?

Divisibility

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

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

dvdAbs :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)) Source #

\(a \mid |b| \iff a \mid b\)

A number divides another exactly when it also divides its absolute value. While this property seems obvious, I was unable to get z3 to prove it. Even CVC5 needs a bit of help to guide it through the case split on b.

Proof

Expand
>>> runTP dvdAbs
Lemma: dvdAbs_l2r
  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.
Lemma: dvdAbs_r2l
  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.
Lemma: dvdAbs                           Q.E.D.
[Proven] dvdAbs :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool

dvdMul :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> Forall "k" Integer -> SBool)) Source #

\(d \mid a \implies d \mid ka\)

Proof

Expand
>>> runTP dvdMul
Lemma: dvdMul
  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] dvdMul :: Ɐd ∷ Integer → Ɐa ∷ Integer → Ɐk ∷ Integer → Bool

dvdOddThenOdd :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool)) Source #

\(d \mid (2a + 1) \implies \mathrm{isOdd}(d)\)

Proof

Expand
>>> runTP dvdOddThenOdd
Lemma: dvdOddThenOdd
  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] dvdOddThenOdd :: Ɐd ∷ Integer → Ɐa ∷ Integer → Bool

dvdEvenWhenOdd :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool)) Source #

\(\mathrm{isOdd}(d) \land d \mid 2a \implies d \mid a\)

Proof

Expand
>>> runTP dvdEvenWhenOdd
Lemma: dvdEvenWhenOdd
  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.
  Step: 7                               Q.E.D.
  Result:                               Q.E.D.
[Proven] dvdEvenWhenOdd :: Ɐd ∷ Integer → Ɐa ∷ Integer → Bool

dvdSum1 :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> Forall "b" Integer -> SBool)) Source #

\(d \mid a \land d \mid b \implies d \mid (a + b)\)

Proof

Expand
>>> runTP dvdSum1
Lemma: dvdSum1
  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] dvdSum1 :: Ɐd ∷ Integer → Ɐa ∷ Integer → Ɐb ∷ Integer → Bool

dvdSum2 :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> Forall "b" Integer -> SBool)) Source #

\(d \mid (a + b) \land d \mid b \implies d \mid a \)

Proof

Expand
>>> runTP dvdSum2
Lemma: dvdSum2
  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] dvdSum2 :: Ɐd ∷ Integer → Ɐa ∷ Integer → Ɐb ∷ Integer → Bool

Correctness of GCD

gcdDivides :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)) Source #

\(\gcd\,a\,b \mid a \land \gcd\,a\,b \mid b\)

GCD of two numbers divide these numbers. This is part one of the proof, where we are not concerned with maximality. Our goal is to show that the calculated gcd divides both inputs.

Proof

Expand
>>> runTP gcdDivides
Lemma: dvdAbs                           Q.E.D.
Lemma: helper
  Step: 1                               Q.E.D.
  Result:                               Q.E.D.
Inductive lemma (strong): dvdNGCD
  Step: Measure is non-negative         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.
Lemma: gcdDivides                       Q.E.D.
[Proven] gcdDivides :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool

gcdMaximal :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "x" Integer -> SBool)) Source #

\(x \mid a \land x \mid b \implies x \mid \gcd\,a\,b\)

Maximality. Any divisor of the inputs divides the GCD.

Proof

Expand
>>> runTP gcdMaximal
Lemma: dvdAbs                           Q.E.D.
Lemma: gcdComm                          Q.E.D.
Lemma: eDiv                             Q.E.D.
Lemma: helper
  Step: 1 (x `dvd` a && x `dvd` b)      Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Result:                               Q.E.D.
Inductive lemma (strong): mNGCD
  Step: Measure is non-negative         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.
Lemma: gcdMaximal
  Step: 1 (2 way case split)
    Step: 1.1.1                         Q.E.D.
    Step: 1.1.2                         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.2.4                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] gcdMaximal :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐx ∷ Integer → Bool

gcdCorrect :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)) Source #

\(\gcd\,a\,b \mid a \land \gcd\,a\,b \mid b \land (x \mid a \land x \mid b \implies x \mid \gcd\,a\,b)\)

Putting it all together: GCD divides both arguments, and its maximal.

Proof

Expand
>>> runTP gcdCorrect
Lemma: gcdDivides                       Q.E.D.
Lemma: gcdMaximal                       Q.E.D.
Lemma: gcdCorrect
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Result:                               Q.E.D.
[Proven] gcdCorrect :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool

gcdLargest :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "x" Integer -> SBool)) Source #

\(\bigl((a \neq 0 \lor b \neq 0) \land x \mid a \land x \mid b \bigr) \implies x \leq \gcd\,a\,b\)

Additionally prove that GCD is really maximum, i.e., it is the largest in the regular sense. Note that we have to make an exception for gcd 0 0 since by definition the GCD is 0, which is clearly not the largest divisor of 0 and 0. (Since any number is a GCD for the pair (0, 0), there is no maximum.)

Proof

Expand
>>> runTP gcdLargest
Lemma: gcdMaximal                       Q.E.D.
Lemma: gcdZero                          Q.E.D.
Lemma: gcdNonNegative                   Q.E.D.
Lemma: gcdLargest
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Result:                               Q.E.D.
[Proven] gcdLargest :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐx ∷ Integer → Bool

Other GCD Facts

gcdAdd :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)) Source #

\(\gcd\, a\, b = \gcd\, (a + b)\, b\)

Proof

Expand
>>> runTP gcdAdd
Lemma: dvdSum1                          Q.E.D.
Lemma: dvdSum2                          Q.E.D.
Lemma: gcdDivides                       Q.E.D.
Lemma: gcdLargest                       Q.E.D.
Lemma: gcdAdd
  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.
  Step: 7                               Q.E.D.
  Result:                               Q.E.D.
[Proven] gcdAdd :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool

gcdEvenEven :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)) Source #

\(\gcd\, (2a)\, (2b) = 2 (\gcd\,a\, b)\)

Proof

Expand
>>> runTP gcdEvenEven
Lemma: modEE                            Q.E.D.
Inductive lemma (strong): nGCDEvenEven
  Step: Measure is non-negative         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.2.3                         Q.E.D.
    Step: 1.2.4                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
Lemma: gcdEvenEven
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Result:                               Q.E.D.
[Proven] gcdEvenEven :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool

gcdOddEven :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)) Source #

\(\gcd\, (2a+1)\, (2b) = \gcd\,(2a+1)\, b\)

Proof

Expand
>>> runTP gcdOddEven
Lemma: gcdDivides                       Q.E.D.
Lemma: gcdLargest                       Q.E.D.
Lemma: dvdMul                           Q.E.D.
Lemma: dvdOddThenOdd                    Q.E.D.
Lemma: dvdEvenWhenOdd                   Q.E.D.
Lemma: gcdOddEven
  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.
  Step: 7                               Q.E.D.
  Step: 8                               Q.E.D.
  Result:                               Q.E.D.
[Proven] gcdOddEven :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool

GCD via subtraction

nGCDSub :: SInteger -> SInteger -> SInteger Source #

nGCDSub is the original verision of Euclid, which uses subtraction instead of modulus. This is the version that works on non-negative numbers. It has the precondition that a >= b >= 0, and maintains this invariant in each recursive call.

gcdSub :: SInteger -> SInteger -> SInteger Source #

Generalized version of subtraction based GCD, working over all integers.

gcdSubEquiv :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)) Source #

\(\mathrm{gcdSub}\, a\, b = \gcd\, a\, b\)

Instead of proving gcdSub correct, we'll simply show that it is equivalent to gcd, hence it has all the properties we already established.

Proof

Expand
>>> runTP gcdSubEquiv
Lemma: commutative                      Q.E.D.
Lemma: gcdAdd                           Q.E.D.
Inductive lemma (strong): nGCDSubEquiv
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (5 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2                           Q.E.D.
    Step: 1.3                           Q.E.D.
    Step: 1.4.1                         Q.E.D.
    Step: 1.4.2                         Q.E.D.
    Step: 1.4.3                         Q.E.D.
    Step: 1.5.1                         Q.E.D.
    Step: 1.5.2                         Q.E.D.
    Step: 1.5.3                         Q.E.D.
    Step: 1.5.4                         Q.E.D.
    Step: 1.5.5                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
Lemma: gcdSubEquiv
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Result:                               Q.E.D.
[Proven] gcdSubEquiv :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool

Binary GCD

nGCDBin :: SInteger -> SInteger -> SInteger Source #

nGCDBin is the binary GCD algorithm that works on non-negative numbers.

gcdBin :: SInteger -> SInteger -> SInteger Source #

Generalized version that works on arbitrary integers.

gcdBinEquiv :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)) Source #

\(\mathrm{gcdBin}\, a\, b = \gcd\, a\, b\)

Instead of proving gcdBin correct, we'll simply show that it is equivalent to gcd, hence it has all the properties we already established.

Proof

Expand
>>> runTP gcdBinEquiv
Lemma: gcdEvenEven                      Q.E.D.
Lemma: gcdOddEven                       Q.E.D.
Lemma: gcdAdd                           Q.E.D.
Lemma: commutative                      Q.E.D.
Inductive lemma (strong): nGCDBinEquiv
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (5 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2                           Q.E.D.
    Step: 1.3.1                         Q.E.D.
    Step: 1.3.2                         Q.E.D.
    Step: 1.3.3                         Q.E.D.
    Step: 1.4.1                         Q.E.D.
    Step: 1.4.2                         Q.E.D.
    Step: 1.4.3                         Q.E.D.
    Step: 1.5 (3 way case split)
      Step: 1.5.1                       Q.E.D.
      Step: 1.5.2.1                     Q.E.D.
      Step: 1.5.2.2                     Q.E.D.
      Step: 1.5.2.3                     Q.E.D.
      Step: 1.5.2.4                     Q.E.D.
      Step: 1.5.2.5                     Q.E.D.
      Step: 1.5.2.6                     Q.E.D.
      Step: 1.5.3.1                     Q.E.D.
      Step: 1.5.3.2                     Q.E.D.
      Step: 1.5.3.3                     Q.E.D.
      Step: 1.5.3.4                     Q.E.D.
      Step: 1.5.Completeness            Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
Lemma: gcdBinEquiv
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Result:                               Q.E.D.
[Proven] gcdBinEquiv :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool