# [Haskell-cafe] Stuck in proof of trivial compiler

Jonas Scholl anselm.scholl at tu-harburg.de
Wed Sep 9 09:54:47 UTC 2015

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 473 bytes
Desc: OpenPGP digital signature