[Haskell-cafe] Stuck in proof of trivial compiler

[Jonas Scholl]

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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> 


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 473 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150909/783f17d9/attachment.sig>