BEGIN 16_12_06_CorrectnessOfGCD.lhs

This script complements several earlier scripts on induction:
   16_12_01_Reasoning_about_Programs.part_1.lhs
   16_12_01_Reasoning_about_Programs.part_2.lhs
   16_12_01_ProofByStrongInduction.lhs

The Greatest Common Divisor (GCD) is already a library function
in Haskell. But we can implement it differently ourselves:

> anotherGCD 0 n = n
> anotherGCD m n = anotherGCD (n `mod` m) m

> euclidGCD m n =
>       if m == n then n else
>       if m > n  then euclidGCD (m-n) n else euclidGCD m (n-m)

EXERCISE 1: 

The types inferred for these two functions, anotherGCD and
euclidGCD, are different. Explain the difference (even though
both functions correctly compute the greatest common divisor
of two integers).

EXERCISE 2:

How do you prove that the function anotherGCD is correct, i.e.,
that it correctly computes the greatest common divisor of m and n?

Hint 1: You will never be wrong in saying "I will prove it by induction".

Hint 2: The real question is, what kind of induction will do? What is
the induction parameter? What is the induction hypothesis (i.e. the
"invariant" of the induction)?

Hint 3: Choose m as the induction parameter and note that (n `mod` m)
is always smaller than n, if n is greater or equal to m.

EXERCISE 3:

How do you prove that the function euclidGCD is correct, i.e.,
that it correctly computes the greatest common divisor of m and n?

Hint 1: This exercise is a little more complicated than EXERCISE 2,
because the function involves two (not only one) recursive calls: In
one of the recursive calls, the first argument becomes smaller, and in
the other call, the second argument gets smaller.

Hint 2: For the induction parameter, choose a pair (a,b) of integers
and defined the ordering:

    (a,b) < (a',b') iff max {a,b} < max {a',b'}

The induction hypothesis (i.e. the "invariant" of the induction) is:

    For any m > 0 and n > 0, (euclidGCD m n) returns the greatest 
    common divisor of m and n, assuming that (euclidGCD m' n') returns
    the g.c.d. for all m' and n' such that max {m',n'} < max {m,n}

Using Hint 1 and Hint 2, complete the details of the induction on pairs (m,n).

Hint 3: The base step of the induction is when m = n. For the induction
step, consider two cases: m > n and m < n.

END 16_12_06_CorrectnessOfGCD.lhs