Require Import List. Import ListNotations. Inductive binop := Plus | Times. Inductive exp := | Const : nat -> exp | Binop : binop -> exp -> exp -> exp. Definition binopDenote (b : binop) : nat -> nat -> nat := match b with | Plus => plus | Times => mult end. Fixpoint expDenote (e : exp) : nat := match e with | Const n => n | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2) end. Inductive instr := | IConst : nat -> instr | IBinop : binop -> instr. Definition prog := list instr. Definition stack := list nat. Definition instrDenote (i : instr) (s : stack) : option stack := match i with | IConst n => Some (n::s) | IBinop b => match s with | arg1::arg2::s' => Some (((binopDenote b) arg1 arg2)::s') | _ => None end end. Fixpoint progDenote (p : prog) (s : stack) : option stack := match p with | [] => Some s | i::p' => match instrDenote i s with | Some s' => progDenote p' s' | None => None end end. Fixpoint compile (e : exp) : prog := match e with | Const n => [IConst n] | Binop b e1 e2 => compile e2 ++ compile e1 ++ [IBinop b] end. Lemma compile_correct' : forall e p s, progDenote (compile e ++ p) s = progDenote p (expDenote e::s). Proof. induction e. intros p s. trivial. intros p s. simpl. rewrite <- app_assoc. rewrite IHe2. rewrite <- app_assoc. rewrite IHe1. trivial. Qed. Theorem compile_correct : forall e, progDenote (compile e) [] = Some [expDenote e]. Proof. intro e. rewrite <- (app_nil_r (compile e)). rewrite compile_correct'. trivial. Qed.