EquivProgram Equivalence
Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Coq.omega.Omega.
Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import SfLib.
Require Import Maps.
Require Import Imp.
Some general advice for working on exercises:
- 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.
- The Coq proofs we're doing now are sufficiently complicated that
it is more or less impossible to complete them simply by random
experimentation or "following your nose." You need to start
with an idea about why the property is true and how the proof is
going to go. The best way to do this is to write out at least a
sketch of an informal proof on paper — one that intuitively
convinces you of the truth of the theorem — before starting to
work on the formal one. Alternately, grab a friend and try to
convince them that the theorem is true; then try to formalize
your explanation.
- Use automation to save work! Some of the proofs in this chapter's exercises are pretty long if you try to write out all the cases explicitly.
Behavioral Equivalence
Definitions
Definition aequiv (a1 a2 : aexp) : Prop :=
∀(st:state),
aeval st a1 = aeval st a2.
Definition bequiv (b1 b2 : bexp) : Prop :=
∀(st:state),
beval st b1 = beval st b2.
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 started in the
same initial state," because some commands (in some starting
states) don't terminate in any final state at all! What we need
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. A compact way to express this
is "if the first one terminates in a particular state then so does
the second, and vice versa."
Exercise: 2 stars (equiv_classes)
[ [prog_a;prog_b;prog_c;prog_d;prog_e;prog_f;prog_g;prog_h] ;
[prog_i] ]
[prog_i] ]
Definition prog_a : com :=
WHILE BNot (BLe (AId X) (ANum 0)) DO
X ::= APlus (AId X) (ANum 1)
END.
Definition prog_b : com :=
IFB BEq (AId X) (ANum 0) THEN
X ::= APlus (AId X) (ANum 1);;
Y ::= ANum 1
ELSE
Y ::= ANum 0
FI;;
X ::= AMinus (AId X) (AId Y);;
Y ::= ANum 0.
Definition prog_c : com :=
SKIP.
Definition prog_d : com :=
WHILE BNot (BEq (AId X) (ANum 0)) DO
X ::= APlus (AMult (AId X) (AId Y)) (ANum 1)
END.
Definition prog_e : com :=
Y ::= ANum 0.
Definition prog_f : com :=
Y ::= APlus (AId X) (ANum 1);;
WHILE BNot (BEq (AId X) (AId Y)) DO
Y ::= APlus (AId X) (ANum 1)
END.
Definition prog_g : com :=
WHILE BTrue DO
SKIP
END.
Definition prog_h : com :=
WHILE BNot (BEq (AId X) (AId X)) DO
X ::= APlus (AId X) (ANum 1)
END.
Definition prog_i : com :=
WHILE BNot (BEq (AId X) (AId Y)) DO
X ::= APlus (AId Y) (ANum 1)
END.
Definition equiv_classes : list (list com) :=
(* FILL IN HERE *) admit.
(* GRADE_TEST 2: check_equiv_classes equiv_classes *)
☐
Theorem aequiv_example:
aequiv (AMinus (AId X) (AId X)) (ANum 0).
Proof.
intros st. simpl. omega.
Qed.
intros st. simpl. omega.
Qed.
Theorem bequiv_example:
bequiv (BEq (AMinus (AId X) (AId X)) (ANum 0)) BTrue.
For examples of command equivalence, let's start by looking at
some trivial program transformations involving SKIP:
Theorem skip_left: ∀c,
cequiv
(SKIP;; c)
c.
Proof.
(* WORKED IN CLASS *)
intros c st st'.
split; intros H.
- (* -> *)
inversion H. subst.
inversion H2. subst.
assumption.
- (* <- *)
apply E_Seq with st.
apply E_Skip.
assumption.
Qed.
Exercise: 2 stars (skip_right)
Prove that adding a SKIP after a command results in an equivalent program
☐
Similarly, here is a simple transformations that simplifies IFB
commands:
Theorem IFB_true_simple: ∀c1 c2,
cequiv
(IFB BTrue THEN c1 ELSE c2 FI)
c1.
Proof.
intros c1 c2.
split; intros H.
- (* -> *)
inversion H; subst. assumption. inversion H5.
- (* <- *)
apply E_IfTrue. reflexivity. assumption. Qed.
intros c1 c2.
split; intros H.
- (* -> *)
inversion H; subst. assumption. inversion H5.
- (* <- *)
apply E_IfTrue. reflexivity. assumption. Qed.
Of course, few programmers would be tempted to write a conditional
whose guard is literally BTrue. A more interesting case is when
the guard is equivalent to true:
Theorem: If b is equivalent to BTrue, then IFB b THEN c1
ELSE c2 FI is equivalent to c1.
Proof:
Here is the formal version of this proof:
- (→) We must show, for all st and st', that if IFB b
THEN c1 ELSE c2 FI / st ⇓ st' then c1 / st ⇓ st'.
- Suppose the final rule rule in the derivation of IFB b THEN
c1 ELSE c2 FI / st ⇓ st' was E_IfTrue. We then have, by
the premises of E_IfTrue, that c1 / st ⇓ st'. This is
exactly what we set out to prove.
- On the other hand, suppose the final rule in the derivation
of IFB b THEN c1 ELSE c2 FI / st ⇓ st' was E_IfFalse.
We then know that beval st b = false and c2 / st ⇓ st'.
- Suppose the final rule rule in the derivation of IFB b THEN
c1 ELSE c2 FI / st ⇓ st' was E_IfTrue. We then have, by
the premises of E_IfTrue, that c1 / st ⇓ st'. This is
exactly what we set out to prove.
- (←) We must show, for all st and st', that if c1 / st
⇓ st' then IFB b THEN c1 ELSE c2 FI / st ⇓ st'.
Theorem IFB_true: ∀b c1 c2,
bequiv b BTrue →
cequiv
(IFB b THEN c1 ELSE c2 FI)
c1.
Proof.
intros b c1 c2 Hb.
split; intros H.
- (* -> *)
inversion H; subst.
+ (* b evaluates to true *)
assumption.
+ (* b evaluates to false (contradiction) *)
unfold bequiv in Hb. simpl in Hb.
rewrite Hb in H5.
inversion H5.
- (* <- *)
apply E_IfTrue; try assumption.
unfold bequiv in Hb. simpl in Hb.
rewrite Hb. reflexivity. Qed.
Theorem IFB_false: ∀b c1 c2,
bequiv b BFalse →
cequiv
(IFB b THEN c1 ELSE c2 FI)
c2.
Proof.
(* FILL IN HERE *) Admitted.
bequiv b BFalse →
cequiv
(IFB b THEN c1 ELSE c2 FI)
c2.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars (swap_if_branches)
Show that we can swap the branches of an IF by negating its conditionTheorem swap_if_branches: ∀b e1 e2,
cequiv
(IFB b THEN e1 ELSE e2 FI)
(IFB BNot b THEN e2 ELSE e1 FI).
Proof.
(* FILL IN HERE *) Admitted.
☐
For WHILE loops, we can give a similar pair of theorems. A loop
whose guard is equivalent to BFalse is equivalent to SKIP,
while a loop whose guard is equivalent to BTrue is equivalent to
WHILE BTrue DO SKIP END (or any other non-terminating program).
The first of these facts is easy.
Theorem WHILE_false : ∀b c,
bequiv b BFalse →
cequiv
(WHILE b DO c END)
SKIP.
Proof.
intros b c Hb. split; intros H.
- (* -> *)
inversion H; subst.
+ (* E_WhileEnd *)
apply E_Skip.
+ (* E_WhileLoop *)
rewrite Hb in H2. inversion H2.
- (* <- *)
inversion H; subst.
apply E_WhileEnd.
rewrite Hb.
reflexivity. Qed.
intros b c Hb. split; intros H.
- (* -> *)
inversion H; subst.
+ (* E_WhileEnd *)
apply E_Skip.
+ (* E_WhileLoop *)
rewrite Hb in H2. inversion H2.
- (* <- *)
inversion H; subst.
apply E_WhileEnd.
rewrite Hb.
reflexivity. Qed.
Exercise: 2 stars, advanced, optional (WHILE_false_informal)
Write an informal proof of WHILE_false.☐
- Suppose (WHILE b DO c END) / st ⇓ st' is proved using rule
E_WhileEnd. Then by assumption beval st b = false. But
this contradicts the assumption that b is equivalent to
BTrue.
- Suppose (WHILE b DO c END) / st ⇓ st' is proved using rule
E_WhileLoop. Then we are given the induction hypothesis
that (WHILE b DO c END) / st ⇓ st' is contradictory, which
is exactly what we are trying to prove!
- Since these are the only rules that could have been used to prove (WHILE b DO c END) / st ⇓ st', the other cases of the induction are immediately contradictory. ☐
Lemma WHILE_true_nonterm : ∀b c st st',
bequiv b BTrue →
~( (WHILE b DO c END) / st ⇓ st' ).
Proof.
(* WORKED IN CLASS *)
intros b c st st' Hb.
intros H.
remember (WHILE b DO c END) as cw eqn:Heqcw.
induction H;
(* Most rules don't apply, and we can rule them out
by inversion *)
inversion Heqcw; subst; clear Heqcw.
(* The two interesting cases are the ones for WHILE loops: *)
- (* E_WhileEnd *) (* contradictory -- b is always true! *)
unfold bequiv in Hb.
(* rewrite is able to instantiate the quantifier in st *)
rewrite Hb in H. inversion H.
- (* E_WhileLoop *) (* immediate from the IH *)
apply IHceval2. reflexivity. Qed.
Exercise: 2 stars, optional (WHILE_true_nonterm_informal)
Explain what the lemma WHILE_true_nonterm means in English.☐
Exercise: 2 stars, recommended (WHILE_true)
Prove the following theorem. Hint: You'll want to use WHILE_true_nonterm here.Theorem WHILE_true: ∀b c,
bequiv b BTrue →
cequiv
(WHILE b DO c END)
(WHILE BTrue DO SKIP END).
Proof.
(* FILL IN HERE *) Admitted.
☐
Theorem loop_unrolling: ∀b c,
cequiv
(WHILE b DO c END)
(IFB b THEN (c;; WHILE b DO c END) ELSE SKIP FI).
Proof.
(* WORKED IN CLASS *)
intros b c st st'.
split; intros Hce.
- (* -> *)
inversion Hce; subst.
+ (* loop doesn't run *)
apply E_IfFalse. assumption. apply E_Skip.
+ (* loop runs *)
apply E_IfTrue. assumption.
apply E_Seq with (st' := st'0). assumption. assumption.
- (* <- *)
inversion Hce; subst.
+ (* loop runs *)
inversion H5; subst.
apply E_WhileLoop with (st' := st'0).
assumption. assumption. assumption.
+ (* loop doesn't run *)
inversion H5; subst. apply E_WhileEnd. assumption. Qed.
split; intros Hce.
- (* -> *)
inversion Hce; subst.
+ (* loop doesn't run *)
apply E_IfFalse. assumption. apply E_Skip.
+ (* loop runs *)
apply E_IfTrue. assumption.
apply E_Seq with (st' := st'0). assumption. assumption.
- (* <- *)
inversion Hce; subst.
+ (* loop runs *)
inversion H5; subst.
apply E_WhileLoop with (st' := st'0).
assumption. assumption. assumption.
+ (* loop doesn't run *)
inversion H5; subst. apply E_WhileEnd. assumption. Qed.
Theorem seq_assoc : ∀c1 c2 c3,
cequiv ((c1;;c2);;c3) (c1;;(c2;;c3)).
Proof.
(* FILL IN HERE *) Admitted.
cequiv ((c1;;c2);;c3) (c1;;(c2;;c3)).
Proof.
(* FILL IN HERE *) Admitted.
☐
Proving program properties involving assignments is one place
where the functional-extensionality axiom introduced in the
Logic chapter often comes in handy. Here are an example and an
exercise.
Theorem identity_assignment : ∀(X:id),
cequiv
(X ::= AId X)
SKIP.
Proof.
intros. split; intro H.
- (* -> *)
inversion H; subst. simpl.
replace (t_update st X (st X)) with st.
constructor.
apply functional_extensionality. intro.
rewrite t_update_same; reflexivity.
- (* <- *)
inversion H; subst.
assert (st' = (t_update st' X (st' X))).
apply functional_extensionality. intro.
rewrite t_update_same; reflexivity.
rewrite H0 at 2.
constructor. reflexivity.
Qed.
Theorem assign_aequiv : ∀X e,
aequiv (AId X) e →
cequiv SKIP (X ::= e).
Proof.
(* FILL IN HERE *) Admitted.
aequiv (AId X) e →
cequiv SKIP (X ::= e).
Proof.
(* FILL IN HERE *) Admitted.
☐
Properties of Behavioral Equivalence
Behavioral Equivalence is an Equivalence
Lemma refl_aequiv : ∀(a : aexp), aequiv a a.
Proof.
intros a st. reflexivity. Qed.
intros a st. reflexivity. Qed.
Lemma sym_aequiv : ∀(a1 a2 : aexp),
aequiv a1 a2 → aequiv a2 a1.
Proof.
intros a1 a2 H. intros st. symmetry. apply H. Qed.
intros a1 a2 H. intros st. symmetry. apply H. Qed.
Lemma trans_aequiv : ∀(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.
unfold aequiv. intros a1 a2 a3 H12 H23 st.
rewrite (H12 st). rewrite (H23 st). reflexivity. Qed.
Lemma refl_bequiv : ∀(b : bexp), bequiv b b.
Lemma sym_bequiv : ∀(b1 b2 : bexp),
bequiv b1 b2 → bequiv b2 b1.
Lemma trans_bequiv : ∀(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.
unfold bequiv. intros b1 b2 b3 H12 H23 st.
rewrite (H12 st). rewrite (H23 st). reflexivity. Qed.
Lemma refl_cequiv : ∀(c : com), cequiv c c.
Lemma sym_cequiv : ∀(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'.
{ (* Proof of assertion *) apply H. }
apply iff_sym. assumption.
Qed.
unfold cequiv. intros c1 c2 H st st'.
assert (c1 / st ⇓ st' ↔ c2 / st ⇓ st') as H'.
{ (* Proof of assertion *) apply H. }
apply iff_sym. assumption.
Qed.
Lemma iff_trans : ∀(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.
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 : ∀(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 iff_trans with (c2 / st ⇓ st'). apply H12. apply H23. Qed.
unfold cequiv. intros c1 c2 c3 H12 H23 st st'.
apply iff_trans with (c2 / st ⇓ st'). apply H12. apply H23. Qed.
Behavioral Equivalence is a Congruence
aequiv a1 a1' | |
cequiv (i ::= a1) (i ::= a1') |
cequiv c1 c1' | |
cequiv c2 c2' | |
cequiv (c1;;c2) (c1';;c2') |
Theorem CAss_congruence : ∀i a1 a1',
aequiv a1 a1' →
cequiv (CAss i a1) (CAss i a1').
Proof.
intros i a1 a2 Heqv st st'.
split; intros Hceval.
- (* -> *)
inversion Hceval. subst. apply E_Ass.
rewrite Heqv. reflexivity.
- (* <- *)
inversion Hceval. subst. apply E_Ass.
rewrite Heqv. reflexivity. Qed.
intros i a1 a2 Heqv st st'.
split; intros Hceval.
- (* -> *)
inversion Hceval. subst. apply E_Ass.
rewrite Heqv. reflexivity.
- (* <- *)
inversion Hceval. subst. apply E_Ass.
rewrite Heqv. reflexivity. Qed.
The congruence property for loops is a little more interesting,
since it requires induction.
Theorem: Equivalence is a congruence for WHILE — that is, if
b1 is equivalent to b1' and c1 is equivalent to c1', then
WHILE b1 DO c1 END is equivalent to WHILE b1' DO c1' END.
Proof: Suppose b1 is equivalent to b1' and c1 is
equivalent to c1'. We must show, for every st and st', that
WHILE b1 DO c1 END / st ⇓ st' iff WHILE b1' DO c1' END / st
⇓ st'. We consider the two directions separately.
- (→) We show that WHILE b1 DO c1 END / st ⇓ st' implies
WHILE b1' DO c1' END / st ⇓ st', by induction on a
derivation of WHILE b1 DO c1 END / st ⇓ st'. The only
nontrivial cases are when the final rule in the derivation is
E_WhileEnd or E_WhileLoop.
- E_WhileEnd: In this case, the form of the rule gives us
beval st b1 = false and st = st'. But then, since
b1 and b1' are equivalent, we have beval st b1' =
false, and E-WhileEnd applies, giving us WHILE b1' DO
c1' END / st ⇓ st', as required.
- E_WhileLoop: The form of the rule now gives us beval st
b1 = true, with c1 / st ⇓ st'0 and WHILE b1 DO c1
END / st'0 ⇓ st' for some state st'0, with the
induction hypothesis WHILE b1' DO c1' END / st'0 ⇓
st'.
- E_WhileEnd: In this case, the form of the rule gives us
beval st b1 = false and st = st'. But then, since
b1 and b1' are equivalent, we have beval st b1' =
false, and E-WhileEnd applies, giving us WHILE b1' DO
c1' END / st ⇓ st', as required.
- (←) Similar. ☐
Theorem CWhile_congruence : ∀b1 b1' c1 c1',
bequiv b1 b1' → cequiv c1 c1' →
cequiv (WHILE b1 DO c1 END) (WHILE b1' DO c1' END).
Proof.
(* WORKED IN CLASS *)
unfold bequiv,cequiv.
intros b1 b1' c1 c1' Hb1e Hc1e st st'.
split; intros Hce.
- (* -> *)
remember (WHILE b1 DO c1 END) as cwhile eqn:Heqcwhile.
induction Hce; inversion Heqcwhile; subst.
+ (* E_WhileEnd *)
apply E_WhileEnd. rewrite ← Hb1e. apply H.
+ (* E_WhileLoop *)
apply E_WhileLoop with (st' := st').
× (* show loop runs *) rewrite ← Hb1e. apply H.
× (* body execution *)
apply (Hc1e st st'). apply Hce1.
× (* subsequent loop execution *)
apply IHHce2. reflexivity.
- (* <- *)
remember (WHILE b1' DO c1' END) as c'while eqn:Heqc'while.
induction Hce; inversion Heqc'while; subst.
+ (* E_WhileEnd *)
apply E_WhileEnd. rewrite → Hb1e. apply H.
+ (* E_WhileLoop *)
apply E_WhileLoop with (st' := st').
× (* show loop runs *) rewrite → Hb1e. apply H.
× (* body execution *)
apply (Hc1e st st'). apply Hce1.
× (* subsequent loop execution *)
apply IHHce2. reflexivity. Qed.
Theorem CSeq_congruence : ∀c1 c1' c2 c2',
cequiv c1 c1' → cequiv c2 c2' →
cequiv (c1;;c2) (c1';;c2').
Proof.
(* FILL IN HERE *) Admitted.
cequiv c1 c1' → cequiv c2 c2' →
cequiv (c1;;c2) (c1';;c2').
Proof.
(* FILL IN HERE *) Admitted.
Theorem CIf_congruence : ∀b b' c1 c1' c2 c2',
bequiv b b' → cequiv c1 c1' → cequiv c2 c2' →
cequiv (IFB b THEN c1 ELSE c2 FI) (IFB b' THEN c1' ELSE c2' FI).
Proof.
(* FILL IN HERE *) Admitted.
bequiv b b' → cequiv c1 c1' → cequiv c2 c2' →
cequiv (IFB b THEN c1 ELSE c2 FI) (IFB b' THEN c1' ELSE c2' FI).
Proof.
(* FILL IN HERE *) Admitted.
☐
For example, here are two equivalent programs and a proof of their
equivalence...
Example congruence_example:
cequiv
(* Program 1: *)
(X ::= ANum 0;;
IFB (BEq (AId X) (ANum 0))
THEN
Y ::= ANum 0
ELSE
Y ::= ANum 42
FI)
(* Program 2: *)
(X ::= ANum 0;;
IFB (BEq (AId X) (ANum 0))
THEN
Y ::= AMinus (AId X) (AId X) (* <--- changed here *)
ELSE
Y ::= ANum 42
FI).
Proof.
apply CSeq_congruence.
apply refl_cequiv.
apply CIf_congruence.
apply refl_bequiv.
apply CAss_congruence. unfold aequiv. simpl.
symmetry. apply minus_diag.
apply refl_cequiv.
Qed.
Program Transformations
Definition atrans_sound (atrans : aexp → aexp) : Prop :=
∀(a : aexp),
aequiv a (atrans a).
Definition btrans_sound (btrans : bexp → bexp) : Prop :=
∀(b : bexp),
bequiv b (btrans b).
Definition ctrans_sound (ctrans : com → com) : Prop :=
∀(c : com),
cequiv c (ctrans c).
The Constant-Folding Transformation
Fixpoint fold_constants_aexp (a : aexp) : 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 (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 (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 (n1 × n2)
| (a1', a2') ⇒ AMult a1' a2'
end
end.
Example fold_aexp_ex1 :
fold_constants_aexp
(AMult (APlus (ANum 1) (ANum 2)) (AId X))
= AMult (ANum 3) (AId X).
Proof. reflexivity. Qed.
Note that this version of constant folding doesn't eliminate
trivial additions, etc. — we are focusing attention on a single
optimization for the sake of simplicity. It is not hard to
incorporate other ways of simplifying expressions; the definitions
and proofs just get longer.
Example fold_aexp_ex2 :
fold_constants_aexp
(AMinus (AId X) (APlus (AMult (ANum 0) (ANum 6)) (AId Y)))
= AMinus (AId X) (APlus (ANum 0) (AId Y)).
Proof. reflexivity. Qed.
Not only can we lift fold_constants_aexp to bexps (in the
BEq and BLe cases), we can also find constant boolean
expressions and reduce them in-place.
Fixpoint fold_constants_bexp (b : bexp) : 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
| BLe a1 a2 ⇒
match (fold_constants_aexp a1, fold_constants_aexp a2) with
| (ANum n1, ANum n2) ⇒ if leb n1 n2 then BTrue else BFalse
| (a1', a2') ⇒ BLe 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
end.
Example fold_bexp_ex1 :
fold_constants_bexp (BAnd BTrue (BNot (BAnd BFalse BTrue)))
= BTrue.
Proof. reflexivity. Qed.
Example fold_bexp_ex2 :
fold_constants_bexp
(BAnd (BEq (AId X) (AId Y))
(BEq (ANum 0)
(AMinus (ANum 2) (APlus (ANum 1) (ANum 1)))))
= BAnd (BEq (AId X) (AId Y)) BTrue.
Proof. reflexivity. Qed.
To fold constants in a command, we apply the appropriate folding
functions on all embedded expressions.
Fixpoint fold_constants_com (c : com) : com :=
match c with
| SKIP ⇒
SKIP
| i ::= a ⇒
CAss i (fold_constants_aexp a)
| c1 ;; c2 ⇒
(fold_constants_com c1) ;; (fold_constants_com c2)
| IFB b THEN c1 ELSE c2 FI ⇒
match fold_constants_bexp b with
| BTrue ⇒ fold_constants_com c1
| BFalse ⇒ fold_constants_com c2
| b' ⇒ IFB b' THEN fold_constants_com c1
ELSE fold_constants_com c2 FI
end
| WHILE b DO c END ⇒
match fold_constants_bexp b with
| BTrue ⇒ WHILE BTrue DO SKIP END
| BFalse ⇒ SKIP
| b' ⇒ WHILE b' DO (fold_constants_com c) END
end
end.
Example fold_com_ex1 :
fold_constants_com
(* Original program: *)
(X ::= APlus (ANum 4) (ANum 5);;
Y ::= AMinus (AId X) (ANum 3);;
IFB BEq (AMinus (AId X) (AId Y)) (APlus (ANum 2) (ANum 4)) THEN
SKIP
ELSE
Y ::= ANum 0
FI;;
IFB BLe (ANum 0) (AMinus (ANum 4) (APlus (ANum 2) (ANum 1))) THEN
Y ::= ANum 0
ELSE
SKIP
FI;;
WHILE BEq (AId Y) (ANum 0) DO
X ::= APlus (AId X) (ANum 1)
END)
= (* After constant folding: *)
(X ::= ANum 9;;
Y ::= AMinus (AId X) (ANum 3);;
IFB BEq (AMinus (AId X) (AId Y)) (ANum 6) THEN
SKIP
ELSE
(Y ::= ANum 0)
FI;;
Y ::= ANum 0;;
WHILE BEq (AId Y) (ANum 0) DO
X ::= APlus (AId X) (ANum 1)
END).
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.
induction a; 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 ((aeval st a1) + (aeval st a2))
= aeval st (ANum ((aeval st a1) + (aeval st a2)))
(and similarly for AMinus/minus and AMult/mult) *)
try (destruct (fold_constants_aexp a1);
destruct (fold_constants_aexp a2);
rewrite IHa1; rewrite IHa2; reflexivity). Qed.
unfold atrans_sound. intros a. unfold aequiv. intros st.
induction a; 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 ((aeval st a1) + (aeval st a2))
= aeval st (ANum ((aeval st a1) + (aeval st a2)))
(and similarly for AMinus/minus and AMult/mult) *)
try (destruct (fold_constants_aexp a1);
destruct (fold_constants_aexp a2);
rewrite IHa1; rewrite IHa2; reflexivity). Qed.
Exercise: 3 stars, optional (fold_bexp_Eq_informal)
Here is an informal proof of the BEq case of the soundness argument for boolean expression constant folding. Read it carefully and compare it to the formal proof that follows. Then fill in the BLe case of the formal proof (without looking at the BEq case, if possible).
beval st (BEq a1 a2)
= beval st (fold_constants_bexp (BEq a1 a2)).
There are two cases to consider:
= beval st (fold_constants_bexp (BEq a1 a2)).
- First, suppose fold_constants_aexp a1 = ANum n1 and
fold_constants_aexp a2 = ANum n2 for some n1 and n2.
fold_constants_bexp (BEq a1 a2)and
= if beq_nat n1 n2 then BTrue else BFalsebeval st (BEq a1 a2)By the soundness of constant folding for arithmetic expressions (Lemma fold_constants_aexp_sound), we know
= beq_nat (aeval st a1) (aeval st a2).aeval st a1and
= aeval st (fold_constants_aexp a1)
= aeval st (ANum n1)
= n1aeval st a2so
= aeval st (fold_constants_aexp a2)
= aeval st (ANum n2)
= n2,beval st (BEq a1 a2)Also, it is easy to see (by considering the cases n1 = n2 and n1 ≠ n2 separately) that
= beq_nat (aeval a1) (aeval a2)
= beq_nat n1 n2.beval st (if beq_nat n1 n2 then BTrue else BFalse)So
= if beq_nat n1 n2 then beval st BTrue else beval st BFalse
= if beq_nat n1 n2 then true else false
= beq_nat n1 n2.beval st (BEq a1 a2)as required.
= beq_nat n1 n2.
= beval st (if beq_nat n1 n2 then BTrue else BFalse), - Otherwise, one of fold_constants_aexp a1 and
fold_constants_aexp a2 is not a constant. In this case, we
must show
beval st (BEq a1 a2)which, by the definition of beval, is the same as showing
= beval st (BEq (fold_constants_aexp a1)
(fold_constants_aexp a2)),beq_nat (aeval st a1) (aeval st a2)But the soundness of constant folding for arithmetic expressions (fold_constants_aexp_sound) gives us
= beq_nat (aeval st (fold_constants_aexp a1))
(aeval st (fold_constants_aexp a2)).aeval st a1 = aeval st (fold_constants_aexp a1)completing the case. ☐
aeval st a2 = aeval st (fold_constants_aexp a2),
Theorem fold_constants_bexp_sound:
btrans_sound fold_constants_bexp.
Proof.
unfold btrans_sound. intros b. unfold bequiv. intros st.
induction b;
(* BTrue and BFalse are immediate *)
try reflexivity.
- (* BEq *)
(* Doing induction when there are a lot of constructors makes
specifying variable names a chore, but Coq doesn't always
choose nice variable names. We can rename entries in the
context with the rename tactic: rename a into a1 will
change a to a1 in the current goal and context. *)
rename a into a1. rename a0 into a2. simpl.
remember (fold_constants_aexp a1) as a1' eqn:Heqa1'.
remember (fold_constants_aexp a2) as a2' eqn:Heqa2'.
replace (aeval st a1) with (aeval st a1') by
(subst a1'; rewrite ← fold_constants_aexp_sound; reflexivity).
replace (aeval st a2) with (aeval st a2') by
(subst a2'; rewrite ← fold_constants_aexp_sound; reflexivity).
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.
- (* BLe *)
(* FILL IN HERE *) admit.
- (* BNot *)
simpl. remember (fold_constants_bexp b) as b' eqn:Heqb'.
rewrite IHb.
destruct b'; reflexivity.
- (* BAnd *)
simpl.
remember (fold_constants_bexp b1) as b1' eqn:Heqb1'.
remember (fold_constants_bexp b2) as b2' eqn:Heqb2'.
rewrite IHb1. rewrite IHb2.
destruct b1'; destruct b2'; reflexivity.
(* FILL IN HERE *) Admitted.
Theorem fold_constants_com_sound :
ctrans_sound fold_constants_com.
Proof.
unfold ctrans_sound. intros c.
induction c; simpl.
- (* SKIP *) apply refl_cequiv.
- (* ::= *) apply CAss_congruence. apply fold_constants_aexp_sound.
- (* ;; *) apply CSeq_congruence; assumption.
- (* IFB *)
assert (bequiv b (fold_constants_bexp b)).
{ (* Pf of assertion *) apply fold_constants_bexp_sound. }
destruct (fold_constants_bexp b) eqn:Heqb;
(* If the optimization doesn't eliminate the if, then the result
is easy to prove from the IH and fold_constants_bexp_sound *)
try (apply CIf_congruence; assumption).
+ (* b always true *)
apply trans_cequiv with c1; try assumption.
apply IFB_true; assumption.
+ (* b always false *)
apply trans_cequiv with c2; try assumption.
apply IFB_false; assumption.
- (* WHILE *)
(* FILL IN HERE *) Admitted.
☐
Soundness of (0 + n) Elimination, Redux
Exercise: 4 stars, advanced, optional (optimize_0plus)
Recall the definition optimize_0plus from Imp.v:
Fixpoint optimize_0plus (e:aexp) : 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.
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.
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 — otherwise it will be long!)
optimize_0plus_bexp
optimize_0plus_com
- Give a meaningful example of this optimizer's output.
- Prove that the optimizer is sound. (This part should be very easy.)
(* FILL IN HERE *)
☐
Proving That Programs Are Not Equivalent
c1 = (X ::= 42 + 53;;
Y ::= Y + X)
c2 = (X ::= 42 + 53;;
Y ::= Y + (42 + 53))
Clearly, this particular c1 and c2 are equivalent. Is this
true in general?
Y ::= Y + X)
c2 = (X ::= 42 + 53;;
Y ::= Y + (42 + 53))
Fixpoint subst_aexp (i : id) (u : aexp) (a : aexp) : aexp :=
match a with
| ANum n ⇒ ANum n
| AId i' ⇒ if beq_id 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 (APlus (ANum 42) (ANum 53)) (APlus (AId Y) (AId X)) =
(APlus (AId Y) (APlus (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 := ∀i1 i2 a1 a2,
cequiv (i1 ::= a1;; i2 ::= a2)
(i1 ::= a1;; i2 ::= subst_aexp i1 a1 a2).
Sadly, the property does not always hold.
Theorem: It is not the case that, for all i1, i2, a1,
and a2,
By our assumption, we know that
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
(i1 ::= a1;; i2 ::= subst_aexp i1 a1 a2).
cequiv (i1 ::= a1;; i2 ::= a2)
(i1 ::= a1;; i2 ::= subst_aexp i1 a1 a2).
Consider the following program:
(i1 ::= a1;; i2 ::= subst_aexp i1 a1 a2).
X ::= APlus (AId X) (ANum 1);; Y ::= AId X
Note that
(X ::= APlus (AId X) (ANum 1);; Y ::= AId X)
/ empty_state ⇓ st1,
where st1 = { X ↦ 1, Y ↦ 1 }.
/ empty_state ⇓ st1,
cequiv (X ::= APlus (AId X) (ANum 1);; Y ::= AId X)
(X ::= APlus (AId X) (ANum 1);; Y ::= APlus (AId X) (ANum 1))
so, by the definition of cequiv, we have
(X ::= APlus (AId X) (ANum 1);; Y ::= APlus (AId X) (ANum 1))
(X ::= APlus (AId X) (ANum 1);; Y ::= APlus (AId X) (ANum 1))
/ empty_state ⇓ st1.
But we can also derive
/ empty_state ⇓ st1.
(X ::= APlus (AId X) (ANum 1);; Y ::= APlus (AId X) (ANum 1))
/ empty_state ⇓ st2,
where st2 = { X ↦ 1, Y ↦ 2 }. Note that st1 ≠ st2; this
is a contradiction, since ceval is deterministic! ☐
/ empty_state ⇓ st2,
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... *)
remember (X ::= APlus (AId X) (ANum 1);;
Y ::= AId X)
as c1.
remember (X ::= APlus (AId X) (ANum 1);;
Y ::= APlus (AId X) (ANum 1))
as c2.
assert (cequiv c1 c2) by (subst; apply Contra).
(* ... allows us to show that the command c2 can terminate
in two different final states:
st1 = {X |-> 1, Y |-> 1}
st2 = {X |-> 1, Y |-> 2}. *)
remember (t_update (t_update empty_state X 1) Y 1) as st1.
remember (t_update (t_update empty_state X 1) Y 2) as st2.
assert (H1: c1 / empty_state ⇓ st1);
assert (H2: c2 / empty_state ⇓ st2);
try (subst;
apply E_Seq with (st' := (t_update empty_state X 1));
apply E_Ass; reflexivity).
apply H in H1.
(* Finally, we use the fact that evaluation is deterministic
to obtain a contradiction. *)
assert (Hcontra: st1 = st2)
by (apply (ceval_deterministic c2 empty_state); assumption).
assert (Hcontra': st1 Y = st2 Y)
by (rewrite Hcontra; reflexivity).
subst. inversion Hcontra'. Qed.
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... *)
remember (X ::= APlus (AId X) (ANum 1);;
Y ::= AId X)
as c1.
remember (X ::= APlus (AId X) (ANum 1);;
Y ::= APlus (AId X) (ANum 1))
as c2.
assert (cequiv c1 c2) by (subst; apply Contra).
(* ... allows us to show that the command c2 can terminate
in two different final states:
st1 = {X |-> 1, Y |-> 1}
st2 = {X |-> 1, Y |-> 2}. *)
remember (t_update (t_update empty_state X 1) Y 1) as st1.
remember (t_update (t_update empty_state X 1) Y 2) as st2.
assert (H1: c1 / empty_state ⇓ st1);
assert (H2: c2 / empty_state ⇓ st2);
try (subst;
apply E_Seq with (st' := (t_update empty_state X 1));
apply E_Ass; reflexivity).
apply H in H1.
(* Finally, we use the fact that evaluation is deterministic
to obtain a contradiction. *)
assert (Hcontra: st1 = st2)
by (apply (ceval_deterministic c2 empty_state); assumption).
assert (Hcontra': st1 Y = st2 Y)
by (rewrite Hcontra; reflexivity).
subst. inversion Hcontra'. Qed.
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.Inductive var_not_used_in_aexp (X:id) : aexp → Prop :=
| VNUNum: ∀n, var_not_used_in_aexp X (ANum n)
| VNUId: ∀Y, X ≠ Y → var_not_used_in_aexp X (AId Y)
| VNUPlus: ∀a1 a2,
var_not_used_in_aexp X a1 →
var_not_used_in_aexp X a2 →
var_not_used_in_aexp X (APlus a1 a2)
| VNUMinus: ∀a1 a2,
var_not_used_in_aexp X a1 →
var_not_used_in_aexp X a2 →
var_not_used_in_aexp X (AMinus a1 a2)
| VNUMult: ∀a1 a2,
var_not_used_in_aexp X a1 →
var_not_used_in_aexp X a2 →
var_not_used_in_aexp X (AMult a1 a2).
Lemma aeval_weakening : ∀i st a ni,
var_not_used_in_aexp i a →
aeval (t_update st i ni) a = aeval st a.
Proof.
(* FILL IN HERE *) Admitted.
Using var_not_used_in_aexp, formalize and prove a correct verson
of subst_equiv_property.
(* FILL IN HERE *)
☐
Exercise: 3 stars, optional (inequiv_exercise)
Prove that an infinite loop is not equivalent to SKIPTheorem inequiv_exercise:
¬ cequiv (WHILE BTrue DO SKIP END) SKIP.
Proof.
(* FILL IN HERE *) Admitted.
☐
As we have seen (in theorem ceval_deterministic in the Imp
chapter), Imp's evaluation relation is deterministic. However,
non-determinism is an important part of the definition of many
real programming languages. For example, in many imperative
languages (such as C and its relatives), the order in which
function arguments are evaluated is unspecified. The program
fragment
In this exercise, we will extend Imp with a simple
non-deterministic command and study how this change affects
program equivalence. The new command has the syntax HAVOC X,
where X is an identifier. The effect of executing HAVOC X is
to assign an arbitrary number to the variable X,
non-deterministically. For example, after executing the program:
In a sense a variable on which we do HAVOC roughly corresponds
to an unitialized variable in the C programming language. After
the HAVOC the variable holds a fixed but arbitrary number. Most
sources of nondeterminism in language definitions are there
precisely because programmers don't care which choice is made (and
so it is good to leave it open to the compiler to choose whichever
will run faster).
We call this new language Himp (``Imp extended with HAVOC'').
Extended exercise: Non-deterministic Imp
x = 0;;
f(++x, x)
might call f with arguments (1, 0) or (1, 1), depending how
the compiler chooses to order things. This can be a little
confusing for programmers, but it gives the compiler writer useful
freedom.
f(++x, x)
HAVOC Y;;
Z ::= Y × 2
the value of Y can be any number, while the value of Z is
twice that of Y (so Z is always even). Note that we are not
saying anything about the probabilities of the outcomes — just
that there are (infinitely) many different outcomes that can
possibly happen after executing this non-deterministic code.
Z ::= Y × 2
To formalize the language, we first add a clause to the definition of
commands.
Inductive com : Type :=
| CSkip : com
| CAss : id → aexp → com
| CSeq : com → com → com
| CIf : bexp → com → com → com
| CWhile : bexp → com → com
| CHavoc : id → com. (* <---- new *)
Notation "'SKIP'" :=
CSkip.
Notation "X '::=' a" :=
(CAss X a) (at level 60).
Notation "c1 ;; c2" :=
(CSeq c1 c2) (at level 80, right associativity).
Notation "'WHILE' b 'DO' c 'END'" :=
(CWhile b c) (at level 80, right associativity).
Notation "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" :=
(CIf e1 e2 e3) (at level 80, right associativity).
Notation "'HAVOC' l" := (CHavoc l) (at level 60).
Exercise: 2 stars (himp_ceval)
Now, we must extend the operational semantics. We have provided a template for the ceval relation below, specifying the big-step semantics. What rule(s) must be added to the definition of ceval to formalize the behavior of the HAVOC command?Reserved Notation "c1 '/' st '⇓' st'" (at level 40, st at level 39).
Inductive ceval : com → state → state → Prop :=
| E_Skip : ∀st : state, SKIP / st ⇓ st
| E_Ass : ∀(st : state) (a1 : aexp) (n : nat) (X : id),
aeval st a1 = n → (X ::= a1) / st ⇓ t_update st X n
| E_Seq : ∀(c1 c2 : com) (st st' st'' : state),
c1 / st ⇓ st' → c2 / st' ⇓ st'' → (c1 ;; c2) / st ⇓ st''
| E_IfTrue : ∀(st st' : state) (b1 : bexp) (c1 c2 : com),
beval st b1 = true →
c1 / st ⇓ st' → (IFB b1 THEN c1 ELSE c2 FI) / st ⇓ st'
| E_IfFalse : ∀(st st' : state) (b1 : bexp) (c1 c2 : com),
beval st b1 = false →
c2 / st ⇓ st' → (IFB b1 THEN c1 ELSE c2 FI) / st ⇓ st'
| E_WhileEnd : ∀(b1 : bexp) (st : state) (c1 : com),
beval st b1 = false → (WHILE b1 DO c1 END) / st ⇓ st
| E_WhileLoop : ∀(st st' st'' : state) (b1 : bexp) (c1 : com),
beval st b1 = true →
c1 / st ⇓ st' →
(WHILE b1 DO c1 END) / st' ⇓ st'' →
(WHILE b1 DO c1 END) / st ⇓ st''
(* FILL IN HERE *)
where "c1 '/' st '⇓' st'" := (ceval c1 st st').
As a sanity check, the following claims should be provable for
your definition:
Example havoc_example1 : (HAVOC X) / empty_state ⇓ t_update empty_state X 0.
Proof.
(* FILL IN HERE *) Admitted.
Example havoc_example2 :
(SKIP;; HAVOC Z) / empty_state ⇓ t_update empty_state Z 42.
Proof.
(* FILL IN HERE *) Admitted.
☐
Finally, we repeat the definition of command equivalence from above:
This definition still makes perfect sense in the case of always
terminating programs, so let's apply it to prove some
non-deterministic programs equivalent or non-equivalent.
Exercise: 3 stars (havoc_swap)
Are the following two programs equivalent?
If you think they are equivalent, prove it. If you think they are
not, prove that.
If you think they are equivalent, then prove it. If you think they
are not, then prove that. (Hint: You may find the assert tactic
useful.)
Theorem ptwice_cequiv_pcopy :
cequiv ptwice pcopy ∨ ¬cequiv ptwice pcopy.
Proof. (* FILL IN HERE *) Admitted.
☐
The definition of program equivalence we are using here has some
subtle consequences on programs that may loop forever. What
cequiv says is that the set of possible terminating outcomes
of two equivalent programs is the same. However, in a language
with non-determinism, like Himp, some programs always terminate,
some programs always diverge, and some programs can
non-deterministically terminate in some runs and diverge in
others. The final part of the following exercise illustrates this
phenomenon.
Exercise: 5 stars, advanced (p1_p2_equiv)
Prove that p1 and p2 are equivalent. In this and the following exercises, try to understand why the cequiv definition has the behavior it has on these examples.Definition p1 : com :=
WHILE (BNot (BEq (AId X) (ANum 0))) DO
HAVOC Y;;
X ::= APlus (AId X) (ANum 1)
END.
Definition p2 : com :=
WHILE (BNot (BEq (AId X) (ANum 0))) DO
SKIP
END.
Intuitively, the programs have the same termination
behavior: either they loop forever, or they terminate in the
same state they started in. We can capture the termination
behavior of p1 and p2 individually with these lemmas:
Lemma p1_may_diverge : ∀st st', st X ≠ 0 →
¬ p1 / st ⇓ st'.
Proof. (* FILL IN HERE *) Admitted.
Lemma p2_may_diverge : ∀st st', st X ≠ 0 →
¬ p2 / st ⇓ st'.
Proof.
(* FILL IN HERE *) Admitted.
You should use these lemmas to prove that p1 and p2 are actually
equivalent.
Definition p3 : com :=
Z ::= ANum 1;;
WHILE (BNot (BEq (AId X) (ANum 0))) DO
HAVOC X;;
HAVOC Z
END.
Definition p4 : com :=
X ::= (ANum 0);;
Z ::= (ANum 1).
Theorem p3_p4_inequiv : ¬ cequiv p3 p4.
Proof. (* FILL IN HERE *) Admitted.
Definition p5 : com :=
WHILE (BNot (BEq (AId X) (ANum 1))) DO
HAVOC X
END.
Definition p6 : com :=
X ::= ANum 1.
Theorem p5_p6_equiv : cequiv p5 p6.
Proof. (* FILL IN HERE *) Admitted.
☐
Doing Without Extensionality (Optional)
Definition stequiv (st1 st2 : state) : Prop :=
∀(X:id), st1 X = st2 X.
Notation "st1 '~~' st2" := (stequiv st1 st2) (at level 30).
It is easy to prove that stequiv is an equivalence (i.e., it
is reflexive, symmetric, and transitive), so it partitions the set
of all states into equivalence classes.
Exercise: 1 star, optional (stequiv_refl)
Lemma stequiv_sym : ∀(st1 st2 : state),
st1 ~~ st2 →
st2 ~~ st1.
Proof.
(* FILL IN HERE *) Admitted.
st1 ~~ st2 →
st2 ~~ st1.
Proof.
(* FILL IN HERE *) Admitted.
Lemma stequiv_trans : ∀(st1 st2 st3 : state),
st1 ~~ st2 →
st2 ~~ st3 →
st1 ~~ st3.
Proof.
(* FILL IN HERE *) Admitted.
st1 ~~ st2 →
st2 ~~ st3 →
st1 ~~ st3.
Proof.
(* FILL IN HERE *) Admitted.
Lemma stequiv_t_update : ∀(st1 st2 : state),
st1 ~~ st2 →
∀(X:id) (n:nat),
t_update st1 X n ~~ t_update st2 X n.
Proof.
(* FILL IN HERE *) Admitted.
st1 ~~ st2 →
∀(X:id) (n:nat),
t_update st1 X n ~~ t_update st2 X n.
Proof.
(* FILL IN HERE *) Admitted.
☐
It is then straightforward to show that aeval and beval behave
uniformly on all members of an equivalence class:
Exercise: 2 stars, optional (stequiv_aeval)
Lemma stequiv_aeval : ∀(st1 st2 : state),
st1 ~~ st2 →
∀(a:aexp), aeval st1 a = aeval st2 a.
Proof.
(* FILL IN HERE *) Admitted.
st1 ~~ st2 →
∀(a:aexp), aeval st1 a = aeval st2 a.
Proof.
(* FILL IN HERE *) Admitted.
Lemma stequiv_beval : ∀(st1 st2 : state),
st1 ~~ st2 →
∀(b:bexp), beval st1 b = beval st2 b.
Proof.
(* FILL IN HERE *) Admitted.
st1 ~~ st2 →
∀(b:bexp), beval st1 b = beval st2 b.
Proof.
(* FILL IN HERE *) Admitted.
☐
We can also characterize the behavior of ceval on equivalent
states (this result is a bit more complicated to write down
because ceval is a relation).
Lemma stequiv_ceval: ∀(st1 st2 : state),
st1 ~~ st2 →
∀(c: com) (st1': state),
(c / st1 ⇓ st1') →
∃st2' : state,
((c / st2 ⇓ st2') ∧ st1' ~~ st2').
Proof.
intros st1 st2 STEQV c st1' CEV1. generalize dependent st2.
induction CEV1; intros st2 STEQV.
- (* SKIP *)
∃st2. split.
constructor.
assumption.
- (* := *)
∃(t_update st2 x n). split.
constructor. rewrite ← H. symmetry. apply stequiv_aeval.
assumption. apply stequiv_t_update. assumption.
- (* ; *)
destruct (IHCEV1_1 st2 STEQV) as [st2' [P1 EQV1]].
destruct (IHCEV1_2 st2' EQV1) as [st2'' [P2 EQV2]].
∃st2''. split.
apply E_Seq with st2'; assumption.
assumption.
- (* IfTrue *)
destruct (IHCEV1 st2 STEQV) as [st2' [P EQV]].
∃st2'. split.
apply E_IfTrue. rewrite ← H. symmetry. apply stequiv_beval.
assumption. assumption. assumption.
- (* IfFalse *)
destruct (IHCEV1 st2 STEQV) as [st2' [P EQV]].
∃st2'. split.
apply E_IfFalse. rewrite ← H. symmetry. apply stequiv_beval.
assumption. assumption. assumption.
- (* WhileEnd *)
∃st2. split.
apply E_WhileEnd. rewrite ← H. symmetry. apply stequiv_beval.
assumption. assumption.
- (* WhileLoop *)
destruct (IHCEV1_1 st2 STEQV) as [st2' [P1 EQV1]].
destruct (IHCEV1_2 st2' EQV1) as [st2'' [P2 EQV2]].
∃st2''. split.
apply E_WhileLoop with st2'. rewrite ← H. symmetry.
apply stequiv_beval. assumption. assumption. assumption.
assumption.
Qed.
Now we need to redefine cequiv to use ¬ instead of =. It is
not completely trivial to do this in a way that keeps the
definition simple and symmetric, but here is one approach (thanks
to Andrew McCreight). We first define a looser variant of ⇓
that "folds in" the notion of equivalence.
Reserved Notation "c1 '/' st '⇓'' st'" (at level 40, st at level 39).
Inductive ceval' : com → state → state → Prop :=
| E_equiv : ∀c st st' st'',
c / st ⇓ st' →
st' ~~ st'' →
c / st ⇓' st''
where "c1 '/' st '⇓'' st'" := (ceval' c1 st st').
Now the revised definition of cequiv' looks familiar:
A sanity check shows that the original notion of command
equivalence is at least as strong as this new one. (The converse
is not true, naturally.)
Lemma cequiv__cequiv' : ∀(c1 c2: com),
cequiv c1 c2 → cequiv' c1 c2.
Proof.
unfold cequiv, cequiv'; split; intros.
inversion H0 ; subst. apply E_equiv with st'0.
apply (H st st'0); assumption. assumption.
inversion H0 ; subst. apply E_equiv with st'0.
apply (H st st'0). assumption. assumption.
Qed.
Exercise: 2 stars, optional (identity_assignment')
Finally, here is our example once more... Notice that we use the t_update_same_no_ext lemma in order to avoid invoking functional extensionality. (You can complete the proofs.)Theorem t_update_same_no_ext : ∀X x1 x2 (m : total_map X),
t_update m x1 (m x1) x2 = m x2.
Proof.
(* FILL IN HERE *) Admitted.
Example identity_assignment' :
cequiv' SKIP (X ::= AId X).
Proof.
unfold cequiv'. intros. split; intros.
- (* -> *)
inversion H; subst; clear H. inversion H0; subst.
apply E_equiv with (t_update st'0 X (st'0 X)).
constructor. { reflexivity. }
assert (t_update st'0 X (st'0 X) ~~ st'0) as H.
{ unfold stequiv. intros Y.
apply t_update_same_no_ext. }
apply (stequiv_trans _ _ _ H H1).
- (* <- *)
(* FILL IN HERE *) Admitted.
☐
On the whole, this explicit equivalence approach is considerably
harder to work with than relying on functional
extensionality. (Coq does have an advanced mechanism called
"setoids" that makes working with equivalences somewhat easier, by
allowing them to be registered with the system so that standard
rewriting tactics work for them almost as well as for equalities.)
But it is worth knowing about, because it applies even in
situations where the equivalence in question is not over
functions. For example, if we chose to represent state mappings
as binary search trees, we would need to use an explicit
equivalence of this kind.
Additional Exercises
Exercise: 4 stars, optional (for_while_equiv)
This exercise extends the optional add_for_loop exercise from Imp.v, where you were asked to extend the language of commands with C-style for loops. Prove that the command:
for (c1 ; b ; c2) {
c3
}
is equivalent to:
c3
}
c1 ;
WHILE b DO
c3 ;
c2
END
WHILE b DO
c3 ;
c2
END
(* FILL IN HERE *)
Theorem swap_noninterfering_assignments: ∀l1 l2 a1 a2,
l1 ≠ l2 →
var_not_used_in_aexp l1 a2 →
var_not_used_in_aexp l2 a1 →
cequiv
(l1 ::= a1;; l2 ::= a2)
(l2 ::= a2;; l1 ::= a1).
Proof.
(* Hint: You'll need functional_extensionality *)
(* FILL IN HERE *) Admitted.
l1 ≠ l2 →
var_not_used_in_aexp l1 a2 →
var_not_used_in_aexp l2 a1 →
cequiv
(l1 ::= a1;; l2 ::= a2)
(l2 ::= a2;; l1 ::= a1).
Proof.
(* Hint: You'll need functional_extensionality *)
(* FILL IN HERE *) Admitted.
☐