Use a dependently typed RPN definition

1 files changed, 59 insertions, 70 deletions

diff --git a/expr.v b/expr.v
index 2288b3a..5c8794c 100644
--- a/expr.v
+++ b/expr.v
@@ -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