Library ex8
Blatt 8 —- Program Equivalences
SemProg SoSe 2013, Set 8
Require Export Equiv.
Exercise 1: 5 points (Lemmas on behavorial equivalence)
Behavioral Equivalence is an Equivalence
Lemma refl_aequiv : forall (a : aexp), aequiv a a.
Proof.
Admitted.
Lemma sym_aequiv : forall (a1 a2 : aexp),
aequiv a1 a2 -> aequiv a2 a1.
Proof.
Admitted.
Lemma trans_aequiv : forall (a1 a2 a3 : aexp),
aequiv a1 a2 -> aequiv a2 a3 -> aequiv a1 a3.
Proof.
Admitted.
Lemma refl_bequiv : forall (b : bexp), bequiv b b.
Proof.
Admitted.
Lemma sym_bequiv : forall (b1 b2 : bexp),
bequiv b1 b2 -> bequiv b2 b1.
Proof.
Admitted.
Lemma trans_bequiv : forall (b1 b2 b3 : bexp),
bequiv b1 b2 -> bequiv b2 b3 -> bequiv b1 b3.
Proof.
Admitted.
Lemma refl_cequiv : forall (c : com), cequiv c c.
Proof.
Admitted.
Lemma sym_cequiv : forall (c1 c2 : com),
cequiv c1 c2 -> cequiv c2 c1.
Proof.
Admitted.
Lemma iff_trans : forall (P1 P2 P3 : Prop),
(P1 <-> P2) -> (P2 <-> P3) -> (P1 <-> P3).
Proof.
Admitted.
Lemma trans_cequiv : forall (c1 c2 c3 : com),
cequiv c1 c2 -> cequiv c2 c3 -> cequiv c1 c3.
Proof.
Admitted.
Exercise 2: 5 points (skip_right)
Recall that during the lecutre we did a theorem skip_left. Now prove that adding a SKIP after a command results in an equivalent programTheorem skip_right: forall c,
cequiv
(c; SKIP)
c.
Proof. Admitted.
Exercise 3: 7.5 points (swap_if_branches)
Show that we can swap the branches of an IF by negating its conditionTheorem swap_if_branches: forall b e1 e2,
cequiv
(IFB b THEN e1 ELSE e2 FI)
(IFB BNot b THEN e2 ELSE e1 FI).
Proof. Admitted.
Theorem seq_assoc : forall c1 c2 c3,
cequiv ((c1;c2);c3) (c1;(c2;c3)).
Proof. Admitted.
Theorem assign_aequiv : forall X e,
aequiv (AId X) e ->
cequiv SKIP (X ::= e).
Proof. Admitted.
Exercise 6: 7.5 points (CWhile_congruence, CSeq_congruence, CIf_congruence)
Theorem CWhile_congruence : forall b1 b1' c1 c1',
bequiv b1 b1' -> cequiv c1 c1' ->
cequiv (WHILE b1 DO c1 END) (WHILE b1' DO c1' END).
Proof.
unfold bequiv,cequiv.
intros b1 b1' c1 c1' Hb1e Hc1e st st'.
split; intros Hce.
Case "->".
remember (WHILE b1 DO c1 END) as cwhile.
induction Hce; inversion Heqcwhile; subst.
SCase "E_WhileEnd". apply E_WhileEnd. rewrite <- Hb1e. assumption.
SCase "E_WhileLoop". apply E_WhileLoop with (st' := st').
SSCase "a) show that guard evaluates to true". rewrite <- Hb1e. assumption.
SSCase "b) c1' indeed evaluates to st'". apply Hc1e. assumption.
SSCase "c) subsequent loop execution". apply IHHce2. reflexivity.
Case "<-". Admitted.
Theorem CSeq_congruence : forall c1 c1' c2 c2',
cequiv c1 c1' -> cequiv c2 c2' ->
cequiv (c1;c2) (c1';c2').
Proof.
Admitted.
Theorem CIf_congruence : forall 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.
Admitted.
This is the end of obligatory exercises.
Extended Bonusaufgabe: 15 points (Non-deterministic Imp)
Module Himp.
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.
Tactic Notation "com_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "SKIP" | Case_aux c "::=" | Case_aux c ";"
| Case_aux c "IFB" | Case_aux c "WHILE" | Case_aux c "HAVOC" ].
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).
(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 : forall st : state, SKIP / st || st
| E_Ass : forall (st : state) (a1 : aexp) (n : nat) (X : id),
aeval st a1 = n -> (X ::= a1) / st || update st X n
| E_Seq : forall (c1 c2 : com) (st st' st'' : state),
c1 / st || st' -> c2 / st' || st'' -> (c1 ; c2) / st || st''
| E_IfTrue : forall (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 : forall (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 : forall (b1 : bexp) (st : state) (c1 : com),
beval st b1 = false -> (WHILE b1 DO c1 END) / st || st
| E_WhileLoop : forall (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''
where "c1 '/' st '||' st'" := (ceval c1 st st').
Tactic Notation "ceval_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "E_Skip" | Case_aux c "E_Ass" | Case_aux c "E_Seq"
| Case_aux c "E_IfTrue" | Case_aux c "E_IfFalse"
| Case_aux c "E_WhileEnd" | Case_aux c "E_WhileLoop"
].
As a sanity check, the following claims should be provable for
your definition:
Example havoc_example1 : (HAVOC X) / empty_state || update empty_state X 0.
Proof.
Admitted.
Example havoc_example2 :
(SKIP; HAVOC Z) / empty_state || update empty_state Z 42.
Proof.
Admitted.
☐
Finally, we repeat the definition of command equivalence from above:
Definition cequiv (c1 c2 : com) : Prop := forall st st' : state,
c1 / st || st' <-> c2 / st || st'.
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.
The first reasonably difficult past of the exercise: (havoc_swap)
Are the following two programs equivalent?Definition pXY :=
HAVOC X; HAVOC Y.
Definition pYX :=
HAVOC Y; HAVOC X.
If you think they are equivalent, prove it. If you think they are
not, prove that.
Theorem pXY_cequiv_pYX :
cequiv pXY pYX \/ ~cequiv pXY pYX.
Proof. Admitted.
Definition ptwice :=
HAVOC X; HAVOC Y.
Definition pcopy :=
HAVOC X; Y ::= AId X.
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. 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.
The really interesting and difficult part of the exercise: (havoc_diverge)
Prove the following program equivalences and non-equivalences, and 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.
Just a bunch of lemmas you can find useful and illuminating...
Lemma nateq_helper : forall n m, negb (beq_nat n m) = false -> n = m.
Proof. Admitted.
Super-easy, just like the next one...
Lemma natneq_helper : forall n m, negb (beq_nat n m) = true -> n <> m.
Proof. Admitted.
Lemma p1_may_diverge : forall st st', st X <> 0 ->
~ p1 / st || st'.
Proof.
Admitted.
Lemma p2_may_diverge : forall st st', st X <> 0 ->
~ p2 / st || st'.
Proof. Admitted.
Theorem p1_p2_equiv : cequiv p1 p2.
Proof. Admitted.
Programs p3 and p4 are not equivalent:
when p3 terminates, even though X definitely has value 0,
Z might have any natural number as the value.
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. Admitted.
Definition p5 : com :=
WHILE (BNot (BEq (AId X) (ANum 1))) DO
HAVOC X
END.
Definition p6 : com :=
X ::= ANum 1.
Programs p5 and p6 are equivalent although p5 may diverge,
while p6 always terminates. The definition we took for cequiv
cannot distinguish between these two scenarios. It accepts the two
programs as equivalent on the basis that: if p5 terminates it
produces the same final state as p6, and there exists an
execution in which p5 terminates and does exactly as p6.
There are two directions to the proof:
->: Observe that whenever p5 terminates, it does so with X
set to 1, and no other variable changed. But this is exactly the
behavior of p6. Thus given a pair of states st and st' and
that p5 / st || st', the answer to the question "Does p6 / st
|| st'?" is "Yes".
<- (and more controversially): Given that p6 / st || st' for
some st and st', can we show that p5 / st | st'? Observe
that we can use the hypothesis to conclude that st' = update st X
1. Is there some execution of p5 starting from st which also
ends up in st'? Yes!
Hence their equivalence.
Lemma p5_summary : forall st st', p5 / st || st' -> st' = update st X 1.
Proof. Admitted.
Theorem p5_p6_equiv : cequiv p5 p6.
Proof. Admitted.
☐
End Himp.