File template

Template for a Simulation Proof of Compiler Correctness.

These are all of the pieces that you likely will need. sim is your choice, and what you choose will affect how difficult sim_step and compile_sim are to prove (or whether they are both provable at all!). correct should be relatively mechanical; the difficult part is in the other lemmas.

Inductive term :=
| Base : nat -> term

.

Inductive step : term -> term -> Prop := .

Inductive Rstar {T : Type} (P : T -> T -> Prop) : T -> T -> Prop :=
| RRefl : forall a, Rstar P a a
| RStep : forall a b c, P a b -> Rstar P b c -> Rstar P a c
.

Fixpoint compile (t : term) : term := t.

Inductive sim : term -> term -> Prop := .

Lemma sim_step : forall t1 t1',
    step t1 t1' ->
    forall t2,
    sim t1 t2 ->
    exists t2', Rstar step t2 t2' /\ sim t1' t2'.
Admitted.

Lemma compile_sim : forall t,
    sim t (compile t).
Admitted.

Theorem correct : forall t v, Rstar step t (Base v) ->
                         Rstar step (compile t) (Base v).
Admitted.