Equiv: Program equivalence
- 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.
- 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.
- Use automation to save work! Some of these proofs are extremely long and tedious if you try to write out all the cases explicitly.
The tactic admit automatically solves the current subgoal
in any proof. This can be useful for skipping to the
interesting parts of proofs, and we'll use it in exercises
where we'd like you to finish just one case. Don't use it in
anything you turn in, though - it's cheating.
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:
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''."
- "If c1 takes st to st' and c2 takes st' to st'', then c1;c2 takes st to st'' by rule CESeq."
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:
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_l.
assert (i2 <= i1 + i2) as Hle2 by (rewrite plus_comm; apply le_plus_l).
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.
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 Imp 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.
To talk about the correctness of program transformations in the full Imp 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.
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').
Theorem aequiv_example:
aequiv (!X --- !X) A0.
Proof.
unfold aequiv. intros st. simpl.
apply minus_diag. Qed.
Theorem bequiv_example:
bequiv (!X --- !X === A0) BTrue.
Proof.
unfold bequiv. intros. unfold beval.
rewrite aequiv_example. reflexivity.
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.
☐
Theorem CIf_true_simple: forall c1 c2,
cequiv
(CIf BTrue c1 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
(CIf b c1 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)".
rewrite Hb in H5.
inversion H5.
Case "<-".
apply CEIfTrue; try assumption.
rewrite Hb. reflexivity. Qed.
An informal proof of CIf_true:
Theorem: forall b c1 c2, if b is equivalent to BTrue, then IFB b THEN c1 ELSE c2 is equivalent to c1.
Proof:
Theorem: forall b c1 c2, if b is equivalent to BTrue, then IFB 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 (IFB b THEN c1 ELSE
c2) / st ~~> st' then c1 / st ~~> st'.
There are only two ways we can have IFB b THEN c1 ELSE c2) / st ~~> st', using CEIfTrue or CEIfFalse.
- Suppose the final rule used to show (IFB 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 (IFB 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.
- Suppose the final rule used to show (IFB 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.
- (<-) Again, we are given that b is equivalent to BTrue.
We must show, for all st and st', that if c1 / st ~~> st'
then (IFB 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 (IFB b THEN c1 ELSE c2) / st ~~> st'. ☐
Theorem CIf_false: forall b c1 c2,
bequiv b BFalse
-> cequiv
(CIf b c1 c2)
c2.
Proof.
(* FILL IN HERE *) Admitted.
bequiv b BFalse
-> cequiv
(CIf b c1 c2)
c2.
Proof.
(* FILL IN HERE *) Admitted.
☐
Theorem CWhile_true_nonterm : forall b c st st',
bequiv b BTrue
-> ~( (WHILE b DO c LOOP) / st ~~> st' ).
Proof.
intros b c st st' Hb.
intros H.
remember (WHILE b DO c LOOP) 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! *)
rewrite Hb in H. inversion H.
Case "CEWhileLoop". (* immediate from the IH *)
apply IHceval2. reflexivity. Qed.
Explain what the lemma CWhile_true_nonterm means in English.
(* FILL IN HERE *)
(* FILL IN HERE *)
☐
You'll want to use CWhile_true_nonterm here...
Theorem CWhile_true: forall b c,
bequiv b BTrue
-> cequiv
(WHILE b DO c LOOP)
(WHILE BTrue DO SKIP LOOP).
Proof.
(* FILL IN HERE *) Admitted.
☐
Theorem CWhile_false : forall b c,
bequiv b BFalse
-> cequiv
(WHILE b DO c LOOP)
SKIP.
Proof.
intros b c Hb.
unfold cequiv. split; intros.
Case "->".
inversion H; subst.
SCase "CEWhileEnd".
apply CESkip.
SCase "CEWhileLoop".
rewrite Hb in H2. inversion H2.
Case "<-".
inversion H; subst.
apply CEWhileEnd.
rewrite Hb.
reflexivity. Qed.
Write an informal proof of CWhile_false.
(* FILL IN HERE *)
☐
(* FILL IN HERE *)
☐
Theorem loop_unrolling: forall b c,
cequiv
(WHILE b DO c LOOP)
(CIf b (c; WHILE b DO c LOOP) 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 "loop doesn't run".
inversion H5; subst. apply CEWhileEnd. assumption. Qed.
Theorem seq_assoc : forall 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.
☐
Theorem swap_if_branches: forall b e1 e2,
cequiv
(CIf b e1 e2)
(CIf (BNot b) e2 e1).
Proof.
(* FILL IN HERE *) Admitted.
cequiv
(CIf b e1 e2)
(CIf (BNot b) e2 e1).
Proof.
(* FILL IN HERE *) Admitted.
☐
The equivalences on aexps, bexps, and coms 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.
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.
apply iff_sym. assumption.
Qed.
Lemma iff_trans : 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 iff_trans with (c2 / st ~~> st'). apply H12. apply H23. Qed.
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:
Motivating example (see below): fold_constants_com_sound
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.
Both directions of this next proof are a little tricky - we
need to go by induction...
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.
Case "->".
remember (WHILE b1 DO c1 LOOP) 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' LOOP) 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.
Theorem CSeq_congruence : forall 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 : 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 *) Admitted.
bequiv b b' -> cequiv c1 c1' -> cequiv c2 c2' ->
cequiv (CIf b c1 c2) (CIf b' c1' c2').
Proof.
(* FILL IN HERE *) Admitted.
☐
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.
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 coms.
We can define a notion of soundness for translations of aexps, bexps, and coms.
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).
An expression is constant when it contains no variable
references.
Constant folding is an optimization that finds constant expressions and reduces them.
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 BfEq and BLe 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
| BLe 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') => 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
| 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;
(CIf (!X --- !Y === A2 +++ A4)
SKIP
(Y ::= A0));
(CIf (A0 <<= A4 --- (A2 +++ A1))
(Y ::= A0)
SKIP);
WHILE (!Y === A0) DO X ::= !X +++ A1 LOOP) =
(X ::= ANum 9;
Y ::= !X --- A3;
(CIf (!X --- !Y === A6)
SKIP
(Y ::= A0));
Y ::= A0;
WHILE (!Y === A0) DO X ::= !X +++ A1 LOOP).
Proof. reflexivity. Qed.
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.
Or, here's 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 (destruct (fold_constants_aexp a1);
destruct (fold_constants_aexp a2);
rewrite IHa1; rewrite IHa2; reflexivity). Qed.
Complete the BLe 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 "BLe".
(* FILL IN HERE *) admit.
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.
☐
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 if, 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 *) Admitted.
☐
Recall the definition optimize_0plus from Imp.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 functions:
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).
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 functions:
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 *)
☐
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).
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_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 ((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.
First, a helper lemma:
First, a helper lemma:
Lemma cequiv_state: forall c1 c2 st st' st'',
cequiv c1 c2 ->
c1 / st ~~> st' ->
c2 / st ~~> st'' ->
st' = st''.
Proof.
intros c1 c2 st st' st'' Hcequiv Hc1 Hc2.
unfold cequiv in Hcequiv. destruct (Hcequiv st st') as [Hc12 _].
(* By equivalence c2 / st ~~> st' *)
apply Hc12 in Hc1.
(* By determinacy, st' = st'' *)
apply (ceval_deterministic c2 st); assumption. Qed.
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 ::= !X +++ A1; Y ::= !X) as c1.
remember (X ::= !X +++ A1; Y ::= !X +++ A1) as c2.
assert (cequiv c1 c2) by (subst; apply Contra).
(* This 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 (override (override empty_state X 1) Y 1) as st'.
remember (override (override empty_state X 1) Y 2) as st''.
assert (st' = st'') as Hcontra.
Case "Pf of Hcontra".
(* This can be shown by using cequiv_state,
with appropriate "final" states for c1 and c2 *)
assert (c1 / empty_state ~~> st') as H1;
assert (c2 / empty_state ~~> st'') as H2;
try (subst;
apply CESeq with (st' := (override empty_state X 1));
apply CEAss; reflexivity).
apply (cequiv_state c1 c2 empty_state st' st''); try assumption.
(* Finally, we use the "equality" of the different states
to obtain a contradiction. *)
assert (st' Y = st'' Y) as Hcontra'
by (rewrite Hcontra; reflexivity).
subst; inversion Hcontra'. Qed.
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 (override (override empty_state X 1) Y 1) as st'.
remember (override (override 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 (override 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 (override 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! ☐
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! ☐
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.
Formalize this claim and prove that it is correct.
(* FILL IN HERE *)
☐
Theorem inequiv_exercise:
~ cequiv (WHILE BTrue DO SKIP LOOP) SKIP.
Proof.
(* FILL IN HERE *) Admitted.
~ cequiv (WHILE BTrue DO SKIP LOOP) SKIP.
Proof.
(* FILL IN HERE *) Admitted.
☐
(* Recall the factorial program: *)
(* Print fact_body. Print fact_loop. Print fact_com. *)
Fixpoint real_fact (n:nat) {struct n} : nat :=
match n with
| O => 1
| S n' => mult n (real_fact n')
end.
Definition fact_invariant (x:nat) (st:state) :=
exists y, exists z,
st Y = y
/\ st Z = z
/\ mult y (real_fact z) = real_fact x.
Theorem fact_body_preserves_invariant: forall st st' x,
fact_invariant x st
-> st Z <> 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]. rewrite Heqz in HZ.
(* 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 HZ.
rewrite (override_neq Z Y); auto.
rewrite (override_neq Y Z); auto.
repeat rewrite override_eq in *.
split. Case "Y correct".
reflexivity.
split. Case "Z correct".
(* Here's one of those pesky arithmetic proofs that often
come up. We want to solve the goal st Z - 1 = z', which is
obviously true given the hypothesis HZ: st Z = S z'.
It is beneath the dignity of us humans to search
around for the right lemma to do this. Fortunately, there's
a powerful tactic for solving linear arithmetic inequalities (and
equalities). It's called omega, and it's based on the Omega
algorithm invented in 1992 by William Pugh. *)
omega.
(* omega isn't magic. For example, it can't handle nonlinear
equations such as x*x*y. But it often helps. *)
Case "mult invariant preserved".
rewrite <- Hm.
simpl. rewrite <- mult_assoc.
assert (mult (S z') (real_fact z') = plus (real_fact z') (mult z' (real_fact z'))).
simpl. omega.
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 (st Z <> 0) as HZnz.
intros Contra.
inversion H0; subst. symmetry in H2; apply negb_sym 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 LOOP) / st ~~> st'
-> beval st' b = false.
Proof.
intros b c st st' Hce.
remember (WHILE b DO c LOOP) 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,
st X = x
-> fact_com / st ~~> st'
-> st' Y = real_fact 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 (override (override st Z (aeval st (!X))) Y
(aeval (override st Z (aeval st (!X))) A1)) as st'.
assert (fact_invariant (st X) st').
unfold fact_invariant.
exists 1. exists (st X).
split.
subst st'. reflexivity.
split.
subst st'. simpl. reflexivity.
apply mult_1_l.
(* and that when the loop is done running, the invariant is maintained *)
assert (fact_invariant (st 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. symmetry in H0; apply negb_sym in H0.
rewrite HZ in H0. symmetry in H0.
apply beq_nat_eq in H0. subst z.
simpl in Hf. rewrite H0 in Hf. rewrite mult_1_r in Hf. subst y.
assumption. Qed.
st X = x
-> fact_com / st ~~> st'
-> st' Y = real_fact 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 (override (override st Z (aeval st (!X))) Y
(aeval (override st Z (aeval st (!X))) A1)) as st'.
assert (fact_invariant (st X) st').
unfold fact_invariant.
exists 1. exists (st X).
split.
subst st'. reflexivity.
split.
subst st'. simpl. reflexivity.
apply mult_1_l.
(* and that when the loop is done running, the invariant is maintained *)
assert (fact_invariant (st 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. symmetry in H0; apply negb_sym in H0.
rewrite HZ in H0. symmetry in H0.
apply beq_nat_eq in H0. subst z.
simpl in Hf. rewrite H0 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!
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',
st X = x'
/\ st Z = z'
/\ minus z' x' = minus z x.
(* FILL IN HERE *)
☐
The way override_eq is stated (in the section on mappings
in Imp.v) may have looked a bit surprising: wouldn't it be
simpler just to say lookup k (override 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 override_eq need to be changed to use the
simplified version.
☐
Add C-style for loops to the language of commands in
Imp.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 Imp.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
LOOP
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
LOOP
(* FILL IN HERE *)
☐