# File Smallstep

Set Warnings "-notation-overridden,-parsing".

Require Import mathcomp.ssreflect.all_ssreflect.

Set Implicit Arguments.

Unset Strict Implicit.

Unset Printing Implicit Defensive.

Set Bullet Behavior "Strict Subproofs".

From Coq Require Import Strings.String.

The evaluators we have seen so far (for aexps, bexps,
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 it, called it
Another shortcoming of the big-step style is more technical, but
critical in many situations. Suppose we want to define a variant
of Imp where variables could hold
A much more natural approach is simply to say that the behavior of
an expression like 2+nil is
Now, however, we encounter a serious deficiency. In this
language, a command might fail to map a given starting state to
any ending state for
These two outcomes -- nontermination vs. getting stuck in an
erroneous configuration -- should not be confused. In particular, we
want to
So, for lots of reasons, we'd often like to have a finer-grained
way of defining and reasoning about program behaviors. This is
the topic of the present chapter. Our goal is to 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.*either*numbers*or*lists of numbers. In the syntax of this extended language, it will be possible to write strange expressions like 2 + nil, and our semantics for arithmetic expressions will then need to say something about how such expressions behave. One possibility is to maintain the convention that every arithmetic expression evaluates to some number by choosing some way of viewing a list as a number -- e.g., by specifying that a list should be interpreted as 0 when it occurs in a context expecting a number. But this is really a bit of a hack.*undefined*-- i.e., it doesn't evaluate to any result at all. And we can easily do this: we just have to formulate aeval and beval as Inductive propositions rather than Fixpoints, so that we can make them partial functions instead of total ones.*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 adding a number to a list, so that none of the evaluation rules can be applied.*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*typechecking*to the language. As a first step, we need a way of presenting the semantics that allows us to distinguish nontermination from erroneous "stuck states."# A Toy Language

Inductive tm : Type :=

| C : nat -> tm

| P : tm -> tm -> tm.

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

Fixpoint evalF (t : tm) : nat :=

match t with

| C n => n

| P a1 a2 => evalF a1 + evalF a2

end.

Here is the same evaluator, written in exactly the same
style, but formulated as an inductively defined relation.
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 ==> n1 + n2

Reserved Notation " t '==>e' n " (at level 50, left associativity).

Inductive eval : tm -> nat -> Prop :=

| E_Const : forall n,

C n ==>e n

| E_Plus : forall t1 t2 n1 n2,

t1 ==>e n1 ->

t2 ==>e n2 ->

P t1 t2 ==>e (n1 + n2)

where " t '==>e' n " := (eval t n).

Module SimpleArith1.

Inductive eval : tm -> nat -> Prop :=

| E_Const : forall n,

C n ==>e n

| E_Plus : forall t1 t2 n1 n2,

t1 ==>e n1 ->

t2 ==>e n2 ->

P t1 t2 ==>e (n1 + n2)

where " t '==>e' n " := (eval t n).

Module SimpleArith1.

Now, here is the corresponding

*small-step*evaluation relation.------------------------------- (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 '-->s' t' " (at level 40).

Inductive step : tm -> tm -> Prop :=

| ST_PlusConstConst : forall n1 n2,

P (C n1) (C n2) -->s C (n1 + n2)

| ST_Plus1 : forall t1 t1' t2,

t1 -->s t1' ->

P t1 t2 -->s P t1' t2

| ST_Plus2 : forall n1 t2 t2',

t2 -->s t2' ->

P (C n1) t2 -->s P (C n1) t2'

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

Hint Constructors step.

Things to notice:
Let's pause and check a couple of examples of reasoning with
the step relation...
If t1 can take a step to t1', then P t1 t2 steps
to P 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))

-->s

P

(C (0 + 3))

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

Proof.

auto.

Qed.

End SimpleArith1.

# Relations

*binary 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 reduction relation, -->, and its multi-step
variant, -->* (defined below), but there are many other
examples -- e.g., 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.
One simple property of the --> relation is that, like the
big-step evaluation relation for Imp, it is
Formally:

*deterministic*.*Theorem*: For each t, there is at most one t' such that t steps to t' (t --> t' is provable).*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 the last rule 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 t11 t12 and the form C n. ☐

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

forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2.

Module SimpleArith2.

Import SimpleArith1.

Theorem step_deterministic:

deterministic step.

Proof.

rewrite /deterministic.

move=> x y1 y2 Hy1 Hy2.

elim: Hy1 y2 Hy2.

- move=> n1 n2 y2 Hy2.

inversion Hy2; subst.

+ done.

+ inversion H2.

+ inversion H2.

- move=> t1 t1' t2 t1s IH y2 Hy2.

inversion Hy2; subst. inversion t1s.

rewrite (IH t1'0 H2) //=.

inversion t1s.

- move=> n1 t2 t2' t2s IH y2 Hy2.

inversion Hy2; subst; move=> {Hy2}.

+ inversion t2s.

+ inversion H2.

+ rewrite (IH t2'0 H2) //=.

Qed.

End SimpleArith2.

## 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 : forall n, value (C n).

Hint Constructors value.

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 brevity.)
Here are the formal rules:

------------------------------- (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 '-->s' t' " (at level 40).

Inductive step : tm -> tm -> Prop :=

| ST_PlusConstConst : forall n1 n2,

P (C n1) (C n2)

-->s C (n1 + n2)

| ST_Plus1 : forall t1 t1' t2,

t1 -->s t1' ->

P t1 t2 -->s P t1' t2

| ST_Plus2 : forall v1 t2 t2',

value v1 ->

t2 -->s t2' ->

P v1 t2 -->s P v1 t2'

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

Hint Constructors step.

## Strong Progress and Normal Forms

*Theorem*(

*Strong Progress*): If t is a term, then either t is a value or else 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 either is 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 : forall t,

value t \/ (exists t', t -->s t').

Proof.

elim.

- by left.

- right. case H => [v1 | [t1 t1s]]. case H0 => [v2 | [t2 t2s]].

+ inversion v1. inversion v2. subst.

by exists (C (n + n0)).

+ by exists (P t t2); constructor.

+ by exists (P t1 t0); constructor.

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
To state this observation formally, let's begin by giving a name
to terms that cannot make progress. We'll call them

*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 just*progress*.)*cannot*make progress in this sense.*normal forms*.Definition normal_form {X : Type} (R : relation X) (t : X) : Prop :=

~ exists t', R t t'.

Note that this definition 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 : forall v,

value v -> normal_form step v.

Proof.

rewrite /normal_form => v H.

inversion H.

move=> contra.

inversion contra.

inversion H1.

Qed.

Lemma nf_is_value : forall t,

normal_form step t -> value t.

Proof. rewrite /normal_form => t H.

have [G | G]: value t \/ exists t', t -->s t' by apply: strong_progress.

- apply: G.

- exfalso. by apply: H.

Qed.

Corollary nf_same_as_value : forall t,

normal_form step t <-> value t.

Proof.

split.

- apply: nf_is_value.

- apply: value_is_nf.

Qed.

Why is this interesting?
Because value is a syntactic concept -- it is 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, we could easily have written the definitions incorrectly
so that they would

*not*coincide.# 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 (including zero) of single reduction steps. - Then we define a "result" of a term t as a normal form that t can reach by multi-step reduction.

*multi-step closure of R*as follows.

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

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

| multi_step : forall (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 if
Thus, if R describes a single-step of computation, then z1 ... zn
is the sequence of intermediate steps of computation between x and
y.
We write -->* for the multi step relation on terms.

- x = y, or
- R x y, or
- there is some nonempty sequence z1, z2, ..., zn such that

R x z1 R z1 z2 ... R zn y.

Notation " t '-->*' t' " := (multi step t t') (at level 40).

The relation multi R has several crucial properties.
First, it is obviously
Second, it contains R -- that is, single-step executions are a
particular case of multi-step executions. (It is this fact that
justifies the word "closure" in the term "multi-step closure of
R.")

*reflexive*(that is, forall x, multi R x x). In the case of the -->* (i.e., multi step) relation, the intuition is that a term can execute to itself by taking zero steps of execution.Theorem multi_R : forall (X : Type) (R : relation X) (x y : X),

R x y -> (multi R) x y.

Proof.

move=> X R x y H.

apply: multi_step. apply: H. apply: multi_refl.

Qed.

Third, multi R is

*transitive*.Theorem multi_trans :

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

multi R x y ->

multi R y z ->

multi R x z.

Proof.

move=> X R x y z G H.

move: G z H.

elim.

- done.

- move=> x0 y0 z G IH z0 H H'.

apply: multi_step. apply: G. apply: z0. done.

Qed.

In particular, for the multi step relation on terms, if
t1 -->* t2 and t2 -->* t3, then t1 -->* t3.

Lemma test_multistep_1:

P

(P (C 0) (C 3))

(P (C 2) (C 4))

-->*

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

Proof.

apply: multi_step.

apply: ST_Plus1.

apply: ST_PlusConstConst.

apply: multi_step.

apply: ST_Plus2.

apply: v_const.

apply: ST_PlusConstConst.

apply: multi_R.

apply: ST_PlusConstConst.

Qed.

## 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
Indeed, something stronger is true for this language (though not
for all languages): the reduction of

*the*normal form of t."*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) :=

forall t, exists 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 : forall t1 t1' t2,

t1 -->* t1' ->

P t1 t2 -->* P t1' t2.

Proof.

move=> t1 t1' t2.

elim.

- move=> x. apply: multi_refl.

- move=> x y z xS yS H. apply: multi_step.

+ apply: ST_Plus1. apply: xS.

+ apply: H.

Qed.

Lemma multistep_congr_2 : forall t1 t2 t2',

value t1 ->

t2 -->* t2' ->

P t1 t2 -->* P t1 t2'.

Proof.

move=> t1 t1' t2 v.

elim.

- move=> x. apply: multi_refl.

- move=> x y z xS yS IH.

apply: multi_step. apply: ST_Plus2.

exact: v. exact: xS. exact: IH.

Qed.

With these lemmas in hand, the main proof is a straightforward
induction.

*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 using multi_congr_1 and
multi_congr_2 to prove that P t1 t2 reduces in many steps to
C (n1 + n2).

Theorem step_normalizing :

normalizing step.

Proof.

Admitted.

## Equivalence of Big-Step and Small-Step

# Small-Step Imp

Definition state := string -> nat.

Inductive aexp : Type :=

| ANum (n : nat)

| AId (x : string)

| APlus (a1 a2 : aexp)

| AMinus (a1 a2 : aexp)

| AMult (a1 a2 : aexp).

Inductive bexp : Type :=

| BTrue

| BFalse

| BEq (a1 a2 : aexp)

| BLe (a1 a2 : aexp)

| BNot (b : bexp)

| BAnd (b1 b2 : bexp).

Inductive com : Type :=

| CSkip

| CAss (x : string) (a : aexp)

| CSeq (c1 c2 : com)

| CIf (b : bexp) (c1 c2 : com)

| CWhile (b : bexp) (c : com).

The small-step reduction relations for arithmetic and
boolean expressions are straightforward extensions of the tiny
language we've been working up to now. To make them easier to
read, we introduce the symbolic notations -->a and -->b for
the arithmetic and boolean step relations.

Inductive aval : aexp -> Prop :=

| av_num : forall n, aval (ANum n).

We are not actually going to bother to define boolean
values, since 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 : forall st i,

AId i / st -->a ANum (st i)

| AS_Plus1 : forall st a1 a1' a2,

a1 / st -->a a1' ->

(APlus a1 a2) / st -->a (APlus a1' a2)

| AS_Plus2 : forall st v1 a2 a2',

aval v1 ->

a2 / st -->a a2' ->

(APlus v1 a2) / st -->a (APlus v1 a2')

| AS_Plus : forall st n1 n2,

APlus (ANum n1) (ANum n2) / st -->a ANum (n1 + n2)

| AS_Minus1 : forall st a1 a1' a2,

a1 / st -->a a1' ->

(AMinus a1 a2) / st -->a (AMinus a1' a2)

| AS_Minus2 : forall st v1 a2 a2',

aval v1 ->

a2 / st -->a a2' ->

(AMinus v1 a2) / st -->a (AMinus v1 a2')

| AS_Minus : forall st n1 n2,

(AMinus (ANum n1) (ANum n2)) / st -->a (ANum (minus n1 n2))

| AS_Mult1 : forall st a1 a1' a2,

a1 / st -->a a1' ->

(AMult a1 a2) / st -->a (AMult a1' a2)

| AS_Mult2 : forall st v1 a2 a2',

aval v1 ->

a2 / st -->a a2' ->

(AMult v1 a2) / st -->a (AMult v1 a2')

| AS_Mult : forall st n1 n2,

(AMult (ANum n1) (ANum n2)) / st -->a (ANum (mult n1 n2))

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_Eq1 : forall st a1 a1' a2,

a1 / st -->a a1' ->

(BEq a1 a2) / st -->b (BEq a1' a2)

| BS_Eq2 : forall st v1 a2 a2',

aval v1 ->

a2 / st -->a a2' ->

(BEq v1 a2) / st -->b (BEq v1 a2')

| BS_Eq : forall st n1 n2,

(BEq (ANum n1) (ANum n2)) / st -->b

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

| BS_LtEq1 : forall st a1 a1' a2,

a1 / st -->a a1' ->

(BLe a1 a2) / st -->b (BLe a1' a2)

| BS_LtEq2 : forall st v1 a2 a2',

aval v1 ->

a2 / st -->a a2' ->

(BLe v1 a2) / st -->b (BLe v1 a2')

| BS_LtEq : forall st n1 n2,

(BLe (ANum n1) (ANum n2)) / st -->b

(if (n1 <= n2) then BTrue else BFalse)

| BS_NotStep : forall st b1 b1',

b1 / st -->b b1' ->

(BNot b1) / st -->b (BNot b1')

| BS_NotTrue : forall st,

(BNot BTrue) / st -->b BFalse

| BS_NotFalse : forall st,

(BNot BFalse) / st -->b BTrue

| BS_AndTrueStep : forall st b2 b2',

b2 / st -->b b2' ->

(BAnd BTrue b2) / st -->b (BAnd BTrue b2')

| BS_AndStep : forall st b1 b1' b2,

b1 / st -->b b1' ->

(BAnd b1 b2) / st -->b (BAnd b1' b2)

| BS_AndTrueTrue : forall st,

(BAnd BTrue BTrue) / st -->b BTrue

| BS_AndTrueFalse : forall st,

(BAnd BTrue BFalse) / st -->b BFalse

| BS_AndFalse : forall st b2,

(BAnd BFalse b2) / st -->b BFalse

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 reduced.)

- 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).

We'll also re-define the notational shorthand introduced previously for Imp.

Bind Scope imp_scope with aexp.

Bind Scope imp_scope with bexp.

Delimit Scope imp_scope with imp.

Coercion AId : string >-> aexp.

Coercion ANum : nat >-> aexp.

Notation "x + y" := (APlus x y) (at level 50, left associativity) : imp_scope.

Notation "x - y" := (AMinus x y) (at level 50, left associativity) : imp_scope.

Notation "x * y" := (AMult x y) (at level 40, left associativity) : imp_scope.

Notation "x <= y" := (BLe x y) (at level 70, no associativity) : imp_scope.

Notation "x = y" := (BEq x y) (at level 70, no associativity) : imp_scope.

Notation "x && y" := (BAnd x y) (at level 40, left associativity) : imp_scope.

Notation "'~' b" := (BNot b) (at level 75, right associativity) : imp_scope.

Bind Scope imp_scope with com.

Notation "'SKIP'" :=

CSkip : imp_scope.

Notation "x '::=' a" :=

(CAss x a) (at level 60) : imp_scope.

Notation "c1 ;; c2" :=

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

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

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

Notation "'TEST' c1 'THEN' c2 'ELSE' c3 'FI'" :=

(CIf c1 c2 c3) (at level 80, right associativity) : imp_scope.

Definition empty_st := fun (_ : string) => 0.

Definition extend_st a x (st : state) :=

(fun (a' : string) => if String.eqb a a' then x

else st a').

Notation "a '!->' x" := (extend_st a x empty_st) (at level 100).

Notation "a '!->' x ';' s" := (extend_st a x s)

(at level 100, x at next level, right associativity).

Open Scope imp_scope.

Inductive cstep : (com * state) -> (com * state) -> Prop :=

| CS_AssStep : forall st i a a',

a / st -->a a' ->

(i ::= a) / st --> (i ::= a') / st

| CS_Ass : forall st i n,

(i ::= (ANum n)) / st --> SKIP / (i !-> n ; st)

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

c1 / st --> c1' / st' ->

(c1 ;; c2) / st --> (c1' ;; c2) / st'

| CS_SeqFinish : forall st c2,

(SKIP ;; c2) / st --> c2 / st

| CS_IfStep : forall st b b' c1 c2,

b / st -->b b' ->

TEST b THEN c1 ELSE c2 FI / st

-->

(TEST b' THEN c1 ELSE c2 FI) / st

| CS_IfTrue : forall st c1 c2,

TEST BTrue THEN c1 ELSE c2 FI / st --> c1 / st

| CS_IfFalse : forall st c1 c2,

TEST BFalse THEN c1 ELSE c2 FI / st --> c2 / st

| CS_While : forall st b c1,

WHILE b DO c1 END / st

-->

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

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

Close Scope imp_scope.

Bind Scope imp_scope with bexp.

Delimit Scope imp_scope with imp.

Coercion AId : string >-> aexp.

Coercion ANum : nat >-> aexp.

Notation "x + y" := (APlus x y) (at level 50, left associativity) : imp_scope.

Notation "x - y" := (AMinus x y) (at level 50, left associativity) : imp_scope.

Notation "x * y" := (AMult x y) (at level 40, left associativity) : imp_scope.

Notation "x <= y" := (BLe x y) (at level 70, no associativity) : imp_scope.

Notation "x = y" := (BEq x y) (at level 70, no associativity) : imp_scope.

Notation "x && y" := (BAnd x y) (at level 40, left associativity) : imp_scope.

Notation "'~' b" := (BNot b) (at level 75, right associativity) : imp_scope.

Bind Scope imp_scope with com.

Notation "'SKIP'" :=

CSkip : imp_scope.

Notation "x '::=' a" :=

(CAss x a) (at level 60) : imp_scope.

Notation "c1 ;; c2" :=

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

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

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

Notation "'TEST' c1 'THEN' c2 'ELSE' c3 'FI'" :=

(CIf c1 c2 c3) (at level 80, right associativity) : imp_scope.

Definition empty_st := fun (_ : string) => 0.

Definition extend_st a x (st : state) :=

(fun (a' : string) => if String.eqb a a' then x

else st a').

Notation "a '!->' x" := (extend_st a x empty_st) (at level 100).

Notation "a '!->' x ';' s" := (extend_st a x s)

(at level 100, x at next level, right associativity).

Open Scope imp_scope.

Inductive cstep : (com * state) -> (com * state) -> Prop :=

| CS_AssStep : forall st i a a',

a / st -->a a' ->

(i ::= a) / st --> (i ::= a') / st

| CS_Ass : forall st i n,

(i ::= (ANum n)) / st --> SKIP / (i !-> n ; st)

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

c1 / st --> c1' / st' ->

(c1 ;; c2) / st --> (c1' ;; c2) / st'

| CS_SeqFinish : forall st c2,

(SKIP ;; c2) / st --> c2 / st

| CS_IfStep : forall st b b' c1 c2,

b / st -->b b' ->

TEST b THEN c1 ELSE c2 FI / st

-->

(TEST b' THEN c1 ELSE c2 FI) / st

| CS_IfTrue : forall st c1 c2,

TEST BTrue THEN c1 ELSE c2 FI / st --> c1 / st

| CS_IfFalse : forall st c1 c2,

TEST BFalse THEN c1 ELSE c2 FI / st --> c2 / st

| CS_While : forall st b c1,

WHILE b DO c1 END / st

-->

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

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

Close Scope imp_scope.

# Concurrent Imp

Module CImp.

Inductive com : Type :=

| CSkip : com

| CAss : string -> aexp -> com

| CSeq : com -> com -> com

| CIf : bexp -> com -> com -> com

| CWhile : bexp -> com -> com

| CPar : com -> com -> com.

Notation "'SKIP'" :=

CSkip.

Notation "x '::=' a" :=

(CAss x 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 "'TEST' b 'THEN' c1 'ELSE' c2 'FI'" :=

(CIf b c1 c2) (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 :=

| CS_AssStep : forall st i a a',

a / st -->a a' ->

(i ::= a) / st --> (i ::= a') / st

| CS_Ass : forall st i n,

(i ::= (ANum n)) / st --> SKIP / (i !-> n ; st)

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

c1 / st --> c1' / st' ->

(c1 ;; c2) / st --> (c1' ;; c2) / st'

| CS_SeqFinish : forall st c2,

(SKIP ;; c2) / st --> c2 / st

| CS_IfStep : forall st b b' c1 c2,

b /st -->b b' ->

(TEST b THEN c1 ELSE c2 FI) / st

--> (TEST b' THEN c1 ELSE c2 FI) / st

| CS_IfTrue : forall st c1 c2,

(TEST BTrue THEN c1 ELSE c2 FI) / st --> c1 / st

| CS_IfFalse : forall st c1 c2,

(TEST BFalse THEN c1 ELSE c2 FI) / st --> c2 / st

| CS_While : forall st b c1,

(WHILE b DO c1 END) / st

--> (TEST b THEN (c1;; (WHILE b DO c1 END)) ELSE SKIP FI) / st

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

c1 / st --> c1' / st' ->

(PAR c1 WITH c2 END) / st --> (PAR c1' WITH c2 END) / st'

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

c2 / st --> c2' / st' ->

(PAR c1 WITH c2 END) / st --> (PAR c1 WITH c2' END) / st'

| CS_ParDone : forall 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 W : string := "W".

Definition X : string := "X".

Definition Y : string := "Y".

Definition Z : string := "Z".

Definition par_loop : com :=

PAR

Y ::= 1

WITH

WHILE Y = 0 DO

X ::= X + 1

END

END.

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

Example par_loop_example_0:

exists st',

par_loop / empty_st -->* SKIP / st'

/\ st' X = 0.

Proof.

apply: ex_intro.

split.

- rewrite /par_loop.

apply: multi_step. apply: CS_Par1. apply: CS_Ass.

apply: multi_step. apply: CS_Par2. apply: CS_While.

apply: multi_step. apply: CS_Par2. apply: CS_IfStep. apply: BS_Eq1. apply: AS_Id.

apply: multi_step. apply: CS_Par2. apply: CS_IfStep. apply: BS_Eq => //=.

apply: multi_step. apply: CS_Par2. apply: CS_IfFalse.

apply: multi_step. apply: CS_ParDone.

apply: multi_refl.

- done.

Qed.

It can also terminate with X set to 2:

Example par_loop_example_2:

exists st',

par_loop / empty_st -->* SKIP / st'

/\ st' X = 2.

Proof.

apply: ex_intro.

split.

- rewrite /par_loop.

apply: multi_step. apply: CS_Par2. apply: CS_While.

apply: multi_step. apply: CS_Par2. apply: CS_IfStep. apply: BS_Eq1. apply: AS_Id.

apply: multi_step. apply: CS_Par2. apply: CS_IfStep. apply: BS_Eq => //=.

apply: multi_step. apply: CS_Par2. apply: CS_IfTrue.

apply: multi_step. apply: CS_Par2. apply: CS_SeqStep. apply: CS_AssStep. apply: AS_Plus1. apply: AS_Id.

apply: multi_step. apply: CS_Par2. apply: CS_SeqStep. apply: CS_AssStep. apply: AS_Plus.

apply: multi_step. apply: CS_Par2. apply: CS_SeqStep. apply: CS_Ass.

apply: multi_step. apply: CS_Par2. apply: CS_SeqFinish.

apply: multi_step. apply: CS_Par2. apply: CS_While.

apply: multi_step. apply: CS_Par2. apply: CS_IfStep.

apply: BS_Eq1. apply: AS_Id.

apply: multi_step. apply: CS_Par2. apply: CS_IfStep.

apply: BS_Eq. simpl.

apply: multi_step. apply: CS_Par2. apply: CS_IfTrue.

apply: multi_step. apply: CS_Par2. apply: CS_SeqStep.

apply: CS_AssStep. apply: AS_Plus1. apply: AS_Id.

apply: multi_step. apply: CS_Par2. apply: CS_SeqStep.

apply: CS_AssStep. apply: AS_Plus.

apply: multi_step. apply: CS_Par2. apply: CS_SeqStep.

apply: CS_Ass.

apply: multi_step. apply: CS_Par1. apply: CS_Ass.

apply: multi_step. apply: CS_Par2. apply: CS_SeqFinish.

apply: multi_step. apply: CS_Par2. apply: CS_While.

apply: multi_step. apply: CS_Par2. apply: CS_IfStep.

apply: BS_Eq1. apply: AS_Id.

apply: multi_step. apply: CS_Par2. apply: CS_IfStep.

apply: BS_Eq. simpl.

apply: multi_step. apply: CS_Par2. apply: CS_IfFalse.

apply: multi_step. apply: CS_ParDone.

apply: multi_refl.

- done.

Qed.

More generally...

Lemma par_body_n__Sn : forall n st,

st X = n /\ st Y = 0 ->

par_loop / st -->* par_loop / (X !-> S n ; st).

Proof.

Admitted.

Lemma par_body_n : forall n (st : state),

st X = 0 /\ st Y = 0 ->

exists st',

par_loop / st -->* par_loop / st' /\ st' X = n /\ st' Y = 0.

Proof.

Admitted.

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

Theorem par_loop_any_X:

forall n, exists st',

par_loop / empty_st -->* SKIP / st'

/\ st' X = n.

Proof.

move=> n.

case (@par_body_n n empty_st (conj (erefl 0) (erefl 0)))=> st H.

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

exists (Y !-> 1 ; st).

split.

- apply: multi_trans. apply: H'.

apply: multi_step. apply: CS_Par1. apply: CS_Ass.

apply: multi_step. apply: CS_Par2. apply: CS_While.

apply: multi_step. apply: CS_Par2. apply: CS_IfStep. apply: BS_Eq1. apply: AS_Id.

apply: multi_step. apply: CS_Par2. apply: CS_IfStep. apply: BS_Eq. simpl.

apply: multi_step. apply: CS_Par2. apply: CS_IfFalse.

apply: multi_step. apply: CS_ParDone.

apply multi_refl.

- done.

Qed.

End CImp.