Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.TP.GCD

Contents

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

nGCD :: SInteger -> SInteger -> SInteger
gcd :: SInteger -> SInteger -> SInteger
gcdNonNegative :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdZero :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
commutative :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
negGCD :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
zeroGCD :: TP (Proof (Forall "a" Integer -> SBool))
isEven :: SInteger -> SBool
isOdd :: SInteger -> SBool
dvd :: SInteger -> SInteger -> SBool
dvdAbs :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
dvdMul :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> Forall "k" Integer -> SBool))
dvdOddThenOdd :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
dvdEvenWhenOdd :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool))
dvdSum1 :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> Forall "b" Integer -> SBool))
dvdSum2 :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdDivides :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdMaximal :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "x" Integer -> SBool))
gcdCorrect :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdLargest :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "x" Integer -> SBool))
gcdAdd :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdEvenEven :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
gcdOddEven :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
nGCDSub :: SInteger -> SInteger -> SInteger
gcdSub :: SInteger -> SInteger -> SInteger
gcdSubEquiv :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))
nGCDBin :: SInteger -> SInteger -> SInteger
gcdBin :: SInteger -> SInteger -> SInteger
gcdBinEquiv :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool))

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