Require Import List. Import ListNotations. Inductive type := Nat | Bool. Inductive tbinop : type -> type -> type -> Type := | TPlus : tbinop Nat Nat Nat | TTimes : tbinop Nat Nat Nat | TEq : forall (t : type), tbinop t t Bool | TLe : tbinop Nat Nat Bool. Inductive texp : type -> Type := | TNConst : nat -> texp Nat | TBConst : bool -> texp Bool | TBinop : forall {t1 t2 t : type}, tbinop t1 t2 t -> texp t1 -> texp t2 -> texp t. Definition typeDenote (t : type) : Type := match t with | Nat => nat | Bool => bool end. Definition tbinopDenote {arg1 arg2 res : type} (b : tbinop arg1 arg2 res) : typeDenote arg1 -> typeDenote arg2 -> typeDenote res := match b with | TPlus => plus | TTimes => mult | TEq Nat => Nat.eqb | TEq Bool => Bool.eqb | TLe => Nat.leb end. Fixpoint texpDenote {t : type} (e : texp t) : typeDenote t := match e with | TNConst n => n | TBConst b => b | TBinop b e1 e2 => (tbinopDenote b) (texpDenote e1) (texpDenote e2) end. Definition tstack := list type. Inductive tinstr : tstack -> tstack -> Type := | TiNConst : forall {s : tstack}, nat -> tinstr s (Nat::s) | TiBConst : forall {s : tstack}, bool -> tinstr s (Bool::s) | TiBinop : forall {arg1 arg2 res : type} {s : tstack}, tbinop arg1 arg2 res -> tinstr (arg1::arg2::s) (res::s). Inductive tprog : tstack -> tstack -> Type := | TNil : forall {s : tstack}, tprog s s | TCons : forall {s1 s2 s3 : tstack}, tinstr s1 s2 -> tprog s2 s3 -> tprog s1 s3. Notation "'[]p'" := TNil. Notation "i '::p' p" := (TCons i p) (at level 55). Notation "'[' i ']p'" := (TCons i TNil). Fixpoint vstack (ts : tstack) : Type := match ts with | [] => unit | t::ts' => typeDenote t * vstack ts' end. Definition tinstrDenote {ts ts' : tstack} (i : tinstr ts ts') : vstack ts -> vstack ts' := match i with | TiNConst n => fun s => (n,s) | TiBConst b => fun s => (b,s) | TiBinop b => fun s => let '(arg1, (arg2, s')) := s in ((tbinopDenote b) arg1 arg2,s') end. Fixpoint tprogDenote {ts ts' : tstack} (p : tprog ts ts') : vstack ts -> vstack ts' := match p with | []p => fun s => s | i ::p p' => fun s => tprogDenote p' (tinstrDenote i s) end. Fixpoint tconcat {ts ts' ts'' : tstack} (p : tprog ts ts') : tprog ts' ts'' -> tprog ts ts'' := match p in tprog ts ts' return tprog ts' ts'' -> tprog ts ts'' with | []p => fun p' => p' | i ::p p1 => fun p' => i ::p (tconcat p1 p') end. Infix "++p" := tconcat (at level 50, left associativity). Lemma tconcat_assoc {ts1 ts2 ts3 ts4 : tstack} : forall (p1 : tprog ts1 ts2) (p2 : tprog ts2 ts3) (p3 : tprog ts3 ts4), p1 ++p (p2 ++p p3) = (p1 ++p p2) ++p p3. Proof. induction p1; intros. trivial. simpl. rewrite IHp1. trivial. Qed. Lemma tconcat_nil_r : forall (ts1 ts2 : tstack) (p : tprog ts1 ts2), p ++p []p = p. Proof. induction p. trivial. simpl. rewrite IHp. trivial. Qed. Fixpoint tcompile' {t : type} (e : texp t) {ts : tstack} : tprog ts (t::ts) := match e with | TNConst n => [ TiNConst n ]p | TBConst b => [ TiBConst b ]p | TBinop b e1 e2 => tcompile' e2 ++p tcompile' e1 ++p [ TiBinop b ]p end. Definition tcompile {t : type} (e : texp t) := @tcompile' t e []. Lemma tcompile_correct' : forall (t : type) (e : texp t) (ts1 ts2 : tstack) (s : vstack ts1) (p : tprog (t::ts1) ts2), tprogDenote (tcompile' e ++p p) s = tprogDenote p (texpDenote e,s). Proof. induction e; intros. trivial. trivial. simpl. rewrite <- ?tconcat_assoc. rewrite IHe2. rewrite IHe1. trivial. Qed. Theorem tcompile_correct : forall (t : type) (e : texp t), tprogDenote (tcompile e) tt = (texpDenote e,tt). Proof. intros. rewrite <- (tconcat_nil_r _ _ (tcompile e)). unfold tcompile. rewrite tcompile_correct'. trivial. Qed.