\chapter{Hoare Logic}
\label{chap:hoare-logic}

If operational semantics corresponds to an idealized interpreter, \emph{Hoare
logic} corresponds to an idealized verifier. Hoare logic can be used to specify
the semantics of a programming language, but it is particularly convenient to
reason about concrete programs and prove them correct. It is named after its
inventor, Charles Antony Richard (Tony) Hoare. Hoare logic is also called
\emph{axiomatic semantics}.

This chapter is heavily inspired by Chapter~12 of \emph{Concrete
Semantics: With Isa\-belle\slash HOL}~\cite{nipkow-klein-2014}.

\section{Hoare Triples}
\label{sec:hoare-triples}

Hoare logic is a framework for deducing valid correctness formulas in a
mechanical way, using a set of derivation rules. It allows us to reason
directly about a program's syntax, without concerning ourselves with its
operational semantics. The approach is mechanical in the sense that the
applicability of a derivation rule can easily be checked.

We start by introducing Hoare logic abstractly, without any connection to Lean.
In a second step, we will see how we can embed Hoare logic judgments in Lean in
a natural way. The basic judgments of Hoare logic are called \emph{Hoare
triples}. They have the form \li|{P} S {Q}|, where \li{S} is a WHILE
statement, and \li{P} and \li{Q} are logical formulas over the program
variables. For the moment, we imagine the formulas as syntactic objects built
using the familiar connectives and quantifiers. The intended meaning of a Hoare
triple is as follows:
%
%%% TYPESETTING: repeated text
\begin{quote}
If the \emph{precondition} \li{P} is true before \li{S} is executed and the
execution terminates normally, the \emph{postcondition} \li{Q} is true at
termination.
\end{quote}
%
This is a \emph{partial correctness} statement: The program is correct
\emph{if} it terminates normally; otherwise, we do not know or care. For WHILE
programs, the only way not to terminate normally is to enter an infinite loop.
For other programming languages, infinite recursion and run-time errors such as
division by zero may also result in divergence or abnormal termination.

Intuitively, all of the Hoare triples below should be valid:
%
\begin{center}
\li|{true} b := 4 {b = 4}| \\[\jot]
\li|{a = 2} b := 2 * a {a = 2 ∧ b = 4}| \\[\jot]
\li|{b ≥ 5} b := b + 1 {b ≥ 6}| \\[\jot]
\li|{false} skip {b = 10}| \\[\jot]
\li|{true} while i ≠ 10 do i := i + 1 {i = 10}|
\end{center}
%
The first three Hoare triples should be fairly natural.
The fourth triple is vacuously true, since the precondition \li{false} can
%%% TYPESETTING: repeated text
never be met. The part ``If the \relax{precondition} \li{P} is true'' of the
definition of Hoare triple is always false; hence the triple is true. The
triple is equivalent to the proposition \li|false → b = 10|, which holds for
any value of \li|b|. As for the fifth triple, there are no guarantees that
control will escape the loop (if \li{i > 10} initially), but if it does
escape, then the loop's condition must be false and hence we have the
postcondition \li{i = 10}.

The following triples are bizarre but interesting:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\li${false}$ & \li$S {true}$ \\[\jot]
\li${false}$ & \li$S {false}$ \\[\jot]
\li${true}$ & \li$S {true}$ \\[\jot]
\li${true}$ & \li$S {false}$
\end{tabular}
\end{center}
%
The first two triples are true of any statement \li{S} (and therefore
pointless): The precondition is never satisfied, so any postcondition holds
vacuously. The third triple is always true as well, regardless of \li{S}. The
fourth triple is true if \li{S} never terminates (e.g., \li{S :=}
\li{while true do skip}); otherwise, it is false.

\section{Hoare Rules}
\label{sec:hoare-rules}

Below we give a complete set of derivation rules for reasoning about WHILE
programs:

\ifdefined\TABLET
\vskip\abovedisplayskip
\else
\vskip\abovedisplayshortskip
\fi

\centerline{\prftree[r]{\textsc{Skip}}
  {\strut\texttt{\{{\relax P\/}\}~skip~\{{\relax P\/}\}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Asn}}
  {\strut\texttt{\{{\relax Q}[{\relax a\/}/{\relax x\/}]\}~{\relax x\/} := {\relax a\/}~\{{\relax Q\/}\}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Seq}}
  {\strut\texttt{\{{\relax P\/}\}~{\relax S}~\{{\relax R\/}\}}}
  {\strut\texttt{\{{\relax R\/}\}~{\relax T}~\{{\relax Q\/}\}}}
  {\strut\texttt{\{{\relax P\/}\}~{\relax S}; {\relax T}~\{{\relax Q\/}\}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{If}}
  {\strut\texttt{\{{\relax P} $\land$ {\relax b\/}\}~{\relax S}~\{{\relax Q\/}\}}}
  {\strut\texttt{\{{\relax P} $\land$ $\lnot${\relax b\/}\}~{\relax T}~\{{\relax Q\/}\}}}
  {\strut\texttt{\{{\relax P\/}\}~if {\relax b\/} then {\relax S} else {\relax T}~\{{\relax Q\/}\}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{While}}
  {\strut\texttt{\{P $\land$ {\relax b\/}\}~{\relax S}~\{P\}}}
  {\strut\texttt{\{P\}~while {\relax b\/} do {\relax S}~\{{\relax P\/} $\land$ $\lnot${\relax b\/}\}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Conseq}}
  {\strut\texttt{{\relax P\/}$'$ $\rightarrow$ {\relax P}}}
  {\strut\texttt{\{{\relax P\/}\}~{\relax S}~\{{\relax Q\/}\}}}
  {\strut\texttt{{\relax Q} $\rightarrow$ {\relax Q\/}$'$}}
  {\strut\texttt{\{{\relax P\/}$'$\}~{\relax S}~\{{\relax Q\/}$'$\}}}}

\vskip\belowdisplayskip

\noindent
In the \textsc{Asn} rule, the
syntax $\texttt{{\relax Q}[{\relax a\/}/{\relax x\/}]}$
denotes the condition $\texttt{\relax Q}$ in which all occurrences of
$\texttt{\relax x}$ are replaced by~$\texttt{\relax a}$. The rule is sometimes
presented as
%
\[\prftree[r]{\textsc{Asn}}
  {\strut\texttt{\{{\relax Q}[{\relax a\/}]\}~{\relax x\/} := {\relax a\/}~\{{\relax Q}[{\relax x\/}]\}}}\]
%
where $\texttt{[{\relax x\/}]}$ factors out the occurrences of
\texttt{\relax x} in \texttt{\relax Q}.

The \textsc{Asn} rule may seem counterintuitive because it works backwards: From
the postcondition, it computes a precondition. Nevertheless, it correctly
captures the semantics of the assignment statement, as illustrated below:
%
\begin{center}
\li|{0 = 0} x := 0 {x = 0}| \\[\jot]
\li|{0 = 0 ∧ y = 5} x := 0 {x = 0 ∧ y = 5}| \\[\jot]
\li|{x + 1 ≥ 5} x := x + 1 {x ≥ 5}|
\end{center}
%
Using elementary arithmetic, we can simplify the computed preconditions; for
example, \li{0 = 0} is equivalent to true, and \li{x + 1 ≥ 5} is equivalent to
\li{x ≥ 4}.

The \textsc{Seq} rule requires us to come up with an intermediate condition
\texttt{\relax R} that holds after executing \texttt{\relax S}
and before executing \texttt{\relax T}. Here is an example of \textsc{Seq}
in action:
%
\[\prftree[r]{\textsc{Seq}}
  {\prftree[r]{\textsc{Asn}}
    {\strut\texttt{\{a = 2\} b := a \{b = 2\}}}}
  {\prftree[r]{\textsc{Asn}}
    {\strut\texttt{\{b = 2\} c := b \{c = 2\}}}}
  {\strut\texttt{\{a = 2\} b := a; c := b \{c = 2\}}}\]

The \textsc{While} rule is the most intricate. The condition \li{P} is called an
\emph{invariant}. It is the pre-~and the postcondition of the loop itself but
also of its body. The body's precondition is strengthened with the knowledge
that \texttt{\relax b} must be true before executing the body. Similarly, the
loop's postcondition is strengthened with the knowledge that \texttt{\relax b}
must be false when the loop exits.

Consider an execution of a loop with
$\text{\textit n}$~iterations. Suppose that the initial state is \li{s₀} and
that the state after the \textit{i}th iteration of the loop is
\li{s}$_\text{\textit i}$. Then the following conditions will hold:
%
\begin{center}
\begin{tabular}{@{}c@{\qquad}c@{\qquad}c@{\qquad}c@{\qquad}c@{}}
\li|P s₀| & \li|P s₁ ∧ b s₁| & $\cdots$
& \li|P s|$_{\text{\textit n}-\texttt{1}}$\li| ∧ b s|$_{\text{\textit n}-\texttt{1}}$
& \li|P s|$_{\text{\textit n}}$\li| ∧ ¬ b s|$_{\text{\textit n}}$
\end{tabular}
\end{center}
%
If \text{\textit n}\li{ = 0}, we immediately have that \li|P s₀ ∧ ¬ b s₀| and
never enter the loop.

The \textsc{Conseq} rule is the only rule that has logical formulas among its
premises, as opposed to Hoare triples. These conditions must be discharged,
whether using pen and paper or a proof assistant. \textsc{Conseq} can be used
to strengthen a precondition (i.e., make it more strict), weaken a
postcondition (i.e., make it less strict), or both. An example derivation
follows:
%
\[\tabletsmall\prftree[r]{\textsc{Conseq}}
  {\strut\texttt{x > 8 $\rightarrow$ x > 4}}
  {\prftree[r]{\textsc{Asn}\!\!\!\!\!\!\!\!\!\!} %%% TYPESETTING: hack
    {\strut\texttt{\{x > 4\} y := x \{y > 4\}}}}
  {\strut\texttt{y > 4 $\rightarrow$ y > 0}}
  {\strut\texttt{\{x > 8\} y := x \{y > 0\}}}\]
%
Reading the tree from top to bottom, we have \relax{strengthened} the triple's
precondition from \li{x > 4} to \li{x > 8} and \relax{weakened} the
postcondition from \li{y > 4} to \li{y > 0}. We can also read the tree from
the bottom up: To prove the triple \texttt{\{x > 8\} y := x \{y > 0\}}, it
suffices to prove \texttt{\{x > 4\} y := x \{y > 4\}}, where the precondition
is \relax{weakened} and the postcondition is \relax{strengthened}.

Except for \textsc{Conseq}, the rules are \emph{syntax-driven}: We know which
rule to apply in each case, simply by inspecting the statement at hand. For an
assignment, we apply \textsc{Asn}; for a \li{while} loop, we apply
\textsc{While}; and so on.

The rules \textsc{Seq}, \textsc{If}, and \textsc{Conseq} are
\emph{bidirectional}: Their conclusions are of the form \li|{P}| \li|…|
\li|{Q}|, for distinct mathematical metavariables \li{P}, \li{Q}. This can make
them convenient to apply. By combining the other rules with \textsc{Conseq}, we
can derive bidirectional variants:

\vskip\abovedisplayskip

\centerline{\prftree[r]{\textsc{Skip}$'$}
  {\strut\texttt{\relax P} \rightarrow \texttt{\relax Q}}
  {\strut\texttt{\{{\relax P\/}\}~skip~\{{\relax Q\/}\}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Asn}$'$}
  {\strut\texttt{{\relax P} $\rightarrow$ {\relax Q}[{\relax a\/}/{\relax x\/}]}}
  {\strut\texttt{\{{\relax P\/}\}~\texttt{\relax x} := \texttt{\relax a}~\{\texttt{\relax Q\/}\}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{While}$'$}
  {\strut\texttt{\{{\relax P} $\land$ {\relax b\/}\}~{\relax S}~\{P\}}}
  {\strut\texttt{P $\land$ $\lnot${\relax b\/} $\rightarrow$ Q}}
  {\strut\texttt{\{P\}~while {\relax b\/} do {\relax S}~\{{\relax Q\/}\}}}}

\vskip\belowdisplayskip

\noindent
As an easy exercise, you could try to derive each of these rules from
\textsc{Skip}, \textsc{Asn}, or \textsc{While} in conjunction with
\textsc{Conseq}.

\section{A Semantic Approach to Hoare Logic}
\label{sec:a-semantic-approach-to-hoare-logic}

A natural way to encode Hoare logic in Lean would be to proceed as we
have done for the big- and small-step semantics: Define a syntactic notion of
Hoare triple and an inductive predicate, with one introduction rule for each
core Hoare rule; to represent pre-~and postconditions, use predicates on
states (\li{state} \li{→ Prop}). Then we could prove \emph{soundness} with
respect to the big-step semantics, meaning the following: Whenever
\li|{P} S {Q}| is derivable, if \li{P s} and \li{(S, s) ⟹ t}, then
\li{Q t}. This is merely a logical rendition of the intuitive meaning of a
Hoare triple:
%
%%% TYPESETTING: repeated text
\begin{quote}
If the \relax{precondition} \li{P} is true before \li{S} is executed (i.e.,
\li{P s}) and the execution terminates normally (i.e., \hbox{\li{(S, s)}} \li{⟹ t}), the
\relax{postcondition} \li{Q} is true at termination (i.e., \li{Q t}).
\end{quote}

Instead of pursuing this approach, we propose to define Hoare triples
semantically in Lean, in terms of the big-step semantics, so that they are
\emph{correct by definition}. Then we will derive the Hoare rules as lemmas,
instead of stating them as introduction rules. In conjunction with the use of
predicates to represent formulas, this approach is resolutely semantic.

Hoare triple (for partial correctness) are defined as follows:

\lstinputlisting[linerange=partial_hoare-q]{../lean/love09_hoare_logic_demo_master.lean}
%
Instead of writing \li{partial_hoare P S Q}, we introduce some syntactic
sugar to allow \li|{* P *} S {* Q *}|, which is closer to the
informal syntax \li|{P} S {Q}|.

The core Hoare rules are stated as follows:
%
\lstinputlisting[linerange=skip_intro-q]{../lean/love09_hoare_logic_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=assign_intro-q]{../lean/love09_hoare_logic_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=seq_intro-q]{../lean/love09_hoare_logic_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=ite_intro-q]{../lean/love09_hoare_logic_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=while_intro-q]{../lean/love09_hoare_logic_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=consequence-q]{../lean/love09_hoare_logic_demo_master.lean}

All of the above lemmas have proofs based on the big-step semantics. Some of
the triples---for example, the precondition in \li{assign_intro}---need to
refer to the state explicitly. In such case, we use a \li{λ}-expression to
access it. Recall that \li{P} and \li{λs, P s} are the same by
\li{η}-conversion. Moreover, for a premise written informally as \li{P → Q}, in
Lean we must write \li{∀s, P s → Q s}. This reflects the difference between
syntactic formulas and semantic predicates. As in
Chapter~\ref{chap:operational-semantics}, the syntax \hbox{\li|s{x ↦ n}|} in the
assignment rule denotes the state that is identical to \li{s} at all points
except \li{x} and that maps \li{x} to \li{n}.

The following convenience rules can be derived from the core rules:

\lstinputlisting[linerange=consequence_left-q]{../lean/love09_hoare_logic_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=consequence_right-q]{../lean/love09_hoare_logic_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=skip_intro'-q]{../lean/love09_hoare_logic_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=assign_intro'-q]{../lean/love09_hoare_logic_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=seq_intro'-q]{../lean/love09_hoare_logic_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=while_intro'-q]{../lean/love09_hoare_logic_demo_master.lean}

Using the bidirectional \li{assign_intro'}, we can derive a forward version of
the assignment rule:
%
\lstinputlisting[linerange=assign_intro_forward-q]{../lean/love09_hoare_logic_demo_master.lean}
%
The bound variable \li{n₀} stands for the value of \li{x} before the
assignment. Hence, in the postcondition, \li$s{x ↦ n₀}$ denotes the state
\emph{before} the assignment. Since \li{P} is a precondition, we have
\hbox{\li$P (s{x ↦ n₀})$.} In addition, the new value of~\li{x}, given by \li{s x},
must be equal to the value of the arithmetic expression \li{a} evaluated in the
old state \li$s{x ↦ n₀}$.

The forward rule is less convenient than the backward rule, because the
postcondition contains an existential quantifier. It is possible to state a
backward rule in a similar style, revealing a hidden symmetry:
%
\lstinputlisting[linerange=assign_intro_backward-q]{../lean/love09_hoare_logic_demo_master.lean}
%
Notice that this existential quantifier can be eliminated using a one-point
rule (Section~\ref{sec:forward-reasoning-about-connectives-and-quantifiers}).
We then get the familiar backward rule \li{assign_intro}, with
\li|λs, P (s{x ↦ a s})| as the precondition.

\section{First Program: Exchanging Two Variables}
\label{sec:first-program-exchanging-two-variables}

Let us use the Hoare logic to verify our first program:\ a three-line program
that exchanges the values of its variables \li{a} and \li{b}, using \li{t} for
temporary storage. The program is defined as follows:
%
\lstinputlisting[linerange=SWAP-q]{../lean/love09_hoare_logic_demo_master.lean}

The correctness statement is as follows:
%
\lstinputlisting[linerange=SWAP_correct_statement-q]{../lean/love09_hoare_logic_demo_master.lean}
%
The logical variables \li{a₀} and \li{b₀} ``freeze'' the initial value of the
program variables \li{a} and \li{b} so that we can refer to them in the
postcondition. After all, it would make no sense to put
\li{λs, s "a" = s "b" ∧ s "b" = s "a"} as the postcondition.

The correctness proof follows:
%
\lstinputlisting[linerange=SWAP_correct_proof-q]{../lean/love09_hoare_logic_demo_master.lean}
%
The applications of the sequential composition and assignment rules are guided
by the program's syntax. There are two sequential compositions and three
assignments in the program and therefore as many invocations of the
corresponding rules. We end up with a very aesthetically challenged subgoal:
%
\begin{center}
\tabletfootnotesize
\begin{tabular}{@{}l@{}}
\lic$⊢ ∀s : state,$ \\
\noindent\hbox{}\qquad\lic$s "a" = a₀ ∧ s "b" = b₀ →$ \\
\noindent\hbox{}\qquad\lic$s{"t" ↦ s "a"}{"a" ↦ s{"t" ↦ s "a"} "b"}$ \\
\noindent\hbox{}\qquad\quad\lic${"b" ↦ s{"t" ↦ s "a"}{"a" ↦ s{"t" ↦ s "a"} "b"} "t"} "a" = b₀ ∧$ \\
\noindent\hbox{}\qquad\lic$s{"t" ↦ s "a"}{"a" ↦ s{"t" ↦ s "a"} "b"}$ \\
\noindent\hbox{}\qquad\quad\lic${"b" ↦ s{"t" ↦ s "a"}{"a" ↦ s{"t" ↦ s "a"} "b"} "t"} "b" = a₀$
\end{tabular}
\end{center}
%
Fortunately, \li{simp} can reduce the subgoal dramatically, and if we enable
\emph{contextual rewriting}---an option that tells \li{simp} to use any
assumptions in the goal's target (such as \li{s "a" = a₀} and \hbox{\li{s "b" = b₀})}
as left-to-right rewrite rules---\li{simp} can even prove the subgoal.

The above proof could also be carried out directly in terms of the big-step
semantics, without using the Hoare rules:
%
\lstinputlisting[linerange=SWAP_correct₂-q]{../lean/love09_hoare_logic_demo_master.lean}
%
The \li{finish} tactic combines various techniques, including normalization of
logical connectives and quantifiers, simplification, congruence closure, and
quantifier instantiation. Like \li{tautology}
(Section~\ref{sec:tautology-tactic}), it provides strong automation that can
ruin many logical exercises if introduced too early in a course.

\section{Second Program: Adding Two Numbers}
\label{sec:second-program-adding-two-numbers}

Our second example computes \li{m + n}, leaving the result in \li{m},
using only these primitive operations: \li{k + 1}, \li{k - 1}, and \li{k ≠ 0}
(for arbitrary \li{k}):

\lstinputlisting[linerange=ADD-q]{../lean/love09_hoare_logic_demo_master.lean}

Because of the presence of a \li{while} loop, the proof is more involved:
%
\lstinputlisting[linerange=ADD_correct-q]{../lean/love09_hoare_logic_demo_master.lean}
%
The first step is to apply the derived \li{while} rule with a loop invariant.
Our invariant is that the sum of the program variables \li{n} and \li{m} must
be equal to the desired mathematical result \li{n₀ +} \hbox{\li{m₀},} where
\li{n₀} and \li{m₀} correspond to the initial values of \li{n} and \li{m}, as
required by the precondition.

How did we come up with this invariant? Even for a simple loop, finding a
suitable invariant can be challenging. The difficulty is that the invariant
must
%
\begin{itemize}
\item[1.] be true before we enter the loop;

\item[2.] remain true after each iteration of the loop if it was true before the
iteration;

\item[3.] be strong enough to imply the desired loop postcondition.
\end{itemize}
%
An invariant such as \li{true} meets requirements~1 and 2 but usually not
3. Similarly, \li{false} meets requirements 2 and 3 but usually not 1.
In practice, suitable invariants tend to be of the form
%
\[\text{\emph{work done} \texttt{+} \emph{work remaining} \texttt{=} \emph{desired
  result}}\]
%
where \li{+} stands for some appropriate operator (not necessarily
addition). When we enter the loop, \emph{work done} will often be \li{0} (or
some other appropriate ``zero'' value), and the invariant becomes
%
\[\text{\emph{work remaining} \texttt{=} \emph{desired result}}\]
%
This invariant would have to be provable at the beginning of the
loop---either from the postcondition of the previous statement or from the
desired precondition of the entire program if there is no previous statement.
When we exit the loop, \emph{work remaining} should be \li{0} (or
some variant thereof), and the invariant becomes
%
\[\text{\emph{work done} \texttt{=} \emph{desired result}}\]
%
Often, \emph{work done} takes the form of a variable in which we
accumulate the result, whereas \emph{work remaining} is similar to
\emph{desired result} but depends on program variables whose values change inside
the loop and must account for \emph{work done}.

For the \li{ADD} program's loop, the \emph{work done} is \li{m}, the \emph{work
remaining} is \li{n}, and the \emph{desired result} is \li{n₀ + m₀}.
When entering the loop, the invariant \li{m + n = n₀ + m₀} holds because then
\li{m = m₀} and \li{n = n₀}. (Unusually, the \emph{work done} is not
\li{0} for this example, because we reuse the input \li{m} as our accumulator,
as an optimization.) When exiting the loop, we have that \li{n = 0}, so the
invariant becomes \hbox{\li{m = n₀}} \li{+ m₀}. We can retrieve the result from~\li{m}.

The \li{while_intro'} lemma is used directly as a proof term. It
gives rise to three subgoals. The proofs that the invariant is implied by the
desired precondition and that it implies the desired postcondition are trivial:
They consist of a call to \li{simp} with contextual rewriting enabled. The
only nontrivial subgoal is the condition that executing the body maintains the
invariant. There is some ugly arithmetic on natural numbers necessary due to the
use of the truncated minus operator. Our proof simply performs a case
distinction to isolate the zero case (where \li{0 - 1 = 0})
from the nonzero case.

For this example, Hoare logic really helps. Reasoning directly about the
operational semantics would be inconvenient, because we would need induction to
reason about the \li{while} loop. With Hoare logic, this induction is performed
out once and for all in the proof of the \li{while_intro} rule.

\section{Finish Tactic}
\label{sec:finish-tactic}

\subsection*{finish}

\smallskip

\begin{quote}
\lic|finish| $\bigl[$\lic|[h₁, …, hₘ]|$\bigr]$ $\bigl[$\li|using [k₁, …, kₙ]|$\bigr]$
\end{quote}
%
The \li{finish} tactic first normalizes and simplifies the hypotheses, using
the optionally supplied lemmas \li{h₁}, \ldots, \li{hₘ}. Then it applies the
congruence closure (\li{cc}) together with the optionally supplied lemmas
\li{k₁}, \ldots, \li{kₙ}. Universally quantified hypotheses and lemmas are
instantiated automatically. Like \li{cc}, \li{finish} either fully succeeds
or fails. The tactic is complete for propositional logic.

\section{A Verification Condition Generator}
\label{sec:a-verification-condition-generator}

\emph{Verification condition generators} (VCGs) are programs that apply Hoare
logic rules, producing \emph{verification conditions} that must be proved
manually. We can think of them as mechanical civil servants that take care of
the Hoare logic bureaucracy. As users, we must provide strong enough loop
invariants as annotations in our programs. Hundreds of program verification
tools are based on these principles.

VCGs typically work backwards from the postcondition, using \emph{backward}
rules---rules stated to have an arbitrary \li{Q} as their postcondition. This
works well because the central rule of Hoare logic---the assignment rule---is
backward. If it were not for the assignment statement, the state would never
change, and there would be no need for Hoare logic.

We can use Lean's metaprogramming framework to define a simple VCG. First, we
introduce a constant called \li{stmt.while_inv} that carries a user-supplied
invariant~\li{P} in addition to the loop condition \li{b} and body \li{S}:

\lstinputlisting[linerange=while_inv-q]{../lean/love09_hoare_logic_demo_master.lean}

We provide two Hoare rules for the construct:\ a backward rule and a
bidirectional rule. Both are justified in terms of the bidirectional
\li{while_intro'} rule:

\lstinputlisting[linerange=while_inv_intro-q]{../lean/love09_hoare_logic_demo_master.lean}
%
The rules simply use the invariant annotation as their invariant. When using the
framework, we will have to be careful to annotate all \li{while} loops with
suitable invariants. If we specify a wrong invariant, we will face unprovable
subgoals, indicating that we must revise the invariant.

The code of the VCG is fairly concise:

\lstinputlisting[linerange=vcg-q]{../lean/love09_hoare_logic_demo_master.lean}

The VCG extracts the current goal's target and inspects it. If it is a
Hoare triple, it inspects its precondition \li{P} and statement \li{S}. If the
precondition is a metavariable (e.g., \li{?P}), it applies a backward rule if
there exists one (e.g., the standard assignment rule \li{assign_intro}) because
this will instantiate the metavariable. Otherwise, a bidirectional rule is
used, with an arbitrary variable as its precondition, which can be matched
against the target's precondition. For \li{while} loops, we only consider
programs that use \li{stmt.while_inv}, because we cannot guess the invariant
programmatically.

The VCG calls itself recursively on all newly emerging subgoals (via the
tactic combinator \li{;}) for the compound statements.

\section{Second Program Revisited: Adding Two Numbers}
\label{sec:second-program-revisited-adding-two-numbers}

Using the verification condition generator, we can revisit the correctness
proof for the \li{ADD} program presented above:
%
\lstinputlisting[linerange=ADD_correct₂-q]{../lean/love09_hoare_logic_demo_master.lean}

We use \li{show} to annotate the \li{while} loop with an invariant. Recall that
the \li{show} command restates the goal in a computationally equivalent
way. Here, we use this facility to replace \hbox{\li{stmt.while}} by
\li{stmt.while_inv}, which equals \li{stmt.while} by definition. The
program and its pre-~and postconditions are otherwise the same as in the lemma
statement.

We invoke \li{vcg} as the first proof step. This will apply all the necessary
Hoare rules and leave us with some subgoals. We first simplify them with
contextual rewriting enabled; this already takes care of two of the three
subgoals. For the third subgoal, the proof is as in
Section~\ref{sec:second-program-adding-two-numbers}.

\section{Hoare Triples for Total Correctness}
\label{sec:hoare-triples-for-total-correctness}

The focus so far in this chapter has been on partial correctness. When we
state the Hoare triple \li|{P} S {Q}|, we claim that the final state will
satisfy \li{Q} \emph{if} the program~\li{S} terminates, but we say nothing
when \li{S} does not terminate. In particular, we can prove any
postcondition for the program \li{while true do skip}. This is admittedly too
liberal: If you are asked to program a sorting algorithm at an exam, you should
certainly not give \li{while true do skip} as your answer.

\emph{Total correctness} is a stronger notion that asserts, in addition to
partial correctness, that the program terminates normally. One reason to focus
on partial correctness is that it is a necessary component of total correctness.
It is also simpler, which is a benefit in the classroom.

The Hoare triples for total correctness have the form \hbox{\li{[P] S [Q]},}
with the following intended meaning:
%
\begin{quote}
If the precondition \li{P} holds before \li{S} is executed, the
execution terminates normally and the postcondition \li{Q} holds in the
final state.
\end{quote}
%
For deterministic programs, this can be expressed equivalently as follows:
%
\begin{quote}
If the precondition \li{P} holds before \li{S} is executed, there exists a
state in which execution terminates normally and the postcondition \li{Q}
holds in that state.
\end{quote}

Here is an example Hoare triple that is valid:

\begin{center}
\li{[i ≤ 10] while i < 10 do i := i + 1 [i = 10]}
\end{center}

For the WHILE language, the distinction between partial and total correctness
only concerns \li{while} loops (and programs containing them). The Hoare
rule for \li{while} must now be annotated by a \emph{variant} \li{V}---a
natural number that decreases by~one or more with each iteration:
%
\[\prftree[r]{\textsc{While-Var}}
  {\strut\texttt{[P $\land$ {\relax b\/} $\land$ V = v₀]~{\relax S}~[P $\land$ V < v₀]}}
  {\strut\texttt{[P]~while {\relax b\/} do {\relax S}~[{\relax P\/} $\land$ $\lnot${\relax b\/}]}}
\]
%
Here, \li{v₀} is a logical variable that freezes \li{V}'s initial value
and whose scope is the entire premise, whereas \li{V} is a mathematical
metavariable (like \li{P}, \li{b}, and \li{S}). For the example above, we could
take \li{10 - i} as the variant (or \li{50 - i} or \li{1024 - i * i}).

Consider an execution \li{s₀}, \li{s₁}, $\dotsc$,
\li{s}$_{\text{\textit n}-\texttt{1}}$, \li{s}$_{\text{\textit n}}$ corresponding
to $\text{\textit n}$~loop iterations, as in Section~\ref{sec:hoare-rules}.
The following conditions will hold:

\begin{center}
\begin{tabular}{@{}c@{}c@{}c@{}c@{}c@{}c@{}c@{}c@{}c@{}}
\li|P s₀| & \hbox{\qquad} & \li|P s₁ ∧ b s₁| & \hbox{\qquad} & $\cdots$
& \hbox{\qquad}
& \li|P s|$_{\text{\textit n}-\texttt{1}}$\li| ∧ b s|$_{\text{\textit n}-\texttt{1}}$
& \hbox{\qquad}
& \li|P s|$_{\text{\textit n}}$\li| ∧ ¬ b s|$_{\text{\textit n}}$ \\[\jot]
\li|V s₀| & \li|>| & \li|V s₁| & \li|>| & $\cdots$ & \li|>| & \li|V s|$_{\text{\textit n}-\texttt{1}}$
& \li|>| & \li|V s|$_{\text{\textit n}}$ \\
\end{tabular}
\end{center}

\section{Summary of New Lean Constructs}

\begingroup
\summarysize

\subsection*{Tactics}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|finish| & normalizes, simplifies, performs congruence closure, \hbox{and more} \\
\lic|simp …| \rlap{\texttt{\char`\{} \lic|contextual := tt| \texttt{\char`\}}} \\
  & simplifies using assumptions in the goal's target as rewrite rules \\
\end{xltabular}

\endgroup
