# Problem Set 3

Inductive step_com : com -> state -> com -> state -> Prop :=

| Step_assign: forall s x e,

step_com (Assign x e) s

(Skip) (set x (eval_aexp e s) s)

| Step_seqL: forall c1 c2 c1' s s', step_com c1 s c1' s' ->

step_com (Seq c1 c2) s (Seq c1' c2) s'

| Step_seqR: forall c s, step_com (Seq Skip c) s c s

| Step_if_true: forall b c1 c2 s, eval_bexp b s = true ->

step_com (If b c1 c2) s c1 s

| Step_if_false: forall b c1 c2 s, eval_bexp b s = false ->

step_com (If b c1 c2) s c2 s

| Step_while: forall b c s,

step_com (While b c) s

(If b (Seq c (While b c)) Skip) s.

## 1. Give a definition of the same small-step semantics, as a function.

Note that a final configuration should step to None.Variable step_com_fn : com -> state -> option (com * state)

^^^ replace me ^^^

.

Lemma progress : forall c s, step_com_fn c s = None -> c = Skip.

Admitted.

## 3. Prove that all steps in the functional semantics work in the relational one.

*Hints*:

- You will need to use induction, and you will need to use it at the right level of quantifier nesting in order to have a strong enough induction hypothesis.
- Try doing the Seq case early to work out the inductive step. Some of the other cases will be doable in a specialized way, but everything other than Skip can be handled uniformly.
- some handy tactics to try: discriminate, congruence, specialize, assumption, crush.
- some handy tacticals to try: ;, try, ||

Theorem forward_sim : forall c s c' s', step_com_fn c s = Some (c', s') -> step_com c s c' s'.

Admitted.

Theorem backward_sim : forall c s c' s', step_com c s c' s' -> step_com_fn c s = Some (c', s').

Admitted.

This page has been generated by coqdoc