<div dir="ltr"><div><div>Trying to prove a trivial compiler with respect to a corresponding interpreter<br></div>--------------- Code ------------------<br></div><div>+-* Expression tree<br></div><div>data Exp = Lf Int | Add Exp Exp | Mul Exp Exp<br><br>eval (Lf x) = x<br>eval (Add el er) = eval el + eval er<br>eval (Mul el er) = eval el * eval er<br><br><br>Simple stack machine instructions (LC is load constant)<br>data Instr = LC Int | AddI | MulI<br><br>compile (Lf x) = [LC x]     <br>compile (Add el er) = compile el ++ compile er ++ [AddI]<br>compile (Mul el er) = compile el ++ compile er ++ [MulI]<br><br>mac [] stk = stk<br>mac (LC x : is) stk = mac is (x:stk)<br>mac (AddI : is) (r : l : stk) = mac is (l+r : stk)<br>mac (MulI : is) (r : l : stk) = mac is (l*r : stk)<br><br></div>------------ Proof Attempt -----------------------<br><div><div><div><div dir="ltr"><div><div dir="ltr"><div>Theorem mac(compile e).s = eval.e : s<br><br>Base case <br>mac(compile (Lf x)) s = eval (Lf x) : s<br><br>LHS =<br>mac (compile (Lf x)) s<br>mac [LC x] s<br>mac [] (x: s)<br>x: s<br><br>RHS =<br>eval (Lf x) : s<br>x: s<br><br>Induction Step:<br>Assumption l: mac (comp el).s = eval el : s<br>Assumption r: mac (comp er).s = eval er : s<br><br>LHS <br>= mac (Add el er) s<br>= mac (comp el ++ comp er ++ [AddI])<br><br><br>RHS<br>= eval (Add el er) : s<br>= (eval el + eval er) : s<br><br>Now What???<br></div></div></div></div>
</div></div></div></div>