[Haskell-cafe] Stuck in proof of trivial compiler

[Rustom Mody]

Trying to prove a trivial compiler with respect to a corresponding
interpreter
--------------- Code ------------------
+-* Expression tree
data Exp = Lf Int | Add Exp Exp | Mul Exp Exp

eval (Lf x) = x
eval (Add el er) = eval el + eval er
eval (Mul el er) = eval el * eval er


Simple stack machine instructions (LC is load constant)
data Instr = LC Int | AddI | MulI

compile (Lf x) = [LC x]
compile (Add el er) = compile el ++ compile er ++ [AddI]
compile (Mul el er) = compile el ++ compile er ++ [MulI]

mac [] stk = stk
mac (LC x : is) stk = mac is (x:stk)
mac (AddI : is) (r : l : stk) = mac is (l+r : stk)
mac (MulI : is) (r : l : stk) = mac is (l*r : stk)

------------ Proof Attempt -----------------------
Theorem mac(compile e).s = eval.e : s

Base case
mac(compile (Lf x)) s = eval (Lf x) : s

LHS =
mac (compile (Lf x)) s
mac [LC x] s
mac [] (x: s)
x: s

RHS =
eval (Lf x) : s
x: s

Induction Step:
Assumption l: mac (comp el).s = eval el : s
Assumption r: mac (comp er).s = eval er : s

LHS
= mac (Add el er) s
= mac (comp el ++ comp er ++ [AddI])


RHS
= eval (Add el er) : s
= (eval el + eval er) : s

Now What???
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150909/807c29af/attachment.html>