Correctness of an Expression Compiler in Coq

This is based on Correctness Of A Compiler For Arithmetic Expressions and A type-correct, stack-safe, provably correct expression compiler in Epigram

Require Import List.

Fixpoint Tuple (types : list Set) : Type :=
  match types with
    | nil => unit
    | t::ts => (t * Tuple ts)%type
  end.

Inductive Exp : Set -> Type :=
| Num : nat -> Exp nat
| Boo : bool -> Exp bool
| Sum : Exp nat -> Exp nat -> Exp nat
| Eql : Exp nat -> Exp nat -> Exp bool
| Iff : forall (a : Set), Exp bool -> Exp a -> Exp a -> Exp a.

Fixpoint nat_eq_bool (x y : nat) {struct x} : bool :=
  match x, y with
    | O, O => true
    | S x', S y' => nat_eq_bool x' y'
    | _,_ => false
  end.

Fixpoint eval (a : Set) (e : Exp a) : a :=
  match e in Exp t return t with
    | Num n => n
    | Boo b => b
    | Sum p q => eval _ p + eval _ q
    | Eql x y => nat_eq_bool (eval _ x) (eval _ y)
    | Iff _ b t e => if eval _ b then eval _ t else eval _ e
  end.

(* example *)
Eval compute in
  (eval _
    (Iff _ (Eql (Num 7) (Sum (Num 4) (Num 3)))
      (Sum (Num 5) (Num 8))
      (Num 0))).

Notation "x --> y" := (x,y) (at level 120, right associativity).

Inductive INST : list Set * list Set -> Type :=
| PUSHN : forall s, nat -> INST (s --> nat::s)
| PUSHB : forall s, bool -> INST (s --> bool::s)
| SUM : forall s, INST (nat::nat::s --> nat::s)
| EQL : forall s, INST (nat::nat::s --> bool::s)
| COND : forall s, forall a, INST (bool::a::a::s --> a::s).

Inductive stack : list Set -> Type :=
| snil : stack nil
| scons : forall p q, INST (p --> q) -> stack p -> stack q.

Fixpoint compile
  (a : Set) (e : Exp a)
  (tail : list Set) (rest : stack tail)
  { struct e } : stack (a::tail) :=
  match e in Exp a return stack (a::tail) with
    | Num n =>
      scons _ _ (PUSHN _ n) rest
    | Boo b =>
      scons _ _ (PUSHB _ b) rest
    | Sum u v =>
      scons _ _ (SUM _)
      (compile _ u _
        (compile _ v _ rest))
    | Eql x y =>
      scons _ _ (EQL _)
      (compile _ x _
        (compile _ y _ rest))
    | Iff a b t e =>
      scons _ _ (COND _ _)
      (compile _ b _
        (compile _ t _
          (compile _ e _ rest)))
  end.

Definition evinst :
  forall p q,
    forall (i : INST (p --> q)),
      Tuple p -> Tuple q :=
      fun p q i =>
        match i in INST pq return Tuple (fst pq) -> Tuple (snd pq) with
          | PUSHN _ n => fun s =>
            (n, s)
          | PUSHB _ b => fun s =>
            (b, s)
          | SUM _ => fun s =>
            match s with
              | (u, (v, s)) => (u + v, s)
            end
          | EQL _ => fun s =>
            match s with
              | (x, (y, s)) => (nat_eq_bool x y, s)
            end
          | COND _ _ => fun s =>
            match s with
              | (b, (t, (e, s))) =>
                (if b then t else e, s)
            end
        end.

Fixpoint evstack typs (program : stack typs)
  { struct program } : Tuple typs :=
  match program in stack typs return Tuple typs with
    | snil => tt
    | scons t ts i is => evinst _ _ i (evstack _ is)
  end.

Eval compute in
  (evstack _ (compile _
    (Iff _ (Eql (Num 7) (Sum (Num 4) (Num 3)))
      (Sum (Num 5) (Num 8))
      (Num 0)) nil snil)).

Lemma eval_correct :
  forall a (e : Exp a),
    forall typs (program_tail : stack typs),
      (eval a e, (evstack typs program_tail))
      =
      evstack (a::typs) (compile a e typs program_tail).
Proof.
  induction e.
  
  reflexivity.
  
  reflexivity.
  
  intros.
  unfold compile; fold compile; simpl.
  rewrite <- IHe1.
  rewrite <- IHe2.
  reflexivity.
  
  intros.
  unfold compile; fold compile; simpl.
  rewrite <- IHe1.
  rewrite <- IHe2.
  reflexivity.
  
  intros.
  unfold compile; fold compile; simpl.
  rewrite <- IHe1.
  rewrite <- IHe2.
  rewrite <- IHe3.
  reflexivity.
Qed.