Inductive Exp (v : Type) :=
  | elit : nat -> Exp v
  | evar : v   -> Exp v
  | eadd : Exp v -> Exp v -> Exp v.

Fixpoint eval {v} (env : v -> nat) (e : Exp v) : nat :=
  match e with
  | elit _ n   => n
  | evar _ n   => env n
  | eadd _ a b => eval env a + eval env b
  end.

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_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 cast: forall {A m} (v: RPN A m) {n}, m = n -> RPN A n.
intros.
rewrite <- H.
exact v.
Defined.

Require Import Coq.Arith.Plus.
Require Import Coq.Program.Equality.
Lemma rpn_app_assoc_jmeq {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.
induction a.
simpl.
reflexivity.
simpl.
Admitted.

Lemma rpn_app_assoc {v} {p} {q} {r} (a : RPN v p) (b : RPN v q) (c : RPN v r) :
  rpn_app (rpn_app a b) c = cast (rpn_app a (rpn_app b c)) (plus_assoc _ _ _).


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.

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.

Definition rpn_eval {v} (env : v -> nat) (rpn : RPN v 1) : nat :=
  match rpn_eval' env rpn with
  | cons _ x _ _ => x
  | nil _ => 0
  end.

Fixpoint exprsize {v} (e : Exp v) : nat :=
  match e with
  | elit _ _ => 1
  | evar _ _ => 1
  | eadd _ a b => 1 + exprsize a + exprsize b
  end.

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.
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).
Qed.