5.1.1. Notations for Assertions🔗

This way of writing assertions can be a little bit heavy, for two reasons: (1) every single assertion that we ever write is going to begin with fun st => ; and (2) this state st is the only one that we ever use to look up variables in assertions (we will almost never need to talk about two different memory states at the same time). For discussing examples informally, we'll adopt some simplifying conventions: we'll drop the initial fun st =>, and we'll write just X to mean st[X]. Thus, instead of writing

fun st => st[X] = m

we'll write just

{{ X = m }}.

Here the "doubly curly" braces {{ and }} delimit the scope of an assertion. We'll see more examples below.

This example also illustrates a convention that we'll use throughout the Hoare Logic chapters: in informal assertions, capital letters like X, Y, and Z are Imp variables, while lowercase letters like x, y, m, and n are ordinary Lean variables (of type Nat). This is why, when translating from informal to formal, we replace X with st[X] but leave m alone.

The convention described above can be implemented with a little syntax magic, using coercions and a custom grammar, much as we did with the imp { … } notation in Imp. This new notation automatically lifts Aexps, numbers, and Props into Assertions when they appear between the {{ _ }} brackets, or when Lean knows that the type of an expression is Assertion.

There is no need to understand the details of how these notations work.

Function applications inside assertions automatically interpret their arguments in the current state. Thus, {{ f e1 ... en }} stands for fun st => f (e1 st) ... (en st).

Occasionally it is simpler to write an assertion directly as a Lean function. Such a function can be placed inside the assertion notation without an escape marker.

For example, {{ fun st => ∀ x, st[x] = 0 }} indicates an assertion that every variable maps to 0 in the given state.

5.1.2. Example Assertions🔗

Here are some example assertions that take advantage of this new notation.

5.1.3. Printing Assertions🔗

As in the Imp chapter, the assertion notation above is input only: Lean reads {{ X ≤ 5 }} but still prints the underlying function, as #print assertion8 just showed. The delaborators below close the loop for plain assertions: a state lambda whose body Lean can rebuild is printed back in {{ … }} notation, and an assertion Lean cannot rebuild falls back to the raw fun st => … form, which is exactly this notation's escape syntax, so what you see is always valid input. Each time a new notation involving assertions appears below (implication, Hoare triples, substitution), a small delaborator defined next to it will extend this printing to cover it. As before, there is no need to understand the details.

5.1.4. Assertion Implication🔗

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.

Note that the notation for assertion implication is analogous to the "usual" Lean implication →.

We'll also want the "iff" variant of implication between assertions:

The matching delaborators print implications and equivalences between assertions back in ->> and <<->> notation.

5.4.1. Skip🔗

Since skip doesn't change the state, it preserves any assertion P:

--------------------  (hoare_skip)
{{ P }} skip {{ P }}

5.4.2. 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 }}

Note that, in the formal rule hoare_seq, the premises are given in backwards order (c2 before c1). This matches the natural flow of information in many of the situations where we'll use the rule, since the natural way to construct a Hoare-logic proof is to begin at the end of the program (with the final postcondition) and push postconditions backwards through commands until we reach the beginning.

5.4.3. Assignment🔗

The rule for assignment is the most fundamental of the Hoare logic proof rules. Here's how it works.

Consider this incomplete Hoare triple:

{{ ??? }}  X := Y  {{ X = 1 }}

We want to assign Y to X and finish in a state where X is 1. What could the precondition be?

One possibility is Y = 1, because if Y is already 1 then assigning it to X causes X to be 1. That leads to a valid Hoare triple:

{{ Y = 1 }}  X := Y  {{ X = 1 }}

It may seem as though coming up with that precondition must have taken some clever thought. But there is a mechanical way we could have done it: if we take the postcondition X = 1 and in it replace X with Y---that is, replace the left-hand side of the assignment statement with the right-hand side---we get the precondition, Y = 1.

That same idea works in more complicated cases. For example:

{{ ??? }}  X := X + Y  {{ X = 1 }}

If we replace the X in X = 1 with X + Y, we get X + Y = 1. That again leads to a valid Hoare triple:

{{ X + Y = 1 }}  X := X + Y  {{ X = 1 }}

Why does this technique work? The postcondition identifies some property P that we want to hold of the variable X being assigned. In this case, P is "equals 1". To complete the triple and make it valid, we need to identify a precondition that guarantees that property will hold of X. Such a precondition must ensure that the same property holds of whatever is being assigned to X. So, in the example, we need "equals 1" to hold of X + Y. That's exactly what the technique guarantees.

In general, the postcondition could be some arbitrary assertion Q, and the right-hand side of the assignment could be some arbitrary 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 this idea of replacing occurrences: Define Q \[X ↦ a] to mean "Q where a is substituted in place of X".

This yields the Hoare logic rule for assignment:

{{ Q [X ↦ a] }}  X := a  {{ Q }}

One way of reading this 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 will be true after running the code.

Nonetheless, it's also 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 Assertion.subst.

Intuitively, 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.

This operation is related to the idea of substituting Imp expressions for Imp variables that we saw in Equiv (subst_aexp and friends). The difference is that, here, P is an arbitrary Lean assertion, so we can't directly "edit" its text.

However, we can achieve the same effect by evaluating P in an updated state, defined as follows:

This notation allows us to write this operation as:

P [ X ↦ a ]

That is, P [X ↦ a] stands for an assertion -- let's call it P' -- that behaves 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 in more detail, 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 Lean expression

fun st =>
  (fun st' => st'[X] ≤ 5)
  (X →ₜ Aexp.eval 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 Lean expression

fun st =>
  (fun st' => st'[X] ≤ 5)
  (X →ₜ Aexp.eval st (aexp { X + 1 }) ; st),

which simplifies to

fun st =>
  (X →ₜ Aexp.eval st (aexp { X + 1 }) ; st)[X] ≤ 5

and further simplifies to

fun st =>
  (Aexp.eval st (aexp { X + 1 })) ≤ 5.

That is, P' is the assertion that X + 1 is at most 5.

We can demonstrate formally that we have captured intuitive meaning of "assertion subsitution" by proving some example logical equivalences: