# 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.