5.1.1. Notations for Assertions🔗

We'll use Lean's notation features to make assertions look as much like informal math as possible.

For example, instead of writing

fun st => st[X] = m

we'll usually write just

{{ X = m }}

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.

Here, the {{ A }} brackets delimit the scope of the assertion notation.

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:

{{ f e1 ... en }} stands for (fun st => f (e1 st) ... (en st)).

We can place a raw Lean function directly inside assertion notation:

For example: {{ fun st => ∀ x, st[x] = 0 }}

5.1.2. Example Assertions🔗

5.1.3. Printing Assertions🔗

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:

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

5.4.3. Assignment🔗

How can we complete this triple?

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

One natural possibility is:

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

The precondition is just the postcondition, but with X replaced by Y.

How about this one?

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

Replace X with X + Y:

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

This works because "equals 1" holding of X is guaranteed by the property "equals 1" holding of whatever is being assigned to X.

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.

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.

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