SmallstepSmall-step Operational Semantics
Set Warnings "-notation-overridden,-parsing".
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Coq.omega.Omega.
Require Import Coq.Lists.List.
Import ListNotations.
Require Import Maps.
Require Import Imp.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Coq.omega.Omega.
Require Import Coq.Lists.List.
Import ListNotations.
Require Import Maps.
Require Import Imp.
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 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.
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 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 expressions
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.
A much more natural approach is simply to say that the behavior of
an expression like 2+nil is 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.
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 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.
These two outcomes — nontermination vs. getting stuck in an
erroneous configuration — should not be confused. 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
typechecking to the language. Indeed, this will be a major
topic for the rest of the course. As a first step, we need a way
of presenting the semantics that allows us to distinguish
nontermination from erroneous "stuck states."
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.
A Toy Language
Inductive tm : Type :=
| C : nat → tm (* Constant *)
| P : tm → tm → tm. (* Plus *)
| C : nat → tm (* Constant *)
| P : tm → tm → tm. (* Plus *)
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 a_{1} a_{2} ⇒ evalF a_{1} + evalF a_{2}
end.
match t with
| C n ⇒ n
| P a_{1} a_{2} ⇒ evalF a_{1} + evalF a_{2}
end.
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 |
t_{1} \\ n_{1} | |
t_{2} \\ n_{2} | (E_Plus) |
P t_{1} t_{2} \\ n_{1} + n_{2} |
Reserved Notation " t '\\' n " (at level 50, left associativity).
Inductive eval : tm → nat → Prop :=
Module SimpleArith1.
Inductive eval : tm → nat → Prop :=
| E_Const : ∀ n,
C n \\ n
| E_Plus : ∀ t_{1} t_{2} n_{1} n_{2},
t_{1} \\ n_{1} →
t_{2} \\ n_{2} →
P t_{1} t_{2} \\ (n_{1} + n_{2})
where " t '\\' n " := (eval t n).
C n \\ n
| E_Plus : ∀ t_{1} t_{2} n_{1} n_{2},
t_{1} \\ n_{1} →
t_{2} \\ n_{2} →
P t_{1} t_{2} \\ (n_{1} + n_{2})
where " t '\\' n " := (eval t n).
Module SimpleArith1.
Now, here is the corresponding small-step evaluation relation.
(ST_PlusConstConst) | |
P (C n_{1}) (C n_{2}) ==> C (n_{1} + n_{2}) |
t_{1} ==> t_{1}' | (ST_Plus1) |
P t_{1} t_{2} ==> P t_{1}' t_{2} |
t_{2} ==> t_{2}' | (ST_Plus2) |
P (C n_{1}) t_{2} ==> P (C n_{1}) t_{2}' |
Reserved Notation " t '==>' t' " (at level 40).
Inductive step : tm → tm → Prop :=
| ST_PlusConstConst : ∀ n_{1} n_{2},
P (C n_{1}) (C n_{2}) ==> C (n_{1} + n_{2})
| ST_Plus1 : ∀ t_{1} t_{1}' t_{2},
t_{1} ==> t_{1}' →
P t_{1} t_{2} ==> P t_{1}' t_{2}
| ST_Plus2 : ∀ n_{1} t_{2} t_{2}',
t_{2} ==> t_{2}' →
P (C n_{1}) t_{2} ==> P (C n_{1}) t_{2}'
where " t '==>' t' " := (step t t').
Inductive step : tm → tm → Prop :=
| ST_PlusConstConst : ∀ n_{1} n_{2},
P (C n_{1}) (C n_{2}) ==> C (n_{1} + n_{2})
| ST_Plus1 : ∀ t_{1} t_{1}' t_{2},
t_{1} ==> t_{1}' →
P t_{1} t_{2} ==> P t_{1}' t_{2}
| ST_Plus2 : ∀ n_{1} t_{2} t_{2}',
t_{2} ==> t_{2}' →
P (C n_{1}) t_{2} ==> P (C n_{1}) t_{2}'
where " t '==>' t' " := (step t t').
Things to notice:
Let's pause and check a couple of examples of reasoning with
the step relation...
If t_{1} can take a step to t_{1}', then P t_{1} t_{2} steps
to P t_{1}' t_{2}:
- 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)).
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: 1 star (test_step_2)
Right-hand sides of sums can take a step only when the left-hand side is finished: if t_{2} can take a step to t_{2}', then P (C n) t_{2} steps to P (C n) t_{2}':
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.
☐
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.
End SimpleArith1.
Relations
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 deterministic.
Theorem: For each t, there is at most one t' such that t
steps to t' (t ==> t' is provable). This is the
same as saying that ==> is deterministic.
Proof sketch: We show that if x steps to both y_{1} and
y_{2}, then y_{1} and y_{2} are equal, by induction on a derivation
of step x y_{1}. 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 y_{2}.
Formally:
- 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 t_{1} t_{2} where both t_{1} and t_{2} are
constants (by ST_PlusConstConst) and one of t_{1} or t_{2}
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 t_{1} t_{2} where t_{1} has both the form P t_{11} t_{12} and the form C n. ☐
Definition deterministic {X: Type} (R: relation X) :=
∀ x y_{1} y_{2} : X, R x y_{1} → R x y_{2} → y_{1} = y_{2}.
Module SimpleArith2.
Import SimpleArith1.
Theorem step_deterministic:
deterministic step.
End SimpleArith2.
∀ x y_{1} y_{2} : X, R x y_{1} → R x y_{2} → y_{1} = y_{2}.
Module SimpleArith2.
Import SimpleArith1.
Theorem step_deterministic:
deterministic step.
Proof.
unfold deterministic. intros x y_{1} y_{2} Hy_{1} Hy_{2}.
generalize dependent y_{2}.
induction Hy_{1}; intros y_{2} Hy_{2}.
- (* ST_PlusConstConst *) inversion Hy_{2}.
+ (* ST_PlusConstConst *) reflexivity.
+ (* ST_Plus1 *) inversion H_{2}.
+ (* ST_Plus2 *) inversion H_{2}.
- (* ST_Plus1 *) inversion Hy_{2}.
+ (* ST_PlusConstConst *)
rewrite <- H_{0} in Hy_{1}. inversion Hy_{1}.
+ (* ST_Plus1 *)
rewrite <- (IHHy1 t_{1}'0).
reflexivity. assumption.
+ (* ST_Plus2 *)
rewrite <- H in Hy_{1}. inversion Hy_{1}.
- (* ST_Plus2 *) inversion Hy_{2}.
+ (* ST_PlusConstConst *)
rewrite <- H_{1} in Hy_{1}. inversion Hy_{1}.
+ (* ST_Plus1 *) inversion H_{2}.
+ (* ST_Plus2 *)
rewrite <- (IHHy1 t_{2}'0).
reflexivity. assumption.
Qed.
unfold deterministic. intros x y_{1} y_{2} Hy_{1} Hy_{2}.
generalize dependent y_{2}.
induction Hy_{1}; intros y_{2} Hy_{2}.
- (* ST_PlusConstConst *) inversion Hy_{2}.
+ (* ST_PlusConstConst *) reflexivity.
+ (* ST_Plus1 *) inversion H_{2}.
+ (* ST_Plus2 *) inversion H_{2}.
- (* ST_Plus1 *) inversion Hy_{2}.
+ (* ST_PlusConstConst *)
rewrite <- H_{0} in Hy_{1}. inversion Hy_{1}.
+ (* ST_Plus1 *)
rewrite <- (IHHy1 t_{1}'0).
reflexivity. assumption.
+ (* ST_Plus2 *)
rewrite <- H in Hy_{1}. inversion Hy_{1}.
- (* ST_Plus2 *) inversion Hy_{2}.
+ (* ST_PlusConstConst *)
rewrite <- H_{1} in Hy_{1}. inversion Hy_{1}.
+ (* ST_Plus1 *) inversion H_{2}.
+ (* ST_Plus2 *)
rewrite <- (IHHy1 t_{2}'0).
reflexivity. assumption.
Qed.
End SimpleArith2.
There is some annoying repetition in this proof. Each use of
inversion Hy_{2} results in three subcases, only one of which is
relevant (the one that matches the current case in the induction
on Hy_{1}). The other two subcases need to be dismissed by finding
the contradiction among the hypotheses and doing inversion on it.
The following custom tactic, called solve_by_inverts, can be
helpful in such cases. It will solve the goal if it can be solved
by inverting some hypothesis; otherwise, it fails.
Ltac solve_by_inverts n :=
match goal with | H : ?T |- _ ⇒
match type of T with Prop ⇒
solve [
inversion H;
match n with S (S (?n')) ⇒ subst; solve_by_inverts (S n') end ]
end end.
match goal with | H : ?T |- _ ⇒
match type of T with Prop ⇒
solve [
inversion H;
match n with S (S (?n')) ⇒ subst; solve_by_inverts (S n') end ]
end end.
The details of how this works are not important for now, but it
illustrates the power of Coq's Ltac language for
programmatically defining special-purpose tactics. It looks
through the current proof state for a hypothesis H (the first
match) of type Prop (the second match) such that performing
inversion on H (followed by a recursive invocation of the same
tactic, if its argument n is greater than one) completely solves
the current goal. If no such hypothesis exists, it fails.
We will usually want to call solve_by_inverts with argument
1 (especially as larger arguments can lead to very slow proof
checking), so we define solve_by_invert as a shorthand for this
case.
Ltac solve_by_invert :=
solve_by_inverts 1.
solve_by_inverts 1.
Let's see how a proof of the previous theorem can be simplified
using this tactic...
Module SimpleArith3.
Import SimpleArith1.
Theorem step_deterministic_alt: deterministic step.
Proof.
intros x y_{1} y_{2} Hy_{1} Hy_{2}.
generalize dependent y_{2}.
induction Hy_{1}; intros y_{2} Hy_{2};
inversion Hy_{2}; subst; try solve_by_invert.
- (* ST_PlusConstConst *) reflexivity.
- (* ST_Plus1 *)
apply IHHy1 in H_{2}. rewrite H_{2}. reflexivity.
- (* ST_Plus2 *)
apply IHHy1 in H_{2}. rewrite H_{2}. reflexivity.
Qed.
End SimpleArith3.
Import SimpleArith1.
Theorem step_deterministic_alt: deterministic step.
Proof.
intros x y_{1} y_{2} Hy_{1} Hy_{2}.
generalize dependent y_{2}.
induction Hy_{1}; intros y_{2} Hy_{2};
inversion Hy_{2}; subst; try solve_by_invert.
- (* ST_PlusConstConst *) reflexivity.
- (* ST_Plus1 *)
apply IHHy1 in H_{2}. rewrite H_{2}. reflexivity.
- (* ST_Plus2 *)
apply IHHy1 in H_{2}. rewrite H_{2}. reflexivity.
Qed.
End SimpleArith3.
Values
- 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.
Inductive value : tm → Prop :=
| v_const : ∀ n, value (C n).
| 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, v_{1} ranges only over values, while t_{1} and t_{2}
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 n_{1}) (C n_{2}) ==> C (n_{1} + n_{2}) |
t_{1} ==> t_{1}' | (ST_Plus1) |
P t_{1} t_{2} ==> P t_{1}' t_{2} |
value v_{1} | |
t_{2} ==> t_{2}' | (ST_Plus2) |
P v_{1} t_{2} ==> P v_{1} t_{2}' |
Reserved Notation " t '==>' t' " (at level 40).
Inductive step : tm → tm → Prop :=
| ST_PlusConstConst : ∀ n_{1} n_{2},
P (C n_{1}) (C n_{2})
==> C (n_{1} + n_{2})
| ST_Plus1 : ∀ t_{1} t_{1}' t_{2},
t_{1} ==> t_{1}' →
P t_{1} t_{2} ==> P t_{1}' t_{2}
| ST_Plus2 : ∀ v_{1} t_{2} t_{2}',
value v_{1} → (* <----- n.b. *)
t_{2} ==> t_{2}' →
P v_{1} t_{2} ==> P v_{1} t_{2}'
where " t '==>' t' " := (step t t').
Inductive step : tm → tm → Prop :=
| ST_PlusConstConst : ∀ n_{1} n_{2},
P (C n_{1}) (C n_{2})
==> C (n_{1} + n_{2})
| ST_Plus1 : ∀ t_{1} t_{1}' t_{2},
t_{1} ==> t_{1}' →
P t_{1} t_{2} ==> P t_{1}' t_{2}
| ST_Plus2 : ∀ v_{1} t_{2} t_{2}',
value v_{1} → (* <----- n.b. *)
t_{2} ==> t_{2}' →
P v_{1} t_{2} ==> P v_{1} t_{2}'
where " t '==>' t' " := (step t t').
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 t_{1} t_{2} where both t_{1} and t_{2} are constants (by
ST_PlusConstConst) and one of t_{1} or t_{2} 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
t_{1} t_{2} where t_{1} both has the form P t_{11} t_{12} 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. ☐
Theorem step_deterministic :
deterministic step.
Proof.
(* FILL IN HERE *) Admitted.
☐
deterministic step.
Proof.
(* FILL IN HERE *) Admitted.
Strong Progress and Normal Forms
- Suppose t = C n. Then t is a value.
- Suppose t = P t_{1} t_{2}, where (by the IH) t_{1} either is a value
or can step to some t_{1}', and where t_{2} is either a value or
can step to some t_{2}'. We must show P t_{1} t_{2} is either a value
or steps to some t'.
- If t_{1} and t_{2} are both values, then t can take a step, by
ST_PlusConstConst.
- If t_{1} is a value and t_{2} can take a step, then so can t,
by ST_Plus2.
- If t_{1} can take a step, then so can t, by ST_Plus1. ☐
- If t_{1} and t_{2} are both values, then t can take a step, by
ST_PlusConstConst.
Theorem strong_progress : ∀ t,
value t ∨ (∃ t', t ==> t').
value t ∨ (∃ t', t ==> t').
Proof.
induction t.
- (* C *) left. apply v_const.
- (* P *) right. inversion IHt1.
+ (* l *) inversion IHt2.
* (* l *) inversion H. inversion H_{0}.
∃ (C (n + n_{0})).
apply ST_PlusConstConst.
* (* r *) inversion H_{0} as [t' H_{1}].
∃ (P t_{1} t').
apply ST_Plus2. apply H. apply H_{1}.
+ (* r *) inversion H as [t' H_{0}].
∃ (P t' t_{2}).
apply ST_Plus1. apply H_{0}. Qed.
induction t.
- (* C *) left. apply v_const.
- (* P *) right. inversion IHt1.
+ (* l *) inversion IHt2.
* (* l *) inversion H. inversion H_{0}.
∃ (C (n + n_{0})).
apply ST_PlusConstConst.
* (* r *) inversion H_{0} as [t' H_{1}].
∃ (P t_{1} t').
apply ST_Plus2. apply H. apply H_{1}.
+ (* r *) inversion H as [t' H_{0}].
∃ (P t' t_{2}).
apply ST_Plus1. apply H_{0}. Qed.
This important property is called 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.)
The idea of "making progress" can be extended to tell us something
interesting about values: in this language, values are exactly the
terms that cannot make progress in this sense.
To state this observation formally, 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'.
¬ ∃ t', R t t'.
Note that this definition specifies what it is to be a normal form
for an 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.
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.
Lemma value_is_nf : ∀ v,
value v → normal_form step v.
Lemma nf_is_value : ∀ t,
normal_form step t → value t.
Corollary nf_same_as_value : ∀ t,
normal_form step t ↔ value t.
value v → normal_form step v.
Proof.
unfold normal_form. intros v H. inversion H.
intros contra. inversion contra. inversion H_{1}.
Qed.
unfold normal_form. intros v H. inversion H.
intros contra. inversion contra. inversion H_{1}.
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').
{ apply strong_progress. }
inversion G.
+ (* l *) apply H_{0}.
+ (* r *) exfalso. apply H. assumption. Qed.
unfold normal_form. intros t H.
assert (G : value t ∨ ∃ t', t ==> t').
{ apply strong_progress. }
inversion G.
+ (* l *) apply H_{0}.
+ (* r *) exfalso. 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?
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 so that they
would not coincide.
Exercise: 3 stars, optional (value_not_same_as_normal_form1)
We might, for example, mistakenly define value so that it includes some terms that are not finished reducing. (Even if you don't work this exercise and the following ones in Coq, make sure you can think of an example of such a term.)
Module Temp1.
Inductive value : tm → Prop :=
| v_const : ∀ n, value (C n)
| v_funny : ∀ t_{1} n_{2}, (* <---- *)
value (P t_{1} (C n_{2})).
Reserved Notation " t '==>' t' " (at level 40).
Inductive step : tm → tm → Prop :=
| ST_PlusConstConst : ∀ n_{1} n_{2},
P (C n_{1}) (C n_{2}) ==> C (n_{1} + n_{2})
| ST_Plus1 : ∀ t_{1} t_{1}' t_{2},
t_{1} ==> t_{1}' →
P t_{1} t_{2} ==> P t_{1}' t_{2}
| ST_Plus2 : ∀ v_{1} t_{2} t_{2}',
value v_{1} →
t_{2} ==> t_{2}' →
P v_{1} t_{2} ==> P v_{1} t_{2}'
where " t '==>' t' " := (step t t').
Lemma value_not_same_as_normal_form :
∃ v, value v ∧ ¬ normal_form step v.
Proof.
(* FILL IN HERE *) Admitted.
End Temp1.
☐
Inductive value : tm → Prop :=
| v_const : ∀ n, value (C n)
| v_funny : ∀ t_{1} n_{2}, (* <---- *)
value (P t_{1} (C n_{2})).
Reserved Notation " t '==>' t' " (at level 40).
Inductive step : tm → tm → Prop :=
| ST_PlusConstConst : ∀ n_{1} n_{2},
P (C n_{1}) (C n_{2}) ==> C (n_{1} + n_{2})
| ST_Plus1 : ∀ t_{1} t_{1}' t_{2},
t_{1} ==> t_{1}' →
P t_{1} t_{2} ==> P t_{1}' t_{2}
| ST_Plus2 : ∀ v_{1} t_{2} t_{2}',
value v_{1} →
t_{2} ==> t_{2}' →
P v_{1} t_{2} ==> P v_{1} t_{2}'
where " t '==>' t' " := (step t t').
Lemma value_not_same_as_normal_form :
∃ v, value v ∧ ¬ normal_form step v.
Proof.
(* FILL IN HERE *) Admitted.
End Temp1.
Exercise: 2 stars, optional (value_not_same_as_normal_form2)
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 : ∀ n_{1} n_{2},
P (C n_{1}) (C n_{2}) ==> C (n_{1} + n_{2})
| ST_Plus1 : ∀ t_{1} t_{1}' t_{2},
t_{1} ==> t_{1}' →
P t_{1} t_{2} ==> P t_{1}' t_{2}
| ST_Plus2 : ∀ v_{1} t_{2} t_{2}',
value v_{1} →
t_{2} ==> t_{2}' →
P v_{1} t_{2} ==> P v_{1} t_{2}'
where " t '==>' t' " := (step t t').
Lemma value_not_same_as_normal_form :
∃ v, value v ∧ ¬ normal_form step v.
☐
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 : ∀ n_{1} n_{2},
P (C n_{1}) (C n_{2}) ==> C (n_{1} + n_{2})
| ST_Plus1 : ∀ t_{1} t_{1}' t_{2},
t_{1} ==> t_{1}' →
P t_{1} t_{2} ==> P t_{1}' t_{2}
| ST_Plus2 : ∀ v_{1} t_{2} t_{2}',
value v_{1} →
t_{2} ==> t_{2}' →
P v_{1} t_{2} ==> P v_{1} t_{2}'
where " t '==>' t' " := (step t t').
Lemma value_not_same_as_normal_form :
∃ v, value v ∧ ¬ normal_form step v.
Proof.
(* FILL IN HERE *) Admitted.
End Temp2.(* FILL IN HERE *) Admitted.
Exercise: 3 stars, optional (value_not_same_as_normal_form3)
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, even 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 : ∀ n_{1} n_{2},
P (C n_{1}) (C n_{2}) ==> C (n_{1} + n_{2})
| ST_Plus1 : ∀ t_{1} t_{1}' t_{2},
t_{1} ==> t_{1}' →
P t_{1} t_{2} ==> P t_{1}' t_{2}
where " t '==>' t' " := (step t t').
Inductive value : tm → Prop :=
| v_const : ∀ n, value (C n).
Reserved Notation " t '==>' t' " (at level 40).
Inductive step : tm → tm → Prop :=
| ST_PlusConstConst : ∀ n_{1} n_{2},
P (C n_{1}) (C n_{2}) ==> C (n_{1} + n_{2})
| ST_Plus1 : ∀ t_{1} t_{1}' t_{2},
t_{1} ==> t_{1}' →
P t_{1} t_{2} ==> P t_{1}' t_{2}
where " t '==>' t' " := (step t t').
(Note that ST_Plus2 is missing.)
Lemma value_not_same_as_normal_form :
∃ t, ¬ value t ∧ normal_form step t.
Proof.
(* FILL IN HERE *) Admitted.
End Temp3.
☐
∃ 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 addition expressions 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 : ∀ t_{1} t_{2},
tif ttrue t_{1} t_{2} ==> t_{1}
| ST_IfFalse : ∀ t_{1} t_{2},
tif tfalse t_{1} t_{2} ==> t_{2}
| ST_If : ∀ t_{1} t_{1}' t_{2} t_{3},
t_{1} ==> t_{1}' →
tif t_{1} t_{2} t_{3} ==> tif t_{1}' t_{2} t_{3}
where " t '==>' t' " := (step t t').
| 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 : ∀ t_{1} t_{2},
tif ttrue t_{1} t_{2} ==> t_{1}
| ST_IfFalse : ∀ t_{1} t_{2},
tif tfalse t_{1} t_{2} ==> t_{2}
| ST_If : ∀ t_{1} t_{1}' t_{2} t_{3},
t_{1} ==> t_{1}' →
tif t_{1} t_{2} t_{3} ==> tif t_{1}' t_{2} t_{3}
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 *)
☐
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, optional (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.
☐
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 : ∀ t_{1} t_{2},
tif ttrue t_{1} t_{2} ==> t_{1}
| ST_IfFalse : ∀ t_{1} t_{2},
tif tfalse t_{1} t_{2} ==> t_{2}
| ST_If : ∀ t_{1} t_{1}' t_{2} t_{3},
t_{1} ==> t_{1}' →
tif t_{1} t_{2} t_{3} ==> tif t_{1}' t_{2} t_{3}
(* 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.
☐
Inductive step : tm → tm → Prop :=
| ST_IfTrue : ∀ t_{1} t_{2},
tif ttrue t_{1} t_{2} ==> t_{1}
| ST_IfFalse : ∀ t_{1} t_{2},
tif tfalse t_{1} t_{2} ==> t_{2}
| ST_If : ∀ t_{1} t_{1}' t_{2} t_{3},
t_{1} ==> t_{1}' →
tif t_{1} t_{2} t_{3} ==> tif t_{1}' t_{2} t_{3}
(* 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.
End Temp4.
Multi-Step Reduction
- 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.
Since we'll want to reuse the idea of multi-step reduction many
times, let's take a little extra trouble and define it
generically.
Given a relation R, we define a relation multi R, called the
multi-step closure of R as follows.
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.
| 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.
(In the Rel chapter of Logical Foundations and
the Coq standard library, this relation is called
clos_refl_trans_1n. We give it a shorter name here for the sake
of readability.)
The effect of this definition is that multi R relates two
elements x and y if
We write ==>* for the multi step relation on terms.
- x = y, or
- R x y, or
- there is some nonempty sequence z_{1}, z_{2}, ..., zn such that
R x z_{1}
R z_{1} z_{2}
...
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 reflexive (that is, ∀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.
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.")
Theorem multi_R : ∀ (X:Type) (R:relation X) (x y : X),
R x y → (multi R) x y.
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.
intros X R x y H.
apply multi_step with y. apply H. apply multi_refl. Qed.
Third, multi R is transitive.
Theorem multi_trans :
∀ (X:Type) (R: relation X) (x y z : X),
multi R x y →
multi R y z →
multi R x z.
∀ (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.
induction G.
- (* multi_refl *) assumption.
- (* multi_step *)
apply multi_step with y. assumption.
apply IHG. assumption. Qed.
intros X R x y z G H.
induction G.
- (* multi_refl *) assumption.
- (* multi_step *)
apply multi_step with y. assumption.
apply IHG. assumption. Qed.
In particular, for the multi step relation on terms, if
t_{1}==>*t_{2} and t_{2}==>*t_{3}, then t_{1}==>*t_{3}.
Lemma test_multistep_1:
P
(P (C 0) (C 3))
(P (C 2) (C 4))
==>*
C ((0 + 3) + (2 + 4)).
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 of the same fact 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.
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.
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').
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.
(* We recommend using this initial setup as-is! *)
unfold deterministic. unfold normal_form_of.
intros x y_{1} y_{2} P_{1} P_{2}.
inversion P_{1} as [P_{11} P_{12}]; clear P_{1}.
inversion P_{2} as [P_{21} P_{22}]; clear P_{2}.
generalize dependent y_{2}.
(* FILL IN HERE *) Admitted.
☐
deterministic normal_form_of.
Proof.
(* We recommend using this initial setup as-is! *)
unfold deterministic. unfold normal_form_of.
intros x y_{1} y_{2} P_{1} P_{2}.
inversion P_{1} as [P_{11} P_{12}]; clear P_{1}.
inversion P_{2} as [P_{21} P_{22}]; clear P_{2}.
generalize dependent y_{2}.
(* FILL IN HERE *) Admitted.
Definition normalizing {X:Type} (R:relation X) :=
∀ t, ∃ t',
(multi R) t t' ∧ normal_form R t'.
∀ 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 : ∀ t_{1} t_{1}' t_{2},
t_{1} ==>* t_{1}' →
P t_{1} t_{2} ==>* P t_{1}' t_{2}.
t_{1} ==>* t_{1}' →
P t_{1} t_{2} ==>* P t_{1}' t_{2}.
Proof.
intros t_{1} t_{1}' t_{2} H. induction H.
- (* multi_refl *) apply multi_refl.
- (* multi_step *) apply multi_step with (P y t_{2}).
apply ST_Plus1. apply H.
apply IHmulti. Qed.
intros t_{1} t_{1}' t_{2} H. induction H.
- (* multi_refl *) apply multi_refl.
- (* multi_step *) apply multi_step with (P y t_{2}).
apply ST_Plus1. apply H.
apply IHmulti. Qed.
Lemma multistep_congr_2 : ∀ t_{1} t_{2} t_{2}',
value t_{1} →
t_{2} ==>* t_{2}' →
P t_{1} t_{2} ==>* P t_{1} t_{2}'.
Proof.
(* FILL IN HERE *) Admitted.
☐
value t_{1} →
t_{2} ==>* t_{2}' →
P t_{1} t_{2} ==>* P t_{1} t_{2}'.
Proof.
(* FILL IN HERE *) Admitted.
- 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 t_{1} t_{2} for some t_{1} and t_{2}. By the IH, t_{1} and t_{2}
have normal forms t_{1}' and t_{2}'. Recall that normal forms are
values (by nf_same_as_value); we know that t_{1}' = C n_{1} and
t_{2}' = C n_{2}, for some n_{1} and n_{2}. We can combine the ==>*
derivations for t_{1} and t_{2} using multi_congr_1 and
multi_congr_2 to prove that P t_{1} t_{2} reduces in many steps to
C (n_{1} + n_{2}).
Theorem step_normalizing :
normalizing step.
normalizing step.
Proof.
unfold normalizing.
induction t.
- (* C *)
∃ (C n).
split.
+ (* l *) apply multi_refl.
+ (* r *)
(* We can use rewrite with "iff" statements, not
just equalities: *)
rewrite nf_same_as_value. apply v_const.
- (* P *)
destruct IHt1 as [t_{1}' [H_{11} H_{12}]].
destruct IHt2 as [t_{2}' [H_{21} H_{22}]].
rewrite nf_same_as_value in H_{12}. rewrite nf_same_as_value in H_{22}.
inversion H_{12} as [n_{1} H]. inversion H_{22} as [n_{2} H'].
rewrite <- H in H_{11}.
rewrite <- H' in H_{21}.
∃ (C (n_{1} + n_{2})).
split.
+ (* l *)
apply multi_trans with (P (C n_{1}) t_{2}).
* apply multistep_congr_1. apply H_{11}.
* apply multi_trans with
(P (C n_{1}) (C n_{2})).
{ apply multistep_congr_2. apply v_const. apply H_{21}. }
{ apply multi_R. apply ST_PlusConstConst. }
+ (* r *)
rewrite nf_same_as_value. apply v_const. Qed.
unfold normalizing.
induction t.
- (* C *)
∃ (C n).
split.
+ (* l *) apply multi_refl.
+ (* r *)
(* We can use rewrite with "iff" statements, not
just equalities: *)
rewrite nf_same_as_value. apply v_const.
- (* P *)
destruct IHt1 as [t_{1}' [H_{11} H_{12}]].
destruct IHt2 as [t_{2}' [H_{21} H_{22}]].
rewrite nf_same_as_value in H_{12}. rewrite nf_same_as_value in H_{22}.
inversion H_{12} as [n_{1} H]. inversion H_{22} as [n_{2} H'].
rewrite <- H in H_{11}.
rewrite <- H' in H_{21}.
∃ (C (n_{1} + n_{2})).
split.
+ (* l *)
apply multi_trans with (P (C n_{1}) t_{2}).
* apply multistep_congr_1. apply H_{11}.
* apply multi_trans with
(P (C n_{1}) (C n_{2})).
{ apply multistep_congr_2. apply v_const. apply H_{21}. }
{ apply multi_R. apply ST_PlusConstConst. }
+ (* r *)
rewrite nf_same_as_value. apply v_const. Qed.
Equivalence of Big-Step and Small-Step
Exercise: 3 stars (eval__multistep)
Theorem eval__multistep : ∀ t n,
t \\ n → t ==>* C n.
t \\ n → t ==>* C n.
The key ideas in the proof can be seen in 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 t_{1} t_{2} ==> (by ST_Plus1)
P t_{1}' t_{2} ==> (by ST_Plus1)
P t_{1}'' t_{2} ==> (by ST_Plus1)
...
P (C n_{1}) t_{2} ==> (by ST_Plus2)
P (C n_{1}) t_{2}' ==> (by ST_Plus2)
P (C n_{1}) t_{2}'' ==> (by ST_Plus2)
...
P (C n_{1}) (C n_{2}) ==> (by ST_PlusConstConst)
C (n_{1} + n_{2})
That is, the multistep reduction of a term of the form P t_{1} t_{2}
proceeds in three phases:
P t_{1}' t_{2} ==> (by ST_Plus1)
P t_{1}'' t_{2} ==> (by ST_Plus1)
...
P (C n_{1}) t_{2} ==> (by ST_Plus2)
P (C n_{1}) t_{2}' ==> (by ST_Plus2)
P (C n_{1}) t_{2}'' ==> (by ST_Plus2)
...
P (C n_{1}) (C n_{2}) ==> (by ST_PlusConstConst)
C (n_{1} + n_{2})
- First, we use ST_Plus1 some number of times to reduce t_{1} to a normal form, which must (by nf_same_as_value) be a term of the form C n_{1} for some n_{1}.
- Next, we use ST_Plus2 some number of times to reduce t_{2} to a normal form, which must again be a term of the form C n_{2} for some n_{2}.
- Finally, we use ST_PlusConstConst one time to reduce P (C n_{1}) (C n_{2}) to C (n_{1} + n_{2}).
Proof.
(* FILL IN HERE *) Admitted.
☐
(* FILL IN HERE *) Admitted.
Exercise: 3 stars, advanced (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.
Exercise: 3 stars (multistep__eval)
Theorem multistep__eval : ∀ t t',
normal_form_of t t' → ∃ n, t' = C n ∧ t \\ n.
Proof.
(* FILL IN HERE *) Admitted.
☐
normal_form_of t t' → ∃ n, t' = C n ∧ t \\ n.
Proof.
(* FILL IN HERE *) Admitted.
Additional Exercises
Exercise: 3 stars, optional (interp_tm)
Remember that we also defined big-step evaluation of terms as a function evalF. Prove that it is equivalent to the existing semantics. (Hint: we just proved that eval and multistep are equivalent, so logically it doesn't matter which you choose. One will be easier than the other, though!)
Theorem evalF_eval : ∀ t n,
evalF t = n ↔ t \\ n.
Proof.
(* FILL IN HERE *) Admitted.
☐
evalF t = n ↔ t \\ n.
Proof.
(* FILL IN HERE *) Admitted.
Exercise: 4 stars (combined_properties)
We've considered 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.
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 : ∀ n_{1} n_{2},
P (C n_{1}) (C n_{2}) ==> C (n_{1} + n_{2})
| ST_Plus1 : ∀ t_{1} t_{1}' t_{2},
t_{1} ==> t_{1}' →
P t_{1} t_{2} ==> P t_{1}' t_{2}
| ST_Plus2 : ∀ v_{1} t_{2} t_{2}',
value v_{1} →
t_{2} ==> t_{2}' →
P v_{1} t_{2} ==> P v_{1} t_{2}'
| ST_IfTrue : ∀ t_{1} t_{2},
tif ttrue t_{1} t_{2} ==> t_{1}
| ST_IfFalse : ∀ t_{1} t_{2},
tif tfalse t_{1} t_{2} ==> t_{2}
| ST_If : ∀ t_{1} t_{1}' t_{2} t_{3},
t_{1} ==> t_{1}' →
tif t_{1} t_{2} t_{3} ==> tif t_{1}' t_{2} t_{3}
where " t '==>' t' " := (step t t').
Inductive tm : Type :=
| C : nat → tm
| P : tm → tm → tm
| ttrue : tm
| tfalse : tm
| tif : tm → tm → tm → tm.
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 : ∀ n_{1} n_{2},
P (C n_{1}) (C n_{2}) ==> C (n_{1} + n_{2})
| ST_Plus1 : ∀ t_{1} t_{1}' t_{2},
t_{1} ==> t_{1}' →
P t_{1} t_{2} ==> P t_{1}' t_{2}
| ST_Plus2 : ∀ v_{1} t_{2} t_{2}',
value v_{1} →
t_{2} ==> t_{2}' →
P v_{1} t_{2} ==> P v_{1} t_{2}'
| ST_IfTrue : ∀ t_{1} t_{2},
tif ttrue t_{1} t_{2} ==> t_{1}
| ST_IfFalse : ∀ t_{1} t_{2},
tif tfalse t_{1} t_{2} ==> t_{2}
| ST_If : ∀ t_{1} t_{1}' t_{2} t_{3},
t_{1} ==> t_{1}' →
tif t_{1} t_{2} t_{3} ==> tif t_{1}' t_{2} t_{3}
where " t '==>' t' " := (step t t').
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.
☐
End Combined.
Small-Step Imp
Inductive aval : aexp → Prop :=
| av_num : ∀ n, aval (ANum n).
| av_num : ∀ 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 : ∀ st i,
AId i / st ==>a ANum (st i)
| AS_Plus : ∀ st n_{1} n_{2},
APlus (ANum n_{1}) (ANum n_{2}) / st ==>a ANum (n_{1} + n_{2})
| AS_Plus1 : ∀ st a_{1} a_{1}' a_{2},
a_{1} / st ==>a a_{1}' →
(APlus a_{1} a_{2}) / st ==>a (APlus a_{1}' a_{2})
| AS_Plus2 : ∀ st v_{1} a_{2} a_{2}',
aval v_{1} →
a_{2} / st ==>a a_{2}' →
(APlus v_{1} a_{2}) / st ==>a (APlus v_{1} a_{2}')
| AS_Minus : ∀ st n_{1} n_{2},
(AMinus (ANum n_{1}) (ANum n_{2})) / st ==>a (ANum (minus n_{1} n_{2}))
| AS_Minus1 : ∀ st a_{1} a_{1}' a_{2},
a_{1} / st ==>a a_{1}' →
(AMinus a_{1} a_{2}) / st ==>a (AMinus a_{1}' a_{2})
| AS_Minus2 : ∀ st v_{1} a_{2} a_{2}',
aval v_{1} →
a_{2} / st ==>a a_{2}' →
(AMinus v_{1} a_{2}) / st ==>a (AMinus v_{1} a_{2}')
| AS_Mult : ∀ st n_{1} n_{2},
(AMult (ANum n_{1}) (ANum n_{2})) / st ==>a (ANum (mult n_{1} n_{2}))
| AS_Mult1 : ∀ st a_{1} a_{1}' a_{2},
a_{1} / st ==>a a_{1}' →
(AMult a_{1} a_{2}) / st ==>a (AMult a_{1}' a_{2})
| AS_Mult2 : ∀ st v_{1} a_{2} a_{2}',
aval v_{1} →
a_{2} / st ==>a a_{2}' →
(AMult v_{1} a_{2}) / st ==>a (AMult v_{1} a_{2}')
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 n_{1} n_{2},
(BEq (ANum n_{1}) (ANum n_{2})) / st ==>b
(if (beq_nat n_{1} n_{2}) then BTrue else BFalse)
| BS_Eq_{1} : ∀ st a_{1} a_{1}' a_{2},
a_{1} / st ==>a a_{1}' →
(BEq a_{1} a_{2}) / st ==>b (BEq a_{1}' a_{2})
| BS_Eq_{2} : ∀ st v_{1} a_{2} a_{2}',
aval v_{1} →
a_{2} / st ==>a a_{2}' →
(BEq v_{1} a_{2}) / st ==>b (BEq v_{1} a_{2}')
| BS_LtEq : ∀ st n_{1} n_{2},
(BLe (ANum n_{1}) (ANum n_{2})) / st ==>b
(if (leb n_{1} n_{2}) then BTrue else BFalse)
| BS_LtEq1 : ∀ st a_{1} a_{1}' a_{2},
a_{1} / st ==>a a_{1}' →
(BLe a_{1} a_{2}) / st ==>b (BLe a_{1}' a_{2})
| BS_LtEq2 : ∀ st v_{1} a_{2} a_{2}',
aval v_{1} →
a_{2} / st ==>a a_{2}' →
(BLe v_{1} a_{2}) / st ==>b (BLe v_{1} a_{2}')
| BS_NotTrue : ∀ st,
(BNot BTrue) / st ==>b BFalse
| BS_NotFalse : ∀ st,
(BNot BFalse) / st ==>b BTrue
| BS_NotStep : ∀ st b_{1} b_{1}',
b_{1} / st ==>b b_{1}' →
(BNot b_{1}) / st ==>b (BNot b_{1}')
| BS_AndTrueTrue : ∀ st,
(BAnd BTrue BTrue) / st ==>b BTrue
| BS_AndTrueFalse : ∀ st,
(BAnd BTrue BFalse) / st ==>b BFalse
| BS_AndFalse : ∀ st b_{2},
(BAnd BFalse b_{2}) / st ==>b BFalse
| BS_AndTrueStep : ∀ st b_{2} b_{2}',
b_{2} / st ==>b b_{2}' →
(BAnd BTrue b_{2}) / st ==>b (BAnd BTrue b_{2}')
| BS_AndStep : ∀ st b_{1} b_{1}' b_{2},
b_{1} / st ==>b b_{1}' →
(BAnd b_{1} b_{2}) / st ==>b (BAnd b_{1}' b_{2})
where " t '/' st '==>b' t' " := (bstep st t 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 n_{1} n_{2},
APlus (ANum n_{1}) (ANum n_{2}) / st ==>a ANum (n_{1} + n_{2})
| AS_Plus1 : ∀ st a_{1} a_{1}' a_{2},
a_{1} / st ==>a a_{1}' →
(APlus a_{1} a_{2}) / st ==>a (APlus a_{1}' a_{2})
| AS_Plus2 : ∀ st v_{1} a_{2} a_{2}',
aval v_{1} →
a_{2} / st ==>a a_{2}' →
(APlus v_{1} a_{2}) / st ==>a (APlus v_{1} a_{2}')
| AS_Minus : ∀ st n_{1} n_{2},
(AMinus (ANum n_{1}) (ANum n_{2})) / st ==>a (ANum (minus n_{1} n_{2}))
| AS_Minus1 : ∀ st a_{1} a_{1}' a_{2},
a_{1} / st ==>a a_{1}' →
(AMinus a_{1} a_{2}) / st ==>a (AMinus a_{1}' a_{2})
| AS_Minus2 : ∀ st v_{1} a_{2} a_{2}',
aval v_{1} →
a_{2} / st ==>a a_{2}' →
(AMinus v_{1} a_{2}) / st ==>a (AMinus v_{1} a_{2}')
| AS_Mult : ∀ st n_{1} n_{2},
(AMult (ANum n_{1}) (ANum n_{2})) / st ==>a (ANum (mult n_{1} n_{2}))
| AS_Mult1 : ∀ st a_{1} a_{1}' a_{2},
a_{1} / st ==>a a_{1}' →
(AMult a_{1} a_{2}) / st ==>a (AMult a_{1}' a_{2})
| AS_Mult2 : ∀ st v_{1} a_{2} a_{2}',
aval v_{1} →
a_{2} / st ==>a a_{2}' →
(AMult v_{1} a_{2}) / st ==>a (AMult v_{1} a_{2}')
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 n_{1} n_{2},
(BEq (ANum n_{1}) (ANum n_{2})) / st ==>b
(if (beq_nat n_{1} n_{2}) then BTrue else BFalse)
| BS_Eq_{1} : ∀ st a_{1} a_{1}' a_{2},
a_{1} / st ==>a a_{1}' →
(BEq a_{1} a_{2}) / st ==>b (BEq a_{1}' a_{2})
| BS_Eq_{2} : ∀ st v_{1} a_{2} a_{2}',
aval v_{1} →
a_{2} / st ==>a a_{2}' →
(BEq v_{1} a_{2}) / st ==>b (BEq v_{1} a_{2}')
| BS_LtEq : ∀ st n_{1} n_{2},
(BLe (ANum n_{1}) (ANum n_{2})) / st ==>b
(if (leb n_{1} n_{2}) then BTrue else BFalse)
| BS_LtEq1 : ∀ st a_{1} a_{1}' a_{2},
a_{1} / st ==>a a_{1}' →
(BLe a_{1} a_{2}) / st ==>b (BLe a_{1}' a_{2})
| BS_LtEq2 : ∀ st v_{1} a_{2} a_{2}',
aval v_{1} →
a_{2} / st ==>a a_{2}' →
(BLe v_{1} a_{2}) / st ==>b (BLe v_{1} a_{2}')
| BS_NotTrue : ∀ st,
(BNot BTrue) / st ==>b BFalse
| BS_NotFalse : ∀ st,
(BNot BFalse) / st ==>b BTrue
| BS_NotStep : ∀ st b_{1} b_{1}',
b_{1} / st ==>b b_{1}' →
(BNot b_{1}) / st ==>b (BNot b_{1}')
| BS_AndTrueTrue : ∀ st,
(BAnd BTrue BTrue) / st ==>b BTrue
| BS_AndTrueFalse : ∀ st,
(BAnd BTrue BFalse) / st ==>b BFalse
| BS_AndFalse : ∀ st b_{2},
(BAnd BFalse b_{2}) / st ==>b BFalse
| BS_AndTrueStep : ∀ st b_{2} b_{2}',
b_{2} / st ==>b b_{2}' →
(BAnd BTrue b_{2}) / st ==>b (BAnd BTrue b_{2}')
| BS_AndStep : ∀ st b_{1} b_{1}' b_{2},
b_{1} / st ==>b b_{1}' →
(BAnd b_{1} b_{2}) / st ==>b (BAnd b_{1}' b_{2})
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).
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 / (st & { i --> n })
| CS_SeqStep : ∀ st c_{1} c_{1}' st' c_{2},
c_{1} / st ==> c_{1}' / st' →
(c_{1} ;; c_{2}) / st ==> (c_{1}' ;; c_{2}) / st'
| CS_SeqFinish : ∀ st c_{2},
(SKIP ;; c_{2}) / st ==> c_{2} / st
| CS_IfTrue : ∀ st c_{1} c_{2},
IFB BTrue THEN c_{1} ELSE c_{2} FI / st ==> c_{1} / st
| CS_IfFalse : ∀ st c_{1} c_{2},
IFB BFalse THEN c_{1} ELSE c_{2} FI / st ==> c_{2} / st
| CS_IfStep : ∀ st b b' c_{1} c_{2},
b / st ==>b b' →
IFB b THEN c_{1} ELSE c_{2} FI / st
==> (IFB b' THEN c_{1} ELSE c_{2} FI) / st
| CS_While : ∀ st b c_{1},
(WHILE b DO c_{1} END) / st
==> (IFB b THEN (c_{1};; (WHILE b DO c_{1} END)) ELSE SKIP FI) / st
where " t '/' st '==>' t' '/' st' " := (cstep (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 / (st & { i --> n })
| CS_SeqStep : ∀ st c_{1} c_{1}' st' c_{2},
c_{1} / st ==> c_{1}' / st' →
(c_{1} ;; c_{2}) / st ==> (c_{1}' ;; c_{2}) / st'
| CS_SeqFinish : ∀ st c_{2},
(SKIP ;; c_{2}) / st ==> c_{2} / st
| CS_IfTrue : ∀ st c_{1} c_{2},
IFB BTrue THEN c_{1} ELSE c_{2} FI / st ==> c_{1} / st
| CS_IfFalse : ∀ st c_{1} c_{2},
IFB BFalse THEN c_{1} ELSE c_{2} FI / st ==> c_{2} / st
| CS_IfStep : ∀ st b b' c_{1} c_{2},
b / st ==>b b' →
IFB b THEN c_{1} ELSE c_{2} FI / st
==> (IFB b' THEN c_{1} ELSE c_{2} FI) / st
| CS_While : ∀ st b c_{1},
(WHILE b DO c_{1} END) / st
==> (IFB b THEN (c_{1};; (WHILE b DO c_{1} END)) ELSE SKIP FI) / st
where " t '/' st '==>' t' '/' st' " := (cstep (t,st) (t',st')).
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
(* New: *)
| CPar : com → com → com.
Notation "'SKIP'" :=
CSkip.
Notation "x '::=' a" :=
(CAss x a) (at level 60).
Notation "c_{1} ;; c_{2}" :=
(CSeq c_{1} c_{2}) (at level 80, right associativity).
Notation "'WHILE' b 'DO' c 'END'" :=
(CWhile b c) (at level 80, right associativity).
Notation "'IFB' b 'THEN' c_{1} 'ELSE' c_{2} 'FI'" :=
(CIf b c_{1} c_{2}) (at level 80, right associativity).
Notation "'PAR' c_{1} 'WITH' c_{2} 'END'" :=
(CPar c_{1} c_{2}) (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 / st & { i --> n }
| CS_SeqStep : ∀ st c_{1} c_{1}' st' c_{2},
c_{1} / st ==> c_{1}' / st' →
(c_{1} ;; c_{2}) / st ==> (c_{1}' ;; c_{2}) / st'
| CS_SeqFinish : ∀ st c_{2},
(SKIP ;; c_{2}) / st ==> c_{2} / st
| CS_IfTrue : ∀ st c_{1} c_{2},
(IFB BTrue THEN c_{1} ELSE c_{2} FI) / st ==> c_{1} / st
| CS_IfFalse : ∀ st c_{1} c_{2},
(IFB BFalse THEN c_{1} ELSE c_{2} FI) / st ==> c_{2} / st
| CS_IfStep : ∀ st b b' c_{1} c_{2},
b /st ==>b b' →
(IFB b THEN c_{1} ELSE c_{2} FI) / st
==> (IFB b' THEN c_{1} ELSE c_{2} FI) / st
| CS_While : ∀ st b c_{1},
(WHILE b DO c_{1} END) / st
==> (IFB b THEN (c_{1};; (WHILE b DO c_{1} END)) ELSE SKIP FI) / st
(* New part: *)
| CS_Par1 : ∀ st c_{1} c_{1}' c_{2} st',
c_{1} / st ==> c_{1}' / st' →
(PAR c_{1} WITH c_{2} END) / st ==> (PAR c_{1}' WITH c_{2} END) / st'
| CS_Par2 : ∀ st c_{1} c_{2} c_{2}' st',
c_{2} / st ==> c_{2}' / st' →
(PAR c_{1} WITH c_{2} END) / st ==> (PAR c_{1} WITH c_{2}' 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).
Inductive com : Type :=
| CSkip : com
| CAss : string → aexp → com
| CSeq : com → com → com
| CIf : bexp → com → com → com
| CWhile : bexp → com → com
(* New: *)
| CPar : com → com → com.
Notation "'SKIP'" :=
CSkip.
Notation "x '::=' a" :=
(CAss x a) (at level 60).
Notation "c_{1} ;; c_{2}" :=
(CSeq c_{1} c_{2}) (at level 80, right associativity).
Notation "'WHILE' b 'DO' c 'END'" :=
(CWhile b c) (at level 80, right associativity).
Notation "'IFB' b 'THEN' c_{1} 'ELSE' c_{2} 'FI'" :=
(CIf b c_{1} c_{2}) (at level 80, right associativity).
Notation "'PAR' c_{1} 'WITH' c_{2} 'END'" :=
(CPar c_{1} c_{2}) (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 / st & { i --> n }
| CS_SeqStep : ∀ st c_{1} c_{1}' st' c_{2},
c_{1} / st ==> c_{1}' / st' →
(c_{1} ;; c_{2}) / st ==> (c_{1}' ;; c_{2}) / st'
| CS_SeqFinish : ∀ st c_{2},
(SKIP ;; c_{2}) / st ==> c_{2} / st
| CS_IfTrue : ∀ st c_{1} c_{2},
(IFB BTrue THEN c_{1} ELSE c_{2} FI) / st ==> c_{1} / st
| CS_IfFalse : ∀ st c_{1} c_{2},
(IFB BFalse THEN c_{1} ELSE c_{2} FI) / st ==> c_{2} / st
| CS_IfStep : ∀ st b b' c_{1} c_{2},
b /st ==>b b' →
(IFB b THEN c_{1} ELSE c_{2} FI) / st
==> (IFB b' THEN c_{1} ELSE c_{2} FI) / st
| CS_While : ∀ st b c_{1},
(WHILE b DO c_{1} END) / st
==> (IFB b THEN (c_{1};; (WHILE b DO c_{1} END)) ELSE SKIP FI) / st
(* New part: *)
| CS_Par1 : ∀ st c_{1} c_{1}' c_{2} st',
c_{1} / st ==> c_{1}' / st' →
(PAR c_{1} WITH c_{2} END) / st ==> (PAR c_{1}' WITH c_{2} END) / st'
| CS_Par2 : ∀ st c_{1} c_{2} c_{2}' st',
c_{2} / st ==> c_{2}' / st' →
(PAR c_{1} WITH c_{2} END) / st ==> (PAR c_{1} WITH c_{2}' 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 ::= 1
WITH
WHILE Y = 0 DO
X ::= X + 1
END
END.
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:
∃ st',
par_loop / { --> 0 } ==>* SKIP / st'
∧ st' X = 0.
∃ st',
par_loop / { --> 0 } ==>* 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_Eq_{1}. 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_Eq_{1}. 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 / { --> 0 } ==>* SKIP / st'
∧ st' X = 2.
∃ st',
par_loop / { --> 0 } ==>* 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_Eq_{1}. 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_Eq_{1}. 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_Eq_{1}. 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_Eq_{1}. 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_Eq_{1}. 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_Eq_{1}. 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 / st & { X --> S n}.
Proof.
(* FILL IN HERE *) Admitted.
☐
st X = n ∧ st Y = 0 →
par_loop / st ==>* par_loop / 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.
Theorem par_loop_any_X:
∀ n, ∃ st',
par_loop / { --> 0 } ==>* SKIP / st'
∧ st' X = n.
End CImp.
∀ n, ∃ st',
par_loop / { --> 0 } ==>* SKIP / st'
∧ st' X = n.
Proof.
intros n.
destruct (par_body_n n { --> 0 }).
split; unfold t_update; reflexivity.
rename x into st.
inversion H as [H' [HX HY]]; clear H.
∃ (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_Eq_{1}. apply AS_Id. rewrite t_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 t_update_neq. assumption. intro X; inversion X.
Qed.
intros n.
destruct (par_body_n n { --> 0 }).
split; unfold t_update; reflexivity.
rename x into st.
inversion H as [H' [HX HY]]; clear H.
∃ (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_Eq_{1}. apply AS_Id. rewrite t_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 t_update_neq. assumption. intro X; inversion X.
Qed.
End CImp.
A Small-Step Stack Machine
Definition stack := list nat.
Definition prog := list sinstr.
Inductive stack_step : state → prog * stack → prog * stack → Prop :=
| SS_Push : ∀ st stk n p',
stack_step st (SPush n :: p', stk) (p', n :: stk)
| SS_Load : ∀ st stk i p',
stack_step st (SLoad i :: p', stk) (p', st i :: stk)
| SS_Plus : ∀ st stk n m p',
stack_step st (SPlus :: p', n::m::stk) (p', (m+n)::stk)
| SS_Minus : ∀ st stk n m p',
stack_step st (SMinus :: p', n::m::stk) (p', (m-n)::stk)
| SS_Mult : ∀ st stk n m p',
stack_step st (SMult :: p', n::m::stk) (p', (m*n)::stk).
Theorem stack_step_deterministic : ∀ st,
deterministic (stack_step st).
Definition stack_multistep st := multi (stack_step st).
Definition prog := list sinstr.
Inductive stack_step : state → prog * stack → prog * stack → Prop :=
| SS_Push : ∀ st stk n p',
stack_step st (SPush n :: p', stk) (p', n :: stk)
| SS_Load : ∀ st stk i p',
stack_step st (SLoad i :: p', stk) (p', st i :: stk)
| SS_Plus : ∀ st stk n m p',
stack_step st (SPlus :: p', n::m::stk) (p', (m+n)::stk)
| SS_Minus : ∀ st stk n m p',
stack_step st (SMinus :: p', n::m::stk) (p', (m-n)::stk)
| SS_Mult : ∀ st stk n m p',
stack_step st (SMult :: p', n::m::stk) (p', (m*n)::stk).
Theorem stack_step_deterministic : ∀ st,
deterministic (stack_step st).
Proof.
unfold deterministic. intros st x y_{1} y_{2} H_{1} H_{2}.
induction H_{1}; inversion H_{2}; reflexivity.
Qed.
unfold deterministic. intros st x y_{1} y_{2} H_{1} H_{2}.
induction H_{1}; inversion H_{2}; reflexivity.
Qed.
Definition stack_multistep st := multi (stack_step st).
Exercise: 3 stars, advanced (compiler_is_correct)
Remember the definition of compile for aexp given in the Imp chapter of Logical Foundations. We want now to prove compile correct with respect to the stack machine.
Definition compiler_is_correct_statement : Prop
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Theorem compiler_is_correct : compiler_is_correct_statement.
Proof.
(* FILL IN HERE *) Admitted.
☐
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Theorem compiler_is_correct : compiler_is_correct_statement.
Proof.
(* FILL IN HERE *) Admitted.