diff options
| -rw-r--r-- | expr.v | 129 |
1 files changed, 59 insertions, 70 deletions
@@ -1,97 +1,86 @@ -Require Import Omega Wellfounded Coq.Lists.List. -Import ListNotations. - Inductive Exp (v : Type) := | elit : nat -> Exp v | evar : v -> Exp v | eadd : Exp v -> Exp v -> Exp v. -Fixpoint eval (v : Type) (env : v -> nat) (e : Exp v) : nat := +Fixpoint eval {v} (env : v -> nat) (e : Exp v) : nat := match e with | elit _ n => n | evar _ n => env n - | eadd _ a b => eval v env a + eval v env b + | eadd _ a b => eval env a + eval env b end. -Inductive RPNOp (v : Type) := - | rpnlit : nat -> RPNOp v - | rpnvar : v -> RPNOp v - | rpnadd : RPNOp v. +Inductive RPN (v : Type) : nat -> Type := + | rpnnil : RPN v 0 + | rpnlit : forall {n}, RPN v n -> nat -> RPN v (S n) + | rpnvar : forall {n}, RPN v n -> v -> RPN v (S n) + | rpnadd : forall {n}, RPN v (S (S n)) -> RPN v (S n). -Fixpoint rpn (v : Type) (e : Exp v) : list (RPNOp v) := - match e with - | elit _ n => [rpnlit v n] - | evar _ n => [rpnvar v n] - | eadd _ a b => rpn v b ++ rpn v a ++ [rpnadd v] +Fixpoint rpn_app {v} {n} {m} (a : RPN v n) (b : RPN v m) : RPN v (n+m) := + match a with + | rpnnil _ => b + | rpnlit _ rest x => rpnlit _ (rpn_app rest b) x + | rpnvar _ rest x => rpnvar _ (rpn_app rest b) x + | rpnadd _ rest => rpnadd _ (rpn_app rest b) end. -Definition fmap (a : Type) (b : Type) (f : a -> b) (o : option a) : option b := - match o with - | Some x => Some (f x) - | None => None - end. -Notation "x <$> y" := (fmap _ _ x y) (at level 65, left associativity). +Require Import Coq.Program.Tactics Omega. +Program Definition rpn_app_assoc {v} {p} {q} {r} (a : RPN v p) (b : RPN v q) (c : RPN v r) := + rpn_app a (rpn_app b c) = rpn_app (rpn_app a b) c. +Next Obligation. omega. Qed. -Definition bind (a : Type) (b : Type) (f : a -> option b) (o : option a) : option b := - match o with - | Some x => f x - | None => None +Fixpoint rpn {v} (e : Exp v) : RPN v 1 := + match e with + | elit _ n => rpnlit _ (rpnnil _) n + | evar _ n => rpnvar _ (rpnnil _) n + | eadd _ a b => rpnadd _ (rpn_app (rpn a) (rpn b)) end. -Notation "x >>= f" := (bind _ _ f x) (at level 55, left associativity). -Fixpoint pn_eval (v : Type) (env : v -> nat) (rpn : list (RPNOp v)) : option (list nat) := - match rpn with - | [] => Some [] - | rpnlit _ n :: a => cons n <$> pn_eval v env a - | rpnvar _ n :: a => cons (env n) <$> pn_eval v env a - | rpnadd _ :: a => pn_eval v env a >>= fun stack => match stack with - | x :: y :: stack => Some (x+y :: stack) - | _ => None - end - end. +Require Import Coq.Vectors.VectorDef. +Fixpoint rpn_eval' {v} {n} (env : v -> nat) (rpn : RPN v n) : t nat n. +refine (match rpn with + | rpnnil _ => nil _ + | rpnlit _ rest x => cons _ x _ (rpn_eval' _ _ env rest) + | rpnvar _ rest x => cons _ (env x) _ (rpn_eval' _ _ env rest) + | rpnadd _ rest => _ + end). +set (recurse := rpn_eval' _ _ env rest). +remember (S (S n0)) as stack_size. +destruct recurse. +discriminate. (* nil case *) +assert (n1 = S n0) by (abstract congruence). +rewrite H in recurse. +exact recurse. +Defined. -Function rpn_eval (v : Type) (env : v -> nat) (rpn : list (RPNOp v)) : option nat := - match pn_eval v env (rev rpn) with - | Some [x] => Some x - | _ => None +Definition rpn_eval {v} (env : v -> nat) (rpn : RPN v 1) : nat := + match rpn_eval' env rpn with + | cons _ x _ _ => x + | nil _ => 0 end. -Lemma correctness_partial_compilation (v : Type) (e : Exp v) : - forall (env : v -> nat) (rest : list (RPNOp v)) (results : list nat), - Some results = pn_eval v env rest -> - Some (eval v env e :: results) = pn_eval v env (rev (rpn v e) ++ rest). -Proof. - -Fixpoint exprsize (v : Type) (e : Exp v) : nat := +Fixpoint exprsize {v} (e : Exp v) : nat := match e with | elit _ _ => 1 | evar _ _ => 1 - | eadd _ a b => 1 + exprsize v a + exprsize v b + | eadd _ a b => 1 + exprsize a + exprsize b end. -induction e using (well_founded_induction - (wf_inverse_image _ nat _ (exprsize v) PeanoNat.Nat.lt_wf_0)). +Require Import Wellfounded. +Theorem correctness (v : Type) (e : Exp v) : forall env : v -> nat, + forall n rest (results : t nat n), + results = rpn_eval' env rest -> + cons _ (eval env e) _ results = rpn_eval' env (rpn_app (rpn e) rest). +Proof. +induction e using (well_founded_induction + (wf_inverse_image _ nat _ exprsize PeanoNat.Nat.lt_wf_0)). intros. -destruct e; simpl; try rewrite <- H0; try reflexivity. -rewrite (rev_app_distr (rpn v e2)). -rewrite (rev_app_distr (rpn v e1)). -simpl. +destruct e. +simpl; try rewrite <- H0; try reflexivity. +simpl; try rewrite <- H0; try reflexivity. +simpl (rpn (eadd v e1 e2)). +simpl rpn_app. +assert (rpn_app (rpn_app (rpn e1) (rpn e2)) rest = rpn_app (rpn e1) (rpn_app (rpn e2) rest)). + apply rpn_app_assoc. rewrite (app_assoc_reverse (rev (rpn v e1)) (rev (rpn v e2)) rest). -assert (Some (eval v env e1 :: eval v env e2 :: results) - = pn_eval v env (rev (rpn v e1) ++ rev (rpn v e2) ++ rest)) as recstep. - apply H; try apply H; simpl; try assumption; omega. -rewrite <- recstep. -reflexivity. -Qed. - -Theorem correctness (v : Type) (e : Exp v) (env : v -> nat) : - Some (eval v env e) = rpn_eval v env (rpn v e). -Proof. -assert (Some [eval v env e] = pn_eval v env (rev (rpn v e))) as outsourcing. -rewrite <- (app_nil_r (rev (rpn v e))). -apply correctness_partial_compilation. -simpl. reflexivity. -unfold rpn_eval. -rewrite <- outsourcing. -reflexivity. Qed.
\ No newline at end of file |