How about trying to prove the following: mac (compile e ++ x) s = mac x (eval e : s) You can then just break down your term into pieces, build up the stack and evaluate it in your prove. On 09/09/2015 06:13 AM, Rustom Mody wrote:

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???

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe