diff options
| -rw-r--r-- | expr.v | 35 |
1 files changed, 13 insertions, 22 deletions
@@ -56,40 +56,31 @@ Fixpoint exprsize e := | eadd a b => 1 + exprsize a + exprsize b end. -Lemma exprsize_left e1 e2 : exprsize e1 < exprsize (eadd e1 e2). -Proof. simpl. omega. Qed. -Lemma exprsize_right e1 e2 : exprsize e1 < exprsize (eadd e2 e1). -Proof. simpl. omega. Qed. - -Lemma free_append' e1 : +Lemma correctness_partial_compilation e : forall env rest results, Some results = rpn_eval' env rest -> - Some (eval env e1 :: results)%list = rpn_eval' env (app (rpn e1) rest). + Some (eval env e :: results)%list = rpn_eval' env (app (rpn e) rest). Proof. -induction e1 using (well_founded_induction +induction e using (well_founded_induction (wf_inverse_image _ nat _ exprsize PeanoNat.Nat.lt_wf_0)). intros. -destruct e1; simpl; try rewrite <- H0; try reflexivity. +destruct e; simpl; try rewrite <- H0; try reflexivity. (* Only eadd is left now *) -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 (app (rpn e1_1) (app (rpn e1_2) rest))). - apply H. apply exprsize_left. - apply H. apply exprsize_right. - assumption. -rewrite <- H1. +rewrite (List.app_assoc_reverse (rpn e1) (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. + 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). Proof. -assert (Some (eval env e :: nil)%list = rpn_eval' env (rpn e)). -assert (app (rpn e) nil = rpn e). -apply List.app_nil_r. -rewrite <- H. -apply free_append'. +assert (Some (eval env e :: nil)%list = rpn_eval' env (rpn e)) as outsourcing. +rewrite <- (List.app_nil_r (rpn e)). +apply correctness_partial_compilation. simpl. reflexivity. unfold rpn_eval. -rewrite <- H. +rewrite <- outsourcing. reflexivity. Qed.
\ No newline at end of file |