We prove the property P(xs) = (xs /= [] ==> initLast xs = initLast' xs) by induction on xs.

• We start with the base case xs = []: since the premise of P([]) is [] /= [] the claim holds vacuously.

• In the step case xs = y:ys and P(ys) by IH. In principle, we may assume

  y:ys /= []
  

  since the statement we want to show (P(y:ys)) is an implication. However, this assumption trivially reduces to True and hence doesn't help us in our proof.

  We continue by a case analysis on ys, which is either empty or not:

  • If ys = [] then

    initLast [y] = (init [y], last [y]) = ([], y) = initLast' [y]
    

    and we are done.

  • Otherwise, ys /= [] and hence by IH initLast ys = initLast' ys, which implies (init ys, last ys) = initLast'. We conclude by the derivation:

    initLast (y:ys)
    = (init (y:ys), last (y:ys))
    = (y : init ys, last ys)
    = (y : us, u) where (us, u) = initLast' ys -- by IH
    = initLast' (y:ys)
    

We prove the property P(n) = (fac n * k = go k n) for arbitrary k, by induction on n.

• We start with the base case n = 0. Then

  fac 0 * k = k = go k 0
  

• In the step case we try to show P(n+1) under the IH that P(n) holds for arbitrary values of k. We proceed by a case analysis on n:

  • If n = 0 then fac 1 * k = k = go k 1.

  • Otherwise n > 0 and hence:

    fac (n+1) * k
    = (n+1) * fac n * k
    = fac n * ((n + 1) * k)
    = go ((n + 1) * k) n -- by IH
    = go k (n + 1)
    

In the end, from P(n) for all n, we trivially obtain that fac n = fac' n for all n.

A potential sorting function.

The property

prop_sort y xs

does not hold, e.g., for y = 0 and xs = [0,0]. Hence, sort' is not a correct sorting function.

nfold' n f x iteratively for n steps applies the given function f to the argument x

The two implementations of n-fold function application behave the same:

nfold n f x = nfold' n f x