1 files changed, 11 insertions, 8 deletions
diff --git a/expr.v b/expr.v
index 6e1802d..8530764 100644
--- a/expr.v
+++ b/expr.v
@@ -22,7 +22,7 @@ Fixpoint rpn (e : Exp) :=
   match e with
   | elit n => cons (rpnlit n) nil
   | evar n => cons (rpnvar n) nil
-  | eadd a b => cons rpnadd (app (rpn a) (rpn b))
+  | eadd a b => app (rpn b) (app (rpn a) (cons rpnadd nil))
   end.
 
 Definition _fmap A B (f : A -> B) (o : option A) :=
@@ -44,7 +44,7 @@ Fixpoint rpn_eval' (env : nat -> nat) (rpn : list RPNOp) :=
   end.
 
 Function rpn_eval (env : nat -> nat) (rpn : list RPNOp) :=
-  match rpn_eval' env rpn with
+  match rpn_eval' env (List.rev rpn) with
   | Some (cons x nil) => Some x
   | _                 => None
   end.
@@ -59,25 +59,28 @@ Fixpoint exprsize e :=
 Lemma correctness_partial_compilation e :
   forall env rest results,
   Some results = rpn_eval' env rest ->
-  Some (eval env e :: results)%list = rpn_eval' env (app (rpn e) rest).
+  Some (eval env e :: results)%list = rpn_eval' env (app (List.rev (rpn e)) rest).
 Proof.
 induction e using (well_founded_induction
   (wf_inverse_image _ nat _ exprsize PeanoNat.Nat.lt_wf_0)).
 intros.
 destruct e; simpl; try rewrite <- H0; try reflexivity.
+rewrite (List.rev_app_distr (rpn e2)).
+rewrite (List.rev_app_distr (rpn e1)).
+simpl.
 (* Only eadd is left now *)
-rewrite (List.app_assoc_reverse (rpn e1) (rpn e2) rest).
+rewrite (List.app_assoc_reverse (List.rev (rpn e1)) (List.rev (rpn e2)) rest).
 assert (Some (eval env e1 :: eval env e2 :: results)%list
-    = rpn_eval' env (app (rpn e1) (app (rpn e2) rest))) as recstep.
+    = rpn_eval' env (app (List.rev (rpn e1)) (app (List.rev (rpn e2)) rest))) as recstep.
   apply H; try apply H; simpl; try assumption; omega.
 rewrite <- recstep.
 reflexivity.
 Qed.
 
-Lemma correctness e env : Some (eval env e) = rpn_eval env (rpn e).
+Theorem correctness e env : Some (eval env e) = rpn_eval env (rpn e).
 Proof.
-assert (Some (eval env e :: nil)%list = rpn_eval' env (rpn e)) as outsourcing.
-rewrite <- (List.app_nil_r (rpn e)).
+assert (Some (eval env e :: nil)%list = rpn_eval' env (List.rev (rpn e))) as outsourcing.
+rewrite <- (List.app_nil_r (List.rev (rpn e))).
 apply correctness_partial_compilation.
 simpl. reflexivity.
 unfold rpn_eval.