(** * Hoare: Hoare Logic, Part I *)
Set Warnings "-notation-overridden,-parsing".
From PLF Require Import Maps.
From Coq Require Import Bool.Bool.
From Coq Require Import Arith.Arith.
From Coq Require Import Arith.EqNat.
From Coq Require Import Arith.PeanoNat. Import Nat.
From Coq Require Import omega.Omega.
From PLF Require Import Imp.
(** Our goal is to carry out some simple examples of _program
verification_ -- i.e., to use the precise definition of Imp to
prove formally that particular programs satisfy particular
specifications of their behavior. 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 generic "proof rule" that can be used to reason
compositionally about the correctness of programs involving this
construct.
Hoare Logic originated in the 1960s, and it continues to be the
subject of intensive research right up to the present day. It
lies at the core of a multitude of tools that are being used in
academia and industry to specify and verify real software systems.
Hoare Logic combines two beautiful ideas: a natural way of writing
down _specifications_ of programs, and a _compositional proof
technique_ for proving that programs are correct with respect to
such specifications -- where by "compositional" we mean that the
structure of proofs directly mirrors the structure of the programs
that they are about. *)
(* ################################################################# *)
(** * Assertions *)
(** An _assertion_ is a claim about the current state of memory. We will
use assertions to write program specifications. *)
Definition Assertion := state -> Prop.
(** For example,
- [fun st => st X = 3] holds if the value of [X] according to [st] is [3],
- [fun st => True] always holds, and
- [fun st => False] never holds. *)
(* QUIZ
Paraphrase the following assertions in English
(1) [fun st => st X <= st Y]
(2) [fun st => st X = 3 \/ st X <= st Y]
(3) [fun st => st Z * st Z <= st X /\
~ (((S (st Z)) * (S (st Z))) <= st X)]
*)
(** Informally, instead of writing
fun st => st X = m
we'll write just
X = m
*)
(** Given two assertions [P] and [Q], we say that [P] _implies_ [Q],
written [P ->> Q], if, whenever [P] holds in some state [st], [Q]
also holds. *)
Definition assert_implies (P Q : Assertion) : Prop :=
forall st, P st -> Q st.
Notation "P ->> Q" := (assert_implies P Q)
(at level 80) : hoare_spec_scope.
Open Scope hoare_spec_scope.
(** We'll also want the "iff" variant of implication between
assertions: *)
Notation "P <<->> Q" :=
(P ->> Q /\ Q ->> P) (at level 80) : hoare_spec_scope.
(** Our convention can be implemented uses Coq coercions and anotation
scopes (much as we did with [%imp] in [Imp]) to automatically
lift [aexp]s, numbers, and [Prop]s into [Assertion]s when they appear
in the [%assertion] scope or when Coq knows the type of an
expression is [Assertion]. *)
Definition Aexp : Type := state -> nat.
Definition assert_of_Prop (P : Prop) : Assertion := fun _ => P.
Definition Aexp_of_nat (n : nat) : Aexp := fun _ => n.
Definition Aexp_of_aexp (a : aexp) : Aexp := fun st => aeval st a.
Coercion assert_of_Prop : Sortclass >-> Assertion.
Coercion Aexp_of_nat : nat >-> Aexp.
Coercion Aexp_of_aexp : aexp >-> Aexp.
Arguments assert_of_Prop /.
Arguments Aexp_of_nat /.
Arguments Aexp_of_aexp /.
Bind Scope assertion_scope with Assertion.
Bind Scope assertion_scope with Aexp.
Delimit Scope assertion_scope with assertion.
Notation assert P := (P%assertion : Assertion).
Notation mkAexp a := (a%assertion : Aexp).
Notation "~ P" := (fun st => ~ assert P st) : assertion_scope.
Notation "P /\ Q" := (fun st => assert P st /\ assert Q st) : assertion_scope.
Notation "P \/ Q" := (fun st => assert P st \/ assert Q st) : assertion_scope.
Notation "P -> Q" := (fun st => assert P st -> assert Q st) : assertion_scope.
Notation "P <-> Q" := (fun st => assert P st <-> assert Q st) : assertion_scope.
Notation "a = b" := (fun st => mkAexp a st = mkAexp b st) : assertion_scope.
Notation "a <> b" := (fun st => mkAexp a st <> mkAexp b st) : assertion_scope.
Notation "a <= b" := (fun st => mkAexp a st <= mkAexp b st) : assertion_scope.
Notation "a < b" := (fun st => mkAexp a st < mkAexp b st) : assertion_scope.
Notation "a >= b" := (fun st => mkAexp a st >= mkAexp b st) : assertion_scope.
Notation "a > b" := (fun st => mkAexp a st > mkAexp b st) : assertion_scope.
Notation "a + b" := (fun st => mkAexp a st + mkAexp b st) : assertion_scope.
Notation "a - b" := (fun st => mkAexp a st - mkAexp b st) : assertion_scope.
Notation "a * b" := (fun st => mkAexp a st * mkAexp b st) : assertion_scope.
(** Lift functions to operate on assertion expressions. *)
Definition ap {X} (f : nat -> X) (x : Aexp) :=
fun st => f (x st).
Definition ap2 {X} (f : nat -> nat -> X) (x : Aexp) (y : Aexp) (st : state) :=
f (x st) (y st).
Module ExPrettyAssertions.
Definition ex1 : Assertion := X = 3.
Definition ex2 : Assertion := True.
Definition ex3 : Assertion := False.
Definition assn1 : Assertion := X <= Y.
Definition assn2 : Assertion := X = 3 \/ X <= Y.
Definition assn3 : Assertion :=
Z * Z <= X /\ ~ (((ap S Z) * (ap S Z)) <= X).
Definition assn4 : Assertion :=
Z = ap2 max X Y.
End ExPrettyAssertions.
(* ################################################################# *)
(** * Hoare Triples, Informally *)
(** A _Hoare triple_ is a claim about the state before and after executing
a command. A standard notation is
{P} c {Q}
meaning:
- If command [c] begins execution in a state satisfying assertion [P],
- and if [c] eventually terminates in some final state,
- then that final state will satisfy the assertion [Q].
Assertion [P] is called the _precondition_ of the triple, and [Q] is
the _postcondition_.
Because single braces are already used in other ways in Coq, we'll write
Hoare triples with double braces:
{{P}} c {{Q}}
*)
(**
For example,
- [{{X = 0}} X ::= X + 1 {{X = 1}}] is a valid Hoare triple,
stating that command [X ::= X + 1] would transform a state in which
[X = 0] to a state in which [X = 1].
- [{{X = m}} X ::= X + 1 {{X = m + 1}}], is also a valid Hoare triple.
It's even more descriptive of the exact behavior of that command than
the previous example.
*)
(* QUIZ
Paraphrase the following Hoare triples in English.
1) {{True}} c {{X = 5}}
2) {{X = m}} c {{X = m + 5)}}
3) {{X <= Y}} c {{Y <= X}}
4) {{True}} c {{False}}
5) {{X = m}}
c
{{Y = real_fact m}}
6) {{X = m}}
c
{{(Z * Z) <= m /\ ~ (((S Z) * (S Z)) <= m)}}
*)
(* QUIZ
Is the following Hoare triple _valid_ -- i.e., is the
claimed relation between [P], [c], and [Q] true?
{{True}} X ::= 5 {{X = 5}}
(1) Yes
(2) No
*)
(* QUIZ
What about this one?
{{X = 2}} X ::= X + 1 {{X = 3}}
(1) Yes
(2) No
*)
(* QUIZ
What about this one?
{{True}} X ::= 5;; Y ::= 0 {{X = 5}}
(1) Yes
(2) No
*)
(* QUIZ
What about this one?
{{X = 2 /\ X = 3}} X ::= 5 {{X = 0}}
(1) Yes
(2) No
*)
(* QUIZ
What about this one?
{{True}} SKIP {{False}}
(1) Yes
(2) No
*)
(* QUIZ
What about this one?
{{False}} SKIP {{True}}
(1) Yes
(2) No
*)
(* QUIZ
What about this one?
{{True}} WHILE true DO SKIP END {{False}}
(1) Yes
(2) No
*)
(* QUIZ
This one?
{{X = 0}}
WHILE X = 0 DO X ::= X + 1 END
{{X = 1}}
(1) Yes
(2) No
*)
(* QUIZ
This one?
{{X = 1}}
WHILE ~(X = 0) DO X ::= X + 1 END
{{X = 100}}
(1) Yes
(2) No
*)
(* ################################################################# *)
(** * Hoare Triples, Formally *)
(** We can formalize Hoare triples and their notation in Coq as follows: *)
Definition hoare_triple
(P : Assertion) (c : com) (Q : Assertion) : Prop :=
forall st st',
st =[ c ]=> st' ->
P st ->
Q st'.
Notation "{{ P }} c {{ Q }}" :=
(hoare_triple P c Q) (at level 90, c at next level)
: hoare_spec_scope.
(** **** Exercise: 1 star, standard (hoare_post_true) *)
(** Prove that if postcondition [Q] holds in every state, then any triple with
it is valid. *)
Theorem hoare_post_true : forall (P Q : Assertion) c,
(forall st, Q st) ->
{{P}} c {{Q}}.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 1 star, standard (hoare_pre_false) *)
(** Prove that if precondition [P] holds in no state, then any triple with
it is valid. *)
Theorem hoare_pre_false : forall (P Q : Assertion) c,
(forall st, ~ (P st)) ->
{{P}} c {{Q}}.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(* ################################################################# *)
(** * Proof Rules *)
(** Plan:
- introduce one "proof rule" for each Imp syntactic form
- plus a couple of "structural rules" that help glue proofs
together
- prove programs correct using these proof rules, without ever
unfolding the definition of [hoare_triple] *)
(* ================================================================= *)
(** ** Assignment *)
(** How can we complete this triple?
{{ ??? }} X ::= Y {{ X = 1 }}
One possibility is:
{{ Y = 1 }} X ::= Y {{ X = 1 }}
The precondition is just the postcondition, but with [X] replaced
by [Y]. *)
(** Another example:
{{ ??? }} X ::= X + Y {{ X = 1 }}
Replace [X] with [X + Y]:
{{ X + Y = 1 }} X ::= X + Y {{ X = 1 }}
This works because "equals 1" holding of [X] is guaranteed
by "equals 1" holding of whatever is being assigned to [X]. *)
(** In general, the postcondition could be some arbitrary assertion
[Q], and the right-hand side of the assignment could be some
arithmetic expression [a]:
{{ ??? }} X ::= a {{ Q }}
The precondition would then be [Q], but with any occurrences of
[X] in it replaced by [a]. Let's introduce a notation for that
idea of replacing occurrences: let [Q [X |-> a]] mean "[Q] where
[a] is substituted for [X]".
That yields the Hoare logic rule for assignment:
{{ Q [X |-> a] }} X ::= a {{ Q }}
One way of reading that rule is: if you want statement [X ::= a]
to terminate in a state that satisfies assertion [Q], then it
suffices to start in a state that also satisfies [Q], except
where [a] is substituted for every occurrence of [X].
To many people, this rule seems "backwards" at first, because
it proceeds from the postcondition to the precondition. Actually
it makes good sense to go in this direction: the postcondition is
often what is more important, because it characterizes what we
can assume afer running the code.
Nonetheless, it's possible to formulate a "forward" assignment
rule. We'll do that later in some exercises. *)
(** Here are some valid instances of the assignment rule:
{{ (X <= 5) [X |-> X + 1] }} (that is, X + 1 <= 5)
X ::= X + 1
{{ X <= 5 }}
{{ (X = 3) [X |-> 3] }} (that is, 3 = 3)
X ::= 3
{{ X = 3 }}
{{ (0 <= X /\ X <= 5) [X |-> 3] (that is, 0 <= 3 /\ 3 <= 5)
X ::= 3
{{ 0 <= X /\ X <= 5 }}
*)
(** To formalize the rule, we must first formalize the idea of
"substituting an expression for an Imp variable in an assertion",
which we refer to as assertion substitution, or [assn_sub]. That
is, given a proposition [P], a variable [X], and an arithmetic
expression [a], we want to derive another proposition [P'] that is
just the same as [P] except that [P'] should mention [a] wherever
[P] mentions [X]. *)
(** Since [P] is an arbitrary Coq assertion, we can't directly "edit"
its text. However, we can achieve the same effect by evaluating
[P] in an updated state: *)
Definition assn_sub X a (P:Assertion) : Assertion :=
fun (st : state) =>
P (X !-> aeval st a ; st).
Notation "P [ X |-> a ]" := (assn_sub X a P)
(at level 10, X at next level).
(** That is, [P [X |-> a]] stands for an assertion -- let's call it [P'] --
that is just like [P] except that, wherever [P] looks up the
variable [X] in the current state, [P'] instead uses the value
of the expression [a]. *)
(** To see how this works, let's calculate what happens with a couple
of examples. First, suppose [P'] is [(X <= 5) [X |-> 3]] -- that
is, more formally, [P'] is the Coq expression
fun st =>
(fun st' => st' X <= 5)
(X !-> aeval st 3 ; st),
which simplifies to
fun st =>
(fun st' => st' X <= 5)
(X !-> 3 ; st)
and further simplifies to
fun st =>
((X !-> 3 ; st) X) <= 5
and finally to
fun st =>
3 <= 5.
That is, [P'] is the assertion that [3] is less than or equal to
[5] (as expected). *)
(** For a more interesting example, suppose [P'] is [(X <= 5) [X |->
X + 1]]. Formally, [P'] is the Coq expression
fun st =>
(fun st' => st' X <= 5)
(X !-> aeval st (X + 1) ; st),
which simplifies to
fun st =>
(X !-> aeval st (X + 1) ; st) X <= 5
and further simplifies to
fun st =>
(aeval st (X + 1)) <= 5.
That is, [P'] is the assertion that [X + 1] is at most [5].
*)
(** Now, using the concept of substitution, we can give the precise
proof rule for assignment:
------------------------------ (hoare_asgn)
{{Q [X |-> a]}} X ::= a {{Q}}
*)
(** We can prove formally that this rule is indeed valid. *)
Theorem hoare_asgn : forall Q X a,
{{Q [X |-> a]}} X ::= a {{Q}}.
Proof.
unfold hoare_triple.
intros Q X a st st' HE HQ.
inversion HE. subst.
unfold assn_sub in HQ. assumption. Qed.
(** Here's a first formal proof using this rule. *)
Example assn_sub_example :
{{(X < 5) [X |-> X + 1]}}
X ::= X + 1
{{X < 5}}.
Proof.
(* WORK IN CLASS *) Admitted.
(** Of course, what would be even more helpful is to prove this
simpler triple:
{{X < 4}} X ::= X + 1 {{X < 5}}
We will see how to do so in the next section. *)
(* QUIZ
Here is the assignment rule again:
{{ Q [X |-> a] }} X ::= a {{ Q }}
Is the following triple a valid instance of this rule?
{{ X = 5 }} X ::= X + 1 {{ X = 6 }}
(1) Yes
(2) No
*)
(* QUIZ
Here is the assignment rule again:
{{ Q [X |-> a] }} X ::= a {{ Q }}
Is the following triple a valid instance of this rule?
{{ Y < Z }} X ::= Y {{ X < Z }}
(1) Yes
(2) No
*)
(* QUIZ
The assignment rule again:
{{ Q [X |-> a] }} X ::= a {{ Q }}
Is the following triple a valid instance of this rule?
{{ X+1 < Y }} X ::= X + 1 {{ X < Y }}
(1) Yes
(2) No
*)
(* QUIZ
The assignment rule again:
{{ Q [X |-> a] }} X ::= a {{ Q }}
Is the following triple a valid instance of this rule?
{{ X < Y }} X ::= X + 1 {{ X+1 < Y }}
(1) Yes
(2) No
*)
(* QUIZ
The assignment rule again:
{{ Q [X |-> a] }} X ::= a {{ Q }}
Is the following triple a valid instance of this rule?
{{ X < Y }} X ::= X + 1 {{ X < Y+1 }}
(1) Yes
(2) No
*)
(* QUIZ
The assignment rule again:
{{ Q [X |-> a] }} X ::= a {{ Q }}
Is the following triple a valid instance of this rule?
{{ True }} X ::= 3 {{ X = 3 }}
(1) Yes
(2) No
*)
(* ================================================================= *)
(** ** Consequence *)
(** Sometimes the preconditions and postconditions we get from the
Hoare rules won't quite be the ones we want in the particular
situation at hand -- they may 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 (for
preconditions) or stronger (for postconditions) than what we need.
For instance, while
{{(X = 3) [X |-> 3]}} X ::= 3 {{X = 3}},
follows directly from the assignment rule,
{{True}} X ::= 3 {{X = 3}}
does not. This triple is valid, but it is not an instance of
[hoare_asgn] because [True] and [(X = 3) [X |-> 3]] are not
syntactically equal assertions. However, they are logically
_equivalent_, so if one triple is valid, then the other must
certainly be as well. We can capture this observation with the
following rule:
{{P'}} c {{Q}}
P <<->> P'
----------------------------- (hoare_consequence_pre_equiv)
{{P}} c {{Q}}
*)
(** Taking this line of thought a bit further, we can see that
strengthening the precondition or weakening the postcondition of a
valid triple always produces another valid triple. This
observation is captured by two _Rules of Consequence_.
{{P'}} c {{Q}}
P ->> P'
----------------------------- (hoare_consequence_pre)
{{P}} c {{Q}}
{{P}} c {{Q'}}
Q' ->> Q
----------------------------- (hoare_consequence_post)
{{P}} c {{Q}}
*)
(** Here are the formal versions: *)
Theorem hoare_consequence_pre : forall (P P' Q : Assertion) c,
{{P'}} c {{Q}} ->
P ->> P' ->
{{P}} c {{Q}}.
Proof.
unfold hoare_triple, "->>".
intros P P' Q c Hhoare Himp st st' Heval Hpre.
apply Hhoare with (st := st).
- assumption.
- apply Himp. assumption.
Qed.
Theorem hoare_consequence_post : forall (P Q Q' : Assertion) c,
{{P}} c {{Q'}} ->
Q' ->> Q ->
{{P}} c {{Q}}.
Proof.
unfold hoare_triple, "->>".
intros P Q Q' c Hhoare Himp st st' Heval Hpre.
apply Himp.
apply Hhoare with (st := st).
- assumption.
- assumption.
Qed.
(** For example, we can use the first consequence rule like this:
{{ True }} ->>
{{ (X = 1) [X |-> 1] }}
X ::= 1
{{ X = 1 }}
Or, formally... *)
Example hoare_asgn_example1 :
{{True}} X ::= 1 {{X = 1}}.
Proof.
(* WORK IN CLASS *) Admitted.
(** We can also use it to prove the example mentioned earlier.
{{ X < 4 }} ->>
{{ (X < 5)[X |-> X + 1] }}
X ::= X + 1
{{ X < 5 }}
Or, formally ... *)
Example assn_sub_example2 :
{{X < 4}}
X ::= X + 1
{{X < 5}}.
Proof.
(* WORK IN CLASS *) Admitted.
(** Finally, here is a combined rule of consequence that allows us to
vary both the precondition and the postcondition.
{{P'}} c {{Q'}}
P ->> P'
Q' ->> Q
----------------------------- (hoare_consequence)
{{P}} c {{Q}}
*)
Theorem hoare_consequence : forall (P P' Q Q' : Assertion) c,
{{P'}} c {{Q'}} ->
P ->> P' ->
Q' ->> Q ->
{{P}} c {{Q}}.
Proof.
intros P P' Q Q' c Htriple Hpre Hpost.
apply hoare_consequence_pre with (P' := P').
- apply hoare_consequence_post with (Q' := Q').
+ assumption.
+ assumption.
- assumption.
Qed.
(* ================================================================= *)
(** ** Automation *)
(** Many of the proofs we have done so far with Hoare triples can be
streamlined using the automation techniques that we introduced in
the [Auto] chapter of _Logical Foundations_.
Recall that the [auto] tactic can be told to [unfold] definitions
as part of its proof search. Let's give that it hint for the
definitions and coercions we're using: *)
Hint Unfold assert_implies hoare_triple assn_sub t_update.
Hint Unfold assert_of_Prop Aexp_of_nat Aexp_of_aexp.
(** Also recall that [auto] will search for a proof involving [intros]
and [apply]. By default, the theorems that it will apply include
any of the local hypotheses, as well as theorems in a core
database. *)
(** A good candidate for automation: *)
Theorem hoare_consequence_pre' : forall (P P' Q : Assertion) c,
{{P'}} c {{Q}} ->
P ->> P' ->
{{P}} c {{Q}}.
Proof.
unfold hoare_triple, "->>".
intros P P' Q c Hhoare Himp st st' Heval Hpre.
apply Hhoare with (st := st).
- assumption.
- apply Himp. assumption.
Qed.
(** Tactic [eapply] will find [st] for us. *)
Theorem hoare_consequence_pre''' : forall (P P' Q : Assertion) c,
{{P'}} c {{Q}} ->
P ->> P' ->
{{P}} c {{Q}}.
Proof.
unfold hoare_triple, "->>".
intros P P' Q c Hhoare Himp st st' Heval Hpre.
eapply Hhoare.
- eassumption.
- apply Himp. assumption.
Qed.
(** Tactic [eauto] will use [eapply] as part of its proof search.
So, the entire proof can be done in just one line. *)
Theorem hoare_consequence_pre'''' : forall (P P' Q : Assertion) c,
{{P'}} c {{Q}} ->
P ->> P' ->
{{P}} c {{Q}}.
Proof.
eauto.
Qed.
(** As can the same proof for the postcondition consequence
rule. *)
Theorem hoare_consequence_post' : forall (P Q Q' : Assertion) c,
{{P}} c {{Q'}} ->
Q' ->> Q ->
{{P}} c {{Q}}.
Proof.
eauto.
Qed.
(** We can also use [eapply] to streamline a proof,
[hoare_asgn_example1], that we did earlier as an example of using
the consequence rule: *)
Example hoare_asgn_example1' :
{{True}} X ::= 1 {{X = 1}}.
Proof.
eapply hoare_consequence_pre. (* no need to state an assertion *)
- apply hoare_asgn.
- unfold "->>", assn_sub, t_update.
intros st _. simpl. reflexivity.
Qed.
(** The final bullet of that proof also looks like a candidate for
automation. *)
Example hoare_asgn_example1'' :
{{True}} X ::= 1 {{X = 1}}.
Proof.
eapply hoare_consequence_pre.
- apply hoare_asgn.
- auto.
Qed.
(** Now we have quite a nice proof script: it identifies the Hoare
rules that need to be used, and leaves the remaining low-level
details up to Coq to figure out. *)
(** The other example of using consequence that we did earlier,
[hoare_asgn_example2], requires a little more work to automate.
We can streamline the first line with [eapply], but we can't just use
[auto] for the final bullet, since it needs [omega]. *)
Example assn_sub_example2' :
{{X < 4}}
X ::= X + 1
{{X < 5}}.
Proof.
eapply hoare_consequence_pre.
- apply hoare_asgn.
- auto. (* no progress *)
unfold "->>", assn_sub, t_update.
intros st H. simpl in *. omega.
Qed.
(** Let's introduce our own tactic to handle both that bullet, as well as
the bullet from example 1: *)
Ltac assn_auto :=
try auto; (* as in example 1, above *)
try (unfold "->>", assn_sub, t_update;
intros; simpl in *; omega). (* as in example 2 *)
Example assn_sub_example2'' :
{{X < 4}}
X ::= X + 1
{{X < 5}}.
Proof.
eapply hoare_consequence_pre.
- apply hoare_asgn.
- assn_auto.
Qed.
Example hoare_asgn_example1''':
{{True}} X ::= 1 {{X = 1}}.
Proof.
eapply hoare_consequence_pre.
- apply hoare_asgn.
- assn_auto.
Qed.
(** Again, we have quite a nice proof script. All the low-level details
of proof about assertions have been taken care of automatically. Of course,
[assn_auto] isn't able to prove everything about assertions! But it's
good enough so far. *)
(* ================================================================= *)
(** ** Skip *)
(** Since [SKIP] doesn't change the state, it preserves any
assertion [P]:
-------------------- (hoare_skip)
{{ P }} SKIP {{ P }}
*)
Theorem hoare_skip : forall P,
{{P}} SKIP {{P}}.
Proof.
intros P st st' H HP. inversion H; subst. assumption.
Qed.
(* ================================================================= *)
(** ** Sequencing *)
(** If 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 }}
---------------------- (hoare_seq)
{{ 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.
eauto.
Qed.
(** Here's an example of a program involving sequencing. Note the use
of [hoare_seq] in conjunction with [hoare_consequence_pre] and the
[eapply] tactic. *)
Example hoare_asgn_example3 : forall (a:aexp) (n:nat),
{{a = n}}
X ::= a;; SKIP
{{X = n}}.
Proof.
intros a n. eapply hoare_seq.
- (* right part of seq *)
apply hoare_skip.
- (* left part of seq *)
eapply hoare_consequence_pre.
+ apply hoare_asgn.
+ assn_auto.
Qed.
(** Informally, a nice way of displaying a proof using the sequencing
rule is as a "decorated program" where the intermediate assertion
[Q] is written between [c1] and [c2]:
{{ a = n }}
X ::= a;;
{{ X = n }} <--- decoration for Q
SKIP
{{ X = n }}
*)
(* ================================================================= *)
(** ** Conditionals *)
(** What sort of rule do we want for reasoning about conditional
commands?
Certainly, if the same assertion [Q] holds after executing
either of the branches, then it holds after the whole conditional.
So we might be tempted to write:
{{P}} c1 {{Q}}
{{P}} c2 {{Q}}
---------------------------------
{{P}} TEST b THEN c1 ELSE c2 {{Q}}
*)
(** However, this is rather weak. For example, using this rule,
we cannot show
{{ True }}
TEST X = 0
THEN Y ::= 2
ELSE Y ::= X + 1
FI
{{ X <= Y }}
since the rule tells us nothing about the state in which the
assignments take place in the "then" and "else" branches. *)
(** Better:
{{P /\ b}} c1 {{Q}}
{{P /\ ~ b}} c2 {{Q}}
------------------------------------ (hoare_if)
{{P}} TEST b THEN c1 ELSE c2 FI {{Q}}
*)
(** To make this formal, we need a way of formally "lifting"
any bexp [b] to an assertion.
We'll write [bassn b] for the assertion "the boolean expression
[b] evaluates to [true]." *)
Definition bassn b : Assertion :=
fun st => (beval st b = true).
Coercion bassn : bexp >-> Assertion.
Arguments bassn /.
Hint Unfold bassn.
(** A couple of useful facts about [bassn]: *)
Lemma bexp_eval_true : forall b st,
beval st b = true -> (bassn b) st.
Proof. auto. Qed.
Lemma bexp_eval_false : forall b st,
beval st b = false -> ~ ((bassn b) st).
Proof. congruence. Qed.
Hint Resolve bexp_eval_false.
(** Now we can formalize the Hoare proof rule for conditionals
and prove it correct. *)
Theorem hoare_if : forall P Q (b:bexp) c1 c2,
{{ P /\ b }} c1 {{Q}} ->
{{ P /\ ~ b}} c2 {{Q}} ->
{{P}} TEST b THEN c1 ELSE c2 FI {{Q}}.
Proof.
intros P Q b c1 c2 HTrue HFalse st st' HE HP.
inversion HE; subst; eauto.
Qed.
(* ----------------------------------------------------------------- *)
(** *** Example *)
Example if_example :
{{True}}
TEST X = 0
THEN Y ::= 2
ELSE Y ::= X + 1
FI
{{X <= Y}}.
Proof.
apply hoare_if.
- (* Then *)
eapply hoare_consequence_pre.
+ apply hoare_asgn.
+ assn_auto. (* no progress *)
unfold "->>", assn_sub, t_update, bassn.
simpl. intros st [_ H].
apply eqb_eq in H.
rewrite H. omega.
- (* Else *)
eapply hoare_consequence_pre.
+ apply hoare_asgn.
+ assn_auto.
Qed.
(** As we did earlier, it would be nice to eliminate all the low-level
proof script that isn't about the Hoare rules. Unfortunately, the
[assn_auto] tactic we wrote wasn't quite up to the job. Looking
at the proof of [if_example], we can see why. We had to unfold a
definition ([bassn]) and use a theorem ([eqb_eq]) that we didn't
need in earlier proofs. So, let's add those into our tactic,
and clean it up a little in the process. *)
Ltac assn_auto' :=
unfold "->>", assn_sub, t_update, bassn;
intros; simpl in *;
try rewrite -> eqb_eq in *; (* for equalities *)
auto; try omega.
(** Now the proof is quite streamlined. *)
Example if_example'' :
{{True}}
TEST X = 0
THEN Y ::= 2
ELSE Y ::= X + 1
FI
{{X <= Y}}.
Proof.
apply hoare_if.
- eapply hoare_consequence_pre.
+ apply hoare_asgn.
+ assn_auto'.
- eapply hoare_consequence_pre.
+ apply hoare_asgn.
+ assn_auto'.
Qed.
(** We can even shorten it a little bit more. *)
Example if_example''' :
{{True}}
TEST X = 0
THEN Y ::= 2
ELSE Y ::= X + 1
FI
{{X <= Y}}.
Proof.
apply hoare_if; eapply hoare_consequence_pre;
try apply hoare_asgn; try assn_auto'.
Qed.
(** For later proofs, it will help to extend [assn_auto'] to handle
inequalities, too. *)
Ltac assn_auto'' :=
unfold "->>", assn_sub, t_update, bassn;
intros; simpl in *;
try rewrite -> eqb_eq in *;
try rewrite -> leb_le in *; (* for inequalities *)
auto; try omega.
(** [] *)
(* ================================================================= *)
(** ** While Loops *)
(** Assertion [P] is an _invariant_ of [c] if
{{P}} c {{P}}
holds. *)
(** The Hoare while rule combines the idea of an invariant with
information about when guard [b] does or does not hold.
{{P /\ b}} c {{P}}
----------------------------- (hoare_while)
{{P} WHILE b DO c {{P /\ ~b}}
*)
Theorem hoare_while : forall P (b:bexp) c,
{{P /\ b}} c {{P}} ->
{{P}} WHILE b DO c END {{P /\ ~ b}}.
Proof.
intros P b c Hhoare st st' Heval HP.
(* We proceed by induction on [Heval], because, in the "keep looping" case,
its hypotheses talk about the whole loop instead of just [c]. The
[remember] is used to keep the original command in the hypotheses;
otherwise, it would be lost in the [induction]. By using [inversion]
we clear away all the cases except those involing [while]. *)
remember (WHILE b DO c END)%imp as original_command eqn:Horig.
induction Heval;
try (inversion Horig; subst; clear Horig);
eauto.
Qed.
(** We say that [P] is a _loop invariant_ of [WHILE b DO c] if [P]
suffices to prove [hoare_while] for that loop. Being a loop
invariant is different than being an invariant of the body,
because it means being able to prove correctness of the loop. For
example, [X = 0] is a loop invariant of
WHILE X = 2 DO X ::= 1 END
even though [X = 0] is not an invariant of [X ::= 1]. *)
(* QUIZ
Is the assertion
Y = 0
a loop invariant of the following?
WHILE X < 100 DO X ::= X + 1 END
(1) Yes
(2) No
*)
(* QUIZ
Is the assertion
X = 0
a loop invariant of the following?
WHILE X < 100 DO X ::= X + 1 END
(1) Yes
(2) No
*)
(* QUIZ
Is the assertion
X < Y
a loop invariant of the following?
WHILE true DO X ::= X + 1;; Y ::= Y + 1 END
(1) Yes
(2) No
*)
(* QUIZ
Is the assertion
X = Y + Z
a loop invariant of the following?
WHILE Y > 10 DO Y := Y - 1;; Z ::= Z + 1 END
(1) Yes
(2) No
*)
Example while_example :
{{X <= 3}}
WHILE X <= 2 DO
X ::= X + 1
END
{{X = 3}}.
Proof.
eapply hoare_consequence_post.
- apply hoare_while.
eapply hoare_consequence_pre.
+ apply hoare_asgn.
+ assn_auto''.
- assn_auto''.
Qed.
(* QUIZ
Is the assertion
X > 0
a loop invariant of the following?
WHILE X = 0 DO X ::= X - 1 END
(1) Yes
(2) No
*)
(* QUIZ
Is the assertion
X < 100
a loop invariant of the following?
WHILE X < 100 DO X ::= X + 1 END
(1) Yes
(2) No
*)
(* QUIZ
Is the assertion
X > 10
a loop invariant of the following?
WHILE X > 10 DO X ::= X + 1 END
(1) Yes
(2) No
*)
(** If the loop never terminates, any postcondition will work. *)
Theorem always_loop_hoare : forall Q,
{{True}} WHILE true DO SKIP END {{Q}}.
Proof.
intros Q.
eapply hoare_consequence_post.
- apply hoare_while. apply hoare_post_true. auto.
- simpl. intros st [Hinv Hguard]. congruence.
Qed.