Equational Reasoning

Consider these functions:

let twice f x = f (f x)
let compose f g x = f (g x)

We have that twice h x = h (h x), because both sides would evaluate to the same value. Indeed, twice h x -->* h (h x) in the substitution model, and from there some value would be produced (given definitions for h and x). Likewise, compose h h x = h (h x). Thus we have:

twice h x = h (h x) = compose h h x

Therefore can conclude that twice h x = compose h h x. And by extensionality we can simplify that equality: Since twice h x = compose h h x holds for all x, we can conclude twice h = compose h h.

As another example, suppose we define an infix operator for function composition:

let (<<) = compose

Then we can prove that composition is associative, using equational reasoning:

Theorem: (f << g) << h  =  f << (g << h)

Proof: By extensionality, we need to show 
  ((f << g) << h) x  =  (f << (g << h)) x
for an arbitrary x.

  ((f << g) << h) x 
= (f << g) (h x)
= f (g (h x))

and 

  (f << (g << h)) x
= f ((g << h) x)
= f (g (h x))

So ((f << g) << h) x = f (g (h x)) = (f << (g << h)) x.

QED

All of the steps in the equational proof above follow from evaluation. Another format for writing the proof would provide hints as to why each step is valid:

  ((f << g) << h) x 
=   { evaluation of << }
  (f << g) (h x)
=   { evaluation of << }
  f (g (h x))

and

  (f << (g << h)) x
=   { evaluation of << }
  f ((g << h) x)
=   { evaluation of << }
  f (g (h x))