# HoareAsLogicHoare Logic as a Logic

*theorems*about the evaluation behavior of programs, and proofs of program correctness (validity of Hoare triples) were constructed by combining these theorems directly in Coq.

*that*logic. We can do this by giving an inductive definition of

*valid derivations*in this new logic.

*Logical Foundations*(

*Software Foundations*, volume 1).

From PLF Require Import Maps.

From PLF Require Import Imp.

Hint Constructors ceval : core.

From PLF Require Import Hoare.

# Hoare Logic and Model Theory

Pre: X = 0

Com: X ::= X + 1

Post: X = 1

Pre: X = 0

Com: skip

Post: X = 1

Definition valid (P : Assertion) (c : com) (Q : Assertion) : Prop :=

∀ st st',

st =[ c ]=> st' →

P st →

Q st'.

This notion of

Pre: X = 0

Com: X ::= X + 1

Post: X = 1
is

Pre: X = 0

Com: skip

Post: X = 1
is
So far, we have punned between the syntax of a Hoare triple,
written {{P}} c {{Q}}, and its validity, as expressed by
valid. In essence, we have said that the semantic meaning of
that syntax is the proposition returned by valid. This way of
giving semantic meaning to something syntactic is part of the
branch of mathematical logic known as
Our approach to Hoare logic through model theory led us to
state proof rules in terms of that same state-based model, and to
prove program correctness in it, too. But there is another
approach, which is arguably more common in Hoare logic. We turn to
it, next.
Instead of using states and evaluation as the basis for reasoning,
let's take the proof rules from Hoare as the basis. Those
proof rules give us a set of axioms and inference rules that
constitute a logic in their own right. We repeat them here:

---------------- (hoare_skip)

{{P}} skip {{P}}

----------------------------- (hoare_asgn)

{{Q [X ⊢> a]}} X ::= a {{Q}}

{{P}} c

{{Q}} c

------------------ (hoare_seq)

{{P}} c

{{P ∧ b}} c

{{P ∧ ¬b}} c

------------------------------------ (hoare_if)

{{P}} if b then c

{{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}}
Read the Hoare triples in those rules as devoid of any
meaning other than what the rules give them. Forget about states
and evaluations. They are just syntax that the rules tell us how
to manipulate in legal ways.
Through this new lens, triple {{X = 0}} X ::= X + 1 {{X = 1}}
is

--------------------------- (hoare_asgn)

X=0 ->> X+1=1 {{X+1=1}} X ::= X+1 {{X=1}}

---------------------------------------------------------- (hoare_consequence)

{{X=0}} X ::= X+1 {{X=1}}
At each step we have either used one of the rules, or we
have appealed to reasoning about assertions, which do not involve
Hoare triples. (Note that we have left off the trivial part of
hoare_consequence above, namely X=1 ->> X=1, only because of
horizontal space contraints: it's hard to fit that many characters
on a line and have the page still be readable. If you prefer,
think of it as using hoare_consequence_pre instead.)
On the other hand, {{X = 0}} skip {{X = 1}} is
This approach gives meaning to triples not in terms of a model,
but in terms of how they can be used to construct proof trees.
It's a different way of giving semantic meaning to something
syntactic, and it's part of the branch of mathematical logic known
as
Our goal for the rest of this chapter is to formalize Hoare logic
using proof theory, and then to prove that the model-theoretic and
proof-theoretic formalizations are consistent with one another.
To formalize derivability of Hoare triples, we introduce inductive type
derivable, which describes legal proof trees using the Hoare rules.

*validity*is based on the underlying model of how Imp programs execute. That model itself is based on states. So,Pre: X = 0

Com: X ::= X + 1

Post: X = 1

*valid*, because starting from any state in which X is 0, and executing X ::= X + 1, we are guaranteed to reach a state in which X is 1. But,Pre: X = 0

Com: skip

Post: X = 1

*invalid*, because starting from any state in which X is 0, we are guaranteed not to change the state, so X cannot be 1.*model theory*.# Hoare Logic and Proof Theory

---------------- (hoare_skip)

{{P}} skip {{P}}

----------------------------- (hoare_asgn)

{{Q [X ⊢> a]}} X ::= a {{Q}}

{{P}} c

_{1}{{Q}}{{Q}} c

_{2}{{R}}------------------ (hoare_seq)

{{P}} c

_{1};; c_{2}{{R}}{{P ∧ b}} c

_{1}{{Q}}{{P ∧ ¬b}} c

_{2}{{Q}}------------------------------------ (hoare_if)

{{P}} if b then c

_{1}else c_{2}end {{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}}

*derivable*, because we can derive a proof tree using the rules:--------------------------- (hoare_asgn)

X=0 ->> X+1=1 {{X+1=1}} X ::= X+1 {{X=1}}

---------------------------------------------------------- (hoare_consequence)

{{X=0}} X ::= X+1 {{X=1}}

*not*derivable, because there is no way to apply the rules to construct a proof tree with this triple at its root.*proof theory*.# Derivability

Inductive derivable : Assertion → com → Assertion → Type :=

| H_Skip : ∀ P,

derivable P <{skip}> P

| H_Asgn : ∀ Q V a,

derivable (Q [V ⊢> a]) <{V := a}> Q

| H_Seq : ∀ P c Q d R,

derivable P c Q → derivable Q d R → derivable P <{c;d}> R

| H_If : ∀ P Q b c

_{1}c

_{2},

derivable (fun st ⇒ P st ∧ bassn b st) c

_{1}Q →

derivable (fun st ⇒ P st ∧ ~(bassn b st)) c

_{2}Q →

derivable P <{if b then c

_{1}else c

_{2}end}> Q

| H_While : ∀ P b c,

derivable (fun st ⇒ P st ∧ bassn b st) c P →

derivable P <{while b do c end}> (fun st ⇒ P st ∧ ¬ (bassn b st))

| H_Consequence : ∀ (P Q P' Q' : Assertion) c,

derivable P' c Q' →

(∀ st, P st → P' st) →

(∀ st, Q' st → Q st) →

derivable P c Q.

We don't need to include axioms corresponding to
hoare_consequence_pre or hoare_consequence_post, because these
can be proven easily from H_Consequence.

Lemma H_Consequence_pre : ∀ (P Q P': Assertion) c,

derivable P' c Q →

(∀ st, P st → P' st) →

derivable P c Q.

Lemma H_Consequence_post : ∀ (P Q Q' : Assertion) c,

derivable P c Q' →

(∀ st, Q' st → Q st) →

derivable P c Q.

As an example, let's construct a proof tree for

{{(X=3) [X ⊢> X + 2] [X ⊢> X + 1]}}

X ::= X + 1;;

X ::= X + 2

{{X=3}}

{{(X=3) [X ⊢> X + 2] [X ⊢> X + 1]}}

X ::= X + 1;;

X ::= X + 2

{{X=3}}

Example sample_proof :

derivable

((fun st:state ⇒ st X = 3) [X ⊢> X + 2] [X ⊢> X + 1])

<{ X := X + 1; X := X + 2}>

(fun st:state ⇒ st X = 3).

Proof.

eapply H_Seq.

- apply H_Asgn.

- apply H_Asgn.

Qed.

You can see how the structure of the proof script mirrors the structure
of the proof tree: at the root there is a use of the sequence rule; and
at the leaves, the assignment rule.
Show that any Hoare triple whose postcondition is True is derivable. Proceed
by induction on c.

#### Exercise: 3 stars, standard (provable_true_post)

#### Exercise: 3 stars, standard (provable_false_pre)

# Soundness and Completeness

- The model-theoretic approach uses valid to characterize when a Hoare
triple holds in a model, which is based on states.
- The proof-theoretic approach uses derivable to characterize when a Hoare triple is derivable as the end of a proof tree.

- A logic is
*sound*if everything that is derivable is valid. - A logic is
*complete*if everything that is valid is derivable.

#### Exercise: 3 stars, standard (hoare_sound)

*weakest preconditions*(which are also discussed in Hoare2). Given a command c and a desired postcondition assertion Q, the weakest precondition wp c Q is an assertion P such that {{P}} c {{Q}} holds, and moreover, for any other assertion P', if {{P'}} c {{Q}} holds then P' ->> P.

Definition wp (c:com) (Q:Assertion) : Assertion :=

fun s ⇒ ∀ s', s =[ c ]=> s' → Q s'.

Hint Unfold wp : core.

The following two theorems show that the two ways of thinking
about wp are the same.

Theorem wp_is_precondition : ∀ c Q,

{{wp c Q}} c {{Q}}.

Proof. auto. Qed.

Theorem wp_is_weakest : ∀ c Q P',

{{P'}} c {{Q}} →

P' ->> (wp c Q).

Proof. eauto. Qed.

Weakest preconditions are useful because they enable us to
identify assertions that otherwise would require clever thinking.
The next two lemmas show that in action.
What if we have a sequence c

#### Exercise: 1 star, standard (wp_seq)

_{1};; c_{2}, but not an intermediate assertion for what should hold in between c_{1}and c_{2}? No problem. Prove that wp c_{2}Q suffices as such an assertion.Lemma wp_seq : ∀ P Q c

_{1}c

_{2},

derivable P c

_{1}(wp c

_{2}Q) → derivable (wp c

_{2}Q) c

_{2}Q → derivable P <{c

_{1}; c

_{2}}> Q.

Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 2 stars, standard (wp_invariant)

Lemma wp_invariant : ∀ b c Q,

valid (wp <{while b do c end}> Q ∧ b) c (wp <{while b do c end}> Q).

Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 4 stars, standard (hoare_complete)

_{11}/script/Hoare.html

Theorem hoare_complete: ∀ P c Q,

valid P c Q → derivable P c Q.

Proof.

unfold valid. intros P c. generalize dependent P.

induction c; intros P Q HT.

(* FILL IN HERE *) Admitted.

☐

# Postscript: Decidability

*decidable*; that is, that there is an (terminating) algorithm (a

*decision procedure*) that can determine whether or not a given Hoare triple is valid or derivable. But such a decision procedure cannot exist.

(* 2020-09-09 21:08 *)