# HoareHoare Logic, Part I

Require Export Imp.

What we've done so far:
• Formalized Imp
• identifiers and states
• abstract syntax trees
• evaluation functions (for aexps and bexps)
• evaluation relation (for commands)
• Proved some metatheoretic properties
• determinism of evaluation
• equivalence of some different ways of writing down the definitions (e.g. functional and relational definitions of arithmetic expression evaluation)
• guaranteed termination of certain classes of programs
• meaning-preservation of some program transformations
• behavioral equivalence of programs (Equiv)
This chapter:
• A systematic method for reasoning about the correctness of particular programs

# Hoare Logic

Goals:
• a natural notation for program specifications
• a compositional proof technique for program correctness
Plan:
• assertions (Hoare Triples)
• proof rules
• decorated programs
• loop invariants
• examples

## Assertions

Definition Assertion := state Prop.

Paraphrase the following assertions in English
(1) fun st st X = 3
(2) fun st st X st Y
(3) fun st st X = 3 st X st Y
(4) fun st st Z × st Z st X ¬ (((S (st Z)) × (S (st Z))) st X)
(5) fun st True
(6) fun st False

fun st ⇒ (st Z) × (st Z) ≤ m
¬ ((S (st Z)) × (S (st Z)) ≤ m)
we'll write just
Z × Z ≤ m  ~((S Z) × (S Z) ≤ m).
Given two assertions P and Q, we say that P implies Q, written P Q (in ASCII, P ->> Q), if, whenever P holds in some state st, Q also holds.

Definition assert_implies (P Q : Assertion) : Prop :=
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 have occasion to use the "iff" variant of implication between assertions:

Notation "P Q" :=
(P Q Q P) (at level 80) : hoare_spec_scope.

## Hoare Triples

Since the behavior of a command is to transform one state to another, it is natural to express claims about commands in terms of assertions that are true before and after the command executes:
• "If command c is started in a state satisfying assertion P, and if c eventually terminates in some final state, then this final state will satisfy the assertion Q."
Such a claim is called a Hoare Triple. The property P is called the precondition of c, while Q is the postcondition. Formally:

Definition hoare_triple
(P:Assertion) (c:com) (Q:Assertion) : Prop :=
st st',
c / st st'
P st
Q st'.

Since we'll be working a lot with Hoare triples, it's useful to have a compact notation:
{{P}c {{Q}}.

Notation "{{ P }} c {{ Q }}" :=
(hoare_triple P c Q) (at level 90, c at next level)
: hoare_spec_scope.

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) {{True}
c
{{(Z × Z) ≤ m  ¬ (((S Z) × (S Z)) ≤ m)}}

Is the following Hoare triple valid — i.e., the claimed relation between P, c, and Q is true?
{{True}X ::= 5 {{X = 5}}
(1) Yes
(2) No

{{X = 2}X ::= X + 1 {{X = 3}}
(1) Yes
(2) No

{{True}X ::= 5; Y ::= 0 {{X = 5}}
(1) Yes
(2) No

{{X = 2  X = 3}X ::= 5 {{X = 0}}
(1) Yes
(2) No

{{True}SKIP {{False}}
(1) Yes
(2) No

{{False}SKIP {{True}}
(1) Yes
(2) No

{{True}WHILE True DO SKIP END {{False}}
(1) Yes
(2) No

{{X = 0}}
WHILE X == 0 DO X ::= X + 1 END
{{X = 1}}
(1) Yes
(2) No

{{X = 1}}
WHILE X ≠ 0 DO X ::= X + 1 END
{{X = 100}}
(1) Yes
(2) No

Theorem hoare_post_true : (P Q : Assertion) c,
(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 : (P Q : Assertion) c,
(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.
inversion HP. Qed.

## 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

The rule for assignment is the most fundamental of the Hoare logic proof rules. 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.
This can be made even more general. To conclude that an arbitrary property Q holds after X ::= a, we need to assume that Q holds before X ::= a, but with all occurrences of X replaced by a in Q. This leads to the Hoare rule for assignment
{Q [X  a}X ::= a {Q }}
where "Q [X a]" is pronounced "Q where a is substituted for X".
For example, these are valid applications of the assignment rule:
{{ (X ≤ 5) [X  X + 1]
i.e., X + 1 ≤ 5 }}
X ::= X + 1
{X ≤ 5 }}

{{ (X = 3) [X  3]
i.e., 3 = 3}}
X ::= 3
{X = 3 }}

{{ (0 ≤ X  X ≤ 5) [X  3]
i.e., (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." 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, wherever P mentions X, P' should instead mention a.
Since P is an arbitrary Coq proposition, we can't directly "edit" its text. Instead, we can achieve the effect we want by evaluating P in an updated state:

Definition assn_sub X a P : Assertion :=
fun (st : state) ⇒
P (update st X (aeval st a)).

Notation "P [ X |-> a ]" := (assn_sub X a P) (at level 10).

That is, P [X a] is an assertion 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)
(update st X (aeval st (ANum 3))),
which simplifies to
fun st ⇒
(fun st' ⇒ st' X ≤ 5)
(update st X 3)
and further simplifies to
fun st ⇒
((update st X 3) X) ≤ 5)
and by further simplification 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)
(update st X (aeval st (APlus (AId X) (ANum 1)))),
which simplifies to
fun st ⇒
(((update st X (aeval st (APlus (AId X) (ANum 1))))) X) ≤ 5
and further simplifies to
fun st ⇒
(aeval st (APlus (AId X) (ANum 1))) ≤ 5.
That is, P' is the assertion that X+1 is at most 5.
Now 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 : 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 :
{{(fun stst X = 3) [X ANum 3]}}
(X ::= (ANum 3))
{{fun stst X = 3}}.
Proof.
apply hoare_asgn. Qed.

### 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 might 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 : (P P' Q : Assertion) c,
{{P'}} c {{Q}}
P P'
{{P}} c {{Q}}.
Proof.
intros P P' Q c Hhoare Himp.
intros st st' Hc HP. apply (Hhoare st st').
assumption. apply Himp. assumption. Qed.

Theorem hoare_consequence_post : (P Q Q' : Assertion) c,
{{P}} c {{Q'}}
Q' Q
{{P}} c {{Q}}.
Proof.
intros P Q Q' c Hhoare Himp.
intros st st' Hc HP.
apply Himp.
apply (Hhoare st st').
assumption. assumption. Qed.

For example, we might use the first consequence rule like this:
{True }
{{ 1 = 1 }
X ::= 1
{X = 1 }}
Or, formally...

Example hoare_asgn_example1 :
{{fun stTrue}} (X ::= (ANum 1)) {{fun stst X = 1}}.
Proof.
apply hoare_consequence_pre
with (P' := (fun stst X = 1) [X ANum 1]).
apply hoare_asgn.
intros st H. unfold assn_sub, update. simpl. reflexivity.
Qed.

Finally, for convenience in some proofs, we can state 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 : (P P' Q Q' : Assertion) c,
{{P'}} c {{Q'}}
P P'
Q' Q
{{P}} c {{Q}}.
Proof.
intros P P' Q Q' c Hht HPP' HQ'Q.
apply hoare_consequence_pre with (P' := P').
apply hoare_consequence_post with (Q' := Q').
assumption. assumption. assumption. Qed.

### Digression: The eapply Tactic

This is a good moment to introduce another convenient feature of Coq. We had to write "with (P' := ...)" explicitly in the proof of hoare_asgn_example1 and hoare_consequence above, to make sure that all of the metavariables in the premises to the hoare_consequence_pre rule would be set to specific values. (Since P' doesn't appear in the conclusion of hoare_consequence_pre, the process of unifying the conclusion with the current goal doesn't constrain P' to a specific assertion.)
This is a little annoying, both because the assertion is a bit long and also because for hoare_asgn_example1 the very next thing we are going to do — applying the hoare_asgn rule — will tell us exactly what it should be! We can use eapply instead of apply to tell Coq, essentially, "Be patient: The missing part is going to be filled in soon."

Example hoare_asgn_example1' :
{{fun stTrue}}
(X ::= (ANum 1))
{{fun stst X = 1}}.
Proof.
eapply hoare_consequence_pre.
apply hoare_asgn.
intros st H. reflexivity. 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 so-called existential variables (written ?nnn) as placeholders for expressions that will be determined (by further unification) later in the proof.

### Skip

Since SKIP doesn't change the state, it preserves any property P:
 (hoare_skip) {{ P }} SKIP {{ P }}

Theorem hoare_skip : P,
{{P}} SKIP {{P}}.
Proof.
intros P st st' H HP. inversion H. subst.
assumption. Qed.

### Sequencing

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 }} (hoare_seq) {{ P }} c1;;c2 {{ R }}

Theorem hoare_seq : P Q R c1 c2,
{{Q}} c2 {{R}}
{{P}} c1 {{Q}}
{{P}} c1;;c2 {{R}}.
Proof.
intros P Q R c1 c2 H1 H2 st st' H12 Pre.
inversion H12; subst.
apply (H1 st'0 st'); try assumption.
apply (H2 st st'0); assumption. Qed.

Informally, a nice way of recording 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 }}

Example hoare_asgn_example3 : a n,
{{fun staeval st a = n}}
(X ::= a;; SKIP)
{{fun stst 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_asgn.
intros st H. subst. reflexivity. Qed.

### 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}} IFB b THEN c1 ELSE c2 {{Q}}
However, this is rather weak. For example, using this rule, we cannot show that:
{True }
IFB 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}} IFB 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).

Now we can formalize the Hoare proof rule for conditionals and prove it correct.

Theorem hoare_if : P Q b c1 c2,
{{fun stP st bassn b st}} c1 {{Q}}
{{fun stP st ~(bassn b st)}} c2 {{Q}}
{{P}} (IFB b THEN c1 ELSE c2 FI) {{Q}}.
Proof.
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.

Example if_example :
{{fun stTrue}}
IFB (BEq (AId X) (ANum 0))
THEN (Y ::= (ANum 2))
ELSE (Y ::= APlus (AId X) (ANum 1))
FI
{{fun stst Xst Y}}.
Proof.
(* WORK IN CLASS *) Admitted.

### Loops

Suppose we have a loop
WHILE b DO c END
and we want to find a pre-condition P and a post-condition Q such that
{{P}WHILE b DO c END {{Q}
is a valid triple.
First of all, let's think about the case where b is false at the beginning — i.e., let's assume 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 END {{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 END {{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 END {{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 (showing that it establishes the invariant by the time it finishes). This gives us the final version of the rule:
 {{P ∧ b}} c {{P}} (hoare_while) {{P}} WHILE b DO c END {{P ∧ ~b}}
The proposition P is called an invariant of the loop.
One subtlety in the terminology is that calling some assertion P a "loop invariant" doesn't just mean that it is preserved by the body of the loop in question (i.e., {{P}} c {{P}}, where c is the loop body), but rather that P together with the fact that the loop's guard is true is a sufficient precondition for c to ensure P as a postcondition.
This is a slightly (but significantly) weaker requirement. For example, if P is the assertion X = 0, then P is an invariant of the loop
WHILE X = 2 DO X := 1 END
although it is clearly not preserved by the body of the loop.

Lemma hoare_while : P b c,
{{fun stP st bassn b st}} c {{P}}
{{P}} WHILE b DO c END {{fun stP st ¬ (bassn b st)}}.
Proof.
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 "keep looping" case, its hypotheses

remember (WHILE b DO c END) as wcom eqn:Heqwcom.
ceval_cases (induction He) Case;
try (inversion Heqwcom); subst; clear Heqwcom.

Case "E_WhileEnd".
split. assumption. apply bexp_eval_false. assumption.

Case "E_WhileLoop".
apply IHHe2. reflexivity.
apply (Hhoare st st'). assumption.
split. assumption. apply bexp_eval_true. assumption.
Qed.

Is the assertion
X = 0
an invariant of the following loop?
WHILE X<100 DO X ::= X+1 END
(1) Yes
(2) No

Is the assertion
Y = 0
an invariant of the following loop?
WHILE X<100 DO X ::= X+1 END

Is the assertion
X > 0
an invariant of the following loop?
WHILE X<100 DO X ::= X+1 END

Is the assertion
X > 0
an invariant of the following loop?
WHILE X = 0 DO X ::= X+1 END

Is the assertion
X > 10
an invariant of the following loop?
WHILE X>10 DO X ::= X+1 END

Is the assertion
X = Y + Z
an invariant of the following loop?
WHILE Y>10 DO Y := Y-1; Z ::= Z+1 END

We can use the while rule to prove the following Hoare triple, which may seem surprising at first...

Theorem always_loop_hoare : P Q,
{{P}} WHILE BTrue DO SKIP END {{Q}}.
Proof.
(* WORK IN CLASS *) Admitted.

## Review

The rules of Hoare Logic:
 (hoare_asgn) {{Q [X ↦ a]}} X::=a {{Q}}
 (hoare_skip) {{ P }} SKIP {{ P }}
 {{ P }} c1 {{ Q }} {{ Q }} c2 {{ R }} (hoare_seq) {{ P }} c1;;c2 {{ R }}
 {{P ∧  b}} c1 {{Q}} {{P ∧ ~b}} c2 {{Q}} (hoare_if) {{P}} IFB b THEN c1 ELSE c2 FI {{Q}}
 {{P ∧ b}} c {{P}} (hoare_while) {{P}} WHILE b DO c END {{P ∧ ~b}}
 {{P'}} c {{Q'}} P ⇾ P' Q' ⇾ Q (hoare_consequence) {{P}} c {{Q}}
In the next chapter, we'll see how these rules are used to prove that programs satisfy specifications of their behavior.