Problem Set 4

In class we saw both big-step and small-step semantics for IMP. Are these semantics really equivalent?

Here is the small-step semantics we saw in class:

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.

And here is the big-step semantics:

Inductive eval_com : com -> state -> state -> Prop :=
| Eval_skip : forall s, eval_com Skip s s
| Eval_assign : forall s x e, eval_com (Assign x e) s (set x (eval_aexp e s) s)
| Eval_seq : forall c1 s0 s1 c2 s2,
               eval_com c1 s0 s1 -> eval_com c2 s1 s2 -> eval_com (Seq c1 c2) s0 s2
| Eval_if_true : forall b c1 c2 s s',
                   eval_bexp b s = true ->
                   eval_com c1 s s' -> eval_com (If b c1 c2) s s'
| Eval_if_false : forall b c1 c2 s s',
                   eval_bexp b s = false ->
                   eval_com c2 s s' -> eval_com (If b c1 c2) s s'
| Eval_while_false : forall b c s,
                       eval_bexp b s = false ->
                       eval_com (While b c) s s
| Eval_while_true : forall b c s1 s2 s3,
                      eval_bexp b s1 = true ->
                      eval_com c s1 s2 ->
                      eval_com (While b c) s2 s3 ->
                      eval_com (While b c) s1 s3.

Your mission: show that the semantics agree with each other. Try to use tacticals to make your proof short and clear.

The challenge will be to use induction in just right way so your induction hypotheses prove the right things when you need them. It helps to work out proofs on paper so you know what induction hypotheses you are looking for.

Some tips:

You can use induction on anything inductively defined, including inductively defined relations.
The remember tactic can be used to enforce constraints on the induction hypothesis.
The revert tactic is also helpful for controlling the form of the induction hypothesis created by induction.

Inductive steps_com : com -> state -> com -> state -> Prop :=
| Steps_none : forall c s, steps_com c s c s
| Steps_some : forall c s c' s' c'' s'', step_com c s c' s' ->
                steps_com c' s' c'' s'' -> steps_com c s c'' s''.

Lemma concat_seq : forall c1 c2 s1 s2 s3,
              steps_com c1 s1 Skip s2 ->
               steps_com c2 s2 Skip s3 ->
                steps_com (Seq c1 c2) s1 Skip s3.
Proof.

Par: 6 commands (; or .)

Admitted.

Theorem big_to_small:
forall c s s',
eval_com c s s' -> steps_com c s Skip s'.
Proof.

Par: 11 commands

Admitted.

Theorem small_to_big:
forall c s s',
steps_com c s Skip s' -> eval_com c s s'.
Proof.

Par: 28 commands. This one is harder and you'll have to get induction hypotheses just right.

Admitted.

Theorem big_small_agree:
forall c s s',
   eval_com c s s' <-> steps_com c s Skip s'.
Proof.
   Hint Immediate big_to_small small_to_big.
   crush.
Qed.

Finish this proof by completing the admitted lemmas. You are welcome to use your result from the previous assignment, but be sure to include it in your development if so.

This page has been generated by coqdoc