Last element of list with proof

We have last’ defined like:

last' [x] = x
last' (x:xs) = last' xs (*)

Base case: A list of one element is equal to that element itself.

Inductive step: Assume that last’ (x:xs) returns the last element of the list.
Then, if last’ (x:xs) holds, last’ (y:x:xs) must also hold.

We must show that it holds for y:x:xs.

Set zs = x:xs and obtain:
last’ (y:zs) = (*) = last’ zs = last’ (x:xs) = inductive assumption = last element of the list

So the recursion chops elements from beginning until it reaches one element, which will be the last element from our list.


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s