Use fmap; cleanup

1 files changed, 29 insertions, 29 deletions

diff --git a/expr.v b/expr.v
index ab088f7..089ac03 100644
--- a/expr.v
+++ b/expr.v
@@ -3,14 +3,14 @@ Require Import Wellfounded.
 
 Inductive Exp : Set :=
   | elit : nat -> Exp
-  | eadd : Exp -> Exp -> Exp
-  | evar : nat -> Exp.
+  | evar : nat -> Exp
+  | eadd : Exp -> Exp -> Exp.
 
 Fixpoint eval (env : nat -> nat) (e : Exp) :=
   match e with
   | elit n => n
-  | eadd a b => eval env a + eval env b
   | evar n => env n
+  | eadd a b => eval env a + eval env b
   end.
 
 Inductive RPN :=
@@ -19,32 +19,33 @@ Inductive RPN :=
   | rpnvar : nat -> RPN -> RPN
   | rpnadd : RPN -> RPN.
 
-Fixpoint append_rpn (a : RPN) (b : RPN) :=
+Fixpoint rpn_app (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)
+  | rpnlit n a => rpnlit n (rpn_app a b)
+  | rpnvar n a => rpnvar n (rpn_app a b)
+  | rpnadd a   => rpnadd (rpn_app a b)
   end.
 
 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
+  | eadd a b => rpnadd (rpn_app (rpn a) (rpn b))
+  end.
+
+Definition _fmap A B (f : A -> B) (o : option A) :=
+  match o with
+  | Some x => Some (f x)
+  | None   => None
   end.
+Notation fmap := (_fmap _ _).
 
 Fixpoint rpn_eval' (env : nat -> nat) (rpn : RPN) :=
   match rpn with
   | rpnnil => Some nil
-  | rpnlit n a => match rpn_eval' env a with
-    | Some stack => Some (cons n stack) (* TODO: use functor *)
-    | None       => None
-    end
-  | rpnvar n a => match rpn_eval' env a with
-    | Some stack => Some (cons (env n) stack)
-    | None       => None
-    end
+  | rpnlit n a => fmap (cons n) (rpn_eval' env a)
+  | rpnvar n a => fmap (cons (env n)) (rpn_eval' env a)
   | rpnadd a => match rpn_eval' env a with
     | Some (cons x (cons y stack)) => Some (cons (x+y) stack)
     | _                            => None
@@ -69,31 +70,30 @@ Proof. simpl. omega. Qed.
 Lemma exprsize_right e1 e2 : exprsize e1 < exprsize (eadd e2 e1).
 Proof. simpl. omega. Qed.
 
-Lemma append_assoc a b c : append_rpn (append_rpn a b) c = append_rpn a (append_rpn b c).
-Proof.
-induction a; simpl; try rewrite IHa; reflexivity.
-Qed.
+Lemma append_assoc a b c : rpn_app (rpn_app a b) c = rpn_app a (rpn_app b c).
+Proof. induction a; simpl; try rewrite IHa; reflexivity. Qed.
 
 Lemma free_append' e1 :
-  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).
+  forall env rest results,
+  Some results = rpn_eval' env rest ->
+  Some (eval env e1 :: results)%list = rpn_eval' env (rpn_app (rpn e1) rest).
 Proof.
-induction e1 using (well_founded_induction (wf_inverse_image _ nat _ exprsize PeanoNat.Nat.lt_wf_0)).
+induction e1 using (well_founded_induction
+  (wf_inverse_image _ nat _ exprsize PeanoNat.Nat.lt_wf_0)).
 intros.
 destruct e1; simpl; try rewrite <- H0; try reflexivity.
 (* Only eadd is left now *)
 rewrite append_assoc.
-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))).
+assert (Some (eval env e1_1 :: eval env e1_2 :: results)%list
+    = rpn_eval' env (rpn_app (rpn e1_1) (rpn_app (rpn e1_2) rest))).
   apply H. apply exprsize_left.
-  apply H.
-  apply exprsize_right.
+  apply H. apply exprsize_right.
   assumption.
 rewrite <- H1.
 reflexivity.
 Qed.
 
-Lemma append_nil_at_end r : append_rpn r rpnnil = r.
+Lemma append_nil_at_end r : rpn_app r rpnnil = r.
 Proof.
 induction r; simpl; try rewrite IHr; reflexivity.
 Qed.
@@ -101,7 +101,7 @@ Qed.
 Lemma 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)).
-assert (append_rpn (rpn e) rpnnil = rpn e).
+assert (rpn_app (rpn e) rpnnil = rpn e).
 apply append_nil_at_end.
 rewrite <- H.
 apply free_append'.