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.

HIDE: SAZ  2024: I'm confused by the above discussion.  Doesn't
[Add Printing Coercion Aexp_of_nat Aexp_of_aexp assert_of_Prop]
request Rocq to _show_ those coercions?  I've removed it.

HIDE: SAZ 2024:
From what I can tell, the reason the notations expand during
the proofs is that they're writen in such a way that they
inlude type annotations [(a : Aexp)] and explicit lambdas
[(fun st => a st + b st)], neither of which is stable under
simplification.  For example:

 [(fun st =>
    (fun st => (X:Aexp) st + (Y:Aexp) st) st +
    (fun st => (Z:Aexp) st) st)]

Will print as [X + Y + Z] until simplification, at which point
we have [(fun st => st X + st Y + st Z)] but there is no notation
that covers this case.

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.

SAZ 2024 - Why do we want these functions to simplify?
Ans: If [a : aexp] then in the assertion_scope [(X →ₜ a st; st)] and
[(X →ₜ aeval st a; st)] look different but are actually identical
thanks to the coercion [Aexp_of_aexp].

NOTATION: SAZ 2024: I have tried to implement the suggestion above.

There is now a custom entry [assn] for defining the syntax of
assertions.  Like the delimiters <{ }> used for Imp programs,
we now also have {{ }} delimiters for use with Assertions.

Inside that scope, variables, arithmetic and boolean expressions,
propositions, and function arguments are interpreted in the current
state.  This replaces the need for [ap], [ap2], and explicit lifting
markers.

A raw Lean assertion can also be written directly inside {{ }}.

#check {{ st[X] = st[Y] }}

#check {{ fun st => st[X] = st[Y] }}

st✝ : State

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: