## 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

*qed.*

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

### comments

### add a comment

The Trackback URL to this comment is:

http://leo.freeflux.net/blog/plugin=trackback(2814).xml