Generalise to variables

1 files changed, 26 insertions, 19 deletions

diff --git a/expr.v b/expr.v
index e81346e..ab088f7 100644
--- a/expr.v
+++ b/expr.v
@@ -3,23 +3,27 @@ Require Import Wellfounded.
 
 Inductive Exp : Set :=
   | elit : nat -> Exp
-  | eadd : Exp -> Exp -> Exp.
+  | eadd : Exp -> Exp -> Exp
+  | evar : nat -> Exp.
 
-Fixpoint eval (e : Exp) :=
+Fixpoint eval (env : nat -> nat) (e : Exp) :=
   match e with
   | elit n => n
-  | eadd a b => eval a + eval b
+  | eadd a b => eval env a + eval env b
+  | evar n => env n
   end.
 
 Inductive RPN :=
   | rpnnil : RPN
   | rpnlit : nat -> RPN -> RPN
+  | rpnvar : nat -> RPN -> RPN
   | rpnadd : RPN -> RPN.
 
 Fixpoint append_rpn (a : RPN) (b : RPN) :=
   match a with
   | rpnnil     => b
   | rpnlit n a => rpnlit n (append_rpn a b)
+  | rpnvar n a => rpnvar n (append_rpn a b)
   | rpnadd a   => rpnadd (append_rpn a b)
   end.
 
@@ -27,23 +31,28 @@ Fixpoint rpn (e : Exp) :=
   match e with
   | elit n => rpnlit n rpnnil
   | eadd a b => rpnadd (append_rpn (rpn a) (rpn b))
+  | evar n => rpnvar n rpnnil
   end.
 
-Fixpoint rpn_eval' (rpn : RPN) :=
+Fixpoint rpn_eval' (env : nat -> nat) (rpn : RPN) :=
   match rpn with
   | rpnnil => Some nil
-  | rpnlit n a => match rpn_eval' a with
+  | rpnlit n a => match rpn_eval' env a with
     | Some stack => Some (cons n stack) (* TODO: use functor *)
     | None       => None
     end
-  | rpnadd a => match rpn_eval' a with
+  | rpnvar n a => match rpn_eval' env a with
+    | Some stack => Some (cons (env n) stack)
+    | None       => None
+    end
+  | rpnadd a => match rpn_eval' env a with
     | Some (cons x (cons y stack)) => Some (cons (x+y) stack)
     | _                            => None
     end
   end.
 
-Function rpn_eval (rpn : RPN) :=
-  match rpn_eval' rpn with
+Function rpn_eval (env : nat -> nat) (rpn : RPN) :=
+  match rpn_eval' env rpn with
   | Some (cons x nil) => Some x
   | _                 => None
   end.
@@ -51,6 +60,7 @@ Function rpn_eval (rpn : RPN) :=
 Fixpoint exprsize e :=
   match e with
   | elit _ => 1
+  | evar _ => 1
   | eadd a b => 1 + exprsize a + exprsize b
   end.
 
@@ -65,19 +75,16 @@ induction a; simpl; try rewrite IHa; reflexivity.
 Qed.
 
 Lemma free_append' e1 :
-  forall rest rest_results,
-  Some rest_results = rpn_eval' rest ->
-  Some (eval e1 :: rest_results)%list = rpn_eval' (append_rpn (rpn e1) rest).
+  forall env rest rest_results,
+  Some rest_results = rpn_eval' env rest ->
+  Some (eval env e1 :: rest_results)%list = rpn_eval' env (append_rpn (rpn e1) rest).
 Proof.
 induction e1 using (well_founded_induction (wf_inverse_image _ nat _ exprsize PeanoNat.Nat.lt_wf_0)).
 intros.
-destruct e1.
-simpl.
-rewrite <- H0.
-reflexivity.
-simpl.
+destruct e1; simpl; try rewrite <- H0; try reflexivity.
+(* Only eadd is left now *)
 rewrite append_assoc.
-assert (Some (eval e1_1 :: eval e1_2 :: rest_results)%list = rpn_eval' (append_rpn (rpn e1_1) (append_rpn (rpn e1_2) rest))).
+assert (Some (eval env e1_1 :: eval env e1_2 :: rest_results)%list = rpn_eval' env (append_rpn (rpn e1_1) (append_rpn (rpn e1_2) rest))).
   apply H. apply exprsize_left.
   apply H.
   apply exprsize_right.
@@ -91,9 +98,9 @@ Proof.
 induction r; simpl; try rewrite IHr; reflexivity.
 Qed.
 
-Lemma correctness e : Some (eval e) = rpn_eval (rpn e).
+Lemma correctness e env : Some (eval env e) = rpn_eval env (rpn e).
 Proof.
-assert (Some (eval e :: nil)%list = rpn_eval' (rpn e)).
+assert (Some (eval env e :: nil)%list = rpn_eval' env (rpn e)).
 assert (append_rpn (rpn e) rpnnil = rpn e).
 apply append_nil_at_end.
 rewrite <- H.