(** * Hoare Logic
Version of 3/22/2009
Please include the pennkey of every member of your group
(* FILL IN HERE *)
*)
Require Export Logicsol.
(* Over the past two weeks, we've begun applying the mathematical
tools developed in the first part of the course to studying
the theory of a small programming language. (This language is
often called IMP, since it is a language of pure imperative
programs.)
- We defined a type of ABSTRACT SYNTAX TREES for IMP,
together with an EVALUATION RELATION (a partial function on
states) that specifies the OPERATIONAL SEMANTICS of
programs.
If the course had ended at this point, we would still have
gotten to something extremely useful: a set of tools for
defining and discussing programming languages and language
features that are mathematically precise, easy to work
with, and very flexible.
The language we defined, though small, captures some of the
key features of full-blown languages like C, C#, and Java,
including the fundamental notion of mutable state and some
common control structures.
- We proved a number of METATHEORETIC PROPERTIES ("meta" in
the sense that they are properties of the language as a
whole, rather than properties of particular programs in the
language), including:
- determinacy of evaluation
- equivalence of some different ways of writing down
the definition
- guaranteed termination of certain classes of programs
- correctness (in the sense of preserving behavioral
equivalence) of a number of useful program
transformations
All of these properties -- especially the behavioral
equivalences -- are things that language designers,
compiler writers, and users really care about knowing.
Indeed, many of them are so fundamental to our
understanding of the programming languages we deal with
that we may not consciously recognize them as "theorems."
But, as the discussion of [subst_equiv_property] showed,
properties that seem intuitively obvious can sometimes be
quite subtle or, in some cases, actually even wrong!
We'll return to this theme later in the course when we
discuss TYPES and TYPE SOUNDNESS.
- We saw a couple of examples of PROGRAM VERIFICATION --
using the precise definition of IMP to prove formally that
certain particular programs (factorial and slow
subtraction) satisfied particular specifications of their
behavior.
This week, we're going to take this idea further. We'll
develop a reasoning system called FLOYD-HOARE LOGIC (often
shortened to just HOARE LOGIC), in which each of the
syntactic constructs of IMP is equipped with a single,
generic "proof rule" that can be used to reason about
programs involving this construct.
Hoare Logic has a long history, dating back to the 1960s,
and it has been the subject of intensive research right up
to the present day. It lies at the core of a huge variety
of tools that are now being used to specify and verify
real software systems.
*)
(* ------------------------------------------------------- *)
(** * A cleaner presentation of WHILE programs *)
(* Before we begin with Hoare Logic proper, it will be useful to
make a couple of small changes in the way we defined IMP:
- Instead of using bare numbers to represent program
identifiers, we'll define [id] as a new inductive type
with a single constructor [Loc] (taking a [nat] as
argument). This helps keep [id]s separate from numbers
in the proofs.
- We'll simplify the definition of states so that, rather
than mapping [id]s to [option nat]s, they just map [id]s
to [nat]s (returning 0 for identifiers that have not been
bound). This considerably streamlines a lot of low-level
bookkeeping in proofs.
*)
(* ------------------------------------------------------- *)
(* Simplified states *)
Inductive id : Set :=
Loc : nat -> id.
Definition beq_id id1 id2 :=
match (id1, id2) with
(Loc n1, Loc n2) => beq_nat n1 n2
end.
Definition state := id->nat.
Definition empty_state : state := fun _ => 0.
(* redefinitions of basic operations on states to use the new
definition of [id]s *)
Definition override (st : state) (V:id) (n : nat) :=
fun V' => if beq_id V V' then n else st V'.
Theorem override_eq : forall n V st,
(override st V n) V = n.
Proof.
intros n V st.
unfold override.
destruct V. unfold beq_id.
rewrite <- beq_nat_refl.
reflexivity.
Qed.
Theorem override_neq : forall n1 n2 l1 l2 st,
st l1 = n1 ->
beq_id l2 l1 = false ->
(override st l2 n2) l1 = n1.
Proof.
intros n1 n2 l1 l2 st Hn1 Hneq.
unfold override.
rewrite -> Hneq.
apply Hn1.
Qed.
(* ------------------------------------------------------- *)
(* Now we need to redo the basic definitions of aexps, bexps, etc. *)
Inductive aexp : Set :=
| ANum : nat -> aexp
| AId : id -> aexp
| APlus : aexp -> aexp -> aexp
| AMinus : aexp -> aexp -> aexp
| AMult : aexp -> aexp -> aexp.
Tactic Notation "aexp_cases" tactic(first) tactic(c) :=
first;
[ c "ANum" | c "AId" | c "APlus" | c "AMinus" | c "AMult" ].
Notation A0 := (ANum 0).
Notation A1 := (ANum 1).
Notation A2 := (ANum 2).
Notation A3 := (ANum 3).
Notation A4 := (ANum 4).
Notation A5 := (ANum 5).
Notation A6 := (ANum 6).
Notation "a1 '***' a2" := (AMult a1 a2) (at level 50).
Notation "a1 '---' a2" := (AMinus a1 a2) (at level 40).
Notation "a1 '+++' a2" := (APlus a1 a2) (at level 40).
Notation "'!' X" := (AId X) (at level 30).
Definition X : id := Loc 0.
Definition Y : id := Loc 1.
Definition Z : id := Loc 2.
Inductive bexp : Set :=
| BTrue : bexp
| BFalse : bexp
| BEq : aexp -> aexp -> bexp
| BLtEq : aexp -> aexp -> bexp
| BNot : bexp -> bexp
| BAnd : bexp -> bexp -> bexp
| BOr : bexp -> bexp -> bexp.
Notation "b1 '===' b2" := (BEq b1 b2) (at level 60).
Notation "b1 '<<=' b2" := (BLtEq b1 b2) (at level 60).
Tactic Notation "bexp_cases" tactic(first) tactic(c) :=
first;
[ c "BTrue" | c "BFalse" | c "BEq" | c "BLtEq" |
c "BNot" | c "BAnd" | c "BOr" ].
Inductive com : Set :=
| CSkip : com
| CAss : id -> aexp -> com
| CSeq : com -> com -> com
| CIf : bexp -> com -> com -> com
| CWhile : bexp -> com -> com.
Tactic Notation "com_cases" tactic(first) tactic(c) :=
first;
[ c "CSkip" | c "CAss" | c "CSeq" | c "CIf" | c "CWhile" ].
Notation "'skip'" :=
CSkip.
Notation "c1 ; c2" :=
(CSeq c1 c2) (at level 80, right associativity).
Notation "V '::=' a" :=
(CAss V a) (at level 60).
Notation "'while' b 'do' c" :=
(CWhile b c) (at level 80, right associativity).
Notation "'testif' e1 'then' e2 'else' e3" :=
(CIf e1 e2 e3) (at level 80, right associativity).
(* Evaluation: [aeval] becomes a bit simpler in the [AId] case;
everything else is the same as before *)
Fixpoint aeval (st : state) (e : aexp) {struct e} : nat :=
match e with
| ANum n => n
| AId V => st V
| APlus a1 a2 => plus (aeval st a1) (aeval st a2)
| AMinus a1 a2 => minus (aeval st a1) (aeval st a2)
| AMult a1 a2 => mult (aeval st a1) (aeval st a2)
end.
Fixpoint beval (st : state) (e : bexp) {struct e} : bool :=
match e with
| BTrue => true
| BFalse => false
| BEq a1 a2 => beq_nat (aeval st a1) (aeval st a2)
| BLtEq a1 a2 => ble_nat (aeval st a1) (aeval st a2)
| BNot b1 => negb (beval st b1)
| BAnd b1 b2 => andb (beval st b1) (beval st b2)
| BOr b1 b2 => orb (beval st b1) (beval st b2)
end.
Inductive ceval : state -> com -> state -> Prop :=
| CESkip : forall st,
ceval st CSkip st
| CEAss : forall st a1 n V,
aeval st a1 = n ->
ceval st (CAss V a1) (override st V n)
| CESeq : forall c1 c2 st st' st'',
ceval st c1 st' ->
ceval st' c2 st'' ->
ceval st (CSeq c1 c2) st''
| CEIfTrue : forall st st' b1 c1 c2,
beval st b1 = true ->
ceval st c1 st' ->
ceval st (CIf b1 c1 c2) st'
| CEIfFalse : forall st st' b1 c1 c2,
beval st b1 = false ->
ceval st c2 st' ->
ceval st (CIf b1 c1 c2) st'
| CEWhileEnd : forall b1 st c1,
beval st b1 = false ->
ceval st (CWhile b1 c1) st
| CEWhileLoop : forall st st' st'' b1 c1,
beval st b1 = true ->
ceval st c1 st' ->
ceval st' (CWhile b1 c1) st'' ->
ceval st (CWhile b1 c1) st''.
Tactic Notation "ceval_cases" tactic(first) tactic(c) := first; [
c "CESkip" | c "CEAss" | c "CESeq" | c "CEIfTrue" | c "CEIfFalse"
| c "CEWhileEnd" | c "CEWhileLoop" ].
Notation "c1 '/' st '-->' st'" := (ceval st c1 st') (at level 40).
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(** ** Assertions *)
(* If we're going to talk about specifications of programs, the
first thing we'll want is a way of making ASSERTIONS about
properties that hold at particular points in time -- i.e.,
properties that may or may not be true of a given state. *)
Definition Assertion := state->Prop.
(* Exercise: 1 star (assertions) *)
(* Paraphrase the following assertions in English.
fun st => st X = 3
fun st => st X = x
fun st => st X <= st Y
fun st => st X = 3 \/ st X <= st Y
fun st => (mult (st Z) (st Z)) <= x
/\ ~ ((mult (S (st Z)) (S (st Z))) <= x)
fun st => True
fun st => False
(Remember that one-star exercises do not need to be handed in.)
*)
(* This way of writing assertions is correct -- it precisely
captures what we mean, and it is exactly what we will use in
Coq proofs -- but it is not very nice to look at: every single
assertion that we ever write is going to begin with [fun st
=>], and everyplace we refer to a variable in the current
state it is written [st X]. Moreover, this is the *only* way
we use states and the only way we refer to the values of
variables in the current state. (We never need to talk about
two states at the same time, etc.) So when we are writing
down assertions in informal contexts, we can make some
simplifications: drop the initial [fun st =>] and write just
[X] instead of [st X]. For example, instead of
fun st => (mult (st Z) (st Z)) <= x
/\ ~ ((mult (S (st Z)) (S (st Z))) <= x)
we'll write just
(mult Z Z) <= x /\ ~ ((mult (S Z) (S Z)) <= x).
*)
(* ------------------------------------------------------- *)
(** ** Hoare triples *)
(* Next, we need a way of specifying -- making a general claim
about -- the behavior of a command. Since we've defined
assertions as a way of making general claims about the
properties of states, and since the behavior of a command is
to transform one state to another, a general claim about a
command takes the following form:
"If c is started in a state satisfying assertion P, then
when (and if) c terminates, the final state is guaranteed
to satisfy the assertion Q."
Such a claim is called a HOARE TRIPLE. The property P is
called a PRECONDITION, and Q is a POSTCONDITION.
Since we'll be working a lot with Hoare triples, it's useful
to have a compact notation:
{{ P }} c {{ Q }}.
(Traditionally, Hoare triples are written {P} c {Q}, but
single braces are already used in Coq.)
*)
Definition hoare_triple (P:Assertion) (c:com) (Q:Assertion) : Prop :=
forall st st',
c / st --> st'
-> P st
-> Q st'.
Notation "{{ P }} c {{ Q }}" := (hoare_triple P c Q) (at level 90).
(* Exercise: 1 star (triples) *)
(* Paraphrase the following Hoare triples in English. (Note that
we're using the informal convention for writing down assertions.)
{{True}} c {{X = 5}}
{{X = x}} c {{X = plus x 5)}}
{{X <= Y}} c {{Y <= X}}
{{True}} c {{False}}
{{X = x}}
c
{{Y = factorial x}}.
{{True}}
c
{{(mult Z Z) <= x /\ ~ ((mult (S Z) (S Z)) <= x)}}
*)
(* Exercise: 1 star (valid_triples) *)
(* Which of the following Hoare triples are VALID (i.e., the
claimed relation between [P], [c], and [Q] is true)?
{{True}} X ::= A5 {{X = 5}}
{{X = 2}} X ::= !X +++ 1 {{X = 3}}
{{True}} X ::= A5; Y ::= A0 {{X = 5}}
{{X = 2 /\ X = 3}} X ::= A5 {{X = 0}}
{{True}} skip {{False}}
{{False}} skip {{True}}
{{True}} while BTrue do skip {{False}}
{{X = 0}} while !X === A0 do X ::= !X +++ 1 {{X = 1}}
{{X = 1}} while BNot (!X === A0) do X ::= !X +++ 1 {{X = 100}}
*)
(* To get us warmed up, here are two simple lemmas about Hoare
triples *)
Theorem hoare_post_true : forall (P Q : Assertion) c,
(forall st, Q st) ->
{{P}} c {{Q}}.
Proof.
intros P Q c H. unfold hoare_triple.
intros st st' Heval HP.
apply H. Qed.
Theorem hoare_pre_false : forall (P Q : Assertion) c,
(forall st, ~(P st)) ->
{{P}} c {{Q}}.
Proof.
intros P Q c H. unfold hoare_triple.
intros st st' Heval HP.
unfold not in H. apply H in HP.
destruct HP. Qed.
(* ------------------------------------------------------- *)
(** ** Weakest preconditions *)
(* Some Hoare triples are more interesting than others. For example,
{{ False }} X ::= !Y + A1 {{ X <= 5 }}
is perfectly valid, but it tells us nothing useful -- in
particular, it doesn't tell us how we can use the command [X
::= !Y + A1] to achieve the postcondition [X <= 5].
By contrast,
{{ Y <= 4 /\ Z = 0 }} X ::= !Y + A1 {{ X <= 5 }}
is useful: it tells us that, if we can somehow create a
situation in which we know that [Y <= 4 /\ Z = 0], then
running this command will produce a state satisfying this
postcondition. However, this triple is still not as useful as
it could be, because the [Z = 0] clause in the precondition
actually has nothing to do with the postcondition [X <= 5].
The *most* useful triple (with the same command and
postcondition) is this one:
{{ Y <= 4 }} X ::= !Y + A1 {{ X <= 5 }}
We say that [Y <= 4] is the WEAKEST PRECONDITION of the
command [X ::= !Y + A1] for the postcondition [X <= 5].
In general, we say that "P is the weakest precondition of c for Q" if
1) {{P}} c {{Q}}, and
2) if P' is an assertion such that {{P'}}c{{Q}}, then, for
all states st, (P' st) implies (P st).
That is, (1) P suffices to guarantee that Q holds after c,
and (2) P is the weakest (easiest to satisfy) assertion that
guarantees Q after c. *)
(* Exercise: 1 star (wp) *)
(* What are the weakest preconditions of the following commands
for the following postconditions?
{{ ? }} skip {{ X = 5 }}
{{ ? }} X ::= !Y +++ !Z {{ X = 5 }}
{{ ? }} X ::= !Y {{ X = Y }}
{{ ? }}
testif !X === A0
then Y ::= !Z +++ A1
else Y ::= !W +++ A2
{{ Y = 5 }}
{{ ? }}
X ::= 5
{{ X = 0 }}
{{ ? }}
while BTrue do X ::= 0
{{ X = 0 }}
*)
(* ------------------------------------------------------- *)
(** ** Proof rule for assignment *)
(* The rule for reasoning about assignment is the most basic of
the Hoare rules... and probably the trickiest! Here's how it
works.
Consider this (valid) Hoare triple:
{{ Y = 1 }} X ::= !Y {{ X = 1 }}
In English: if we start out in a state where the value of Y is
1 and we assign !Y to X, then we'll finish in a state where X
is 1. That is, the property of being equal to 1 gets
transferred from Y to X.
Similarly, in
{{ Y + Z = 1 }} X ::= !Y +++ !Z {{ X = 1 }}
the same property (being equal to one) gets transferred to X
from the expression [!Y +++ !Z] on the right-hand side of the
assignment.
More generally, if a is *any* arithmetic expression, then
{{ a = 1 }} X ::= a {{ X = 1 }}
is a valid Hoare triple.
Even more generally, if [P] is *any* property of numbers and [a] is
any arithmetic expression, then
{{ P(a) }} X ::= a {{ P(X) }}
is a valid Hoare triple.
Rephrasing this a bit leads us to the general Hoare rule for
assignment:
{{ P where a is substituted for X }} X ::= a {{ P }}
This rule looks backwards to everyone at first -- what it's saying
is that, if P holds in an environment where X is replaced by the
value of a, then P still holds after executing [X ::= a].
For example, these are valid applications of the assignment rule:
{{ X + 1 <= 5 }} X ::= !X +++ A1 {{ X <= 5 }}
{{ 3 = 3 }} X ::= A3 {{ X = 3 }}
{{ 0 <= 3 /\ 3 <= 5 }} X ::= A3 {{ 0 <= X /\ X <= 5 }}
*)
(* We could try to formalize the assignment rule directly in Coq
by treating P as a family of assertions indexed by arithmetic
expressions -- something like this:
Theorem hoare_ass_firsttry : forall (P : aexp->Assertion) V a,
{{fun st => P a st}} (V ::= a) {{fun st => P (AId V) st}}.
But this formulation is not very nice, for two reasons.
First, it is not clear how we'd prove it is valid (we'd need
to somehow reason about all possible propositions). And
second, even if we could prove it, it would be awkward to use.
A much smoother way of formalizing the rule arises from the
following obervation:
For all states st,
"P where a is substituted for X" holds in the state st
<->
P holds in the state (override st V (aeval st a)).
That is, asserting that a substituted variant of P holds in
some state is the same as asserting that P itself holds in a
substituted variant of the state.
*)
(* Substitution: *)
Definition assn_sub P V a : Assertion :=
fun (st : state) =>
P (override st V (aeval st a)).
(* The proof rule for assignment: *)
Theorem hoare_ass : forall P V a,
{{assn_sub P V a}} (V ::= a) {{P}}.
Proof.
unfold hoare_triple.
intros P V a st st' HE HP.
inversion HE. subst.
unfold assn_sub in HP. assumption. Qed.
(* Here's a first formal proof using this rule: *)
Example assn_sub_example :
{{fun st => 3 = 3}} (X ::= A3) {{fun st => st X = 3}}.
Proof.
assert ((fun st => 3 = 3) =
(assn_sub (fun st => st X = 3) X A3)).
Case "Proof of assertion".
unfold assn_sub. reflexivity.
rewrite -> H. apply hoare_ass. Qed.
(* Unfortunately, the [hoare_ass] rule doesn't literally apply to
the initial goal: it only works with triples whose
precondition has precisely the form [assn_sub P V a] for some
P, V, and a. So we start with asserting a little lemma to get
the goal into this form. *)
(* Doing this kind of fiddling with the goal state every time we
want to use [hoare_ass] would gets tiresome pretty quickly.
Fortunately, there are easier alternatives. One simple one is
to state a slightly more general theorem that introduces an
explicit equality hypothesis: *)
Theorem hoare_ass_eq : forall P P' V a,
P' = assn_sub P V a
-> {{P'}} (V ::= a) {{P}}.
Proof.
intros P P' V a H. rewrite H. apply hoare_ass. Qed.
(* With this version of [hoare_ass], we can do the proof much
more smoothly. *)
Example assn_sub_example' :
{{fun st => 3 = 3}} (X ::= A3) {{fun st => st X = 3}}.
Proof.
apply hoare_ass_eq. reflexivity. Qed.
(* Exercise: 2 stars (hoare_ass_examples) *)
(* Translate these informal Hoare triples
{{ X + 1 <= 5 }} X ::= !X +++ A1 {{ X <= 5 }}
{{ 0 <= 3 /\ 3 <= 5 }} X ::= A3 {{ 0 <= X /\ X <= 5 }}
into formal statements and use [hoare_ass_eq] to prove them. *)
(* FILL IN HERE *)
(* Exercise: 3 stars (hoarestate2) *)
(* If the assignment rule still seems "backward", it may help to
think a little about alternative "forward" rules. Here is a
seemingly natural one:
{{ True }} X ::= a {{ X = a }}
Explain what is wrong with this rule.
(* FILL IN HERE *)
*)
(* ------------------------------------------------------- *)
(** ** Rules of consequence *)
(* The above discussion about the awkwardness of applying the
assignment rule illustrates a more general point: sometimes
the preconditions and postconditions we get from the Hoare
rules won't quite be the ones we want -- they may (as in the
above example) be logically equivalent but have a different
syntactic form that fails to unify with the goal we are trying
to prove, or they actually may be logically weaker or stronger
than the goal.
For instance, while
{{3 = 3}} (X ::= A3) {{X = 3}},
is a valid Hoare triple, what we probably have in mind when we
think about the effect of this assignment is something more like this:
{{True}} (X ::= A3) {{X = 3}}.
This triple is also valid, but we can't derive it from
[hoare_ass] (or [hoare_ass_eq]) because [True] and [3 = 3] are
not equal, even after simplification.
In general, if we can derive [{{P}} c {{Q}}], it is valid to
change P to P' as long as P' is still enough to show P, and
change Q to Q' as long as Q is enough to show Q'.
This observation is captured by the following RULE OF
CONSEQUENCE.
{{P'}} c {{Q'}}
P implies P' (in every state)
Q' implies Q (in every state)
-----------------------------
{{P}} c {{Q}}
For convenience, here are two more consequence rules -- one
for situations where we want to just strengthen the
precondition, and one for when we want to just loosen the
postcondition.
{{P'}} c {{Q}}
P implies P' (in every state)
-----------------------------
{{P}} c {{Q}}
{{P}} c {{Q'}}
Q' implies Q (in every state)
-----------------------------
{{P}} c {{Q}}
*)
Theorem hoare_consequence : forall (P P' Q Q' : Assertion) c,
{{P'}} c {{Q'}} ->
(forall st, P st -> P' st) ->
(forall st, Q' st -> Q st) ->
{{P}} c {{Q}}.
Proof.
intros P P' Q Q' c Hht HPP' HQ'Q.
unfold hoare_triple. unfold hoare_triple in Hht.
intros st st' Hc HP.
apply HQ'Q. apply (Hht st st'); try assumption.
apply HPP'. assumption. Qed.
Theorem hoare_consequence_pre : forall (P P' Q : Assertion) c,
{{P'}} c {{Q}} ->
(forall st, P st -> P' st) ->
{{P}} c {{Q}}.
Proof.
intros P P' Q c Hhoare Himp.
apply hoare_consequence with (P' := P') (Q' := Q);
try assumption.
intros st H. apply H. Qed.
Theorem hoare_consequence_post : forall (P Q Q' : Assertion) c,
{{P}} c {{Q'}} ->
(forall st, Q' st -> Q st) ->
{{P}} c {{Q}}.
Proof.
intros P Q Q' c Hhoare Himp.
apply hoare_consequence with (P' := P) (Q' := Q');
try assumption.
intros st H. apply H. Qed.
(* For example, we might use (the "_pre" version of) the
consequence rule like this:
{{ True }} =>
{{ 1 = 1 }}
X ::= A1
{{ X = 1 }}
Or, formally...
*)
Example hoare_ass_example1 :
{{fun st => True}} (X ::= A1) {{fun st => st X = 1}}.
Proof.
apply hoare_consequence_pre
with (P' := assn_sub (fun st => st X = 1) X A1).
apply hoare_ass. intros st H. unfold assn_sub.
apply override_eq. Qed.
(* ------------------------------------------------------- *)
(** ** The [eapply] tactic *)
(* This is a good moment to introduce another convenient feature
of Coq. Having to write P' explicitly in the example above is
a bit annoying because the very next thing we are going to
do -- applying the [[hoare_ass] rule -- is going to determine
exactly what it should be. We can use [eapply] instead of
[apply] to tell Coq, essentially, "The missing part is going
to be filled in later." *)
Example hoare_ass_example1' :
{{fun st => True}} (X ::= A1) {{fun st => st X = 1}}.
Proof.
eapply hoare_consequence_pre.
apply hoare_ass. intros st H. unfold assn_sub.
apply override_eq. Qed.
(* In general, [eapply H] tactic works just like [apply H] except
that, instead of failing if unifying the goal with the
conclusion of [H] does not determine how to instantiate all of
the variables appearing in the premises of [H], [eapply H]
will replace these variables with EXISTENTIAL
VARIABLES (written ?nnn) as placeholders for expressions that
will be determined (by further unification) later in the
proof.
There is also an [eassumption] tactic that works similarly. *)
(* Not sure this is useful... *)
Example hoare_ass_example2 : forall a n,
{{fun st => aeval st a = n}} (X ::= a)
{{fun st => st X = n}}.
Proof.
intros a n.
eapply hoare_consequence_pre. apply hoare_ass.
intros st H. unfold assn_sub. subst. apply override_eq. Qed.
(* Informally:
{{ True }} =>
{{ a = a }}
X ::= a
{{ X = a }}
*)
(* ------------------------------------------------------- *)
(** ** Proof rule for [skip] *)
(* Now we come to some easier rules... *)
(* Since [skip] doesn't change the state, it preserves any
property P:
{{ P }} skip {{ P }}
*)
Theorem hoare_skip : forall P,
{{P}} skip {{P}}.
Proof.
unfold hoare_triple. intros P st st' H HP. inversion H. subst.
assumption. Qed.
(* ------------------------------------------------------- *)
(** ** Proof rule for [;] *)
(* More interestingly, if the command [c1] takes any state where
[P] holds to a state where [Q] holds, and if [c2] takes any
state where [Q] holds to one where [R] holds, then doing [c1]
followed by [c2] will take any state where [P] holds to one
where [R] holds:
{{ P }} c1 {{ Q }}
{{ Q }} c2 {{ R }},
---------------------
{{ P }} c1;c2 {{ R }}
*)
Theorem hoare_seq : forall P Q R c1 c2,
{{Q}} c2 {{R}}
-> {{P}} c1 {{Q}}
-> {{P}} c1;c2 {{R}}.
Proof.
unfold hoare_triple.
intros P Q R c1 c2 H1 H2 st st' H12 Pre.
inversion H12. subst.
apply (H1 st'0 st'). assumption.
apply (H2 st st'0). assumption. assumption. Qed.
(* Note that, in the formal rule [hoare_seq], the premises are
given in "backwards" order ([c2] before [c1]). This matches
the natural flow of information in many of the situations
where we'll use the rule. *)
(* Informally, a nice way of recording a proof using this rule is
as a "decorated program" where the intermediate assertion Q is
written between c1 and c2:
{{ a = n }}
X ::= a;
{{ X = n }} <---- Q
skip
{{ X = n }}
*)
Example hoare_ass_example3 : forall a n,
{{fun st => aeval st a = n}}
(X ::= a; skip)
{{fun st => st X = n}}.
Proof.
intros a n. eapply hoare_seq.
Case "right part of seq".
apply hoare_skip.
Case "left part of seq".
eapply hoare_consequence_pre. apply hoare_ass.
intros st H. unfold assn_sub. subst. apply override_eq. Qed.
(* Exercise: 2 stars (hoare_ass_example4) *)
(* Translate this decorated program into a formal proof:
{{ True }} =>
{{ 1 = 1 }}
X ::= A1;
{{ X = 1 }} =>
{{ X = 1 /\ 2 = 2 }}
Y ::= A2
{{ X = 1 /\ Y = 2 }}
*)
Example hoare_ass_example4 :
{{fun st => True}} (X ::= A1; Y ::= A2)
{{fun st => st X = 1 /\ st Y = 2}}.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* Exercise: 3 stars, optional (swap_exercise) *)
(* Write an IMP program [c] that swaps the values of X and Y and
show (in Coq) that it satisfies the following specification:
{{X <= Y}} c {{Y <= X}}
*)
(* FILL IN HERE *)
(* Exercise: 3 stars, optional (hoarestate1) *)
(* Explain why the following proposition can't be proven:
forall (a : aexp) (n : nat),
{{fun st => aeval st a = n}} (X ::= A3; Y ::= a)
{{fun st => st Y = n}}.
(* FILL IN HERE *)
*)
(* ------------------------------------------------------- *)
(** ** Proof rule for conditionals *)
(* What sort of rule do we want for reasoning about conditional
commands? Certainly, if the same assertion [Q] holds after
executing either branch, then it holds after the whole
conditional. So we might be tempted to write:
{{P}} c1 {{Q}}
{{P}} c2 {{Q}}
------------------------------------
{{P}} testif b then c1 else c2 {{Q}}
But, actually, we can say something more precise. In the
"then" branch, we know that the boolean expression [b]
evaluates to [true], and in the "else" branch, we know it
evaluates to [false]. Making this information available in
the premises of the lemma gives us more information to work
with when reasoning about the behavior of [c1] and [c2] (i.e.,
the reasons why they establish the postcondtion [Q]).
{{P /\ b}} c1 {{Q}}
{{P /\ ~b}} c2 {{Q}}
------------------------------------
{{P}} testif b then c1 else c2 {{Q}}
*)
(* To interpret this rule formally, we need to do a little work.
Strictly speaking, what we've written -- [P /\ b] -- is the
conjunction of an assertion and a boolean expression, which
doesn't typecheck. To fix this, we need a way of formally
"lifting" any bexp [b] to an assertion. We'll write [bassn b]
for the assertion "[b] evaluates to [true] in (a given
state)." *)
Definition bassn b : Assertion :=
fun st => beval st b = true.
(* A couple of facts about [bassn] will be useful in proving the
validity of the proof rule for conditionals. *)
Lemma bexp_eval_true : forall b st,
beval st b = true -> (bassn b) st.
Proof.
intros b st Hbe.
unfold bassn. assumption. Qed.
Lemma bexp_eval_false : forall b st,
beval st b = false -> ~ ((bassn b) st).
Proof.
intros b st Hbe contra.
unfold bassn in contra.
rewrite -> contra in Hbe. inversion Hbe. Qed.
(* Now we can formalize the Hoare proof rule for conditionals (and
prove it correct). *)
Theorem hoare_if : forall P Q b c1 c2,
{{fun st => P st /\ bassn b st}} c1 {{Q}} ->
{{fun st => P st /\ ~(bassn b st)}} c2 {{Q}} ->
{{P}} (CIf b c1 c2) {{Q}}.
Proof.
unfold hoare_triple.
intros P Q b c1 c2 HTrue HFalse st st' HE HP.
inversion HE; subst.
Case "b is true".
apply (HTrue st st'). assumption. split.
assumption. apply bexp_eval_true. assumption.
Case "b is false".
apply (HFalse st st'). assumption. split.
assumption.
apply bexp_eval_false. assumption. Qed.
(* ------------------------------------------------------- *)
(** ** Proof rule for loops *)
(* Finally, we need a rule for reasoning about while loops.
Suppose we have a loop
while b do c
and we want to find a pre-condition P and a post-condition Q such that
{{P}} while b do c {{Q}}
is a valid triple.
First of all, let's think about the case where b is false at
the beginning, so that the loop body never executes at all.
In this case, the loop behaves like [skip], so we might be
tempted to write
{{P}} while b do c {{P}}.
But, as we remarked above for the conditional, we know a
little more at the end -- not just P, but also the fact that b
is false in the current state. So we can enrich the
postcondition a little:
{{P}} while b do c {{P /\ ~b}}
What about the case where the loop body DOES get executed? In
order to ensure that P holds when the loop finally exits, we
certainly need to make sure that the command c guarantees that
P holds whenever c is finished. Moreover, since P holds at
the beginning of the first execution of c, and since each
execution of c re-establishes P when it finishes, we can
always assume that P holds at the beginning of c. This leads
us to the following rule:
{{P}} c {{P}}
------------------------------
{{P}} while b do c {{P /\ ~b}}
This is almost the rule we want, but again it can be improved
a little: at the beginning of the loop body, we know not only
that P holds, but also that the guard b is true in the current
state. This gives us a little more information to use in
reasoning about c. Here is the final version of the rule:
{{P /\ b}} c {{P}}
------------------------------
{{P}} while b do c {{P /\ ~b}}
The proposition P is called an INVARIANT.
*)
(* Formalizing the rule in Coq... *)
Lemma hoare_while : forall P b c,
{{fun st => P st /\ bassn b st}} c {{P}} ->
{{P}} (while b do c) {{fun st => P st /\ ~ (bassn b st)}}.
Proof.
unfold hoare_triple.
intros P b c Hhoare st st' He HP.
(* Like we've seen before, we need to reason by induction on He,
because in the loop case its hypotheses talk about the
whole loop instead of just c *)
remember (while b do c) as wcom.
(ceval_cases (induction He) Case); try (inversion Heqwcom); subst.
Case "CEWhileEnd".
split. assumption. apply bexp_eval_false in H. apply H.
Case "CEWhileLoop".
(* Putting both [assumption] and [reflexivity] here seems to make
the proof work in both Coq 8.1 and Coq 8.2 *)
destruct IHHe2 as [HP' Hbfalse']; try assumption; try reflexivity.
apply (Hhoare st st'); try assumption.
split. assumption. apply bexp_eval_true. assumption.
split; assumption. Qed.
(* ------------------------------------------------------- *)
(** ** Decorated programs *)
(* There are only a few places where we actually need to *think* when
performing a correctness proof in Hoare Logic:
- the outermost pre- and post-conditions
- the intermediate assertion for a sequential composition
[c1;c2]
- the invariant of a while loop
- the "inner" assertions [P'] and [Q'] in the consequence rules
We can completely remove the need for thinking by decorating
programs with appropriate assertions in these situations (as
we've already in several places above). Such a DECORATED
PROGRAM carries with it an (informal) proof of its own
correctness.
Concretely, a decorated program has one of the following forms:
* null program
{{ P }}
skip
{{ P }}
* sequential composition:
{{ P }}
c1;
{{ Q }}
c2
{{ R }}
(where c1 and c2 are decorated programs)
* assignment:
{{ P where a is substituted for V }}
V ::= a
{{ P }}
* conditional:
{{ P }}
testif b then
{{ P /\ b }}
c1
{{ Q }}
else
{{ P /\ ~b }}
c2
{{ Q }}
* loop:
{{ P }}
while b do (
{{ P /\ b }}
c1
{{ P }}
)
{{ P /\ ~b }}
* consequence:
{{ P }} =>
{{ P' }}
c
{{ Q }}
(where (P st) implies (P' st) for all states st)
{{ P }}
c
{{ Q' }} =>
{{ Q }}
(where (Q' st) implies (Q st) for all states st)
SIMPLE EXAMPLE:
{{ True }} =>
{{ x = x }}
X ::= ANum x;
{{ X = x }} =>
{{ X = x /\ z = z }}
Z ::= ANum z;
{{ X = x /\ Z = z }} =>
{{ Z - X = z - x }}
while BNot (!X === A0) do (
{{ Z - X = z - x /\ X <> 0 }} =>
{{ (Z - 1) - (X - 1) = z - x }}
Z ::= !Z --- A1;
{{ Z - (X - 1) = z - x }}
X ::= !X --- A1
{{ Z - X = z - x }}
);
{{ Z - X = z - x /\ ~ (X <> 0) }} =>
{{ Z = z - x }} =>
{{ Z + 1 = z - x + 1 }}
Z ::= !Z + A1
{{ Z = z - x + 1 }}
*)
(* ------------------------------------------------------- *)
(** ** Exercise: hoare rules for 'repeat' *)
Module RepeatExercise.
(* Exercise: 4 stars (hoare_repeat) *)
(* In this exercise, we've added a new construct to our language
of commands: [CRepeat]. You will write the evaluation rule for
[repeat] and add a new hoare logic theorem to the language for
programs involving it.
We recommend that you do this exercise before the ones that
follow - it should help solidify your understanding of the
material. *)
Inductive com : Set :=
| CSkip : com
| CAss : id -> aexp -> com
| CSeq : com -> com -> com
| CIf : bexp -> com -> com -> com
| CWhile : bexp -> com -> com
| CRepeat : com -> bexp -> com
.
(* [repeat] behaves like [while], but the loop guard is checked
AFTER each execution of the body, with the loop repeating as
long as the guard stays FALSE. Because of this, the body will
always execute at least once. The concrete syntax for
[CRepeat c b] often looks like:
repeat c until b
*)
Tactic Notation "com_cases" tactic(first) tactic(c) :=
first;
[ c "CSkip" | c "CAss" | c "CSeq" | c "CIf" | c "CWhile" | c "CRepeat"].
Notation "'skip'" :=
CSkip.
Notation "c1 ; c2" :=
(CSeq c1 c2) (at level 80, right associativity).
Notation "V '::=' a" :=
(CAss V a) (at level 60).
Notation "'while' b 'do' c" :=
(CWhile b c) (at level 80, right associativity).
Notation "'testif' e1 'then' e2 'else' e3" :=
(CIf e1 e2 e3) (at level 80, right associativity).
Notation "'repeat' e1 'until' b2" :=
(CRepeat e1 b2) (at level 80, right associativity).
(* Add new rules for [repeat] to ceval below. You can use the
rules for [while] as a guide, but remember that the body of a
[repeat] should always execute at least once, and that the
loop ends when the guard becomes true. Then update the
ceval_cases tactic to handle these added cases. *)
Inductive ceval : state -> com -> state -> Prop :=
| CESkip : forall st,
ceval st CSkip st
| CEAss : forall st a1 n V,
aeval st a1 = n ->
ceval st (CAss V a1) (override st V n)
| CESeq : forall c1 c2 st st' st'',
ceval st c1 st' ->
ceval st' c2 st'' ->
ceval st (CSeq c1 c2) st''
| CEIfTrue : forall st st' b1 c1 c2,
beval st b1 = true ->
ceval st c1 st' ->
ceval st (CIf b1 c1 c2) st'
| CEIfFalse : forall st st' b1 c1 c2,
beval st b1 = false ->
ceval st c2 st' ->
ceval st (CIf b1 c1 c2) st'
| CEWhileEnd : forall b1 st c1,
beval st b1 = false ->
ceval st (CWhile b1 c1) st
| CEWhileLoop : forall st st' st'' b1 c1,
beval st b1 = true ->
ceval st c1 st' ->
ceval st' (CWhile b1 c1) st'' ->
ceval st (CWhile b1 c1) st''
(* FILL IN HERE *)
.
Tactic Notation "ceval_cases" tactic(first) tactic(c) := first; [
c "CESkip" | c "CEAss" | c "CESeq" | c "CEIfTrue" | c "CEIfFalse"
| c "CEWhileEnd" | c "CEWhileLoop"
(* FILL IN HERE *)
].
(* A couple of definitions from above, copied so they use the new ceval. *)
Notation "c1 '/' st '-->' st'" := (ceval st c1 st') (at level 40).
Definition hoare_triple (P:Assertion) (c:com) (Q:Assertion) : Prop :=
forall st st', (c / st --> st') -> P st -> Q st'.
Notation "{{ P }} c {{ Q }}" := (hoare_triple P c Q) (at level 90).
(* Now state and prove a theorem, [hoare_repeat], that expresses
an appropriate proof rule for [repeat] commands. Use
[hoare_while] as a model. *)
(* FILL IN HERE *)
End RepeatExercise.
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(** * Using Hoare Logic to reason about programs *)
(* ------------------------------------------------------- *)
(** ** Some miscellaneous lemmas for the examples *)
(* Formal Hoare-logic proofs often require a bunch of small
algebraic facts, most of which we wouldn't even bother writing
down in an informal proof. This is a bit clunky in
Coq (though it can be made better using some of the automation
features we haven't discussed yet). The best way to deal with
it is to break them out as separate lemmas so that they don't
clutter the main proofs. Here we collect a bunch of
properties that we'll use in the examples below. *)
Lemma minus_0_n : forall n,
minus 0 n = 0.
Proof.
intros n. induction n as [| n'].
Case "n = 0".
reflexivity.
Case "n = S n'".
simpl. apply IHn'.
Qed.
Lemma neq0_not_true__eq_0 : forall x,
negb (beq_nat x 0) <> true -> x = 0.
Proof.
intros x H. destruct x as [| x'].
Case "x = 0".
reflexivity.
Case "x = S x'".
simpl in H. destruct H. reflexivity.
Qed.
Lemma neq0_true__eq_S : forall n,
negb (beq_nat n 0) = true
-> exists n', n = S n'.
Proof.
intros n H. destruct n as [| n'].
Case "n = 0 (contradiction)".
inversion H.
Case "n = S n'".
exists n'. reflexivity.
Qed.
Lemma S_le__S: forall n m,
S n <= m
-> exists m', n <= m /\ m = S m'.
Proof.
intros n m H. destruct m as [| m'].
Case "m = 0 (contradiction)".
inversion H.
Case "m = S m'".
exists m'. split; try reflexivity.
apply le_S. apply le_S_n. apply H. Qed.
Lemma random_minus_fact : forall n,
minus 1 n = 0 -> n <> 0.
Proof.
intros n H. destruct n as [| n'].
Case "n = 0 (contradiction)".
inversion H.
Case "n = S n'".
intros contra. inversion contra. Qed.
Lemma random_minus_fact' : forall n,
n <> 0 -> minus 1 n = 0.
Proof.
intros n H. destruct n as [| n'].
Case "n = 0 (contradiction)".
destruct H. reflexivity.
Case "n = S n'".
simpl. apply minus_0_n. Qed.
Lemma not_ev_ev_S_gen: forall n,
(~ ev n -> ev (S n)) /\
(~ ev (S n) -> ev (S (S n))).
Proof.
induction n as [| n'].
Case "n = 0".
split; intros H.
SCase "->".
destruct H. apply ev_0.
SCase "<-".
apply ev_SS. apply ev_0.
Case "n = S n'".
destruct IHn' as [Hn HSn]. split; intros H.
SCase "->".
apply HSn. apply H.
SCase "<-".
apply ev_SS. apply Hn. intros contra.
destruct H. apply ev_SS. apply contra. Qed.
Lemma not_ev_ev_S : forall n,
~ ev n -> ev (S n).
Proof.
intros n.
destruct (not_ev_ev_S_gen n) as [H _].
apply H.
Qed.
(* ------------------------------------------------------- *)
(** ** Exercise: Reduce to zero *)
(* a very simple while loop that needs no invariant *)
Definition reduce_to_zero : com :=
while BNot (!X === A0) do (
X ::= !X --- A1
).
(* A decorated version of this program, establishing a simple specification:
{{ True }}
while BNot (!X === A0) do (
{{ True /\ X <> 0 }} =>
{{ True }}
X ::= !X --- A1.
{{ True }}
);
{{ True /\ X = 0 }} =>
{{ X = 0 }}
Your job: translate this proof to Coq. (It may help to look
at the slow_subtraction proof below for ideas.)
*)
(* Exercise: 2 stars (reduce_to_zero_correct) *)
Theorem reduce_to_zero_correct :
{{fun st => True}}
reduce_to_zero
{{fun st => st X = 0}}.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* ------------------------------------------------------- *)
(** ** Example: Slow subtraction *)
Definition subtract_slowly : com :=
while BNot (!X === A0) do
(Z ::= !Z --- A1;
X ::= !X --- A1).
(* The decorated program:
{{ X = x /\ Z = z }} =>
{{ Z - X = z - x }}
while BNot (!X === A0) do (
{{ Z - X = z - x /\ X <> 0 }} =>
{{ (Z - 1) - (X - 1) = z - x }}
Z ::= !Z --- A1;
{{ Z - (X - 1) = z - x }}
X ::= !X --- A1
{{ Z - X = z - x }}
);
{{ Z - X = z - x /\ ~ (X <> 0) }} =>
{{ Z = z - x }}
*)
Definition subtract_slowly_invariant x z :=
fun st => minus (st Z) (st X) = minus z x.
Theorem subtract_slowly_correct : forall x z,
{{fun st => st X = x /\ st Z = z}}
subtract_slowly
{{fun st => st Z = minus z x}}.
Proof.
(* Note that we do NOT unfold the definition of hoare_triple
anywhere in this proof! The goal is to use only the hoare
rules. Your proofs should do the same. *)
intros x z. unfold subtract_slowly.
(* First we need to transform the pre and postconditions so
that hoare_while will apply. In particular, the
precondition should be the loop invariant. *)
eapply hoare_consequence with (P' := subtract_slowly_invariant x z).
apply hoare_while.
Case "Loop body preserves invariant".
(* Split up the two assignments with hoare_seq - using eapply
lets us solve the second one immediately with hoare_ass *)
eapply hoare_seq. apply hoare_ass.
(* Now for the first assignment, transform the precondition
so we can use hoare_ass *)
eapply hoare_consequence_pre. apply hoare_ass.
(* Finally, we need to justify the implication generated by
hoare_consequence_pre (this bit of reasoning is elided in the
informal proof) *)
unfold subtract_slowly_invariant, assn_sub, override, bassn. simpl.
intros st [Inv GuardTrue]. apply neq0_true__eq_S in GuardTrue.
destruct GuardTrue as [n' Hn'].
rewrite Hn'. simpl. rewrite Hn' in Inv. simpl in Inv.
assumption.
Case "Initial state satisfies invariant".
(* This is the subgoal generated by the precondition part of our
first use of hoare_consequence. It's the first implication
written in the decorated program (though we elided the actual
proof there). *)
unfold subtract_slowly_invariant.
intros st [HX HZ].
rewrite <- HX. rewrite HZ. reflexivity.
Case "Invariant and negated guard imply postcondition".
(* This is the subgoal generated by the postcondition part of
out first use of hoare_consequence. This implication is
the one written after the while loop in the informal proof. *)
intros st [Inv GuardFalse].
unfold subtract_slowly_invariant in Inv.
unfold bassn in GuardFalse. simpl in GuardFalse.
apply neq0_not_true__eq_0 in GuardFalse.
rewrite GuardFalse in Inv. simpl in Inv. assumption. Qed.
(* ------------------------------------------------------- *)
(** ** Exercise: Slow addition *)
(* Your turn... *)
(* The following program adds the variable X into the variable Z
by repeatedly decrementing X and incrementing Z. *)
Definition add_slowly : com :=
while BNot (!X === A0) do
(Z ::= !Z +++ A1;
X ::= !X --- A1).
(* Exercise: 3 stars (add_slowly_decoration) *)
(* Following the pattern of the [subtract_slowly] example above,
pick a precondition and postcondition that give an appropriate
specification of add_slowly, then decorate the program
accordingly. *)
(* FILL IN HERE *)
(* Exercise: 3 stars (add_slowly_formal) *)
(* Now write down your specification of add_slowly as a Coq
Hoare_triple and prove it valid. *)
(* FILL IN HERE *)
(* ------------------------------------------------------- *)
(** ** Example: Parity *)
(* Here's another, slightly trickier example. Make sure you
understand the decorated program completely. (Understanding
all the details of the Coq proof is not required, though it is
not actually very hard -- all the required ideas are already
in the informal version, and all the required miscellaneous
facts about arithmetic are recorded above.) *)
Lemma minus_pred : forall n m,
(exists m', m = S m') ->
m <= n ->
minus n (pred m) = S (minus n m).
Proof.
intros n m Hnot0.
destruct Hnot0 as [m' Heq]. rewrite Heq in *.
clear Heq m. revert n.
induction m' as [| m'']; intros n Hle.
Case "m' = 0".
simpl. destruct n. inversion Hle. reflexivity.
Case "m' = S m''".
simpl.
assert (S m'' <= pred n).
SCase "proof of assertion".
destruct n. inversion Hle. apply le_S_n in Hle.
simpl. assumption.
apply IHm'' in H. clear IHm''.
simpl in H. apply H.
Qed.
Definition find_parity : com :=
Y ::= A0;
while (BNot (!X === A0)) do
(Y ::= A1 --- !Y;
X ::= !X --- A1).
(* Proof of correctness:
{{ X = x }} =>
{{ X = x /\ 0 = 0 }}
Y ::= A0;
{{ X = x /\ Y = 0 }}
while BNot (!X === A0) do (
{{ (Y=0 <-> ev (x-X)) /\ X<=x /\ X<>0 }} =>
{{ (1-Y)=0 <-> ev (x-(X-1)) /\ X-1<=x}}
Y ::= A1 --- !Y;
{{ Y=0 <-> ev (x-(X-1)) /\ X-1<=x }}
X ::= !X --- A1
{{ Y=0 <-> ev (x-X) /\ X<=x }}
);
{{ (Y=0 <-> ev (x-X)) /\ X<=x /\ ~(X<>0) }} =>
{{ Y=0 <-> ev x }}
*)
Definition find_parity_invariant x :=
fun st =>
st X <= x
/\ ((st Y) = 0 <-> ev (minus x (st X))).
Theorem find_parity_correct : forall x,
{{fun st => st X = x}}
find_parity
{{fun st => st Y = 0 <-> ev x}}.
Proof.
intros x. unfold find_parity.
apply hoare_seq with (Q := find_parity_invariant x).
eapply hoare_consequence.
apply hoare_while with (P := find_parity_invariant x).
Case "Loop body preserves invariant".
eapply hoare_seq.
apply hoare_ass.
eapply hoare_consequence_pre.
apply hoare_ass.
unfold find_parity_invariant, bassn, assn_sub, override. simpl.
intros st [[Inv1 Inv2] GuardTrue].
apply neq0_true__eq_S in GuardTrue.
rewrite (minus_pred x (st X)); try assumption.
destruct GuardTrue as [X' HX'].
rewrite HX' in Inv1. rewrite HX'. simpl.
rewrite HX' in Inv2. simpl in Inv2. clear HX'.
split.
SCase "first part of invariant".
apply le_Sn_le. assumption.
SCase "second part".
apply S_le__S in Inv1. destruct Inv1 as [x' [Hlt Heq]].
rewrite Heq. rewrite Heq in Inv2. simpl in Inv2.
destruct Inv2 as [Inv2a Inv2b].
split; intros H.
SSCase "->".
apply not_ev_ev_S.
intros Contra. apply Inv2b in Contra.
apply random_minus_fact in H. unfold not in H.
apply H in Contra. assumption.
SSCase "<-".
apply random_minus_fact'.
intros Contra.
apply Inv2a in Contra.
apply ev_not_ev_S in H. unfold not in H.
destruct H. apply ev_SS. assumption.
Case "Precondition implies invariant".
intros st H. assumption.
Case "Invariant implies postcondition".
unfold bassn, find_parity_invariant. simpl.
intros st [[Inv1 Inv2] GuardFalse].
apply neq0_not_true__eq_0 in GuardFalse.
rewrite GuardFalse in Inv2. simpl in Inv2. assumption.
Case "invariant established before loop".
eapply hoare_consequence_pre.
apply hoare_ass.
intros st H.
unfold assn_sub, find_parity_invariant, override. simpl.
subst.
split.
apply le_n.
split; intros H.
rewrite (minus_n_n (st X)). apply ev_0.
reflexivity. Qed.
(* Exercise: 3 stars (wrong_find_parity_invariant) *)
(* My first attempt at stating an invariant for find_parity was
the following. *)
Definition find_parity_invariant' x :=
fun st =>
(st Y) = 0 <-> even (minus x (st X)).
(* Why didn't this work? (Hint: Don't waste time trying to
answer this exercise by attempting a formal proof and seeing
where it goes wrong. Just think about whether the loop body
actually preserves the property.) *)
(* (* FILL IN HERE *)
*)
(* ------------------------------------------------------- *)
(** ** Example: finding square roots *)
Definition sqrt_loop : com :=
while ((A1 +++ !Z) *** (A1 +++ !Z) <<= !X) do
Z ::= A1 +++ !Z.
Definition sqrt_com : com :=
Z ::= ANum 0;
sqrt_loop.
Definition sqrt_spec (x : nat) : Assertion :=
fun st =>
(mult (st Z) (st Z)) <= x
/\ ~ ((mult (S (st Z)) (S (st Z))) <= x).
Definition sqrt_inv (x : nat) : Assertion :=
fun st =>
st X = x
/\ (mult (st Z) (st Z)) <= x.
Theorem random_fact_1 : forall st,
mult (S (st Z)) (S (st Z)) <= st X
-> bassn (A1 +++ !Z *** A1 +++ !Z <<= !X) st.
Proof.
intros st Hle. unfold bassn. simpl.
destruct (st X) as [|x'].
Case "st X = 0".
inversion Hle.
Case "st X = S x'".
simpl in Hle. apply le_S_n in Hle.
remember (ble_nat (plus (st Z) (mult (st Z) (S (st Z)))) x')
as ble.
destruct ble. reflexivity.
apply sym_eq in Heqble. apply ble_nat_false in Heqble.
unfold not in Heqble. apply Heqble in Hle. destruct Hle.
Qed.
Theorem random_fact_2 : forall st,
bassn (A1 +++ !Z *** A1 +++ !Z <<= !X) st
-> mult (aeval st (A1 +++ !Z)) (aeval st (A1 +++ !Z)) <= st X.
Proof.
intros st Hble. unfold bassn in Hble. simpl in *.
destruct (st X) as [| x'].
Case "st X = 0".
inversion Hble.
Case "st X = S x'".
apply ble_nat_true in Hble.
apply n_le_m__Sn_le_Sm. apply Hble. Qed.
Theorem sqrt_com_correct : forall x,
{{fun st => True}} (X ::= ANum x; sqrt_com) {{sqrt_spec x}}.
Proof.
intros x.
apply hoare_seq with (Q := fun st => st X = x).
Case "sqrt_com".
unfold sqrt_com.
apply hoare_seq with (Q := fun st => st X = x /\ st Z = 0).
SCase "sqrt_loop".
unfold sqrt_loop.
eapply hoare_consequence.
apply hoare_while with (P := sqrt_inv x).
SSCase "loop preserves invariant".
eapply hoare_consequence_pre.
apply hoare_ass. intros st H.
unfold assn_sub. unfold sqrt_inv in *.
destruct H as [[HX HZ] HP]. split.
SSSCase "X is preserved".
apply override_neq; try reflexivity; try assumption.
SSSCase "Z is updated correctly".
rewrite (override_eq (aeval st (A1 +++ !Z)) Z st).
subst. apply random_fact_2. assumption.
SSCase "invariant is true initially".
intros st H. destruct H as [HX HZ].
unfold sqrt_inv. split. assumption.
rewrite HZ. apply O_le_n.
SSCase "after loop, spec is satisfied".
intros st H. unfold sqrt_spec.
destruct H as [HX HP].
unfold sqrt_inv in HX. destruct HX as [HX Harith].
split. assumption.
intros contra. apply HP. clear HP.
simpl. simpl in contra.
apply random_fact_1. subst x. assumption.
SCase "Z set to 0".
eapply hoare_consequence_pre. apply hoare_ass.
intros st HX.
unfold assn_sub. split.
apply override_neq; try assumption; try reflexivity.
apply override_eq; try reflexivity.
Case "assignment of X".
eapply hoare_consequence_pre. apply hoare_ass.
intros st H.
unfold assn_sub. apply override_eq. Qed.
(* Exercise: 3 stars (sqrt_informal) *)
(* Write a decorated program corresponding to the above correctness proof. *)
(* FILL IN HERE *)
(* ------------------------------------------------------- *)
(** ** Exercise: Factorial *)
(* Recall the factorial while program: *)
Definition fact_body : com :=
Y ::= !Y *** !Z;
Z ::= !Z --- A1.
Definition fact_loop : com :=
while BNot (!Z === A0) do
fact_body.
Definition fact_com : com :=
Z ::= !X;
Y ::= ANum 1;
fact_loop.
(* Exercise: 4 stars (fact_informal) *)
(* Decorate the fact_com program to show that it satisfies the
specification given by the pre and postconditions below. Just
as we have done above, you may omit the algebraic reasoning
about arithmetic, <=, etc., that is (formally) required by the
rule of consequence:
(* FILL IN HERE *)
{{ X = x }}
Z ::= !X;
Y ::= ANum 1;
while BNot (!Z === A0) do (
Y ::= !Y *** !Z;
Z ::= !Z --- A1
).
{{ Y = factorial X }}
*)
(* Exercise: 4 stars, optional (fact_formal) *)
(* Prove formally that fact_com satisfies this specification,
using your informal proof as a guide. You may want to state
the loop invariant separately (as we did in the examples). *)
Theorem fact_com_correct : forall x,
{{fun st => st X = x}} fact_com
{{fun st => st Y = factorial x}}.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.