diff options
Diffstat (limited to 'expr.v')
| -rw-r--r-- | expr.v | 53 |
1 files changed, 18 insertions, 35 deletions
@@ -13,25 +13,16 @@ Fixpoint eval (env : nat -> nat) (e : Exp) := | eadd a b => eval env a + eval env b end. -Inductive RPN := - | rpnnil : RPN - | rpnlit : nat -> RPN -> RPN - | rpnvar : nat -> RPN -> RPN - | rpnadd : RPN -> RPN. - -Fixpoint rpn_app (a : RPN) (b : RPN) := - match a with - | rpnnil => 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. +Inductive RPNOp := + | rpnlit : nat -> RPNOp + | rpnvar : nat -> RPNOp + | rpnadd : RPNOp. Fixpoint rpn (e : Exp) := match e with - | elit n => rpnlit n rpnnil - | evar n => rpnvar n rpnnil - | eadd a b => rpnadd (rpn_app (rpn a) (rpn b)) + | elit n => cons (rpnlit n) nil + | evar n => cons (rpnvar n) nil + | eadd a b => cons rpnadd (app (rpn a) (rpn b)) end. Definition _fmap A B (f : A -> B) (o : option A) := @@ -41,18 +32,18 @@ Definition _fmap A B (f : A -> B) (o : option A) := end. Notation fmap := (_fmap _ _). -Fixpoint rpn_eval' (env : nat -> nat) (rpn : RPN) := +Fixpoint rpn_eval' (env : nat -> nat) (rpn : list RPNOp) := match rpn with - | rpnnil => Some nil - | 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 + | nil => Some nil + | cons (rpnlit n) a => fmap (cons n) (rpn_eval' env a) + | cons (rpnvar n) a => fmap (cons (env n)) (rpn_eval' env a) + | cons (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 (env : nat -> nat) (rpn : RPN) := +Function rpn_eval (env : nat -> nat) (rpn : list RPNOp) := match rpn_eval' env rpn with | Some (cons x nil) => Some x | _ => None @@ -70,22 +61,19 @@ 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 : 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 results, Some results = rpn_eval' env rest -> - Some (eval env e1 :: results)%list = rpn_eval' env (rpn_app (rpn e1) rest). + Some (eval env e1 :: results)%list = rpn_eval' env (app (rpn e1) rest). Proof. 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. +rewrite (List.app_assoc_reverse (rpn e1_1) (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))). + = rpn_eval' env (app (rpn e1_1) (app (rpn e1_2) rest))). apply H. apply exprsize_left. apply H. apply exprsize_right. assumption. @@ -93,16 +81,11 @@ rewrite <- H1. reflexivity. Qed. -Lemma append_nil_at_end r : rpn_app r rpnnil = r. -Proof. -induction r; simpl; try rewrite IHr; reflexivity. -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 (rpn_app (rpn e) rpnnil = rpn e). -apply append_nil_at_end. +assert (app (rpn e) nil = rpn e). +apply List.app_nil_r. rewrite <- H. apply free_append'. simpl. reflexivity. |