CODEWITHSUNDEEP
haskellequalityinduction
SOAP
SOAP

Reputation: 179

To prove equality of functions

Given the two functions:

sumOne 0 = 0                                     --   I.a
sumOne m | m > 0 = sumOne (m-1) + m              --  II.a

endSum m = helpSum 0 m                           --   I.b
 where helpSum x 0 = x                           --  II.b
       helpSum x m | m > 0 = helpSum (x+m) (m-1) -- III.b

We have to prove sumOne = endSum by using induction.

So I tried:

For n=0

sumOne 0=0 == endSum 0 = helpSum 0 0 = 0   True

Assumption:

sumOne m + k = helpSumm k m

Induction step:

-> m=m+1
helpSum k (m+1)
III.b = helpSum (k+m+1) m

and by using the assumption

= sumOne m + (m+k+1)
II.a = sumOne (m+1) + k  -> True

Is that okay? Or completely wrong?

Upvotes: 1

Views: 212

Answers (1)

chi
chi

Reputation: 116139

I think it's morally OK, but you should be more precise. As it is it's hard to follow -- e.g. where did you use the induction hypothesis?

You should start by clearly stating the property you want to prove by induction, and be explicit on what you are inducing.

In your case, I'd suggest to prove

p(m): forall k. sumOne m + k = helpSum k m

by induction on the natural m. Note the difference between k (universally quantified), and m (parameter of p). This step is very important.

Then, by induction on m, we are left to prove p(0) and p(m)=>p(m+1), as usual.

After proving p(m) for all m, one gets for free

sumOne m = helpSum 0 m = endSum m

Upvotes: 7

Related Questions