Require Import List. (* to obtain "::" notation *)

Section Compilation.
Variable value : Type.
Definition binop : Type := value -> value -> value.

Inductive exp : Type :=
| Val : value -> exp
| Binop : binop -> exp -> exp -> exp.

Fixpoint eval (e : exp) : value :=
  match e with
    | Val v => v
    | Binop o e1 e2 => o (eval e1) (eval e2)
  end.

Inductive instr : Type :=
| iVal : value -> instr
| iBinop : binop -> instr.

Definition prog := list instr.
Definition stack := list value.

Definition runInstr (i : instr) (s : stack) : option stack :=
  match i with
    | iVal v => Some (v :: s)
    | iBinop o =>
      match s with
        | arg1 :: arg2 :: s' => Some (o arg1 arg2 :: s')
        | _ => None
      end
  end.

Fixpoint runProg (p : prog) (s : stack) : option stack :=
  match p with
    | nil => Some s
    | i :: p' =>
      match runInstr i s with
        | None => None
        | Some s' => runProg p' s'
      end
  end.

Fixpoint compile (e : exp) : prog :=
  match e with
    | Val v => iVal v :: nil
    | Binop o e1 e2 => compile e2 ++ compile e1 ++ iBinop o :: nil
  end.

Lemma compile_correct' e p s:
runProg (compile e ++ p) s = runProg p (eval e :: s).

Proof. revert p s. induction e ; intros p s ; simpl.
reflexivity.
rewrite <- app_assoc. rewrite IHe2.
rewrite <- app_assoc. rewrite IHe1. simpl. reflexivity. Qed.

Theorem compile_correct e s :
runProg (compile e) s = Some (eval e :: s).

Proof. rewrite <- (app_nil_r (compile e)).
  rewrite compile_correct'. simpl. reflexivity. Qed.

Inductive evalp : exp -> value -> Prop :=
| evalpV v :
  evalp (Val v) v
| evalpB o e1 e2 v1 v2 :
  evalp e1 v1 -> evalp e2 v2 ->
  evalp (Binop o e1 e2) (o v1 v2).

Goal forall e, evalp e (eval e).

Proof. induction e ; simpl ; constructor ; assumption. Qed.

Goal forall e v, evalp e v <-> eval e = v.

Proof. split ; intros A.
induction A ; simpl ; congruence. (* induction on e more tedious *)
rewrite <- A. clear v A. (* essential, otherwise induction generalizes A *)
induction e ; simpl ; constructor ; assumption. Qed.

Fixpoint decompile' (p : prog) (s : list exp) : option exp :=
match p, s with
 | nil, e :: nil => Some e
 | iVal v :: p', s => decompile' p' (Val v :: s)
 | iBinop o :: p', e1 :: e2 :: s' => decompile' p' (Binop o e1 e2 :: s')
 | _, _ => None
end.

Definition decompile (p : prog) := decompile' p nil.

Lemma decompile_correct' e p s:
decompile' (compile e ++ p) s = decompile' p (e :: s).

Proof. revert p s. induction e; intros p s ; simpl ; try reflexivity.
rewrite <-app_assoc, IHe2. rewrite <-app_assoc, IHe1. reflexivity. Qed.

Lemma decompile_correct e :
decompile (compile e) = Some e.

Proof. rewrite <- (app_nil_r (compile e)).
exact (decompile_correct' e nil nil). Qed.

End Compilation.