# Problem Set 4

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.

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.

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.

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