Structural induction in haskell

haskell

Structural induction is a proof method to prove the correctness of propositions or theorems in math.
For example, prove that for all positive integers, sum(1+2+..n) = n*(n+1)/2 using mathematical induction.

Base case:
sum(1) = 1 = 1 * (1+1)/2  proved for 1
   
Induction hypothesis:
sum(1+2+..+n) = n*(n+1)/2  assume true for n
    
Induction case(prove for n+1): 
sum(1+2+..+n+1) = sum(1+2+..+n) + n+1  (definition of sum)
                = n*(n+1)/2 + n+1      (IH)
                = n*(n+1)+2(n+1)/2     (math computation)
                = (n+1)*(n+2)/2        (RHS proved)

In principal, the proof procedure has 3 steps:

  1. show or prove base case. This is induction start.
  2. assume true of f(n). This is induction hypothesis(IH).
  3. prove f(n+1). This is induction step.

In haskell, it is used to prove the properties of recursive data structure or type class. Proof involves:

  1. substitution equals for equals. It’s the way reasoning about haskell programs.
  2. unfold definition.
  3. fold back to definition.
  4. use already known facts or lemmas.
  5. use induction hypothesis.

Reference: https://www.cs.princeton.edu/~dpw/cos441-11/notes/slides03B-Haskell-Intro.pdf

Example

Prove that length(l1 ++ l2) = length(l1) + length(l2) for all list l1 and l2.

Induction of l1

case l1 is []:   (base case)
length(l1 ++ l2) = length([] ++l2)           (seqeq)
                 = length(l2)                (unfold ++)
                 = 0 + length(l2)            (math)
                 = length [] + length(l2)    (fold length)
                 = length(l1) + length(l2)   (RHS proved)

case l1 is (x:xs): (induction case)
IH: length(xs + l2)  = length(xs) + length(l2)
length((x:xs) ++ l2) = length(x : (xs ++ l2))       (unfold ++)
                     = 1 + length(xs ++l2)          (unfold length)
                     = 1 + length(xs) + length(I2)  (IH) 
                     = length(x:xs) + length(l2)    (fold length, RHS proved)
Support me