Proof by induction example

I just want to write down the proof that we did as an example in the last exercise session as you might want to use it as a reference for the current exercise sheet.

If we have the following haskell programm:

sum 0 = 0              --sum.1

sum n = n+sum (n-1)  --sum.2

And you want to prove forall n element of Nat. sum n = n*(n+1)/2 then we write the following proof:

Lemma: forall n element of Nat. sum n = n*(n+1)/2
Proof: We show forall n element of Nat. sum n = n*(n+1)/2 by induction. Let P(n) = sum n = n*(n+1)/2.

Base Case: Show P(0).

sum 0
= 0 -- sum.1
= 0*(0+1)/2 –- arith

Step Case: Let n element of Nat be arbitrary and assume that P(n) holds. Show P(n+1).

sum (n+1)
= (n+1) + sum ((n+1)-1) -- sum.2
= (n+1) + sum (n) -- arith
= (n+1) + n*(n+1)/2 -- P(n)
= 2*(n+1)/2 + n*(n+1)/2 --arith
= (n+2)*(n+1)/2 --arith
= (n+1)*((n+1)+1)/2 --arith


(The italic text of the proof might be used as a template for all recursiv proofs.)

Ähnliche Beiträge:
Third Week FMFP
Third Week FMFP
Types inference FMFP
Solution Second Week FMFP
Solution First Week FMFP
Comments (0)  Permalink


add a comment

The Trackback URL to this comment is:

Keine (weiteren) neuen Kommentare erlaubt.