# SmallstepSmall-step Operational Semantics

(* $Date: 2012-12-26 16:12:50 -0500 (Wed, 26 Dec 2012) $ *)

Require Export Imp.

The evaluators we have seen so far (e.g., the ones for aexps,
bexps, and commands) have been formulated in a "big-step"
style — they specify how a given expression can be evaluated to
its final value (or a command plus a store to a final store) "all
in one big step."
This style is simple and natural for many purposes (indeed, Gilles
Kahn, who popularized its use, called it
Another shortcoming of the big-step style is more technical, but
critical for some applications. Consider the variant of Imp with
lists that we introduced in the HoareList chapter. We chose to
define the meaning of programs like 0 + nil by specifying that a
list should be interpreted as 0 when it occurs in a context
expecting a number, but this was a bit of a hack. It would be
better simply to say that the behavior of such a program is
However, this way of defining Imp has a serious deficiency. In
this language, a command might
These two outcomes — nontermination vs. getting stuck in an
erroneous configuration — are quite different. In particular, we
want to allow the first (permitting the possibility of infinite
loops is the price we pay for the convenience of programming with
general looping constructs like while) but prevent the
second (which is just wrong), for example by adding some form of
So, for lots of reasons, we'd like to have a finer-grained way of
defining and reasoning about program behaviors. This is the topic
of the present chapter. We replace the "big-step" eval relation
with a "small-step" relation that specifies, for a given program,
how the "atomic steps" of computation are performed.

*natural semantics*), but there are some things it does not do well. In particular, it does not give us a natural way of talking about*concurrent*programming languages, where the "semantics" of a program — i.e., the essence of how it behaves — is not just which input states get mapped to which output states, but also includes the intermediate states that it passes through along the way, since these states can also be observed by concurrently executing code.*undefined*— it doesn't evaluate to any result. We could easily do this: we'd just have to use the formulations of aeval and beval as inductive propositions (rather than Fixpoints), so that we can make them partial functions instead of total ones.*fail*to map a given starting state to any ending state for two quite different reasons: either because the execution gets into an infinite loop or because, at some point, the program tries to do an operation that makes no sense, such as taking the successor of a boolean variable, and none of the evaluation rules can be applied.*typechecking*to the language. Indeed, this will be a major topic for the rest of the course. As a first step, we need a different way of presenting the semantics that allows us to distinguish nontermination from erroneous "stuck states."# Relations

*relation*on a set X is a family of propositions parameterized by two elements of X — i.e., a proposition about pairs of elements of X.

Definition relation (X: Type) := X→X→Prop.

Our main examples of such relations in this chapter will be
the single-step and multi-step reduction relations on terms, ⇒
and ⇒*, but there are many other examples — some that come to
mind are the "equals," "less than," "less than or equal to," and
"is the square of" relations on numbers, and the "prefix of"
relation on lists and strings.
The optional Rel chapter tells a more detailed story about how
relations are treated in Coq.

# A Toy Language

Inductive tm : Type :=

| C : nat → tm

| P : tm → tm → tm.

Tactic Notation "tm_cases" tactic(first) ident(c) :=

first;

[ Case_aux c "C" | Case_aux c "P" ].

Module SimpleArith0.

Here is a standard evaluator for this language, written in the
same (big-step) style as we've been using up to this point.

Fixpoint eval (t : tm) : nat :=

match t with

| C n => n

| P a1 a2 => eval a1 + eval a2

end.

End SimpleArith0.

Now, here is the same evaluator, written in exactly the same
style, but formulated as an inductively defined relation. Again,
we use the notation t ⇓ n for "t evaluates to n."

(E_Const) | |

C n ⇓ n |

t1 ⇓ n1 | |

t2 ⇓ n2 | (E_Plus) |

P t1 t2 ⇓ C (n1 + n2) |

Reserved Notation " t '⇓' n " (at level 50, left associativity).

Inductive eval : tm → nat → Prop :=

| E_Const : ∀n,

C n ⇓ n

| E_Plus : ∀t1 t2 n1 n2,

t1 ⇓ n1 →

t2 ⇓ n2 →

P t1 t2 ⇓ (n1 + n2)

where " t '⇓' n " := (eval t n).

Tactic Notation "eval_cases" tactic(first) ident(c) :=

first;

[ Case_aux c "E_Const" | Case_aux c "E_Plus" ].

Module SimpleArith1.

Now, here is a small-step version.

(ST_PlusConstConst) | |

P (C n1) (C n2) ⇒ C (n1 + n2) |

t1 ⇒ t1' | (ST_Plus1) |

P t1 t2 ⇒ P t1' t2 |

t2 ⇒ t2' | (ST_Plus2) |

P (C n1) t2 ⇒ P (C n1) t2' |

Reserved Notation " t '⇒' t' " (at level 40).

Inductive step : tm → tm → Prop :=

| ST_PlusConstConst : ∀n1 n2,

P (C n1) (C n2) ⇒ C (n1 + n2)

| ST_Plus1 : ∀t1 t1' t2,

t1 ⇒ t1' →

P t1 t2 ⇒ P t1' t2

| ST_Plus2 : ∀n1 t2 t2',

t2 ⇒ t2' →

P (C n1) t2 ⇒ P (C n1) t2'

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" ].

first;

[ Case_aux c "ST_PlusConstConst"

| Case_aux c "ST_Plus1" | Case_aux c "ST_Plus2" ].

Things to notice:
A couple of examples of reasoning with the step
relation...
If t1 can take a step to t1', then P t1 t2 steps
to plus t1' t2:

- We are defining just a single reduction step, in which
one P node is replaced by its value.
- Each step finds the
*leftmost*P node that is ready to go (both of its operands are constants) and rewrites it in place. The first rule tells how to rewrite this P node itself; the other two rules tell how to find it. - A term that is just a constant cannot take a step.

Example test_step_1 :

P

(P (C 0) (C 3))

(P (C 2) (C 4))

⇒

P

(C (0 + 3))

(P (C 2) (C 4)).

Proof.

apply ST_Plus1. apply ST_PlusConstConst. Qed.

apply ST_Plus1. apply ST_PlusConstConst. Qed.

#### Exercise: 2 stars (test_step_2)

Right-hand sides of sums can take a step only when the left-hand side is finished: if t2 can take a step to t2', then P (C n) t2 steps to P (C n) t2':Example test_step_2 :

P

(C 0)

(P

(C 2)

(P (C 0) (C 3)))

⇒

P

(C 0)

(P

(C 2)

(C (0 + 3))).

Proof.

(* FILL IN HERE *) Admitted.

☐
One simple property of the ⇒ relation is that, like the
evaluation relation for our language of Imp programs, it is

*deterministic*.*Theorem*: For each t, there is at most one t' such that t steps to t' (t ⇒ t' is provable). Formally, this is the same as saying that ⇒ is deterministic.*Proof sketch*: We show that if x steps to both y1 and y2 then y1 and y2 are equal, by induction on a derivation of step x y1. There are several cases to consider, depending on the last rule used in this derivation and in the given derivation of step x y2.- If both are ST_PlusConstConst, the result is immediate.
- The cases when both derivations end with ST_Plus1 or
ST_Plus2 follow by the induction hypothesis.
- It cannot happen that one is ST_PlusConstConst and the other
is ST_Plus1 or ST_Plus2, since this would imply that x has
the form P t1 t2 where both t1 and t2 are
constants (by ST_PlusConstConst)
*and*one of t1 or t2 has the form P .... - Similarly, it cannot happen that one is ST_Plus1 and the other is ST_Plus2, since this would imply that x has the form P t1 t2 where t1 has both the form P t1 t2 and the form C n. ☐

Definition deterministic {X: Type} (R: relation X) :=

∀x y1 y2 : X, R x y1 → R x y2 → y1 = y2.

Theorem step_deterministic:

deterministic step.

Proof.

unfold deterministic. intros x y1 y2 Hy1 Hy2.

generalize dependent y2.

step_cases (induction Hy1) Case; intros y2 Hy2.

Case "ST_PlusConstConst". step_cases (inversion Hy2) SCase.

SCase "ST_PlusConstConst". reflexivity.

SCase "ST_Plus1". inversion H2.

SCase "ST_Plus2". inversion H2.

Case "ST_Plus1". step_cases (inversion Hy2) SCase.

SCase "ST_PlusConstConst". rewrite ← H0 in Hy1. inversion Hy1.

SCase "ST_Plus1".

rewrite ← (IHHy1 t1'0).

reflexivity. assumption.

SCase "ST_Plus2". rewrite ← H in Hy1. inversion Hy1.

Case "ST_Plus2". step_cases (inversion Hy2) SCase.

SCase "ST_PlusConstConst". rewrite ← H1 in Hy1. inversion Hy1.

SCase "ST_Plus1". inversion H2.

SCase "ST_Plus2".

rewrite ← (IHHy1 t2'0).

reflexivity. assumption. Qed.

unfold deterministic. intros x y1 y2 Hy1 Hy2.

generalize dependent y2.

step_cases (induction Hy1) Case; intros y2 Hy2.

Case "ST_PlusConstConst". step_cases (inversion Hy2) SCase.

SCase "ST_PlusConstConst". reflexivity.

SCase "ST_Plus1". inversion H2.

SCase "ST_Plus2". inversion H2.

Case "ST_Plus1". step_cases (inversion Hy2) SCase.

SCase "ST_PlusConstConst". rewrite ← H0 in Hy1. inversion Hy1.

SCase "ST_Plus1".

rewrite ← (IHHy1 t1'0).

reflexivity. assumption.

SCase "ST_Plus2". rewrite ← H in Hy1. inversion Hy1.

Case "ST_Plus2". step_cases (inversion Hy2) SCase.

SCase "ST_PlusConstConst". rewrite ← H1 in Hy1. inversion Hy1.

SCase "ST_Plus1". inversion H2.

SCase "ST_Plus2".

rewrite ← (IHHy1 t2'0).

reflexivity. assumption. Qed.

End SimpleArith1.

## Values

*abstract machine*:

- At any moment, the
*state*of the machine is a term. - A
*step*of the machine is an atomic unit of computation — here, a single "add" operation. - The
*halting states*of the machine are ones where there is no more computation to be done.

- Take t as the starting state of the machine.
- Repeatedly use the ⇒ relation to find a sequence of
machine states, starting with t, where each state steps to
the next.
- When no more reduction is possible, "read out" the final state of the machine as the result of execution.

*values*.

Inductive value : tm → Prop :=

v_const : ∀n, value (C n).

Having introduced the idea of values, we can use it in the
definition of the ⇒ relation to write ST_Plus2 rule in a
slightly more elegant way:

Again, the variable names here carry important information:
by convention, v1 ranges only over values, while t1 and t2
range over arbitrary terms. (Given this convention, the explicit
value hypothesis is arguably redundant. We'll keep it for now,
to maintain a close correspondence between the informal and Coq
versions of the rules, but later on we'll drop it in informal
rules, for the sake of brevity.)

(ST_PlusConstConst) | |

P (C n1) (C n2) ⇒ C (n1 + n2) |

t1 ⇒ t1' | (ST_Plus1) |

P t1 t2 ⇒ P t1' t2 |

value v1 | |

t2 ⇒ t2' | (ST_Plus2) |

P v1 t2 ⇒ P v1 t2' |

Reserved Notation " t '⇒' t' " (at level 40).

Inductive step : tm → tm → Prop :=

| ST_PlusConstConst : ∀n1 n2,

P (C n1) (C n2)

⇒ C (n1 + n2)

| ST_Plus1 : ∀t1 t1' t2,

t1 ⇒ t1' →

P t1 t2 ⇒ P t1' t2

| ST_Plus2 : ∀v1 t2 t2',

value v1 → (* <----- n.b. *)

t2 ⇒ t2' →

P v1 t2 ⇒ P v1 t2'

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" ].

first;

[ Case_aux c "ST_PlusConstConst"

| Case_aux c "ST_Plus1" | Case_aux c "ST_Plus2" ].

#### Exercise: 3 stars, recommended (redo_determinism)

As a sanity check on this change, let's re-verify determinism- If both are ST_PlusConstConst, the result is immediate.
- It cannot happen that one is ST_PlusConstConst and the other
is ST_Plus1 or ST_Plus2, since this would imply that x has
the form P t1 t2 where both t1 and t2 are
constants (by ST_PlusConstConst) AND one of t1 or t2 has
the form P ....
- Similarly, it cannot happen that one is ST_Plus1 and the other
is ST_Plus2, since this would imply that x has the form
P t1 t2 where t1 both has the form P t1 t2 and
is a value (hence has the form C n).
- The cases when both derivations end with ST_Plus1 or ST_Plus2 follow by the induction hypothesis. ☐

#### Exercise: 2 stars, optional (step_deterministic)

Theorem step_deterministic :

deterministic step.

Proof.

(* FILL IN HERE *) Admitted.

deterministic step.

Proof.

(* FILL IN HERE *) Admitted.

☐

## Strong Progress and Normal Forms

*Theorem*(

*Strong Progress*): For all t:tm, either t is a value, or there exists a term t' such that t ⇒ t'.

*Proof*: By induction on t.

- Suppose t = C n. Then t is a value.
- Suppose t = P t1 t2, where (by the IH) t1 is either a
value or can step to some t1', and where t2 is either a
value or can step to some t2'. We must show P t1 t2 is
either a value or steps to some t'.
- If t1 and t2 are both values, then t can take a step, by
ST_PlusConstConst.
- If t1 is a value and t2 can take a step, then so can t,
by ST_Plus2.
- If t1 can take a step, then so can t, by ST_Plus1. ☐

- If t1 and t2 are both values, then t can take a step, by
ST_PlusConstConst.

Theorem strong_progress : ∀t,

value t ∨ (∃t', t ⇒ t').

Proof.

tm_cases (induction t) Case.

Case "C". left. apply v_const.

Case "P". right. inversion IHt1.

SCase "l". inversion IHt2.

SSCase "l". inversion H. inversion H0.

∃(C (n + n0)).

apply ST_PlusConstConst.

SSCase "r". inversion H0 as [t' H1].

∃(P t1 t').

apply ST_Plus2. apply H. apply H1.

SCase "r". inversion H as [t' H0].

∃(P t' t2).

apply ST_Plus1. apply H0. Qed.

tm_cases (induction t) Case.

Case "C". left. apply v_const.

Case "P". right. inversion IHt1.

SCase "l". inversion IHt2.

SSCase "l". inversion H. inversion H0.

∃(C (n + n0)).

apply ST_PlusConstConst.

SSCase "r". inversion H0 as [t' H1].

∃(P t1 t').

apply ST_Plus2. apply H. apply H1.

SCase "r". inversion H as [t' H0].

∃(P t' t2).

apply ST_Plus1. apply H0. Qed.

This important property is called
The idea of "making progress" can be extended to tell us something
interesting about values: in this language values are exactly
the terms that

*strong progress*, because every term either is a value or can "make progress" by stepping to some other term. (The qualifier "strong" distinguishes it from a more refined version that we'll see in later chapters, called simply "progress.")*cannot*make progress in this sense. To state this fact, let's begin by giving a name to terms that cannot make progress: We'll call them*normal forms*.Definition normal_form {X:Type} (R:relation X) (t:X) : Prop :=

~ ∃t', R t t'.

This definition actually specifies what it is to be a normal form
for an
We can use this terminology to generalize the observation we made
in the strong progress theorem: in this language, normal forms and
values are actually the same thing.

*arbitrary*relation R over an arbitrary set X, not just for the particular single-step reduction relation over terms that we are interested in at the moment. We'll re-use the same terminology for talking about other relations later in the course.Lemma value_is_nf : ∀t,

value t → normal_form step t.

Proof.

unfold normal_form. intros t H. inversion H.

intros contra. inversion contra. inversion H1.

Qed.

unfold normal_form. intros t H. inversion H.

intros contra. inversion contra. inversion H1.

Qed.

Lemma nf_is_value : ∀t,

normal_form step t → value t.

Proof. (* a corollary of strong_progress... *)

unfold normal_form. intros t H.

assert (G : value t ∨ ∃t', t ⇒ t').

SCase "Proof of assertion". apply strong_progress.

inversion G.

SCase "l". apply H0.

SCase "r". apply ex_falso_quodlibet. apply H. assumption. Qed.

unfold normal_form. intros t H.

assert (G : value t ∨ ∃t', t ⇒ t').

SCase "Proof of assertion". apply strong_progress.

inversion G.

SCase "l". apply H0.

SCase "r". apply ex_falso_quodlibet. apply H. assumption. Qed.

Corollary nf_same_as_value : ∀t,

normal_form step t ↔ value t.

Proof.

split. apply nf_is_value. apply value_is_nf. Qed.

split. apply nf_is_value. apply value_is_nf. Qed.

Why is this interesting? For two reasons:
Let's examine how this can happen...

- Because value is a syntactic concept — it is a defined by
looking at the form of a term — while normal_form is a
semantic one — it is defined by looking at how the term steps.
It is not obvious that these concepts should coincide!
- Indeed, there are lots of languages in which the concepts of
normal form and value do
*not*coincide.

We might, for example, mistakenly define value so that it
includes some terms that are not finished reducing.

Module Temp1.

(* Open an inner module so we can redefine value and step. *)

Inductive value : tm → Prop :=

| v_const : ∀n, value (C n)

| v_funny : ∀t1 n2, (* <---- *)

value (P t1 (C n2)).

Reserved Notation " t '⇒' t' " (at level 40).

Inductive step : tm → tm → Prop :=

| ST_PlusConstConst : ∀n1 n2,

P (C n1) (C n2) ⇒ C (n1 + n2)

| ST_Plus1 : ∀t1 t1' t2,

t1 ⇒ t1' →

P t1 t2 ⇒ P t1' t2

| ST_Plus2 : ∀v1 t2 t2',

value v1 →

t2 ⇒ t2' →

P v1 t2 ⇒ P v1 t2'

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

Lemma value_not_same_as_normal_form :

∃t, value t ∧ ~ normal_form step t.

Proof.

(* FILL IN HERE *) Admitted.

∃t, value t ∧ ~ normal_form step t.

Proof.

(* FILL IN HERE *) Admitted.

☐

End Temp1.

Alternatively, we might mistakenly define step so that it
permits something designated as a value to reduce further.

Module Temp2.

Inductive value : tm → Prop :=

| v_const : ∀n, value (C n).

Reserved Notation " t '⇒' t' " (at level 40).

Inductive step : tm → tm → Prop :=

| ST_Funny : ∀n, (* <---- *)

C n ⇒ P (C n) (C 0)

| ST_PlusConstConst : ∀n1 n2,

P (C n1) (C n2) ⇒ C (n1 + n2)

| ST_Plus1 : ∀t1 t1' t2,

t1 ⇒ t1' →

P t1 t2 ⇒ P t1' t2

| ST_Plus2 : ∀v1 t2 t2',

value v1 →

t2 ⇒ t2' →

P v1 t2 ⇒ P v1 t2'

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

Lemma value_not_same_as_normal_form :

∃t, value t ∧ ~ normal_form step t.

Proof.

(* FILL IN HERE *) Admitted.

∃t, value t ∧ ~ normal_form step t.

Proof.

(* FILL IN HERE *) Admitted.

☐

End Temp2.

Finally, we might define value and step so that there is some
term that is not a value but that cannot take a step in the step
relation. Such terms are said to be

*stuck*. In this case this is caused by a mistake in the semantics, but we will also see situations where, evne in a correct language definition, it makes sense to allow some terms to be stuck.Module Temp3.

Inductive value : tm → Prop :=

| v_const : ∀n, value (C n).

Reserved Notation " t '⇒' t' " (at level 40).

Inductive step : tm → tm → Prop :=

| ST_PlusConstConst : ∀n1 n2,

P (C n1) (C n2) ⇒ C (n1 + n2)

| ST_Plus1 : ∀t1 t1' t2,

t1 ⇒ t1' →

P t1 t2 ⇒ P t1' t2

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

Lemma value_not_same_as_normal_form :

∃t, ~ value t ∧ normal_form step t.

Proof.

(* FILL IN HERE *) Admitted.

∃t, ~ value t ∧ normal_form step t.

Proof.

(* FILL IN HERE *) Admitted.

☐

End Temp3.

Module Temp4.

Here is another very simple language whose terms, instead of being
just plus and numbers, are just the booleans true and false and a
conditional expression...

Inductive tm : Type :=

| ttrue : tm

| tfalse : tm

| tif : tm → tm → tm → tm.

Inductive value : tm → Prop :=

| v_true : value ttrue

| v_false : value tfalse.

Reserved Notation " t '⇒' t' " (at level 40).

Inductive step : tm → tm → Prop :=

| ST_IfTrue : ∀t1 t2,

tif ttrue t1 t2 ⇒ t1

| ST_IfFalse : ∀t1 t2,

tif tfalse t1 t2 ⇒ t2

| ST_If : ∀t1 t1' t2 t3,

t1 ⇒ t1' →

tif t1 t2 t3 ⇒ tif t1' t2 t3

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

#### Exercise: 1 star (smallstep_bools)

Which of the following propositions are provable? (This is just a thought exercise, but for an extra challenge feel free to prove your answers in Coq.)Definition bool_step_prop1 :=

tfalse ⇒ tfalse.

(* FILL IN HERE *)

Definition bool_step_prop2 :=

tif

ttrue

(tif ttrue ttrue ttrue)

(tif tfalse tfalse tfalse)

⇒

ttrue.

(* FILL IN HERE *)

Definition bool_step_prop3 :=

tif

(tif ttrue ttrue ttrue)

(tif ttrue ttrue ttrue)

tfalse

⇒

tif

ttrue

(tif ttrue ttrue ttrue)

tfalse.

(* FILL IN HERE *)

☐

#### Exercise: 3 stars, recommended (progress_bool)

Just as we proved a progress theorem for plus expressions, we can do so for boolean expressions, as well.Theorem strong_progress : ∀t,

value t ∨ (∃t', t ⇒ t').

Proof.

(* FILL IN HERE *) Admitted.

Theorem step_deterministic :

deterministic step.

Proof.

(* FILL IN HERE *) Admitted.

deterministic step.

Proof.

(* FILL IN HERE *) Admitted.

☐

Module Temp5.

#### Exercise: 2 stars (smallstep_bool_shortcut)

Suppose we want to add a "short circuit" to the step relation for boolean expressions, so that it can recognize when the then and else branches of a conditional are the same value (either ttrue or tfalse) and reduce the whole conditional to this value in a single step, even if the guard has not yet been reduced to a value. For example, we would like this proposition to be provable:
tif

(tif ttrue ttrue ttrue)

tfalse

tfalse

⇒

tfalse.

(tif ttrue ttrue ttrue)

tfalse

tfalse

⇒

tfalse.

Reserved Notation " t '⇒' t' " (at level 40).

Inductive step : tm → tm → Prop :=

| ST_IfTrue : ∀t1 t2,

tif ttrue t1 t2 ⇒ t1

| ST_IfFalse : ∀t1 t2,

tif tfalse t1 t2 ⇒ t2

| ST_If : ∀t1 t1' t2 t3,

t1 ⇒ t1' →

tif t1 t2 t3 ⇒ tif t1' t2 t3

(* FILL IN HERE *)

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

☐

Definition bool_step_prop4 :=

tif

(tif ttrue ttrue ttrue)

tfalse

tfalse

⇒

tfalse.

Example bool_step_prop4_holds :

bool_step_prop4.

Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 3 stars, optional (properties_of_altered_step)

It can be shown that the determinism and strong progress theorems for the step relation in the lecture notes also hold for the definition of step given above. After we add the clause ST_ShortCircuit...- Is the step relation still deterministic? Write yes or no and
briefly (1 sentence) explain your answer.

(* FILL IN HERE *)

- Does a strong progress theorem hold? Write yes or no and
briefly (1 sentence) explain your answer.

(* FILL IN HERE *)

- In general, is there any way we could cause strong progress to fail if we took away one or more constructors from the original step relation? Write yes or no and briefly (1 sentence) explain your answer.

☐

End Temp5.

End Temp4.

# Multi-Step Reduction

*single-step reduction*relation ⇒, which formalizes the individual steps of an

*abstract machine*for executing programs.

- First, we define a
*multi-step reduction relation*⇒*, which relates terms t and t' if t can reach t' by any number of single reduction steps (including zero steps!). - Then we define a "result" of a term t as a normal form that t can reach by multi-step reduction.

## Definitions

Inductive multi {X:Type} (R: relation X) : relation X :=

| multi_refl : ∀(x : X), multi R x x

| multi_step : ∀(x y z : X),

R x y →

multi R y z →

multi R x z.

The effect of this definition is that multi R relates two
elements x and y of X if either x = y or else there is
some (possibly empty) sequence z1, z2, ..., zn such that:

R x z1

R z1 z2

...

R zn y

R z1 z2

...

R zn y

Tactic Notation "multi_cases" tactic(first) ident(c) :=

first;

[ Case_aux c "multi_refl" | Case_aux c "multi_step" ].

first;

[ Case_aux c "multi_refl" | Case_aux c "multi_step" ].

Theorem multi_R : ∀(X:Type) (R:relation X) (x y : X),

R x y → (multi R) x y.

Proof.

intros X R x y H.

apply multi_step with y. apply H. apply multi_refl. Qed.

The crucial properties of the multi R relation are

- multi R is reflexive
- multi R is transitive
- multi R relates everything related by R

Theorem multi_trans :

∀(X:Type) (R: relation X) (x y z : X),

multi R x y →

multi R y z →

multi R x z.

Proof.

intros X R x y z G H.

multi_cases (induction G) Case.

Case "multi_refl". assumption.

Case "multi_step".

apply multi_step with y. assumption.

apply IHG. assumption. Qed.

We now write ⇒* for the multi step relation — i.e., the
relation that relates two terms t and t' if we can get from
t to t' using the step relation zero or more times.

Definition multistep := multi step.

Notation " t '⇒*' t' " := (multistep t t') (at level 40).

Lemma test_multistep_1:

P

(P (C 0) (C 3))

(P (C 2) (C 4))

⇒*

C ((0 + 3) + (2 + 4)).

Proof.

apply multi_step with

(P

(C (0 + 3))

(P (C 2) (C 4))).

apply ST_Plus1. apply ST_PlusConstConst.

apply multi_step with

(P

(C (0 + 3))

(C (2 + 4))).

apply ST_Plus2. apply v_const.

apply ST_PlusConstConst.

apply multi_R.

apply ST_PlusConstConst. Qed.

apply multi_step with

(P

(C (0 + 3))

(P (C 2) (C 4))).

apply ST_Plus1. apply ST_PlusConstConst.

apply multi_step with

(P

(C (0 + 3))

(C (2 + 4))).

apply ST_Plus2. apply v_const.

apply ST_PlusConstConst.

apply multi_R.

apply ST_PlusConstConst. Qed.

Here's an alternate proof that uses eapply to avoid explicitly
constructing all the intermediate terms.

Lemma test_multistep_1':

P

(P (C 0) (C 3))

(P (C 2) (C 4))

⇒*

C ((0 + 3) + (2 + 4)).

Proof.

eapply multi_step. apply ST_Plus1. apply ST_PlusConstConst.

eapply multi_step. apply ST_Plus2. apply v_const.

apply ST_PlusConstConst.

eapply multi_step. apply ST_PlusConstConst.

apply multi_refl. Qed.

eapply multi_step. apply ST_Plus1. apply ST_PlusConstConst.

eapply multi_step. apply ST_Plus2. apply v_const.

apply ST_PlusConstConst.

eapply multi_step. apply ST_PlusConstConst.

apply multi_refl. Qed.

Lemma test_multistep_2:

C 3 ⇒* C 3.

Proof.

(* FILL IN HERE *) Admitted.

C 3 ⇒* C 3.

Proof.

(* FILL IN HERE *) Admitted.

Lemma test_multistep_3:

P (C 0) (C 3)

⇒*

P (C 0) (C 3).

Proof.

(* FILL IN HERE *) Admitted.

P (C 0) (C 3)

⇒*

P (C 0) (C 3).

Proof.

(* FILL IN HERE *) Admitted.

Lemma test_multistep_4:

P

(C 0)

(P

(C 2)

(P (C 0) (C 3)))

⇒*

P

(C 0)

(C (2 + (0 + 3))).

Proof.

(* FILL IN HERE *) Admitted.

P

(C 0)

(P

(C 2)

(P (C 0) (C 3)))

⇒*

P

(C 0)

(C (2 + (0 + 3))).

Proof.

(* FILL IN HERE *) Admitted.

☐

## Normal Forms Again

Definition step_normal_form := normal_form step.

Definition normal_form_of (t t' : tm) :=

(t ⇒* t' ∧ step_normal_form t').

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."#### Exercise: 3 stars, optional (normal_forms_unique)

Theorem normal_forms_unique:

deterministic normal_form_of.

Proof.

unfold deterministic. unfold normal_form_of. intros x y1 y2 P1 P2.

inversion P1 as [P11 P12]; clear P1. inversion P2 as [P21 P22]; clear P2.

generalize dependent y2.

(* We recommend using this initial setup as-is! *)

(* FILL IN HERE *) Admitted.

deterministic normal_form_of.

Proof.

unfold deterministic. unfold normal_form_of. intros x y1 y2 P1 P2.

inversion P1 as [P11 P12]; clear P1. inversion P2 as [P21 P22]; clear P2.

generalize dependent y2.

(* We recommend using this initial setup as-is! *)

(* FILL IN HERE *) Admitted.

☐
Indeed, something stronger is true for this language (though not
for all languages): the reduction of

*any*term t will eventually reach a normal form — i.e., normal_form_of is a*total*function. Formally, we say the step relation is*normalizing*.Definition normalizing {X:Type} (R:relation X) :=

∀t, ∃t',

(multi R) t t' ∧ normal_form R t'.

To prove that step is normalizing, we need a couple of lemmas.
First, we observe that, if t reduces to t' in many steps, then
the same sequence of reduction steps within t is also possible
when t appears as the left-hand child of a P node, and
similarly when t appears as the right-hand child of a P
node whose left-hand child is a value.

Lemma multistep_congr_1 : ∀t1 t1' t2,

t1 ⇒* t1' →

P t1 t2 ⇒* P t1' t2.

Proof.

intros t1 t1' t2 H. multi_cases (induction H) Case.

Case "multi_refl". apply multi_refl.

Case "multi_step". apply multi_step with (P y t2).

apply ST_Plus1. apply H.

apply IHmulti. Qed.

intros t1 t1' t2 H. multi_cases (induction H) Case.

Case "multi_refl". apply multi_refl.

Case "multi_step". apply multi_step with (P y t2).

apply ST_Plus1. apply H.

apply IHmulti. Qed.

Lemma multistep_congr_2 : ∀t1 t2 t2',

value t1 →

t2 ⇒* t2' →

P t1 t2 ⇒* P t1 t2'.

Proof.

(* FILL IN HERE *) Admitted.

value t1 →

t2 ⇒* t2' →

P t1 t2 ⇒* P t1 t2'.

Proof.

(* FILL IN HERE *) Admitted.

☐

*Theorem*: The step function is normalizing — i.e., for every t there exists some t' such that t steps to t' and t' is a normal form.*Proof sketch*: By induction on terms. There are two cases to consider:- t = C n for some n. Here t doesn't take a step,
and we have t' = t. We can derive the left-hand side by
reflexivity and the right-hand side by observing (a) that values
are normal forms (by nf_same_as_value) and (b) that t is a
value (by v_const).
- t = P t1 t2 for some t1 and t2. By the IH, t1 and
t2 have normal forms t1' and t2'. Recall that normal
forms are values (by nf_same_as_value); we know that t1' =
C n1 and t2' = C n2, for some n1 and n2.
We can combine the ⇒* derivations for t1 and t2 to prove
that P t1 t2 reduces in many steps to C (n1 + n2).

Theorem step_normalizing :

normalizing step.

Proof.

unfold normalizing.

tm_cases (induction t) Case.

Case "C".

∃(C n).

split.

SCase "l". apply multi_refl.

SCase "r".

(* We can use rewrite with "iff" statements, not

just equalities: *)

rewrite nf_same_as_value. apply v_const.

Case "P".

inversion IHt1 as [t1' H1]; clear IHt1. inversion IHt2 as [t2' H2]; clear IHt2.

inversion H1 as [H11 H12]; clear H1. inversion H2 as [H21 H22]; clear H2.

rewrite nf_same_as_value in H12. rewrite nf_same_as_value in H22.

inversion H12 as [n1]. inversion H22 as [n2].

rewrite ← H in H11.

rewrite ← H0 in H21.

∃(C (n1 + n2)).

split.

SCase "l".

apply multi_trans with (P (C n1) t2).

apply multistep_congr_1. apply H11.

apply multi_trans with

(P (C n1) (C n2)).

apply multistep_congr_2. apply v_const. apply H21.

apply multi_R. apply ST_PlusConstConst.

SCase "r".

rewrite nf_same_as_value. apply v_const. Qed.

unfold normalizing.

tm_cases (induction t) Case.

Case "C".

∃(C n).

split.

SCase "l". apply multi_refl.

SCase "r".

(* We can use rewrite with "iff" statements, not

just equalities: *)

rewrite nf_same_as_value. apply v_const.

Case "P".

inversion IHt1 as [t1' H1]; clear IHt1. inversion IHt2 as [t2' H2]; clear IHt2.

inversion H1 as [H11 H12]; clear H1. inversion H2 as [H21 H22]; clear H2.

rewrite nf_same_as_value in H12. rewrite nf_same_as_value in H22.

inversion H12 as [n1]. inversion H22 as [n2].

rewrite ← H in H11.

rewrite ← H0 in H21.

∃(C (n1 + n2)).

split.

SCase "l".

apply multi_trans with (P (C n1) t2).

apply multistep_congr_1. apply H11.

apply multi_trans with

(P (C n1) (C n2)).

apply multistep_congr_2. apply v_const. apply H21.

apply multi_R. apply ST_PlusConstConst.

SCase "r".

rewrite nf_same_as_value. apply v_const. Qed.

## Equivalence of Big-Step and Small-Step Reduction

#### Exercise: 3 stars (eval__multistep)

Theorem eval__multistep : ∀t n,

t ⇓ n → t ⇒* C n.

t ⇓ n → t ⇒* C n.

The key idea behind the proof comes from the following picture:
To formalize this intuition, you'll need to use the congruence
lemmas from above (you might want to review them now, so that
you'll be able to recognize when they are useful), plus some basic
properties of ⇒*: that it is reflexive, transitive, and
includes ⇒.

P t1 t2 ⇒ (by ST_Plus1)

P t1' t2 ⇒ (by ST_Plus1)

P t1'' t2 ⇒ (by ST_Plus1)

...

P (C n1) t2 ⇒ (by ST_Plus2)

P (C n1) t2' ⇒ (by ST_Plus2)

P (C n1) t2'' ⇒ (by ST_Plus2)

...

P (C n1) (C n2) ⇒ (by ST_PlusConstConst)

C (n1 + n2)

That is, the multistep reduction of a term of the form P t1 t2
proceeds in three phases:
P t1' t2 ⇒ (by ST_Plus1)

P t1'' t2 ⇒ (by ST_Plus1)

...

P (C n1) t2 ⇒ (by ST_Plus2)

P (C n1) t2' ⇒ (by ST_Plus2)

P (C n1) t2'' ⇒ (by ST_Plus2)

...

P (C n1) (C n2) ⇒ (by ST_PlusConstConst)

C (n1 + n2)

- First, we use ST_Plus1 some number of times to reduce t1 to a normal form, which must (by nf_same_as_value) be a term of the form C n1 for some n1.
- Next, we use ST_Plus2 some number of times to reduce t2 to a normal form, which must again be a term of the form C n2 for some n2.
- Finally, we use ST_PlusConstConst one time to reduce P (C n1) (C n2) to C (n1 + n2).

Proof.

(* FILL IN HERE *) Admitted.

☐
(* FILL IN HERE *)

☐
For the other direction of the correspondence, we need one lemma,
which establishes a relation between single-step reduction and
big-step evaluation.

#### Exercise: 3 stars (eval__multistep_inf)

Write a detailed informal version of the proof of eval__multistep.☐

#### Exercise: 3 stars (step__eval)

Lemma step__eval : ∀t t' n,

t ⇒ t' →

t' ⇓ n →

t ⇓ n.

Proof.

intros t t' n Hs. generalize dependent n.

(* FILL IN HERE *) Admitted.

t ⇒ t' →

t' ⇓ n →

t ⇓ n.

Proof.

intros t t' n Hs. generalize dependent n.

(* FILL IN HERE *) Admitted.

☐
The main theorem is now straightforward to prove, once it is
stated correctly. The proof proceeds by induction on the
multipstep reduction sequence that is buried in the hypothesis
normal_form_of t v. Make sure you understand the statement before you start to
work on the proof.

#### Exercise: 3 stars (multistep__eval)

Theorem multistep__eval : ∀t v,

normal_form_of t v → ∃n, v = C n ∧ t ⇓ n.

Proof.

(* FILL IN HERE *) Admitted.

normal_form_of t v → ∃n, v = C n ∧ t ⇓ n.

Proof.

(* FILL IN HERE *) Admitted.

☐

## Additional Exercises

#### Exercise: 4 stars (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 : ∀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 : ∀n1 n2,

P (C n1) (C n2) ⇒ C (n1 + n2)

| ST_Plus1 : ∀t1 t1' t2,

t1 ⇒ t1' →

P t1 t2 ⇒ P t1' t2

| ST_Plus2 : ∀v1 t2 t2',

value v1 →

t2 ⇒ t2' →

P v1 t2 ⇒ P v1 t2'

| ST_IfTrue : ∀t1 t2,

tif ttrue t1 t2 ⇒ t1

| ST_IfFalse : ∀t1 t2,

tif tfalse t1 t2 ⇒ t2

| ST_If : ∀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" ].

Earlier, we separately proved for both plus- and if-expressions...

- that the step relation was deterministic, and
- a strong progress lemma, stating that every term is either a value or can take a step.

(* FILL IN HERE *)

☐

End Combined.

# Small-Step Imp

Inductive aval : aexp → Prop :=

av_num : ∀n, aval (ANum n).

We are not actually going to bother to define boolean
values — they aren't needed in the definition of ⇒b
below (why?), though they might be if our language were a bit
larger (why?).

Reserved Notation " t '/' st '⇒a' t' " (at level 40, st at level 39).

Inductive astep : state → aexp → aexp → Prop :=

| AS_Id : ∀st i,

AId i / st ⇒a ANum (st i)

| AS_Plus : ∀st n1 n2,

APlus (ANum n1) (ANum n2) / st ⇒a ANum (n1 + n2)

| AS_Plus1 : ∀st a1 a1' a2,

a1 / st ⇒a a1' →

(APlus a1 a2) / st ⇒a (APlus a1' a2)

| AS_Plus2 : ∀st v1 a2 a2',

aval v1 →

a2 / st ⇒a a2' →

(APlus v1 a2) / st ⇒a (APlus v1 a2')

| AS_Minus : ∀st n1 n2,

(AMinus (ANum n1) (ANum n2)) / st ⇒a (ANum (minus n1 n2))

| AS_Minus1 : ∀st a1 a1' a2,

a1 / st ⇒a a1' →

(AMinus a1 a2) / st ⇒a (AMinus a1' a2)

| AS_Minus2 : ∀st v1 a2 a2',

aval v1 →

a2 / st ⇒a a2' →

(AMinus v1 a2) / st ⇒a (AMinus v1 a2')

| AS_Mult : ∀st n1 n2,

(AMult (ANum n1) (ANum n2)) / st ⇒a (ANum (mult n1 n2))

| AS_Mult1 : ∀st a1 a1' a2,

a1 / st ⇒a a1' →

(AMult (a1) (a2)) / st ⇒a (AMult (a1') (a2))

| AS_Mult2 : ∀st v1 a2 a2',

aval v1 →

a2 / st ⇒a a2' →

(AMult v1 a2) / st ⇒a (AMult v1 a2')

where " t '/' st '⇒a' t' " := (astep st t t').

Reserved Notation " t '/' st '⇒b' t' " (at level 40, st at level 39).

Inductive bstep : state → bexp → bexp → Prop :=

| BS_Eq : ∀st n1 n2,

(BEq (ANum n1) (ANum n2)) / st ⇒b

(if (beq_nat n1 n2) then BTrue else BFalse)

| BS_Eq1 : ∀st a1 a1' a2,

a1 / st ⇒a a1' →

(BEq a1 a2) / st ⇒b (BEq a1' a2)

| BS_Eq2 : ∀st v1 a2 a2',

aval v1 →

a2 / st ⇒a a2' →

(BEq v1 a2) / st ⇒b (BEq v1 a2')

| BS_LtEq : ∀st n1 n2,

(BLe (ANum n1) (ANum n2)) / st ⇒b

(if (ble_nat n1 n2) then BTrue else BFalse)

| BS_LtEq1 : ∀st a1 a1' a2,

a1 / st ⇒a a1' →

(BLe a1 a2) / st ⇒b (BLe a1' a2)

| BS_LtEq2 : ∀st v1 a2 a2',

aval v1 →

a2 / st ⇒a a2' →

(BLe v1 a2) / st ⇒b (BLe v1 (a2'))

| BS_NotTrue : ∀st,

(BNot BTrue) / st ⇒b BFalse

| BS_NotFalse : ∀st,

(BNot BFalse) / st ⇒b BTrue

| BS_NotStep : ∀st b1 b1',

b1 / st ⇒b b1' →

(BNot b1) / st ⇒b (BNot b1')

| BS_AndTrueTrue : ∀st,

(BAnd BTrue BTrue) / st ⇒b BTrue

| BS_AndTrueFalse : ∀st,

(BAnd BTrue BFalse) / st ⇒b BFalse

| BS_AndFalse : ∀st b2,

(BAnd BFalse b2) / st ⇒b BFalse

| BS_AndTrueStep : ∀st b2 b2',

b2 / st ⇒b b2' →

(BAnd BTrue b2) / st ⇒b (BAnd BTrue b2')

| BS_AndStep : ∀st b1 b1' b2,

b1 / st ⇒b b1' →

(BAnd b1 b2) / st ⇒b (BAnd b1' b2)

where " t '/' st '⇒b' t' " := (bstep st t t').

The semantics of commands is the interesting part. We need two
small tricks to make it work:
(There are other ways of achieving the effect of the latter
trick, but they all share the feature that the original WHILE
command needs to be saved somewhere while a single copy of the loop
body is being evaluated.)

- We use SKIP as a "command value" — i.e., a command that
has reached a normal form.
- An assignment command reduces to SKIP (and an updated
state).
- The sequencing command waits until its left-hand
subcommand has reduced to SKIP, then throws it away so
that reduction can continue with the right-hand
subcommand.

- An assignment command reduces to SKIP (and an updated
state).
- We reduce a WHILE command by transforming it into a conditional followed by the same WHILE.

Reserved Notation " t '/' st '⇒' t' '/' st' "

(at level 40, st at level 39, t' at level 39).

Inductive cstep : (com * state) → (com * state) → Prop :=

| CS_AssStep : ∀st i a a',

a / st ⇒a a' →

(i ::= a) / st ⇒ (i ::= a') / st

| CS_Ass : ∀st i n,

(i ::= (ANum n)) / st ⇒ SKIP / (update st i n)

| CS_SeqStep : ∀st c1 c1' st' c2,

c1 / st ⇒ c1' / st' →

(c1 ; c2) / st ⇒ (c1' ; c2) / st'

| CS_SeqFinish : ∀st c2,

(SKIP ; c2) / st ⇒ c2 / st

| CS_IfTrue : ∀st c1 c2,

IFB BTrue THEN c1 ELSE c2 FI / st ⇒ c1 / st

| CS_IfFalse : ∀st c1 c2,

IFB BFalse THEN c1 ELSE c2 FI / st ⇒ c2 / st

| CS_IfStep : ∀st b b' c1 c2,

b / st ⇒b b' →

IFB b THEN c1 ELSE c2 FI / st ⇒ (IFB b' THEN c1 ELSE c2 FI) / st

| CS_While : ∀st b c1,

(WHILE b DO c1 END) / st

⇒ (IFB b THEN (c1; (WHILE b DO c1 END)) ELSE SKIP FI) / st

where " t '/' st '⇒' t' '/' st' " := (cstep (t,st) (t',st')).

# Concurrent Imp (Optional)

Module CImp.

Inductive com : Type :=

| CSkip : com

| CAss : id → aexp → com

| CSeq : com → com → com

| CIf : bexp → com → com → com

| CWhile : bexp → com → com

(* New: *)

| CPar : com → com → com.

Tactic Notation "com_cases" tactic(first) ident(c) :=

first;

[ Case_aux c "SKIP" | Case_aux c "::=" | Case_aux c ";"

| Case_aux c "IFB" | Case_aux c "WHILE" | Case_aux c "PAR" ].

Notation "'SKIP'" :=

CSkip.

Notation "l '::=' a" :=

(CAss l a) (at level 60).

Notation "c1 ; c2" :=

(CSeq c1 c2) (at level 80, right associativity).

Notation "'WHILE' b 'DO' c 'END'" :=

(CWhile b c) (at level 80, right associativity).

Notation "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" :=

(CIf e1 e2 e3) (at level 80, right associativity).

Notation "'PAR' c1 'WITH' c2 'END'" :=

(CPar c1 c2) (at level 80, right associativity).

Inductive cstep : (com * state) → (com * state) → Prop :=

(* Old part *)

| CS_AssStep : ∀st i a a',

a / st ⇒a a' →

(i ::= a) / st ⇒ (i ::= a') / st

| CS_Ass : ∀st i n,

(i ::= (ANum n)) / st ⇒ SKIP / (update st i n)

| CS_SeqStep : ∀st c1 c1' st' c2,

c1 / st ⇒ c1' / st' →

(c1 ; c2) / st ⇒ (c1' ; c2) / st'

| CS_SeqFinish : ∀st c2,

(SKIP ; c2) / st ⇒ c2 / st

| CS_IfTrue : ∀st c1 c2,

(IFB BTrue THEN c1 ELSE c2 FI) / st ⇒ c1 / st

| CS_IfFalse : ∀st c1 c2,

(IFB BFalse THEN c1 ELSE c2 FI) / st ⇒ c2 / st

| CS_IfStep : ∀st b b' c1 c2,

b /st ⇒b b' →

(IFB b THEN c1 ELSE c2 FI) / st ⇒ (IFB b' THEN c1 ELSE c2 FI) / st

| CS_While : ∀st b c1,

(WHILE b DO c1 END) / st ⇒

(IFB b THEN (c1; (WHILE b DO c1 END)) ELSE SKIP FI) / st

(* New part: *)

| CS_Par1 : ∀st c1 c1' c2 st',

c1 / st ⇒ c1' / st' →

(PAR c1 WITH c2 END) / st ⇒ (PAR c1' WITH c2 END) / st'

| CS_Par2 : ∀st c1 c2 c2' st',

c2 / st ⇒ c2' / st' →

(PAR c1 WITH c2 END) / st ⇒ (PAR c1 WITH c2' END) / st'

| CS_ParDone : ∀st,

(PAR SKIP WITH SKIP END) / st ⇒ SKIP / st

where " t '/' st '⇒' t' '/' st' " := (cstep (t,st) (t',st')).

Definition cmultistep := multi cstep.

Notation " t '/' st '⇒*' t' '/' st' " :=

(multi cstep (t,st) (t',st'))

(at level 40, st at level 39, t' at level 39).

Among the many interesting properties of this language is the fact
that the following program can terminate with the variable X set
to any value...

Definition par_loop : com :=

PAR

Y ::= ANum 1

WITH

WHILE BEq (AId Y) (ANum 0) DO

X ::= APlus (AId X) (ANum 1)

END

END.

In particular, it can terminate with X set to 0:

Example par_loop_example_0:

∃st',

par_loop / empty_state ⇒* SKIP / st'

∧ st' X = 0.

Proof.

eapply ex_intro. split.

unfold par_loop.

eapply multi_step. apply CS_Par1.

apply CS_Ass.

eapply multi_step. apply CS_Par2. apply CS_While.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq1. apply AS_Id.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq. simpl.

eapply multi_step. apply CS_Par2. apply CS_IfFalse.

eapply multi_step. apply CS_ParDone.

eapply multi_refl.

reflexivity. Qed.

eapply ex_intro. split.

unfold par_loop.

eapply multi_step. apply CS_Par1.

apply CS_Ass.

eapply multi_step. apply CS_Par2. apply CS_While.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq1. apply AS_Id.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq. simpl.

eapply multi_step. apply CS_Par2. apply CS_IfFalse.

eapply multi_step. apply CS_ParDone.

eapply multi_refl.

reflexivity. Qed.

It can also terminate with X set to 2:

Example par_loop_example_2:

∃st',

par_loop / empty_state ⇒* SKIP / st'

∧ st' X = 2.

Proof.

eapply ex_intro. split.

eapply multi_step. apply CS_Par2. apply CS_While.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq1. apply AS_Id.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq. simpl.

eapply multi_step. apply CS_Par2. apply CS_IfTrue.

eapply multi_step. apply CS_Par2. apply CS_SeqStep.

apply CS_AssStep. apply AS_Plus1. apply AS_Id.

eapply multi_step. apply CS_Par2. apply CS_SeqStep.

apply CS_AssStep. apply AS_Plus.

eapply multi_step. apply CS_Par2. apply CS_SeqStep.

apply CS_Ass.

eapply multi_step. apply CS_Par2. apply CS_SeqFinish.

eapply multi_step. apply CS_Par2. apply CS_While.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq1. apply AS_Id.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq. simpl.

eapply multi_step. apply CS_Par2. apply CS_IfTrue.

eapply multi_step. apply CS_Par2. apply CS_SeqStep.

apply CS_AssStep. apply AS_Plus1. apply AS_Id.

eapply multi_step. apply CS_Par2. apply CS_SeqStep.

apply CS_AssStep. apply AS_Plus.

eapply multi_step. apply CS_Par2. apply CS_SeqStep.

apply CS_Ass.

eapply multi_step. apply CS_Par1. apply CS_Ass.

eapply multi_step. apply CS_Par2. apply CS_SeqFinish.

eapply multi_step. apply CS_Par2. apply CS_While.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq1. apply AS_Id.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq. simpl.

eapply multi_step. apply CS_Par2. apply CS_IfFalse.

eapply multi_step. apply CS_ParDone.

eapply multi_refl.

reflexivity. Qed.

eapply ex_intro. split.

eapply multi_step. apply CS_Par2. apply CS_While.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq1. apply AS_Id.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq. simpl.

eapply multi_step. apply CS_Par2. apply CS_IfTrue.

eapply multi_step. apply CS_Par2. apply CS_SeqStep.

apply CS_AssStep. apply AS_Plus1. apply AS_Id.

eapply multi_step. apply CS_Par2. apply CS_SeqStep.

apply CS_AssStep. apply AS_Plus.

eapply multi_step. apply CS_Par2. apply CS_SeqStep.

apply CS_Ass.

eapply multi_step. apply CS_Par2. apply CS_SeqFinish.

eapply multi_step. apply CS_Par2. apply CS_While.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq1. apply AS_Id.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq. simpl.

eapply multi_step. apply CS_Par2. apply CS_IfTrue.

eapply multi_step. apply CS_Par2. apply CS_SeqStep.

apply CS_AssStep. apply AS_Plus1. apply AS_Id.

eapply multi_step. apply CS_Par2. apply CS_SeqStep.

apply CS_AssStep. apply AS_Plus.

eapply multi_step. apply CS_Par2. apply CS_SeqStep.

apply CS_Ass.

eapply multi_step. apply CS_Par1. apply CS_Ass.

eapply multi_step. apply CS_Par2. apply CS_SeqFinish.

eapply multi_step. apply CS_Par2. apply CS_While.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq1. apply AS_Id.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq. simpl.

eapply multi_step. apply CS_Par2. apply CS_IfFalse.

eapply multi_step. apply CS_ParDone.

eapply multi_refl.

reflexivity. Qed.

Lemma par_body_n__Sn : ∀n st,

st X = n ∧ st Y = 0 →

par_loop / st ⇒* par_loop / (update st X (S n)).

Proof.

(* FILL IN HERE *) Admitted.

st X = n ∧ st Y = 0 →

par_loop / st ⇒* par_loop / (update st X (S n)).

Proof.

(* FILL IN HERE *) Admitted.

Lemma par_body_n : ∀n st,

st X = 0 ∧ st Y = 0 →

∃st',

par_loop / st ⇒* par_loop / st' ∧ st' X = n ∧ st' Y = 0.

Proof.

(* FILL IN HERE *) Admitted.

st X = 0 ∧ st Y = 0 →

∃st',

par_loop / st ⇒* par_loop / st' ∧ st' X = n ∧ st' Y = 0.

Proof.

(* FILL IN HERE *) Admitted.

... the above loop can exit with X having any value
whatsoever.

Theorem par_loop_any_X:

∀n, ∃st',

par_loop / empty_state ⇒* SKIP / st'

∧ st' X = n.

Proof.

intros n.

destruct (par_body_n n empty_state).

split; unfold update; reflexivity.

rename x into st.

inversion H as [H' [HX HY]]; clear H.

∃(update st Y 1). split.

eapply multi_trans with (par_loop,st). apply H'.

eapply multi_step. apply CS_Par1. apply CS_Ass.

eapply multi_step. apply CS_Par2. apply CS_While.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq1. apply AS_Id. rewrite update_eq.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq. simpl.

eapply multi_step. apply CS_Par2. apply CS_IfFalse.

eapply multi_step. apply CS_ParDone.

apply multi_refl.

rewrite update_neq. assumption. reflexivity.

Qed.

intros n.

destruct (par_body_n n empty_state).

split; unfold update; reflexivity.

rename x into st.

inversion H as [H' [HX HY]]; clear H.

∃(update st Y 1). split.

eapply multi_trans with (par_loop,st). apply H'.

eapply multi_step. apply CS_Par1. apply CS_Ass.

eapply multi_step. apply CS_Par2. apply CS_While.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq1. apply AS_Id. rewrite update_eq.

eapply multi_step. apply CS_Par2. apply CS_IfStep.

apply BS_Eq. simpl.

eapply multi_step. apply CS_Par2. apply CS_IfFalse.

eapply multi_step. apply CS_ParDone.

apply multi_refl.

rewrite update_neq. assumption. reflexivity.

Qed.

End CImp.