diff options
| -rw-r--r-- | expr.v | 58 |
1 files changed, 29 insertions, 29 deletions
@@ -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'. |