WIPdependent-rpn

1 files changed, 19 insertions, 4 deletions

diff --git a/expr.v b/expr.v
index 5c8794c..541b910 100644
--- a/expr.v
+++ b/expr.v
@@ -24,10 +24,25 @@ Fixpoint rpn_app {v} {n} {m} (a : RPN v n) (b : RPN v m) : RPN v (n+m) :=
   | rpnadd _ rest   => rpnadd _ (rpn_app rest b)
   end.
 
-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 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