(** * Simple imperative programs, part 2
Version of 3/4/2009 *)
Require Export Whilesol.
(* ------------------------------------------------------- *)
(** * Advice for the homework *)
(* (1) We've tried to make sure that most of the Coq proofs we
ask you to do are similar to proofs that we've provided.
Before starting to work on the homework problems, take the
time to work through our proofs (both informally, on
paper, and in Coq) and make sure you understand them in
detail. This will save you a lot of time.
(2) Here's another thing that will save a lot of time. The
Coq proofs we're doing now are sufficiently complicated
that it is more or less impossible to complete them simply
by "following your nose" (or random hacking!). You need
to start with an idea in your mind about why the property
is true and how the proof is going to go. The best way to
do this is actually to write out an informal proof on
paper -- one that convinces you of the truth of the
theorem -- before starting to work on the formal one.
(3) Use automation to save work! Some of these proofs are
extremely long and tedious if you try to write out all the
cases explicitly.
*)
(* ------------------------------------------------------- *)
(** * A useful little hack *)
(* We'll use this lemma in a few places where we'd like you to
finish just one case in the middle of a proof. Don't use it
yourself (in anything you turn in)... it's cheating! *)
Lemma cheating : forall P, P.
Proof. Admitted.
(* ------------------------------------------------------- *)
(** * Notation for evaluation *)
(* Last week, we defined a proposition [ceval], indexed by two
states and a command. Formally, this definition is no
different from other indexed propositions we've defined, like
[ev] or [le]. When discussing [ceval], though, it's
convenient (and standard) to use some special notations.
First, from now on, we'll write the Coq proposition [ceval st
c st'] as [c / st --> st'], which can be read as "[c] takes
state [st] to [st']".
Second, we will sometimes (especially in informal discussions)
write the rules for [ceval] in a more "graphical" form called
INFERENCE RULES, where the premises above the line allow you
to derive the conclusion below the line. For example, the
constructor CESeq would be written like this as an inference
rule:
c1 / st --> st' c2 / st' --> st''
------------------------------------ CESeq
c1;c2 / st --> st''
Such rules can read either from the bottom up...
"To show that [c1;c2] takes [st] to [st''], then by rule
CESeq it suffices to show that [c1] takes [st] to [st']
and [c2] takes [st'] to [st'']."
...or from the top down:
"If [c1] takes [st] to [st'] and [c2] takes [st'] to
[st''], then [c1;c2] takes [st] to [st''] by rule CESeq."
Formally, there is nothing deep or complex about such rules:
they are just implications. You can read the rule name on the
right as the name of the constructor and read both the spaces
between premises above the line and the line itself as [->].
*)
Notation "c1 '/' st '-->' st'" := (ceval st c1 st') (at level 40).
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(** * Determinacy of evaluation *)
(* Changing from a computational to a relational definition of
evaluation is a good move because it allows us to escape from
the artificial requirement (imposed by Coq's restrictions on
Fixpoint definitions) that evaluation should be a total
function. But it also raises a question: Is the second
definition of evaluation even a partial function? That is, is
it possible that, beginning from the same state [st], we could
evaluate some command [c] in different ways to reach two
different output states [st'] and [st'']?
In fact, this is not possible: the evaluation relation [ceval]
is a partial function. Here's the proof: *)
Theorem ceval_deterministic: forall c st st1 st2,
c / st --> st1
-> c / st --> st2
-> st1 = st2.
Proof.
intros c st st1 st2 E1 E2.
generalize dependent st2.
(ceval_cases (induction E1) Case); intros st2 E2; inversion E2; subst.
Case "CESkip". reflexivity.
Case "CEAss". reflexivity.
Case "CESeq".
assert (st' = st'0) as EQ1.
SCase "Proof of assertion". apply IHE1_1; assumption.
subst st'0.
apply IHE1_2. assumption.
Case "CEIfTrue".
SCase "b1 evaluates to true".
apply IHE1. assumption.
SCase "b1 evaluates to false (contradiction)".
rewrite H in H5. inversion H5.
Case "CEIfFalse".
SCase "b1 evaluates to true (contradiction)".
rewrite H in H5. inversion H5.
SCase "b1 evaluates to false".
apply IHE1. assumption.
Case "CEWhileEnd".
SCase "b1 evaluates to true".
reflexivity.
SCase "b1 evaluates to false (contradiction)".
rewrite H in H2. inversion H2.
Case "CEWhileLoop".
SCase "b1 evaluates to true (contradiction)".
rewrite H in H4. inversion H4.
SCase "b1 evaluates to false".
assert (st' = st'0) as EQ1.
SSCase "Proof of assertion". apply IHE1_1; assumption.
subst st'0.
apply IHE1_2. assumption. Qed.
(* A slicker proof, using the step-indexed definition of evaluation *)
Theorem ceval_deterministic' : forall c st st1 st2,
c / st --> st1
-> c / st --> st2
-> st1 = st2.
Proof.
intros c st st1 st2 He1 He2.
apply ceval__ceval_step in He1.
apply ceval__ceval_step in He2.
destruct He1 as [i1 He1].
destruct He2 as [i2 He2].
assert (i1 <= i1 + i2) as Hle1 by apply le_plus.
assert (i2 <= i1 + i2) as Hle2 by (rewrite plus_comm; apply le_plus).
assert (ceval_step st c (i1 + i2) = Some st1).
apply ceval_step_more with i1; assumption.
assert (ceval_step st c (i1 + i2) = Some st2).
apply ceval_step_more with i2; assumption.
rewrite -> H in H0. inversion H0. reflexivity. Qed.
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(** * Behavioral equivalence *)
(* In the last lecture, we investigated the correctness of some
very simple program transformations. There, the programming
language we were considering was the first version of the
language of arithmetic expressions -- with no variables -- so
it was very easy to define what it MEANS for a program
transformation to be correct: it should always yield a program
that evaluates to the same number as the original.
To talk about the correctness of program transformations in
the full WHILE language, we need to think about the role of
the state.
For aexps and bexps, the definition we want is clear. We say
that two aexps or bexps are "BEHAVIORALLY EQUIVALENT" if they
evaluate to the same result IN EVERY STATE.
For commands, the situation is a little more subtle. We can't
simply say "two commands are behaviorally equivalent if they
evaluate to the same ending state whenever they are run in the
same initial state," because some commands (in some starting
states) don't terminate in any final state at all! What we
need to say instead is this: two commands are behaviorally
equivalent if, for any given starting state, they either both
diverge or both terminate in the same final state. *)
(* ------------------------------------------------------- *)
(** ** Definitions *)
Definition aequiv (a1 a2 : aexp) : Prop :=
forall (st:state), aeval st a1 = aeval st a2.
Definition bequiv (b1 b2 : bexp) : Prop :=
forall (st:state), beval st b1 = beval st b2.
Definition cequiv (c1 c2 : com) : Prop :=
forall (st st':state), (c1 / st --> st') <-> (c2 / st --> st').
(* ------------------------------------------------------- *)
(** ** Examples of program equivalence *)
Theorem aequiv_example:
aequiv (!X --- !X) A0.
Proof.
unfold aequiv. intros st. unfold aeval.
destruct (lookup X st). apply minus_n_n. reflexivity. Qed.
Theorem bequiv_example:
bequiv (!X --- !X === A0) BTrue.
Proof.
unfold bequiv. intros st. unfold beval.
(* Make sure you understand why this [assert] is here -- i.e.,
why would things go wrong if we tried to get away without
it. *)
assert ((aeval st (!X --- !X)) = (aeval st A0)) as H.
apply aequiv_example. rewrite H. apply sym_eq. apply beq_nat_refl. Qed.
Theorem skip_left: forall c,
cequiv
(skip; c)
c.
Proof.
unfold cequiv. intros c st st'.
split; intros H.
Case "->".
inversion H. subst.
inversion H3. subst.
assumption.
Case "<-".
apply CESeq with st.
apply CESkip.
assumption. Qed.
(* Exercise: 2 stars (skip_right) *)
Theorem skip_right: forall c,
cequiv
(c; skip)
c.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem CIf_true_simple: forall c1 c2,
cequiv
(testif BTrue then c1 else c2)
c1.
Proof.
intros c1 c2.
split; intros H.
Case "->".
inversion H; subst. assumption. inversion H5.
Case "<-".
apply CEIfTrue. reflexivity. assumption. Qed.
Theorem CIf_true: forall b c1 c2,
bequiv b BTrue
-> cequiv
(testif b then c1 else c2)
c1.
Proof.
intros b c1 c2 Hb.
split; intros H.
Case "->".
inversion H; subst.
SCase "b evaluates to true".
assumption.
SCase "b evaluates to false (contradiction)".
unfold bequiv in Hb.
rewrite -> Hb in H5.
inversion H5.
Case "<-".
apply CEIfTrue; try assumption.
unfold bequiv in Hb.
rewrite -> Hb. reflexivity. Qed.
(* An informal proof of CIf_true:
THEOREM: forall b c1 c2, if b is equivalent to BTrue,
then (testif b then c1 else c2) is equivalent to c1.
PROOF:
(->) We are given that b is equivalent to BTrue. We must
show, for all st and st', that if (testif b then c1 else c2) /
st --> st' then c1 / st --> st'.
There are only two ways we can have (testif b then c1 else
c2) / st --> st': using CEIfTrue and CEIfFalse.
- Suppose the final rule used to show (testif b then c1 else
c2) / st --> st' was CEIfTrue. We then have, by the
premises of CEIfTrue, that c1 / st --> st'. This is exactly
what we set out to prove.
- Suppose the final rule used to show (testif b then c1 else
c2) / st --> st' was CEIfFalse. We then know that [beval st
b = false] and c2 / st --> st'.
Recall that b is equivalent to BTrue, i.e. forall st, [beval
st b = beval st BTrue]. In particular, this means that
[beval st b = true], since [beval st BTrue = true]. But
this is a contradiction, since CEIfFalse requires that
[beval st b = false]. We therefore conclude that the final
rule could not have been CEIfFalse.
(<-) Again, we are given that b is equivalent to BTrue. We
must show, for all st and st', that if c1 / st --> st'
then (testif b then c1 else c2) / st --> st'.
Since [b] is equivalent to [BTrue], we know that [beval st b] =
[beval st BTrue] = [true]. Together with the assumption that c1 /
st --> st', we can apply CEIfTrue to derive [(testif b then c1
else c2) / st --> st']. []
*)
(* Exercise: 2 stars (CIf_false) *)
Theorem CIf_false: forall b c1 c2,
bequiv b BFalse
-> cequiv
(testif b then c1 else c2)
c2.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem CWhile_true_nonterm : forall b c st st',
bequiv b BTrue
-> ~( (while b do c) / st --> st' ).
Proof.
intros b c st st' Hb.
intros H.
remember (while b do c) as cw.
(ceval_cases (induction H) Case);
(* most rules don't apply, and we can rule them out by inversion *)
inversion Heqcw; subst; clear Heqcw.
Case "CEWhileEnd". (* contradictory -- b is always true! *)
unfold bequiv in Hb. rewrite Hb in H. inversion H.
Case "CEWhileLoop". (* immediate from the IH *)
apply IHceval2. reflexivity. Qed.
(* Exercise: 3 stars (CWhile_nonterm_understanding) *)
(* Explain what the lemma CWhile_true_nonterm means in English.
(* FILL IN HERE *)
*)
(* Exercise: 2 stars (CWhile_true) *)
Theorem CWhile_true: forall b c,
bequiv b BTrue
-> cequiv
(while b do c)
(while BTrue do skip).
Proof.
(* You'll want to use [CWhile_true_nonterm] here... *)
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem CWhile_false : forall b c,
bequiv b BFalse
-> cequiv
(while b do c)
skip.
Proof.
intros b c Hb.
split; intros H.
Case "->".
inversion H; subst.
SCase "CEWhileEnd".
apply CESkip.
SCase "CEWhileLoop".
unfold bequiv in Hb.
rewrite -> Hb in H2. inversion H2.
Case "<-".
inversion H; subst.
apply CEWhileEnd.
unfold bequiv in Hb. rewrite -> Hb.
reflexivity. Qed.
(* Exercise: 2 stars (CWhile_false_inf) *)
(*
Write an informal proof of CWhile_false.
(* FILL IN HERE *)
*)
Theorem loop_unrolling: forall b c,
cequiv
(while b do c)
(testif b then (c; while b do c) else skip).
Proof.
unfold cequiv. intros b c st st'.
split; intros Hce.
Case "->".
inversion Hce; subst.
SCase "loop doesn't run".
apply CEIfFalse. assumption. apply CESkip.
SCase "loop runs".
apply CEIfTrue. assumption.
apply CESeq with (st' := st'0). assumption. assumption.
Case "<-".
inversion Hce; subst.
SCase "loop runs".
inversion H5; subst.
apply CEWhileLoop with (st' := st'0).
assumption. assumption. assumption.
SCase "look doesn't run".
inversion H5; subst. apply CEWhileEnd. assumption. Qed.
(* Exercise: 2 stars (seq_assoc) *)
Theorem seq_assoc : forall c1 c2 c3,
cequiv ((c1;c2);c3) (c1;(c2;c3)).
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* Exercise: 3 stars (swap_if_branches) *)
Theorem swap_if_branches: forall b e1 e2,
cequiv
(testif b then e1 else e2)
(testif (BNot b) then e2 else e1).
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* ------------------------------------------------------- *)
(** ** Program equivalence is an equivalence *)
(* The equivalences on aexps, bexps, and commands are reflexive,
symmetric, and transitive *)
Lemma refl_aequiv : forall (a : aexp), aequiv a a.
Proof.
unfold aequiv. intros a st. reflexivity. Qed.
Lemma sym_aequiv : forall (a1 a2 : aexp),
aequiv a1 a2 -> aequiv a2 a1.
Proof.
unfold aequiv. intros a1 a2 H. intros st. apply sym_eq. apply H. Qed.
Lemma trans_aequiv : forall (a1 a2 a3 : aexp),
aequiv a1 a2 -> aequiv a2 a3 -> aequiv a1 a3.
Proof.
unfold aequiv. intros a1 a2 a3 H12 H23 st.
rewrite (H12 st). rewrite (H23 st). reflexivity. Qed.
Lemma refl_bequiv : forall (b : bexp), bequiv b b.
Proof.
unfold bequiv. intros b st. reflexivity. Qed.
Lemma sym_bequiv : forall (b1 b2 : bexp),
bequiv b1 b2 -> bequiv b2 b1.
Proof.
unfold bequiv. intros b1 b2 H. intros st. apply sym_eq. apply H. Qed.
Lemma trans_bequiv : forall (b1 b2 b3 : bexp),
bequiv b1 b2 -> bequiv b2 b3 -> bequiv b1 b3.
Proof.
unfold bequiv. intros b1 b2 b3 H12 H23 st.
rewrite (H12 st). rewrite (H23 st). reflexivity. Qed.
Lemma refl_cequiv : forall (c : com), cequiv c c.
Proof.
unfold cequiv. intros c st st'. apply iff_refl. Qed.
Lemma sym_cequiv : forall (c1 c2 : com),
cequiv c1 c2 -> cequiv c2 c1.
Proof.
unfold cequiv. intros c1 c2 H st st'.
assert (c1 / st --> st' <-> c2 / st --> st') as H'.
SCase "Proof of assertion". apply H.
inversion H'.
split; intros H2.
Case "->".
apply H1. assumption.
Case "->".
apply H0. assumption. Qed.
Lemma trans_iff : forall (P1 P2 P3 : Prop),
(P1 <-> P2) -> (P2 <-> P3) -> (P1 <-> P3).
Proof.
intros P1 P2 P3 H12 H23.
inversion H12. inversion H23.
split; intros A.
apply H1. apply H. apply A.
apply H0. apply H2. apply A. Qed.
Lemma trans_cequiv : forall (c1 c2 c3 : com),
cequiv c1 c2 -> cequiv c2 c3 -> cequiv c1 c3.
Proof.
unfold cequiv. intros c1 c2 c3 H12 H23 st st'.
apply trans_iff with (c2 / st --> st'). apply H12. apply H23. Qed.
(* ------------------------------------------------------- *)
(** ** Program equivalence is a congruence *)
(* Program equivalence is also a CONGRUENCE. That is, the
equivalence of two subprograms implies the equivalence of the
whole programs in which they are embedded:
aequiv a1 a1'
-----------------------------
cequiv (i ::= a1) (i ::= a1')
cequiv c1 c1' cequiv c2 c2'
------------------------------
cequiv (c1;c2) (c1';c2')
And so on. We prove these lemmas below.
Motivating example (see below): fold_constants_com_sound
*)
Theorem CAss_congruence : forall i a1 a1',
aequiv a1 a1' ->
cequiv (CAss i a1) (CAss i a1').
Proof.
unfold aequiv,cequiv. intros i a1 a2 Heqv st st'.
split; intros Hceval.
Case "->".
inversion Hceval. subst. apply CEAss.
rewrite Heqv. reflexivity.
Case "<-".
inversion Hceval. subst. apply CEAss.
rewrite Heqv. reflexivity. Qed.
Theorem CWhile_congruence : forall b1 b1' c1 c1',
bequiv b1 b1' -> cequiv c1 c1' ->
cequiv (CWhile b1 c1) (CWhile b1' c1').
Proof.
unfold bequiv,cequiv.
intros b1 b1' c1 c1' Hb1e Hc1e st st'.
split; intros Hce.
(* Both directions of the proof are a little tricky - we need
to go by induction... *)
Case "->".
remember (while b1 do c1) as cwhile.
induction Hce; try (inversion Heqcwhile); subst.
SCase "CEWhileEnd".
apply CEWhileEnd. rewrite <- Hb1e. apply H.
SCase "CEWhileLoop".
apply CEWhileLoop with (st' := st').
SSCase "show loop runs". rewrite <- Hb1e. apply H.
SSCase "body execution".
destruct (Hc1e st st') as [Hc1c1' _].
apply Hc1c1'. apply Hce1.
SSCase "subsequent loop execution".
apply IHHce2. reflexivity.
Case "<-".
remember (while b1' do c1') as c'while.
induction Hce; try (inversion Heqc'while); subst.
SCase "CEWhileEnd".
apply CEWhileEnd. rewrite -> Hb1e. apply H.
SCase "CEWhileLoop".
apply CEWhileLoop with (st' := st').
SSCase "show loop runs". rewrite -> Hb1e. apply H.
SSCase "body execution".
destruct (Hc1e st st') as [_ Hc1'c1].
apply Hc1'c1. apply Hce1.
SSCase "subsequent loop execution".
apply IHHce2. reflexivity. Qed.
(* Exercise: 3 stars (CSeq_congruence) *)
Theorem CSeq_congruence : forall c1 c1' c2 c2',
cequiv c1 c1' -> cequiv c2 c2' ->
cequiv (c1; c2) (c1'; c2').
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* Exercise: 3 stars (CIf_congruence) *)
Theorem CIf_congruence : forall b b' c1 c1' c2 c2',
bequiv b b' -> cequiv c1 c1' -> cequiv c2 c2' ->
cequiv (CIf b c1 c2) (CIf b' c1' c2').
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* ------------------------------------------------------- *)
(** ** Case study: Constant folding *)
(* A PROGRAM TRANSFORMATION is a function that takes a program as
input and produces some variant of the program as its output.
Compiler optimizations such as constant folding are a
canonical example, but there are many others. *)
(* ------------------------------ *)
(* Soundness of program transformations *)
(* A program transformation is SOUND if it preserves the behavior
of the original program.
We can define a notion of soundness for translations of aexps,
bexps, and commands. *)
Definition atrans_sound (atrans : aexp -> aexp) : Prop :=
forall (a : aexp),
aequiv a (atrans a).
Definition btrans_sound (btrans : bexp -> bexp) : Prop :=
forall (b : bexp),
bequiv b (btrans b).
Definition ctrans_sound (ctrans : com -> com) : Prop :=
forall (c : com),
cequiv c (ctrans c).
(* ------------------------------ *)
(* The constant-folding transformation *)
(* An expression is CONSTANT when it contains no variable
references.
Constant folding is an optimization that finds constant
expressions and reduces them. *)
Fixpoint fold_constants_aexp (a : aexp) {struct a} : aexp :=
match a with
| ANum n => ANum n
| AId i => AId i
| APlus a1 a2 =>
match (fold_constants_aexp a1, fold_constants_aexp a2) with
| (ANum n1, ANum n2) => ANum (plus n1 n2)
| (a1', a2') => APlus a1' a2'
end
| AMinus a1 a2 =>
match (fold_constants_aexp a1, fold_constants_aexp a2) with
| (ANum n1, ANum n2) => ANum (minus n1 n2)
| (a1', a2') => AMinus a1' a2'
end
| AMult a1 a2 =>
match (fold_constants_aexp a1, fold_constants_aexp a2) with
| (ANum n1, ANum n2) => ANum (mult n1 n2)
| (a1', a2') => AMult a1' a2'
end
end.
Example fold_aexp_ex1 :
fold_constants_aexp ((A1 +++ A2) *** !X) = A3 *** !X.
Proof. reflexivity. Qed.
(* Note that this version of constant folding doesn't eliminate trivial
additions, etc. *)
Example fold_aexp_ex2 :
fold_constants_aexp (!X --- ((A0 *** A6) +++ !Y))
= !X --- (A0 +++ !Y).
Proof. reflexivity. Qed.
(* Not only can we "lift" fold_constants_aexp to bexps (in the
BEq and BLtEq cases), we can find constant boolean expressions
and "fold" them, too. *)
Fixpoint fold_constants_bexp (b : bexp) {struct b} : bexp :=
match b with
| BTrue => BTrue
| BFalse => BFalse
| BEq a1 a2 =>
match (fold_constants_aexp a1, fold_constants_aexp a2) with
| (ANum n1, ANum n2) => if beq_nat n1 n2 then BTrue else BFalse
| (a1', a2') => BEq a1' a2'
end
| BLtEq a1 a2 =>
match (fold_constants_aexp a1, fold_constants_aexp a2) with
| (ANum n1, ANum n2) => if ble_nat n1 n2 then BTrue else BFalse
| (a1', a2') => BLtEq a1' a2'
end
| BNot b1 =>
match (fold_constants_bexp b1) with
| BTrue => BFalse
| BFalse => BTrue
| b1' => BNot b1'
end
| BAnd b1 b2 =>
match (fold_constants_bexp b1, fold_constants_bexp b2) with
| (BTrue, BTrue) => BTrue
| (BTrue, BFalse) => BFalse
| (BFalse, BTrue) => BFalse
| (BFalse, BFalse) => BFalse
| (b1', b2') => BAnd b1' b2'
end
| BOr b1 b2 =>
match (fold_constants_bexp b1, fold_constants_bexp b2) with
| (BTrue, BTrue) => BTrue
| (BTrue, BFalse) => BTrue
| (BFalse, BTrue) => BTrue
| (BFalse, BFalse) => BFalse
| (b1', b2') => BOr b1' b2'
end
end.
Example fold_bexp_ex1 :
fold_constants_bexp (BAnd BTrue (BOr BFalse BTrue))
= BTrue.
Proof. reflexivity. Qed.
Example fold_bexp_ex2 :
fold_constants_bexp
(BAnd (!X === !Y) (A0 === (A2 --- (A1 +++ A1))))
= BAnd (!X === !Y) BTrue.
Proof. reflexivity. Qed.
Fixpoint fold_constants_com (c : com) {struct c} : com :=
match c with
| CSkip =>
CSkip
| CAss i a =>
CAss i (fold_constants_aexp a)
| CSeq c1 c2 =>
CSeq (fold_constants_com c1) (fold_constants_com c2)
| CIf b c1 c2 =>
match fold_constants_bexp b with
| BTrue => fold_constants_com c1
| BFalse => fold_constants_com c2
| b' => CIf b' (fold_constants_com c1) (fold_constants_com c2)
end
| CWhile b c =>
match fold_constants_bexp b with
| BTrue => CWhile BTrue CSkip
| BFalse => CSkip
| b' => CWhile b' (fold_constants_com c)
end
end.
Example fold_com_ex1 :
fold_constants_com (X ::= A4 +++ A5;
Y ::= !X --- A3;
(testif (!X --- !Y === A2 +++ A4)
then skip
else Y ::= A0);
(testif (A0 <<= A4 --- (A2 +++ A1))
then Y ::= A0
else skip);
while (!Y === A0) do X ::= !X +++ A1) =
(X ::= ANum 9;
Y ::= !X --- A3;
(testif (!X --- !Y === A6)
then skip
else Y ::= A0);
Y ::= A0;
while (!Y === A0) do X ::= !X +++ A1).
Proof. reflexivity. Qed.
(* ------------------------------ *)
(* Soundness of constant folding *)
Theorem fold_constants_aexp_sound:
atrans_sound fold_constants_aexp.
Proof.
unfold atrans_sound. intros a. unfold aequiv. intros st.
aexp_cases (induction a) Case.
Case "ANum". reflexivity.
Case "AId". reflexivity.
Case "APlus". simpl.
remember (fold_constants_aexp a1) as a1'.
remember (fold_constants_aexp a2) as a2'.
rewrite IHa1. rewrite IHa2.
destruct a1'; destruct a2'; reflexivity.
Case "AMinus". simpl.
remember (fold_constants_aexp a1) as a1'.
remember (fold_constants_aexp a2) as a2'.
rewrite IHa1. rewrite IHa2.
destruct a1'; destruct a2'; reflexivity.
Case "AMult". simpl.
remember (fold_constants_aexp a1) as a1'.
remember (fold_constants_aexp a2) as a2'.
rewrite IHa1. rewrite IHa2.
destruct a1'; destruct a2'; reflexivity. Qed.
(* A shorter proof... *)
Theorem fold_constants_aexp_sound' :
atrans_sound fold_constants_aexp.
Proof.
unfold atrans_sound. intros a. unfold aequiv. intros st.
(aexp_cases (induction a) Case); simpl;
(* ANum and AId follow immediately *)
try reflexivity;
(* APlus, AMinus, and AMult follow from the IH
and the observation that
aeval st (APlus a1 a2) =
ANum (plus (aeval st a1) (aeval st a2)) =
aeval st (ANum (plus (aeval st a1) (aeval st a2)))
(and similarly for AMinus/minus and AMult/mult)
*)
try (remember (fold_constants_aexp a1) as a1';
remember (fold_constants_aexp a2) as a2';
rewrite IHa1; rewrite IHa2;
destruct a1'; destruct a2'; reflexivity). Qed.
(* Exercise: 3 stars (fold_constants_bexp_sound_BNot_case) *)
(* Complete the BLtEq case of the following proof *)
Theorem fold_constants_bexp_sound:
btrans_sound fold_constants_bexp.
Proof.
unfold btrans_sound. intros b. unfold bequiv. intros st.
(bexp_cases (induction b) Case);
(* BTrue and BFalse are immediate *)
try reflexivity.
Case "BEq".
(* Informal proof of this case:
TO SHOW: beval st (a1 === a2) = beval st (fold_constants_bexp (a1 === a2))
PROOF: We consider two cases:
- [fold_constants_aexp a1 = ANum n1] and
[fold_constants_aexp a2 = ANum n2] for some n1 and n2.
In this case, we have
fold_constants_bexp (a1 === a2) = if beq_nat n1 n2 then BTrue else BFalse
and
beval st (a1 === a2) = beq_nat (aeval st a1) (aeval st a2)
By the lemma fold_constants_aexp_sound, we know that
aeval st a1 = aeval st (fold_constants_aexp a1) = aeval st (ANum n1) = n1
aeval st a2 = aeval st (fold_constants_aexp a2) = aeval st (ANum n2) = n2
So we show:
beq_nat n1 n2 = beval st (fold_constants_bexp (a1 === a2))
= beval st (if beq_nat n1 n2 then BTrue else BFalse)
= if beq_nat n1 n2 then true else false
= beq_nat n1 n2
This completes this case.
- One of [fold_constants_aexp a1] and [fold_constants_aexp
a2] is not equal to [ANum n] for any n. In this case, we
must show:
beval st (a1 === a2) = beval st (fold_constants_bexp (a1 === a2))
= beval st ((fold_constants_aexp a1) ===
(fold_constants_aexp a2))
which, by the definition of beval, is the same as:
beq_nat (aeval st a1) (aeval st a2) =
beq_nat (aeval st (fold_constants_aexp a1))
(aeval st (fold_constants_aexp a2))
But the lemma fold_constants_aexp_sound shows that
aeval st a1 = aeval st (fold_constants_aexp a1)
aeval st a2 = aeval st (fold_constants_aexp a2)
And we can see that the equation above holds. []
*)
(* Doing induction when there are a lot of constructors makes
specifying variable names a chore, but Coq doesn't always
choose nice variable names. You can rename entries in the
context with the [rename] tactic: [rename a into a1] will
rename [a] into [a1] in the current goal and context. *)
rename a into a1. rename a0 into a2. simpl.
remember (fold_constants_aexp a1) as a1'.
remember (fold_constants_aexp a2) as a2'.
assert (aeval st a1 = aeval st a1') as H1.
SCase "Proof of assertion". subst a1'. apply fold_constants_aexp_sound.
assert (aeval st a2 = aeval st a2') as H2.
SCase "Proof of assertion". subst a2'. apply fold_constants_aexp_sound.
rewrite H1. rewrite H2.
destruct a1'; destruct a2'; try reflexivity.
(* The only interesting case is when both a1 and a2
become constants after folding *)
simpl. destruct (beq_nat n n0); reflexivity.
Case "BLtEq".
(* Delete this application and complete the proof *) apply cheating.
Case "BNot".
simpl. remember (fold_constants_bexp b) as b'.
rewrite IHb.
destruct b'; reflexivity.
Case "BAnd".
simpl.
remember (fold_constants_bexp b1) as b1'.
remember (fold_constants_bexp b2) as b2'.
rewrite IHb1. rewrite IHb2.
destruct b1'; destruct b2'; reflexivity.
Case "BOr".
simpl.
remember (fold_constants_bexp b1) as b1'.
remember (fold_constants_bexp b2) as b2'.
rewrite IHb1. rewrite IHb2.
destruct b1'; destruct b2'; reflexivity. Qed.
(* Exercise: 3 stars (fold_constants_com_sound_CWhile_case) *)
(* Complete the CWhile case of the following proof.
Most cases are easy, following from the congruence lemmas and
the soundness theorems above. *)
Theorem fold_constants_com_sound :
ctrans_sound fold_constants_com.
Proof.
unfold ctrans_sound. intros c.
(com_cases (induction c) Case); simpl.
Case "CSkip". apply refl_cequiv.
Case "CAss". apply CAss_congruence. apply fold_constants_aexp_sound.
Case "CSeq". apply CSeq_congruence; assumption.
Case "CIf".
assert (bequiv b (fold_constants_bexp b)).
SCase "Pf of assertion". apply fold_constants_bexp_sound.
remember (fold_constants_bexp b) as b'.
destruct b';
(* if the optimization doesn't eliminate the testif, then
the result is easy to prove from the IH and
fold_constants_bexp_sound *)
try (apply CIf_congruence; assumption).
SCase "b always true".
apply trans_cequiv with c1; try assumption.
apply CIf_true; assumption.
SCase "b always false".
apply trans_cequiv with c2; try assumption.
apply CIf_false; assumption.
Case "CWhile".
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* ------------------------------ *)
(* Soundness of (0 + n) elimination *)
(* Exercise: 4 stars (optimize_0plus) *)
(* Recall the definition optimize_0plus from While.v:
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.
Note that this function is defined over the old aexps, without
states.
Write a _new_ version of this function, lifting it all the way
up to commands. You should have three versions:
optimize_0plus_aexp
optimize_0plus_bexp
optimize_0plus_com
Prove that these three functions are sound, as we did for
fold_constants_*. (Make sure you use the congruence lemmas in
the proof of optimize_0plus_com!)
Then go on to define an optimizer on commands that first folds
constants (using fold_constants_com) and then eliminates (0 +
n) terms (using optimize_0plus_com).
* Give a meaningful example of this optimizer's output.
* Prove that the optimizer is sound. (Note: this part should
be _very_ easy!)
*)
(* FILL IN HERE *)
(* ------------------------------------------------------- *)
(** ** Case study: Proving that programs are NOT equivalent *)
(* Suppose that c1 is a command of the form (x := a1 ; y := a2)
and c2 is the command (x := a1 ; y := a2'), where a2' is
formed by substituting a1 for all occurrences of !x in a2.
For example, c1 and c2 might be
c1 = (x ::= 42 ++ 53 ; y ::= !y ++ !x)
and
c2 = (x ::= 42 ++ 53 ; y ::= !y ++ (42 ++ 53))
Clearly, this particular [c1] and [c2] are equivalent. But is
this true in general? We will see that it is not, but it is
worthwhile to pause, now, and see if you can find a
counter-example on your own (or remember the one from the
discussion from class). *)
(* Here, formally, is the function [subst] that substitutes an
arithmetic expression for each occurrence of a given location
in another expression *)
Fixpoint subst_aexp (i : id) (u : aexp) (a : aexp) {struct a} : aexp :=
match a with
| ANum n => ANum n
| AId i' => if beq_nat i i' then u else AId i'
| APlus a1 a2 => APlus (subst_aexp i u a1) (subst_aexp i u a2)
| AMinus a1 a2 => AMinus (subst_aexp i u a1) (subst_aexp i u a2)
| AMult a1 a2 => AMult (subst_aexp i u a1) (subst_aexp i u a2)
end.
Example subst_aexp_ex :
subst_aexp X ((ANum 42) +++ (ANum 53)) (!Y +++ !X) =
(!Y +++ ((ANum 42) +++ (ANum 53))).
Proof. reflexivity. Qed.
(* And here is the property we are interested in, expressing the
claim that commands [c1] and [c2] as described above are
always equivalent. *)
Definition subst_equiv_property := forall i1 i2 a1 a2,
cequiv (i1 ::= a1; i2 ::= a2)
(i1 ::= a1; i2 ::= subst_aexp i1 a1 a2).
(* Here is the proof that the property does not hold. *)
Theorem subst_inequiv :
~ subst_equiv_property.
Proof.
unfold subst_equiv_property.
intros Contra.
(* Here is the counterexample: assuming that
[subst_equiv_property] holds allows us to prove that these
two programs are equivalent... *)
assert (cequiv (X ::= !X +++ A1; Y ::= !X)
(X ::= !X +++ A1; Y ::= (subst_aexp X (!X +++ A1) (!X)))) as BAD by apply Contra.
simpl in BAD. unfold cequiv in BAD. clear Contra.
(* This, in turn, allows us to show that the command
[X ::= !X +++ A1; Y ::= !X] can terminate in two different
final states:
st' = {X |-> 1, Y |-> 1}
st'' = {X |-> 1, Y |-> 2}. *)
remember (extend (extend empty_state X 1) Y 1) as st'.
remember (extend (extend empty_state X 1) Y 2) as st''.
(* Show termination in st'' (directly) *)
assert ((X ::= !X +++ A1; Y ::= !X) / empty_state --> st') as H.
Case "Pf of assertion".
apply CESeq with (extend empty_state X 1).
apply CEAss. reflexivity.
subst st'. apply CEAss. reflexivity.
(* Show termination in st' (using BAD equivalence) *)
assert ((X ::= !X +++ A1; Y ::= !X) / empty_state --> st'') as H'.
Case "Pf of assertion".
assert ((X ::= !X +++ A1; Y ::= !X) / empty_state --> st'' <->
(X ::= !X +++ A1; Y ::= !X +++ A1) / empty_state --> st'') as Hequiv.
SCase "Proof of sub-assertion". apply BAD.
inversion Hequiv as [Hequiv1 Hequiv2]. clear Hequiv Hequiv1. apply Hequiv2.
apply CESeq with (extend empty_state X 1).
apply CEAss. reflexivity.
subst st''. apply CEAss. reflexivity.
(* But this contradicts the determinacy of evaluation *)
assert (st' = st'') as WORSE.
Case "Pf of assertion".
apply ceval_deterministic
with (c := (X ::= !X +++ A1; Y ::= !X))
(st := empty_state); assumption.
assert (st' Y = st'' Y) as REALLYBAD.
Case "Pf of assertion". rewrite WORSE. reflexivity.
subst. inversion REALLYBAD. Qed.
(* An informal proof of subst_inequiv
THEOREM: It is not the case that, for all i1, i2, a1, and a2,
cequiv (i1 ::= a1; i2 ::= a2)
(i1 ::= a1; i2 ::= subst_aexp i1 a1 a2)
PROOF: Suppose, for a contradiction, that for all i1, i2, a1,
and a2, we have
cequiv (i1 ::= a1; i2 ::= a2)
(i1 ::= a1; i2 ::= subst_aexp i1 a1 a2)
Consider the following program:
X ::= !X +++ A1; Y ::= !X
And note that
(X ::= !X +++ A1; Y ::= !X) / empty_state --> st'
where [st' = { X |-> 1, Y |-> 1 }].
By our assumption, we know that
cequiv (X ::= !X +++ A1; Y ::= !X)
(X ::= !X +++ A1; Y ::= !X +++ A1)
so, by the definition of cequiv, we have
(X ::= !X +++ A1; Y ::= !X +++ A1) / empty_state --> st'
But we can also derive
(X ::= !X +++ A1; Y ::= !X +++ A1) / empty_state --> st''
where [st'' = { X |-> 1, Y |-> 2 }]. Note that [st' <> st''];
this is a contradiction, since ceval is deterministic! []
*)
(* Exercise: 4 stars, optional (better_subst_equiv) *)
(* The equivalence we had in mind above was not complete
nonsense -- it was actually almost right. To make it correct,
we just need to exclude the case where the variable x occurs
in the right-hand-side of the first assignment statement.
Formalize this claim and prove that it is correct. *)
(* FILL IN HERE *)
(* Exercise: 3 stars *)
Theorem inequiv_exercise:
~ cequiv (while BTrue do skip) skip.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(** * Reasoning about programs *)
(* A slightly different version of the factorial program *)
Definition fact_body : com :=
Y ::= !Y *** !Z;
Z ::= !Z --- A1.
Definition fact_loop : com :=
while BNot (!Z === A0) do
fact_body.
Definition fact_com : com :=
Z ::= !X;
Y ::= ANum 1;
fact_loop.
Definition fact_invariant (x:nat) (st:state) :=
exists y, exists z,
lookup Y st = Some y
/\ lookup Z st = Some z
/\ mult y (factorial z) = factorial x.
Theorem fact_body_preserves_invariant: forall st st' x,
fact_invariant x st
-> lookup Z st <> Some 0
-> fact_body / st --> st'
-> fact_invariant x st'.
Proof.
intros st st' x H HZnz He.
unfold fact_invariant in H.
destruct H as [y [z [HY [HZ Hm]]]].
(* first, note that z = S z' for some z' *)
assert (exists z', z = S z').
destruct z as [| z'].
Case "z = 0 (contra)".
apply ex_falso_quodlibet.
apply HZnz. apply HZ.
Case "z = S z'".
exists z'. reflexivity.
destruct H as [z' Heqz]. subst z.
(* next, we see what reduction of fact_body does...*)
unfold fact_body in He.
unfold fact_invariant.
exists (mult y (S z')).
exists z'.
inversion He; subst.
inversion H2; subst.
inversion H4; subst.
simpl. rewrite HY. rewrite HZ.
assert (lookup Z (extend st Y (mult y (S z'))) = Some (S z')) as HZ'.
apply extend_neq. assumption.
reflexivity.
rewrite HZ'.
split. Case "Y correct".
reflexivity.
split. Case "Z correct".
reflexivity.
Case "mult invariant preserved".
rewrite <- Hm.
simpl. rewrite <- mult_assoc.
assert (mult (S z') (factorial z') = plus (factorial z') (mult z' (factorial z'))).
simpl. reflexivity.
rewrite H. reflexivity. Qed.
Theorem fact_loop_preserves_invariant : forall st st' x,
fact_invariant x st
-> fact_loop / st --> st'
-> fact_invariant x st'.
Proof.
intros st st' x H Hce.
remember fact_loop as c.
(ceval_cases (induction Hce) Case); inversion Heqc; subst; clear Heqc.
Case "CEWhileEnd".
(* trivial when the loop doesn't run... *)
assumption.
Case "CEWhileLoop".
(* if the loop does run, we know that fact_body preserves
fact_invariant -- we just need to assemble the pieces *)
assert (lookup Z st <> Some 0) as HZnz.
intros Contra.
inversion H0; subst. apply negb_flip in H2.
rewrite Contra in H2. inversion H2.
assert (fact_invariant x st').
apply fact_body_preserves_invariant with st; assumption.
apply IHHce2. assumption. reflexivity. Qed.
Theorem guard_false_after_loop: forall b c st st',
(while b do c) / st --> st'
-> beval st' b = false.
Proof.
intros b c st st' Hce.
remember (while b do c) as cloop.
(ceval_cases (induction Hce) Case); try (inversion Heqcloop; subst).
Case "CEWhileEnd".
assumption.
Case "CEWhileLoop".
apply IHHce2. reflexivity. Qed.
(* Patching it all together... *)
Theorem fact_com_correct : forall st st' x,
lookup X st = Some x
-> fact_com / st --> st'
-> lookup Y st' = Some (factorial x).
Proof.
intros st st' x HX Hce.
inversion Hce; subst.
inversion H2; subst.
inversion H4; subst.
inversion H3; subst.
rename st' into st''.
(* we notice that the invariant is set up before the loop runs... *)
remember (extend (extend st Z (aeval st (!X))) Y
(aeval (extend st Z (aeval st (!X))) A1)) as st'.
assert (fact_invariant x st').
unfold fact_invariant.
exists 1. exists x.
split.
subst st'. reflexivity.
split.
subst st'. simpl. rewrite HX. reflexivity.
apply mult_1_l.
(* and that when the loop is done running, the invariant is maintained *)
assert (fact_invariant x st'').
apply fact_loop_preserves_invariant with st'; assumption.
unfold fact_invariant in H0.
destruct H0 as [y [z [HY [HZ Hf]]]].
(* finally, if the loop terminated, then z is 0, so y must be
factorial x *)
assert (beval st'' (BNot (!Z === A0)) = false).
apply guard_false_after_loop with (st := st') (c := fact_body).
apply H6.
simpl in H0. apply negb_flip in H0.
rewrite HZ in H0. symmetry in H0.
apply beq_nat_eq in H0. subst z.
simpl in Hf. rewrite mult_1_r in Hf. subst y.
assumption. Qed.
(* One might wonder whether all this work with poking at states
and unfolding definitions could be ameliorated with some more
powerful lemmas and/or more uniform reasoning
principles... Indeed, this is exactly the topic of next week's
lectures! *)
(* Exercise: 3 stars (subtract_slowly_spec) *)
(* Prove a specification for subtract_slowly, using the above
specification of [fact_com] and the invariant below as
guides. *)
Definition ss_invariant (x:nat) (z:nat) (st:state) :=
exists x', exists z',
lookup X st = Some x'
/\ lookup Z st = Some z'
/\ minus z' x' = minus z x.
(* FILL IN HERE *)
(* ------------------------------------------------------- *)
(** * Additional exercises *)
(* Exercise: 3 stars, optional (extend_eq_variant) *)
(* The way [extend_eq] is stated (in the section on mappings in
While.v) may have looked a bit surprising: wouldn't it be
simpler just to say [lookup k (extend f k x) = Some x]? Try
changing the statement of the theorem to read like this; then
work through some of this file and see how the proofs that use
[extend_eq] need to be changed to use the simplified
version. *)
(* Exercise: 4 stars, optional (add_for_loop) *)
(* Add C-style [for] loops to the language of commands in
While.v, update the cevals definition to define the semantics
of [for] loops, and add cases for [for] loops as needed so
that all the proofs in While.v and this file are accepted by
Coq.
A [for] loop should be parameterized by (a) a statement
executed initially, (b) a test that is run on each iteration
of the loop to determine whether the loop should continue, (c)
a statement executed at the end of each loop iteration,
and (d) a statement that makes up the body of the loop. (You
don't need to worry about making up a concrete Notation for
[for] loops, but feel free to play with this too if you like.)
Next, prove that the command:
for (c1 ; b ; c2) {
c3
}
is equivalent to:
c1 ;
while b do {
c3 ;
c2
}
*)
(* FILL IN HERE *)
(* mode: outline-minor *)
(* outline-heading-end-regexp: "\n" *)