==========================================================
(1) Code Definitions:

let rec rev_aux l r =
  match l with
      [] -> r
    | hd::tl -> rev_aux tl (hd::r)

let rev l = rev_aux l [ ]


let rec rev2 l =
  match l with
      [] -> []
    | hd::tl -> (rev2 tl)@[hd]


==========================================================
(2) Some useful properties of @:

l1 @ (l2 @ l3) == (l1 @ l2) @ l3   (@ associativity)

[x] @ l == x::l                    (@ singleton property)

[] @ l == l                        (@ left identity property)



==========================================================
(3) First attempted theorem (what we really want to show):

for all l:int list, rev l == rev2 l

Claim:  By evaluating rev l 1 step, we can see that
what we really need to prove is Lemma.

Lemma: for all l:int list, rev_aux l [ ] == rev2 l

Proof:  By induction on the structure of the list l.

This proof has two cases:
l = [] 
l = hd::tl

case []:
IMS: rev_aux [] [] = rev2 []
(1)     rev_aux [] []         LHS
(2) ==  match [] with ...     eval rev_aux
(3) ==  []                    eval match
(4) ==  match [] with ...     inv eval match
(5) ==  rev2 []               inv eval rev2

case l=hd::tl:
IMS: rev_aux (hd::tl) [] = rev2 (hd::tl)
IH:  rev_aux tl [ ] == rev2 tl

(1)     rev_aux (hd::tl) []   LHS
(2) ==  match hd::tl with ... eval rev_aux
(3) ==  rev_aux tl ([hd])     eval match hd::tl case
????
(k) ==  (rev_aux tl [])@[hd]  IH
(l) ==  (rev2 tl)@[hd]        eval match
(m) ==  match hd::tl with...  eval rev2
(n)     rev2 (hd::tl)         RHS

This proof doesn't work! We can't get the LHS and RHS to meet
using our equational reasoning rules and our IH.


==========================================================
(4) Introspection: 
Let's take a step back and see if there's a more general
version that we can attack. What is the general invariant
when you are in the middle of this computation?

rev_aux l' r : l' is in order and r is in reverse order,
              having been previously pulled off l

this should be equal to:

(rev2 l') @ r

So let's try to prove a revised, more general theorem.
Instead of just considering what happens when the second parameter
is [], try a more general situation in which the parameter is any
list r.


==========================================================
(5) Second attempted theorem (more general version):

for all l:int list,
for all r:int list,
rev_aux l r = (rev2 l) @ r

Proof: By induction over the structure of l.
There are two cases:
l = [] 
l = hd::tl 

case l=[]:
IMS: for all r. rev_aux [] r = (rev2 []) @ r

First, pick an arbitrary list r.  For that r, I must show:

rev_aux [] r = (rev2 []) @ r

Proof:

(1)     rev_aux [] r           LHS
(2) ==  match [] with ...      eval rev_aux
(3) ==  r                      eval match
(4) ==  [] @ r                 @ left identity
(5) ==  (match [] with ...)@r  inv eval match
(6) ==  (rev2 []) @ r          inv eval rev2

case l=hd::tl:
IMS: for all r. rev_aux (hd::tl) r = rev2 (hd::tl) @ r
IH:  for all r': int list, rev_aux tl r' == (rev2 tl) @ r' 

First, pick an arbitrary list r.  For that r, I must show:
rev_aux (hd::tl) r = rev2 (hd::tl) @ r

Proof:

(1)     rev_aux (hd::tl) r     LHS
(2) ==  rev_aux tl (hd::r)     eval rev_aux)
(3) ==  (rev2 tl) @ (hd::r)    (IH with (hd::tl) for r')
(4) ==  (rev2 tl) @ ([hd]@r)   (singleton property)
(5) ==  (rev2 tl @ hd) @ r     (associativity property)
(6) ==  rev2 (hd::tl) @ r      inv. eval rev2