From 0d9d2667da6c55065779157125748d05b182eba1 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Tue, 29 May 2018 13:40:46 +0200
Subject: WIP

---
 expr.v | 23 +++++++++++++++++++----
 1 file 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
-- 
cgit v1.2.3