(** * Simple imperative programs
Version of 2/25/2009
Please include the pennkey of every member of your group
(* FILL IN HERE *)
*)
Require Export Logicsol.
(* ------------------------------------------------------- *)
(** * Informal proofs, again *)
(* Q: What is the relation between a formal proof of a
proposition P and an informal proof of the same proposition P?
A: The latter should *teach* the reader how to produce the
former.
Q: How much detail is needed?
A: There is no single right answer; rather, there is a range
of choices.
At one end of the spectrum, we can essentially give the
reader the whole formal proof (i.e., the informal proof
amounts to just transcribing the formal one into words).
This gives the reader the *ability* to reproduce the formal
one for themselves, but it doesn't *teach* them anything.
At the other end of the spectrum, we can say "The theorem
is true and you can figure out why for yourself if you
think about it hard enough." This is also not a good
teaching strategy, because usually writing the proof
requires some deep insights into the thing we're proving,
and most readers will give up before they rediscover all
the same insights as we did.
In the middle is the golden mean -- a proof that includes
all of the essential insights (saving the reader the hard
part of work that we went through to find the proof in the
first place) and clear high-level suggestions for the more
routine parts to save the reader from spending too much
time reconstructing these parts (e.g., what the IH says and
what must be shown in each case of an inductive proof), but
not so much detail that the main ideas are obscured.
-----------------
Another key point: if we're talking about a formal proof of a
proposition P and an informal proof of P, the proposition P
doesn't change. That is, formal and informal proofs are
TALKING ABOUT THE SAME WORLD and they must PLAY BY THE SAME
RULES.
In particular, whether we are talking about formal or informal
proofs, propositions and booleans are different things!
* Booleans are VALUES in the COMPUTATIONAL world. Every
expression of type [bool] (with no free variables) can be
simplified to either [true] or [false].
* Propositions are TYPES in the LOGICAL world. They are
either PROVABLE (i.e., there is some expression that has
this type) or not (there is no such expression). It
doesn't make sense to say that a proposition is
"equivalent to [true]," and it is not necessarily the
case that, if a proposition [P] is not provable, then
[~P] is provable.
We do sometimes use the words "true" and "false" when
referring to propositions. Strictly speaking, we should
not: a proposition is either provable or it is not.
*)
(* ------------------------------------------------------- *)
(** * Templates for informal proofs by induction *)
(* In the real world of mathematical communication, written
proofs range from extremely longwinded and pedantic to
extremely brief and telegraphic. The ideal is probably
somewhere in between, but while you are getting used to the
style it is better to go more toward the pedantic end. Also,
during the learning phase, it is probably helpful to have a
clear standard to compare against. So...
For the rest of the course, ALL your inductive proofs should
match one of the two following templates.
1) TEMPLATE FOR INFORMAL PROOFS BY INDUCTION OVER AN
INDUCTIVELY DEFINED SET:
THEOREM:
PROOF: By induction on n.
* Suppose n = c a1 ... ak, where <...and here we state
the IH for each of the a's that has type S, if any>.
We must show <...and here we restate P(c a1 ... ak)>.
* []
EXAMPLE
THEOREM: For all sets X, lists l : list X, and numbers n,
if length l = n then index (S n) l = None.
PROOF: By induction on l.
* Suppose l = []. We must show, for all numbers n,
that, if length [] = n, then index (S n) [] = None.
This follows immediately from the definition of index.
* Suppose l = x :: l' for some x and l', where length l'
= n' implies index (S n') l' = None, for any number n'.
We must show, for all n, that, if length (x::l') = n
then index (S n) (x::l') = None.
Let n be a number with length l = n. Since length l =
length (x::l') = S (length l'), it suffices to show
that index (S (length l')) l' = None. But this
follows directly from the induction hypothesis,
picking n' to be length l'. []
2) TEMPLATE FOR INFORMAL PROOFS BY INDUCTION OVER AN
INDUCTIVELY DEFINED PROPOSITION (I.E., "INDUCTION ON
DERIVATIONS"):
THEOREM: P," where Q is some
inductively defined proposition. (More generally, "For all
x y z, (Q x y z) -> (P x y z),">
PROOF: By induction on a derivation of Q.
* Suppose the final rule used to show Q is c. Then
<...and here we state the types of all of the a's
together with any equalities that follow from the
definition of the constructor and the IH for each of
the a's that has type Q, if there are any>. We must
show <...and here we restate P>.
* []
EXAMPLE
THEOREM: The <= relation is transitive -- i.e., for all
numbers n, m, and o, if n <= m and m <= o, then n <= o.
PROOF: By induction on a derivation of m <= o.
* Suppose the final rule used to show m <= o is le_n.
Then m = o and the result is immediate.
* Suppose the final rule used to show m <= o is le_S.
Then o = S o' for some o' with m <= o'. By induction
hypothesis, n <= o'.
But then, by le_S, n <= o. []
*)
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(** * Evaluating arithmetic expressions *)
Module AExp.
Inductive aexp : Set :=
| ANum : nat -> aexp
| APlus : aexp -> aexp -> aexp
| AMinus : aexp -> aexp -> aexp
| AMult : aexp -> aexp -> aexp.
Definition two_plus_two := APlus (ANum 2) (ANum 2).
(* Since we're going to be writing a lot of these arithmetic
expressions, let's introduce some concrete syntax that's nicer
to look at. *)
Notation "a1 '+++' a2" := (APlus a1 a2) (at level 50).
Notation "a1 '---' a2" := (AMinus a1 a2) (at level 50).
Notation "a1 '***' a2" := (AMult a1 a2) (at level 40).
Notation A0 := (ANum 0).
Notation A1 := (ANum 1).
Notation A2 := (ANum 2).
Notation A3 := (ANum 3).
Notation A4 := (ANum 4).
Notation A5 := (ANum 5).
Definition two_plus_two' := A2 +++ A2.
Fixpoint aeval (e : aexp) {struct e} : nat :=
match e with
| ANum n => n
| APlus a1 a2 => plus (aeval a1) (aeval a2)
| AMinus a1 a2 => minus (aeval a1) (aeval a2)
| AMult a1 a2 => mult (aeval a1) (aeval a2)
end.
Example test_aeval1:
aeval two_plus_two = 4.
Proof. reflexivity. Qed.
Inductive bexp : Set :=
| BTrue : bexp
| BFalse : bexp
| BEq : aexp -> aexp -> bexp
| BLtEq : aexp -> aexp -> bexp
| BNot : bexp -> bexp
| BAnd : bexp -> bexp -> bexp
| BOr : bexp -> bexp -> bexp.
Fixpoint beval (e : bexp) {struct e} : bool :=
match e with
| BTrue => true
| BFalse => false
| BEq a1 a2 => beq_nat (aeval a1) (aeval a2)
| BLtEq a1 a2 => ble_nat (aeval a1) (aeval a2)
| BNot b1 => negb (beval b1)
| BAnd b1 b2 => andb (beval b1) (beval b2)
| BOr b1 b2 => orb (beval b1) (beval b2)
end.
Notation "b1 '===' b2" := (BEq b1 b2) (at level 60).
Notation "b1 '<<=' b2" := (BLtEq b1 b2) (at level 60).
(* ------------------------------------------------------- *)
(** * Correctness of a simple optimization *)
Fixpoint optimize_0plus (e:aexp) {struct e} : aexp :=
match e with
| ANum n => ANum n
| APlus (ANum 0) e2 => optimize_0plus e2
| APlus e1 e2 => APlus (optimize_0plus e1) (optimize_0plus e2)
| AMinus e1 e2 => AMinus (optimize_0plus e1) (optimize_0plus e2)
| AMult e1 e2 => AMult (optimize_0plus e1) (optimize_0plus e2)
end.
Example test_optimize_0plus:
optimize_0plus (A2 +++ (A0 +++ (A0 +++ A1))) = A2 +++ A1.
Proof. reflexivity. Qed.
Theorem optimize_0plus_sound: forall e,
aeval (optimize_0plus e) = aeval e.
Proof.
intros e. induction e.
Case "ANum". reflexivity.
Case "APlus". destruct e1.
SCase "e1 = ANum n". destruct n.
SSCase "n = 0". simpl. apply IHe2.
SSCase "n <> 0". simpl. rewrite IHe2. reflexivity.
SCase "e1 = APlus e1_1 e1_2".
simpl. simpl in IHe1. rewrite IHe1. rewrite IHe2. reflexivity.
SCase "e1 = AMinus e1_1 e1_2".
simpl. simpl in IHe1. rewrite IHe1. rewrite IHe2. reflexivity.
SCase "e1 = AMult e1_1 e1_2".
simpl. simpl in IHe1. rewrite IHe1. rewrite IHe2. reflexivity.
Case "AMinus".
simpl. rewrite IHe1. rewrite IHe2. reflexivity.
Case "AMult".
simpl. rewrite IHe1. rewrite IHe2. reflexivity. Qed.
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(** * Tacticals *)
(* The repetition in this last proof is starting to be a little
annoying. It's still bearable here, but clearly, if either the
language of arithmetic expressions or the optimization being proved
sound were significantly more complex, it would start to be a real
problem.
So far, we've been doing all our proofs using just a small
handful of Coq's tactics and completely ignoring its very
powerful facilities for constructing proofs automatically.
This section introduces some of these facilities, and we will
see more over the next several chapters. Getting used to them
will take some energy -- Coq's automation is a power tool --
but it will allow us to scale up our efforts to more complex
definitions and more interesting properties without becoming
overwhelmed by boring, repetitive, or low-level details.
*)
(* ------------------------------------------------------- *)
(** ** The [try] tactical *)
(* "Tactical" is Coq's term for operations that manipulate
tactics as data -- higher-order tactics, if you will. *)
(* One very simple tactical is [try]: If [T] is a tactic, then
[try T] is a tactic that is just like [T] except that, if [T]
fails, [try T] does nothing at all (instead of failing). *)
(* ------------------------------------------------------- *)
(** ** The [;] tactical *)
(* Another very basic tactical is written [;]. If [T], [T1], ..., [Tn]
are tactics, then
T; [T1 | T2 | ... | Tn]
is a tactic that first performs [T] and then performs [T1] on
the first subgoal generated by [T], performs [T2] on the
second subgoal, etc.
In the special case where all of the [Ti]s are the same tactic
[T'], we can just write [T;T'] instead of:
T; [T' | T' | ... | T']
That is, if [T] and [T'] are tactics, then [T;T'] is a tactic
that first performs [T] and then performs [T'] on EACH SUBGOAL
generated by [T]. This is the form of [;] that is used most
often in practice. *)
(* Using [try] and [;] together, we can get rid of the repetition
in the above proof. *)
Theorem optimize_0plus_sound': forall e,
aeval (optimize_0plus e) = aeval e.
Proof.
intros e.
induction e;
(* Most cases follow directly by the IH *)
try (simpl; rewrite IHe1; rewrite IHe2; reflexivity).
Case "ANum". reflexivity.
Case "APlus".
destruct e1;
(* Most cases follow directly by the IH *)
try (simpl; simpl in IHe1; rewrite IHe1; rewrite IHe2; reflexivity).
(* The interesting case is when e1 = ANum n *)
SCase "e1 = ANum n". destruct n.
SSCase "n = 0". apply IHe2.
SSCase "n <> 0". simpl. rewrite IHe2. reflexivity. Qed.
(* In practice, Coq experts often use [try] with a tactic like
[induction] to take care of many similar "straightforward"
cases all at once. Naturally, this practice has an analog in
informal proofs. Here is an informal proof of our example
theorem that matches the structure of the formal one:
THEOREM: For all arithmetic expressions e,
aeval (optimize_0plus e) = aeval e.
PROOF: By induction on e. The AMinus and AMult cases
follow directly from the IH. The remaining cases are as follows:
* Suppose e = ANum n for some n. We must show
aeval (optimize_0plus (ANum n)) = aeval (ANum n).
This is immediate from the definition of optimize_0plus.
* Suppose e = APlus e1 e2 for some e1 and e2. We must show
aeval (optimize_0plus (APlus e1 e2)) = aeval (APlus e1 e2).
Consider the possible forms of e1. For most of them,
optimize_0plus simply calls itself recursively for the
subexpressions and rebuilds a new expression of the
same form as e1; in these cases, the result follows
directly from the IH.
The interesting case is when e1 = ANum n for some n.
If n = ANum 0, then
optimize_0plus (APlus e1 e2) = optimize_0plus e2
and the IH for e2 is exactly what we need. On the
other hand, if n = S n' for some n', then again
optimize_0plus simply calls itself recursively, and
the result follows from the IH. []
This proof can still be improved: the first case (for e = ANum
n) is very trivial -- even more trivial than the cases that we
said simply followed from the IH -- yet we have chosen to
write it out in full. It would be better and clearer to drop
it and just say, at the top, "Most cases are either immediate
or direct from the IH. The only interesting case is the one
for APlus..."
Of course, we'd like to do the same thing in our formal proof
too! Here's how this looks:
*)
Theorem optimize_0plus_sound'': forall e,
aeval (optimize_0plus e) = aeval e.
Proof.
intros e.
induction e;
(* Most cases follow directly by the IH *)
try (simpl; rewrite IHe1; rewrite IHe2; reflexivity);
(* ... or are immediate by definition *)
try (reflexivity).
(* The interesting case is when e = APlus (ANum 0) e2. *)
Case "APlus".
destruct e1;
try (simpl; simpl in IHe1; rewrite IHe1; rewrite IHe2; reflexivity).
SCase "e1 = ANum n". destruct n.
SSCase "n = 0". apply IHe2.
SSCase "n <> 0". simpl. rewrite IHe2. reflexivity. Qed.
(* ------------------------------------------------------- *)
(** ** Defining new tactic notations *)
(* Coq also provides some handy ways to define "shorthand
tactics" that, when invoked, apply several tactics at the same
time. *)
Tactic Notation "simpl_and_try" tactic(c) :=
simpl;
try c.
(* Here's a more interesting use of this feature... *)
(* ------------------------------------------------------- *)
(** ** Bulletproofing case analyses *)
(* Being able to deal with most of the cases of an [induction] or
[destruct] all at the same time is very convenient, but it can
also be a little confusing. One problem that often comes up
is that MAINTAINING proofs written in this style can be
difficult. For example, suppose that, later, we extended the
definition of [aexp] with another constructor that also
required a special argument. The above proof might break
because Coq generated the subgoals for this constructor before
the one for APlus, so that, at the point when we start working
on the [APlus] case, Coq is actually expecting the argument
for a completely different constructor. What we'd like is to
get a sensible error message saying "I was expecting the
[AFoo] case at this point, but the proof script is talking
about [APlus]." Here's a nice little trick that smoothly
achieves this. *)
Tactic Notation "aexp_cases" tactic(first) tactic(c) :=
first;
[ c "ANum" | c "APlus" | c "AMinus" | c "AMult" ].
(* If [e] is a variable of type [aexp], then doing
aexp_cases (induction e) (Case)
will perform an induction on [e] (the same as if we had just
typed [induction e]) and ALSO add a "Case" tag to each subgoal
labeling which constructor it comes from.
*)
(* Exercise: 3 stars (optimize_0plus_b) *)
(* Since the optimize_0plus tranformation doesn't change the
value of aexps, we should be able to apply it to all the aexps
that appear in a bexp without changing the bexp's value.
Write a function which performs that transformation on bexps,
and prove it is sound. Use the tacticals we've just seen to
make the proof as elegant as possible. *)
(* FILL IN HERE *)
(* Exercise: 4 stars (optimizer) *)
(* DESIGN EXERCISE: The optimization implemented by our
optimize_0plus function is only one of many imaginable
optimizations on arithmetic and boolean expressions. Write a
more sophisticated optimizer and prove it correct.
FILL IN HERE
*)
End AExp.
(* ------------------------------------------------------- *)
(** * A couple more handy tactics *)
(*
clear H remove hypothesis H from the context
subst x find an assumption [x = e] or [e = x]
in the context, replace x with e
throughout the context and current goal,
and clear the assumption
subst substitute away ALL assumptions of the
form [x = e] or [e = x]
assumption tries to find a hypothesis [H] in the context
that exactly matches the goal; if one is found,
behaves just like [apply H]
*)
(* We'll see many examples of these in the proofs below... *)
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(** * While programs *)
(* ----------------------------------------------------- *)
(** ** Mappings *)
(* In the rest of the course, we'll often need to talk about
"identifiers," such as program variables. We could use
strings for this, or (as in a real compiler) some kind of
fancier structures like symbols from a symbol table. For
simplicity, though, let's just use natural numbers as
identifiers. *)
Definition id := nat.
(* Now, a [mapping] is a partial function from identifiers to
members of some other type, [X]. We use an [option] in the
result type to represent partiality: A result of [None] means
that the mapping is not defined for the given id. *)
Definition mapping (X : Set) := id -> option X.
Definition lookup (X : Set) (k : id) (f : mapping X)
: option X :=
f k.
Implicit Arguments lookup [X].
Definition empty_mapping (X:Set) : (mapping X) := constfun None.
Definition extend (X : Set) (f : mapping X) (k:id) (x:X) :=
override f k (Some x).
Implicit Arguments extend [X].
Definition remove (X : Set) (f : mapping X) (k:id) :=
override f k None.
Implicit Arguments remove [X].
(* Since the critical functions on mappings, [extend] and
[remove], are implemented in terms of the [override] operator
that we studied before, their properties can also be derived
from those of [override]. *)
Theorem extend_eq : forall X x x' k (f : mapping X),
x = x' ->
lookup k (extend f k x) = Some x'.
Proof.
intros X x x' k f Heq. rewrite Heq.
unfold lookup, extend.
apply override_eq. Qed.
(* Exercise: 2 stars *)
Theorem extend_neq : forall X o1 x2 k1 k2 (f : mapping X),
lookup k1 f = o1 ->
beq_nat k2 k1 = false ->
lookup k1 (extend f k2 x2) = o1.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* Exercise: 2 stars, optional *)
Theorem extend_example : forall (X:Set) (b:bool),
lookup 3 (extend (empty_mapping _) 2 b) = None.
Proof.
(* Before starting to play with tactics, make sure you
understand exactly what the theorem is saying! *)
(* OPTIONAL EXERCISE *) Admitted.
(* Exercise: 2 stars, optional *)
Theorem extend_shadow : forall X x1 x2 k1 k2 (f : mapping X),
lookup k1 (extend (extend f k2 x1) k2 x2) = lookup k1 (extend f k2 x2).
Proof.
(* OPTIONAL EXERCISE *) Admitted.
(* Exercise: 2 stars, optional *)
Theorem extend_same : forall X x1 k1 k2 (f : mapping X),
lookup k1 f = Some x1 ->
lookup k2 (extend f k1 x1) = lookup k2 f.
Proof.
(* OPTIONAL EXERCISE *) Admitted.
(* Exercise: 2 stars, optional *)
Theorem extend_permute : forall X x1 x2 k1 k2 k3 (f : mapping X),
false = beq_nat k2 k1
-> lookup k3 (extend (extend f k2 x1) k1 x2)
= lookup k3 (extend (extend f k1 x2) k2 x1).
Proof.
(* OPTIONAL EXERCISE *) Admitted.
(* --------------------------------------------------- *)
(** ** WHILE program syntax *)
Definition state := (mapping nat).
Definition empty_state := empty_mapping nat.
(* Adding variables to what we had before *)
Inductive aexp : Set :=
| ANum : nat -> aexp
| AId : id -> aexp
| APlus : aexp -> aexp -> aexp
| AMinus : aexp -> aexp -> aexp
| AMult : aexp -> aexp -> aexp.
Tactic Notation "aexp_cases" tactic(first) tactic(c) :=
first;
[ c "ANum" | c "AId" | c "APlus" | c "AMinus" | c "AMult" ].
(* Same notations as before... *)
Notation A0 := (ANum 0).
Notation A1 := (ANum 1).
Notation A2 := (ANum 2).
Notation A3 := (ANum 3).
Notation A4 := (ANum 4).
Notation A5 := (ANum 5).
Notation A6 := (ANum 6).
Notation "a1 '***' a2" := (AMult a1 a2)
(at level 50).
Notation "a1 '---' a2" := (AMinus a1 a2)
(at level 40).
Notation "a1 '+++' a2" := (APlus a1 a2)
(at level 40).
(* ...plus one more: *)
Notation "'!' X" := (AId X)
(at level 30).
(* Shorthands for variables: *)
Definition X : id := 0.
Definition Y : id := 1.
Definition Z : id := 2.
(* Note that the choice of variable names (X, Y, Z) clashes a bit
with our earlier use of uppercase letters for Sets. Since
we're not using polymorphism heavily in this section, this
overloading will hopefully not cause confusion. *)
(* Same bexps as before (using the new aexps) *)
Inductive bexp : Set :=
| BTrue : bexp
| BFalse : bexp
| BEq : aexp -> aexp -> bexp
| BLtEq : aexp -> aexp -> bexp
| BNot : bexp -> bexp
| BAnd : bexp -> bexp -> bexp
| BOr : bexp -> bexp -> bexp.
Notation "b1 '===' b2" := (BEq b1 b2)
(at level 60).
Notation "b1 '<<=' b2" := (BLtEq b1 b2)
(at level 60).
Tactic Notation "bexp_cases" tactic(first) tactic(c) :=
first;
[ c "BTrue" | c "BFalse" |
c "BEq" | c "BLtEq" |
c "BNot" | c "BAnd" | c "BOr" ].
Inductive com : Set :=
| CSkip : com
| CAss : id -> aexp -> com
| CSeq : com -> com -> com
| CIf : bexp -> com -> com -> com
| CWhile : bexp -> com -> com.
Tactic Notation "com_cases" tactic(first) tactic(c) :=
first;
[ c "CSkip" | c "CAss" | c "CSeq" | c "CIf" | c "CWhile" ].
Notation "'skip'" :=
CSkip.
Notation "c1 ; c2" :=
(CSeq c1 c2) (at level 80, right associativity).
Notation "l '::=' a" :=
(CAss l a) (at level 60).
Notation "'while' b 'do' c" :=
(CWhile b c) (at level 80, right associativity).
Notation "'testif' e1 'then' e2 'else' e3" :=
(CIf e1 e2 e3) (at level 80, right associativity).
(* Note that [CIf] is written [testif...then...else...] to avoid
confusion with Coq's existing [if...then...else...] syntactic
sugar. *)
(* ------------------------------------------------------- *)
(* Some programs... *)
Definition plus2 : com :=
X ::= !X +++ A2.
(* Note that the notations we introduced make it easy to write
down commands that look close to how they would in a real
imperative programming language; for example, here's what
[plus2] looks like fully expanded: *)
Example plus2_notation :
plus2 =
CAss 0 (APlus (AId 0) (ANum 2)).
Proof. reflexivity. Qed.
Definition XtimesYinZ : com :=
Z ::= !X *** !Y.
(* loops *)
Definition subtract_slowly_body : com :=
Z ::= !Z --- A1;
X ::= !X --- A1.
Definition subtract_X_slowly : com :=
while BNot (!X === A0) do
subtract_slowly_body.
Definition subtract_3_from_5_slowly : com :=
X ::= A3;
Z ::= A5;
while BNot (!X === A0) do
subtract_slowly_body.
(* an infinite loop *)
Definition loop : com :=
while BTrue do
skip.
(* factorial *)
Definition fact_body : com :=
Z ::= !Z *** !X;
X ::= !X --- A1.
Definition pfactorial : com :=
while BLtEq A1 (!X) do
fact_body.
(* Note that pfactorial should be run in a state where Z is 1
We could enforce this with the following program:
*)
Definition pfactorial' : com :=
Z ::= ANum 1;
pfactorial.
(* exponentiation *)
Definition exp_body : com :=
Z ::= !Z *** !X;
Y ::= !Y --- A1.
Definition pexp : com :=
while BNot (!Y === (ANum 0)) do
exp_body.
(* Note that pexp should be run in a state where Z is 1 *)
(* Exercise: 2 stars *)
(* Write a While program that sums the numbers from 1 to X
(inclusive: 1 + 2 + ... + X) in the variable Y. *)
(* FILL IN HERE *)
(* Exercise: 2 stars *)
(* Write a While program that sets Z to 0 if X is even and sets Z
to 1 otherwise. *)
(* FILL IN HERE *)
(* --------------------------------------------------- *)
(** ** Evaluation *)
Fixpoint aeval (st : state) (e : aexp) {struct e} : nat :=
match e with
| ANum n => n
| AId l => match lookup l st with
| Some n => n
| None => O
end
| APlus a1 a2 => plus (aeval st a1) (aeval st a2)
| AMinus a1 a2 => minus (aeval st a1) (aeval st a2)
| AMult a1 a2 => mult (aeval st a1) (aeval st a2)
end.
Fixpoint beval (st : state) (e : bexp) {struct e} : bool :=
match e with
| BTrue => true
| BFalse => false
| BEq a1 a2 => beq_nat (aeval st a1) (aeval st a2)
| BLtEq a1 a2 => ble_nat (aeval st a1) (aeval st a2)
| BNot b1 => negb (beval st b1)
| BAnd b1 b2 => andb (beval st b1) (beval st b2)
| BOr b1 b2 => orb (beval st b1) (beval st b2)
end.
(* First try at an evaluator for commands, omitting CWhile *)
Fixpoint ceval_step1 (st : state) (c : com) {struct c} : state :=
match c with
| CSkip =>
st
| CAss l a1 =>
extend st l (aeval st a1)
| CSeq c1 c2 =>
let st' := ceval_step1 st c1 in
ceval_step1 st' c2
| CIf b c1 c2 =>
if (beval st b) then ceval_step1 st c1 else ceval_step1 st c2
| CWhile b1 c1 =>
st (* bogus *)
end.
(* Second try, using an extra "step index" to ensure that
evaluation always terminates *)
Fixpoint ceval_step2 (st : state) (c : com) (i : nat) {struct i} : state :=
match i with
| O => empty_state
| S i' =>
match c with
| CSkip =>
st
| CAss l a1 =>
extend st l (aeval st a1)
| CSeq c1 c2 =>
let st' := ceval_step2 st c1 i' in
ceval_step2 st' c2 i'
| CIf b c1 c2 =>
if (beval st b) then ceval_step2 st c1 i' else ceval_step2 st c2 i'
| CWhile b1 c1 =>
if (beval st b1)
then let st' := ceval_step2 st c1 i' in
ceval_step2 st' (CWhile b1 c1) i'
else st
end
end.
(* NOTE: It is tempting to think that the index [i] here is
counting the "number of steps of evaluation." But if you look
closely you'll see that this is not the case: for example, in
the [CSeq] rule, the same [i] is passed to both recursive
calls. Understanding the exact way that [i] is treated will
be important in the proof of [ceval__ceval_step], which is
given as an exercise below. *)
Definition bind_option (X Y : Set) (xo : option X) (f : X -> option Y)
: option Y :=
match xo with
| None => None
| Some x => f x
end.
Implicit Arguments bind_option [X Y].
(* Third try, returning an [option state] instead of just a
[state] so that we can distinguish between normal and abnormal
termination. *)
Fixpoint ceval_step (st : state) (c : com) (i : nat)
{struct i} : option state :=
match i with
| O => None
| S i' =>
match c with
| CSkip =>
Some st
| CAss l a1 =>
Some (extend st l (aeval st a1))
| CSeq c1 c2 =>
bind_option
(ceval_step st c1 i')
(fun st' => ceval_step st' c2 i')
| CIf b c1 c2 =>
if (beval st b) then ceval_step st c1 i' else ceval_step st c2 i'
| CWhile b1 c1 =>
if (beval st b1)
then bind_option
(ceval_step st c1 i')
(fun st' => ceval_step st' (CWhile b1 c1) i')
else Some st
end
end.
(* A better way: define [ceval] as a RELATION, rather than
a (total) FUNCTION. *)
Inductive ceval : state -> com -> state -> Prop :=
| CESkip : forall st,
ceval st CSkip st
| CEAss : forall st a1 n l,
aeval st a1 = n ->
ceval st (CAss l a1) (extend st l n)
| CESeq : forall c1 c2 st st' st'',
ceval st c1 st' ->
ceval st' c2 st'' ->
ceval st (CSeq c1 c2) st''
| CEIfTrue : forall st st' b1 c1 c2,
beval st b1 = true ->
ceval st c1 st' ->
ceval st (CIf b1 c1 c2) st'
| CEIfFalse : forall st st' b1 c1 c2,
beval st b1 = false ->
ceval st c2 st' ->
ceval st (CIf b1 c1 c2) st'
| CEWhileEnd : forall b1 st c1,
beval st b1 = false ->
ceval st (CWhile b1 c1) st
| CEWhileLoop : forall st st' st'' b1 c1,
beval st b1 = true ->
ceval st c1 st' ->
ceval st' (CWhile b1 c1) st'' ->
ceval st (CWhile b1 c1) st''.
(* Exercise: 3 stars (aeval_beval_rel) *)
(* Write relations [aeval_rel] and [beval_rel] in the same style
as [ceval], and prove that they are equivalent to [aeval] and
[beval]. *)
(* FILL IN HERE *)
Tactic Notation "ceval_cases" tactic(first) tactic(c) := first; [
c "CESkip" | c "CEAss" | c "CESeq" | c "CEIfTrue" | c
"CEIfFalse" | c "CEWhileEnd" | c "CEWhileLoop" ].
Example ceval_example1:
ceval
empty_state
(X ::= A2; testif !X <<= A1 then Y ::= A3 else Z ::= A4)
(extend (extend empty_state X 2) Z 4).
Proof.
apply CESeq with (extend empty_state X 2).
Case "assignment command".
apply CEAss. reflexivity.
Case "if command".
apply CEIfFalse.
reflexivity.
apply CEAss. reflexivity. Qed.
(* And here's the similar output of ceval_step *)
Eval compute in
(ceval_step empty_state
(X ::= A2;
testif !X <<= A1 then Y ::= A3 else Z ::= A4)
500).
Eval compute in
(match ceval_step empty_state
(X ::= A2;
testif !X <<= A1 then Y ::= A3 else Z ::= A4)
500
with
| None => (None,None) (* shouldn't happen, if 500 is big enough *)
| Some st => (lookup X st, lookup Z st)
end).
(* Exercise: 2 stars *)
Example ceval_example2:
ceval
empty_state
(X ::= A0; Y ::= A1; Z ::= A2)
(extend (extend (extend empty_state X 0) Y 1) Z 2).
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* ------------------------------------------------------- *)
(** ** Equivalence of step-indexed and relational evaluation *)
Theorem ceval_step__ceval: forall c st st',
(exists i, ceval_step st c i = Some st')
-> ceval st c st'.
Proof.
intros c st st' H.
inversion H as [i E].
clear H.
generalize dependent st'.
generalize dependent st.
generalize dependent c.
induction i as [| i' ].
Case "i = 0 -- contradictory".
intros c st st' H. inversion H.
Case "i = S i'".
intros c st st' H.
(com_cases (destruct c) SCase); simpl in H; inversion H; subst; clear H.
SCase "CSkip". apply CESkip.
SCase "CAss". apply CEAss. reflexivity.
SCase "CSeq".
remember (ceval_step st c1 i') as r1. destruct r1.
SSCase "Evaluation of r1 terminates normally".
apply CESeq with s.
apply IHi'. rewrite Heqr1. reflexivity.
apply IHi'. simpl in H1. apply H1.
SSCase "Evaluation of r1 terminates abnormally -- contradiction".
inversion H1.
SCase "CIf".
remember (beval st b) as r. destruct r.
SSCase "r = true".
apply CEIfTrue. rewrite Heqr. reflexivity.
apply IHi'. apply H1.
SSCase "r = false".
apply CEIfFalse. rewrite Heqr. reflexivity.
apply IHi'. apply H1.
SCase "CWhile". remember (beval st b) as r. destruct r.
SSCase "r = true".
remember (ceval_step st c i') as r1. destruct r1.
SSSCase "r1 = Some s".
apply CEWhileLoop with s. rewrite Heqr. reflexivity.
apply IHi'. rewrite Heqr1. reflexivity.
apply IHi'. simpl in H1. apply H1.
SSSCase "r1 = None".
inversion H1.
SSCase "r = false".
inversion H1.
apply CEWhileEnd.
rewrite Heqr. subst. reflexivity. Qed.
(* Exercise: 4 stars (ceval_step__ceval_inf) *)
(* Write an informal proof of [ceval_step__ceval], following the
template at the top of the file. (The template for case
analysis on an inductively defined value should look the same
as for induction, except that there are no induction
hypothesis.) Make your proof communicate the main ideas to a
human reader; do *not* simply transcribe the steps of the
formal proof.
(* FILL IN HERE *)
*)
Theorem ceval_step_more: forall i1 i2 st st' c,
i1 <= i2 -> ceval_step st c i1 = Some st' ->
ceval_step st c i2 = Some st'.
Proof.
induction i1 as [|i1']; intros i2 st st' c Hle Hceval.
Case "i1 = 0".
inversion Hceval.
Case "i1 = S i1'".
destruct i2 as [|i2']. inversion Hle.
com_cases (destruct c) SCase.
SCase "CSkip".
simpl in Hceval. inversion Hceval.
reflexivity.
SCase "CAss".
simpl in Hceval. inversion Hceval.
reflexivity.
SCase "CSeq".
simpl in Hceval. simpl. apply le_S_n in Hle.
remember (ceval_step st c1 i1') as i1'o.
destruct i1'o.
SSCase "i1'o = Some".
apply sym_eq in Heqi1'o.
apply (IHi1' i2') in Heqi1'o; try assumption.
rewrite Heqi1'o. simpl. simpl in Hceval.
apply (IHi1' i2') in Hceval; try assumption.
SSCase "i1'o = None".
inversion Hceval.
SCase "CIf".
simpl in Hceval. simpl. apply le_S_n in Hle.
remember (beval st b) as bval.
destruct bval; apply (IHi1' i2') in Hceval; assumption.
SCase "CWhile".
simpl in Hceval. simpl.
destruct (beval st b); try assumption.
apply le_S_n in Hle.
remember (ceval_step st c i1') as i1'o.
destruct i1'o.
SSCase "i1'o = Some".
apply sym_eq in Heqi1'o.
apply (IHi1' i2') in Heqi1'o; try assumption.
rewrite -> Heqi1'o. simpl. simpl in Hceval.
apply (IHi1' i2') in Hceval; try assumption.
SSCase "i1'o = None".
simpl in Hceval. inversion Hceval. Qed.
(* Exercise: 4 stars *)
(* Finish the following proof. You'll need [ceval_step_more] in
a few places, as well as some basic facts about [<=] and [plus]. *)
Theorem ceval__ceval_step: forall c st st',
ceval st c st'
-> exists i, ceval_step st c i = Some st'.
Proof.
intros c st st' Hce.
ceval_cases (induction Hce) Case.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem ceval_and_ceval_step_coincide: forall c st st',
ceval st c st'
<-> exists i, ceval_step st c i = Some st'.
Proof.
intros c st st'.
split. apply ceval__ceval_step. apply ceval_step__ceval.
Qed.
(* ------------------------------------------------------- *)
(** ** Reasoning about programs *)
Theorem plus2_spec : forall st n st',
lookup X st = Some n ->
ceval st plus2 st' ->
lookup X st' = Some (plus n 2).
Proof.
intros st n st' HX Heval.
(* inverting Heval essentially forces coq to expand one step of the ceval
computation - in this case revealing that st' must be st extended with
the new value of X, since plus2 is an assignment *)
inversion Heval. subst.
apply extend_eq. simpl. rewrite -> HX.
reflexivity. Qed.
(* Exercise: 3 stars (XtimesYinZ_spec) *)
(* State and prove a specification of the XtimesYinZ while
program *)
(* FILL IN HERE *)
(* Exercise: 3 stars *)
Theorem loop_never_stops : forall st st',
~(ceval st loop st').
Proof.
intros st st' contra. unfold loop in contra.
remember (while BTrue do skip) as loopdef.
(* Proceed by induction on the assumed derivation showing that
loopdef terminates. Most of the cases are immediately
contradictory (and so can be solved in one step with
[inversion]). *)
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Fixpoint no_whiles (c : com) {struct c} : bool :=
match c with
| CSkip => true
| CAss _ _ => true
| CSeq c1 c2 => andb (no_whiles c1) (no_whiles c2)
| CIf _ ct cf => andb (no_whiles ct) (no_whiles cf)
| CWhile _ _ => false
end.
(* Exercise: 4 stars *)
(* On the other hand, programs that don't involve while loops
always terminate. State and prove a theorem that says this. *)
(* FILL IN HERE *)