Library ex11

Blatt 11 —- Operational semantics

SemProg SoSe 2013, Set 11

Based on the material of the online course "Software Foundations" by Pierce et al. Submit your solutions to tadeusz.m.litak at cs.fau.de

Please submit by Jul 18, anywhere on earth.

MODIFIED VERSION 1.1 POSTED JULY 12 —- see below for a little hint added

All 7 exercises in this Blatt are of the level of difficulty which in the previous Blatts I would put as 7.5 points. To avoid fractional points, let's say everything counts for 5 points in this Blatt; remember it will all be rescaled anyway...

Require Export Smallstep.

Exercise 1: (normal_forms_unique)

We have already seen that, for our language, single-step reduction is deterministic — i.e., a given term can take a single step in at most one way. It follows from this that, if t can reach a normal form, then this normal form is unique. In other words, we can actually pronounce normal_form t t' as "t' is the normal form of t."

ADDED IN VERSION 1.1 Note that, as the definition of one-step semantics has been inessentially changed after Module SimpleArith1 to one employing the notion of value, we need to reprove the determinism of the step relation. However, it does not take much effort to modify the original proof...

Lemma step_deterministic:
deterministic step.
Proof. Admitted.

... END OF CHANGES IN VERSION 1.1

Theorem normal_forms_unique:
deterministic normal_form_of.
Proof. Admitted.

Exercise 2: (stepeval) and (multistepeval)

This exercises finishes what we haven't done in the classroom

We proved one direction of multistep__eval as eval__multistep. For the other direction, we need one lemma, which establishes a relation between single-step reduction and big-step evaluation.

Lemma step__eval : forall t t' n,
     t ==> t' ->
     t' || n ->
     t || n.
Proof.
  intros t t' n Hs. generalize dependent n.
Admitted.

The fact that small-step reduction implies big-step is now straightforward to prove, once it is stated correctly.

The proof proceeds by induction on the multip-step reduction sequence that is buried in the hypothesis normal_form_of t t'.

Theorem multistep__eval : forall t t',
normal_form_of t t' -> exists n, t' = C n /\ t || n.
Proof.
Admitted.

EXERCISE BLOCK: combined_properties

We've considered the arithmetic and conditional expressions separately. This exercise explores how the two interact.

Module Combined.

Inductive tm : Type :=
  | C : nat -> tm
  | P : tm -> tm -> tm
  | ttrue : tm
  | tfalse : tm
  | tif : tm -> tm -> tm -> tm.

Tactic Notation "tm_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "C" | Case_aux c "P"
  | Case_aux c "ttrue" | Case_aux c "tfalse" | Case_aux c "tif" ].

Inductive value : tm -> Prop :=
  | v_const : forall n, value (C n)
  | v_true : value ttrue
  | v_false : value tfalse.

Reserved Notation " t '==>' t' " (at level 40).

Inductive step : tm -> tm -> Prop :=
  | ST_PlusConstConst : forall n1 n2,
      P (C n1) (C n2) ==> C (n1 + n2)
  | ST_Plus1 : forall t1 t1' t2,
      t1 ==> t1' ->
      P t1 t2 ==> P t1' t2
  | ST_Plus2 : forall v1 t2 t2',
      value v1 ->
      t2 ==> t2' ->
      P v1 t2 ==> P v1 t2'
  | ST_IfTrue : forall t1 t2,
      tif ttrue t1 t2 ==> t1
  | ST_IfFalse : forall t1 t2,
      tif tfalse t1 t2 ==> t2
  | ST_If : forall t1 t1' t2 t3,
      t1 ==> t1' ->
      tif t1 t2 t3 ==> tif t1' t2 t3

  where " t '==>' t' " := (step t t').

Tactic Notation "step_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "ST_PlusConstConst"
  | Case_aux c "ST_Plus1" | Case_aux c "ST_Plus2"
  | Case_aux c "ST_IfTrue" | Case_aux c "ST_IfFalse" | Case_aux c "ST_If" ].

Exercise 3 (step_deterministic)

Lemma value_is_nf : forall v,
value v -> normal_form step v.
Proof. Admitted.

Theorem step_deterministic: deterministic step.
Proof. Admitted.

Exercise 4 (failure_of_progress)

Theorem failure_of_progress : exists t, ~(value t) /\ normal_form step t.
Proof. Admitted.

End Combined.

EXERCISE BLOCK: Concurrent Imp

Include CImp.

At the end of the lecture we introduced the concurrent Imp language. As we realized doing our first quiz on it, concurrency is rather confusing. Therefore, let us check in detail what is happening with the first program. Recall its definition:

Definition par_quiz1 : com :=
(PAR
    Y ::= ANum 1
  WITH
    Y ::= APlus (AId Y) (ANum 1)
  END);
  X ::= AId Y.

Exercise 5 (test1_parquiz1), (test2_parquiz1)

First, use the functional extensionality axiom (you can find it in our earlier lectures or in module Coq.Logic.FunctionalExtensionality) to show this lemma:

Lemma ext_update_shadow : forall st Y n n', update (update st Y n) Y n' = update st Y n'.
Proof. Admitted.

Now, observe there are states the quiz program can terminate in regardless of the starting state

Theorem test1_parquiz1 : forall st, par_quiz1/st ==>* SKIP / update (update st Y 1) X 1.
Proof. Admitted.

Theorem test2_parquiz1 : forall st, par_quiz1/st ==>* SKIP / update (update st Y 2) X 2.
Proof. Admitted.

However, some other values of X and Y can only be reached from a very specific starting state...

Exercise 6 (test3_parquiz1), (test4_parquiz1)

Theorem test3_parquiz1 : par_quiz1/(update empty_state Y 2) ==>* SKIP / update (update empty_state Y 3) X 3.
Proof. Admitted.

More generally...

Theorem test4_parquiz1 : forall n, exists st, par_quiz1/st ==>* SKIP / update (update empty_state Y (S n)) X (S n).
Proof. Admitted.

Exercise 7: (par_body_n__Sn) (par_body_n)

Finally, let us prove the two lemmas we needed for par_loop_any_X. Not to create a conflict with existing names, I slightly modify them...

Lemma par_body_n__Sn' : forall n st,
  st X = n /\ st Y = 0 ->
  par_loop / st ==>* par_loop / (update st X (S n)).
Proof. Admitted.

Lemma par_body_n' : forall n st,
  st X = 0 /\ st Y = 0 ->
  exists st',
    par_loop / st ==>* par_loop / st' /\ st' X = n /\ st' Y = 0.
Proof. Admitted.