(** * HoareAsLogic: Hoare Logic as a Logic *)
(** This chapter is optional. It explores how Hoare can be studied
as a logic in its own right, from the perspective of mathematical
logic. *)
From PLF Require Import Maps.
From PLF Require Import Imp.
Hint Constructors ceval.
From PLF Require Import Hoare.
(* ################################################################# *)
(** * Hoare Logic and Model Theory *)
(** A _valid_ Hoare triple expresses a truth about how Imp
program execute. *)
Definition valid (P : Assertion) (c : com) (Q : Assertion) : Prop :=
forall st st',
st =[ c ]=> st' ->
P st ->
Q st'.
(** 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 _model theory_. *)
(* ################################################################# *)
(** * Hoare Logic and Proof Theory *)
(** Proof rules constitute a logic in their own right: *)
(**
---------------- (hoare_skip)
{{P}} SKIP {{P}}
----------------------------- (hoare_asgn)
{{Q [X |-> a]}} X ::= a {{Q}}
{{P}} c1 {{Q}}
{{Q}} c2 {{R}}
------------------ (hoare_seq)
{{P}} c1;; c2 {{R}}
{{P /\ b}} c1 {{Q}}
{{P /\ ~ b}} c2 {{Q}}
------------------------------------ (hoare_if)
{{P}} TEST b THEN c1 ELSE c2 FI {{Q}}
{{P /\ b}} c {{P}}
----------------------------- (hoare_while)
{{P} WHILE b DO c {{P /\ ~b}}
{{P'}} c {{Q'}}
P ->> P'
Q' ->> Q
----------------------------- (hoare_consequence)
{{P}} c {{Q}}
*)
(** Those rules can be used to show that a triple is _derivable_
by constructing a proof tree: *)
(**
--------------------------- (hoare_asgn)
X=0 ->> X+1=1 {{X+1=1}} X ::= X+1 {{X=1}}
---------------------------------------------------------- (hoare_consequence)
{{X=0}} X ::= X+1 {{X=1}}
*)
(** 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 _proof theory_.
Our goal for the rest of this chapter is to formalize Hoare logic using
proof theory, and prove that the model-theoretic and proof-theoretic
formalizations are consistent with one another.
*)
(* ################################################################# *)
(** * Derivability *)
(** To formalize derivability of Hoare triples, we introduce inductive type
[derivable], which describes legal proof trees using the Hoare rules. *)
Inductive derivable : Assertion -> com -> Assertion -> Type :=
| H_Skip : forall P,
derivable P (SKIP) P
| H_Asgn : forall Q X a,
derivable (Q [X |-> a]) (X ::= a) Q
| H_Seq : forall P c Q d R,
derivable P c Q -> derivable Q d R -> derivable P (c;; d) R
| H_If : forall P Q (b : bexp) c1 c2,
derivable (P /\ b) c1 Q ->
derivable (P /\ ~ b) c2 Q ->
derivable P (TEST b THEN c1 ELSE c2 FI) Q
| H_While : forall P (b : bexp) c,
derivable (P /\ b) c P ->
derivable P (WHILE b DO c END) (P /\ ~ b)
| H_Consequence : forall P Q P' Q' c,
derivable P' c Q' ->
P ->> P' ->
Q' ->> Q ->
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}}
*)
Example example_proof :
derivable
((X = 3) [X |-> X + 2] [X |-> X + 1])
(X ::= X + 1;; X ::= X + 2)
(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. *)
(* ################################################################# *)
(** * Soundness and Completeness *)
(** We now have two approaches to formulating Hoare logic:
- 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.
Do these two approaches agree? That is, are the valid Hoare triples exactly
the derivable ones? This is a standard question investigated in
mathematical logic. There are two pieces to answering it:
- A logic is _sound_ if everything that is derivable is valid.
- A logic is _complete_ if everything that is valid is derivable.
We can prove that Hoare logic is sound and complete.
*)
(* ################################################################# *)
(** * Postscript: Decidability *)
(** We might hope that Hoare logic would be _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.
Consider the triple [{{True}} c {{False}}]. This triple is valid if and
only if [c] is non-terminating. So any algorithm that could
determine validity of arbitrary triples could solve the Halting
Problem.
Similarly, the triple [{{True}} SKIP {{P}}] is valid if and only if
[forall s, P s] is valid, where [P] is an arbitrary assertion of Coq's
logic. But it is known that there can be no decision procedure for
this logic. *)