# WPgenWeakest Precondition Generator

Set Implicit Arguments.

From SLF Require Import WPsem.

Implicit Types f : var.

Implicit Types b : bool.

Implicit Types v : val.

Implicit Types h : heap.

Implicit Types P : Prop.

Implicit Types H : hprop.

Implicit Types Q : val→hprop.

From SLF Require Import WPsem.

Implicit Types f : var.

Implicit Types b : bool.

Implicit Types v : val.

Implicit Types h : heap.

Implicit Types P : Prop.

Implicit Types H : hprop.

Implicit Types Q : val→hprop.

# First Pass

_{1}(fun r ⇒ wp t

_{2}Q) ==> wp (trm_seq t

_{1}t

_{2}) Q.

_{2}), which the user must simplify explicitly. On the contrary, when working with wpgen, all the substitutions get automatically simplified during the initial evaluation of wpgen on the source program; the end-user sees none of these substitutions.

- how to define wpgen t as a recursive function that computes in Coq,
- how to integrate support for the frame rule in this recursive definition,
- how to carry out practical proofs using wpgen.

_{1}(fun v ⇒ wp (subst x v t

_{2}) Q) ==> wp (trm_let x t

_{1}t

_{2}) Q, the definition of wpgen is such that wpgen (trm_let x t

_{1}t

_{2}) Q is, by definition, equal to wpgen t

_{1}(fun v ⇒ wpgen (subst x v t

_{2}) Q). One special case is that of applications. We define wpgen (trm_app v

_{1}v

_{2}) as wp (trm_app v

_{1}v

_{2}), that is, we fall back onto the semantical definition of weakest precondition.

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

| trm_var x ⇒ \[False]

| trm_app v

_{1}v

_{2}⇒ wp t Q

| trm_let x t

_{1}t

_{2}⇒ wpgen t

_{1}(fun v ⇒ wpgen (subst x v t

_{2}) Q)

...

end. From there, to obtain the actual definition of wpgen, we need to refine the above definition in four steps.

_{2}) is not made to a strict subterm of trm_let x t

_{1}t

_{2}, thus Coq refuse this definition as it stands.

_{1}t

_{2}, the context E gets extended as (x,v)::E. Observe also how, when reaching a variable x, a lookup for x into the context E is performed for recovering the value that, morally, should have been substituted for x.

Fixpoint wpgen (E:ctx) (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

| trm_var x ⇒

match lookup x E with

| Some v ⇒ Q v

| None ⇒ \[False]

end

| trm_app v

_{1}v

_{2}⇒ wp (isubst E t) Q

| trm_let x t

_{1}t

_{2}⇒ wpgen E t

_{1}(fun v ⇒ wpgen ((x,v)::E) t

_{2}Q)

...

end.

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

match t with

| trm_val v ⇒ fun (Q:val→hprop) ⇒ Q v

| trm_var x ⇒ fun (Q:val→hprop) ⇒

match lookup x E with

| Some v ⇒ Q v

| None ⇒ \[False]

end

| trm_app v

_{1}v

_{2}⇒ fun (Q:val→hprop) ⇒ wp (isubst E t) Q

| trm_let x t

_{1}t

_{2}⇒ fun (Q:val→hprop) ⇒

wpgen E t

_{1}(fun v ⇒ wpgen ((x,v)::E) t

_{2}Q)

...

end.

_{1}F

_{2}be a shorthand for fun (Q:val→hprop) ⇒ F

_{1}(fun v ⇒ F

_{2}Q). Using these auxiliary definitions, the definition of wpgen rewrites as follows.

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

match t with

| trm_val v ⇒ wpgen_val v

| trm_var x ⇒ wpgen_var E x

| trm_app t

_{1}t

_{2}⇒ wp (isubst E t)

| trm_let x t

_{1}t

_{2}⇒ wpgen_let (wpgen E t

_{1}) (fun v ⇒ wpgen ((x,v)::E) t

_{2})

...

end. Each of the auxiliary definitions introduced comes with a custom notation that enables a nice display of the output of wpgen. For example, we set up the notation Let' v := F

_{1}in F

_{2}to stand for wpgen_let F

_{1}(fun v ⇒ F

_{2}). Thanks to this notation, the result of computing wpgen on a source term Let x := t

_{1}in t

_{2}(of type trm) will be a formula displayed in the form Let x := F

_{1}in F

_{2}(of type formula).

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct (match t with

| trm_val v ⇒ ...

| ...

end). Without entering the details, the predicate mkstruct is a function of type formula→formula that captures the essence of the wp-style consequence-frame structural rule. This rule, called wp_conseq_frame in the previous chapter, asserts: Q

_{1}\*+ H ===> Q

_{2}→ (wp t Q

_{1}) \* H ==> (wp t Q

_{2}).

## Definition of wpgen for Term Rules

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ ..

| trm_seq t

_{1}t

_{2}⇒ ..

| trm_let x t

_{1}t

_{2}⇒ ..

| trm_var x ⇒ ..

| trm_app t

_{1}t

_{2}⇒ ..

| trm_fun x t

_{1}⇒ ..

| trm_fix f x t

_{1}⇒ ..

| trm_if v

_{0}t

_{1}t

_{2}⇒ ..

end). Our first goal is to figure out how to fill in the dots for each of the term constructors.

wpgen t Q ==> wp t Q This entailment asserts in particular that, if we are able to establish a statement of the form H ==> wpgen t Q, then we can derive from it H ==> wp t Q. The latter is also equivalent to triple t H Q. Thus, wpgen can be viewed as a practical tool to establish triples.

### Definition of wpgen for Values

The soundness theorem for wpgen requires the entailment
wpgen (trm_val v) Q ==> wp (trm_val v) Q to hold.
To satisfy this entailment, according to the rule wp_val,
it suffices to define wpgen (trm_val v) Q as Q v.
Concretely, we fill in the first dots as follows:

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

...

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

...

### Definition of wpgen for Functions

So, likewise, we can define wpgen for functions and for
recursive functions as follows:

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_fun x t

| trm_fix f x t

...
An important observation is that we here do not attempt to
recursively compute wpgen over the body of the function.
This is something that we could do, and that we will see how
to achiever further on, yet we postpone it for now because it is
relatively technical. In practice, if the program features a
local function definition, the user may explicitly request the
computation of wpgen over the body of that function. Thus,
the fact that we do not recursively traverse functions bodies
does not harm expressiveness.

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_fun x t

_{1}⇒ Q (val_fun x t_{1})| trm_fix f x t

_{1}⇒ Q (val_fix f x t_{1})...

The intention is for wpgen to admit the same semantics as wp.
We thus expect the definition of wpgen (trm_seq t
We therefore define wpgen (trm_seq t

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_seq t

...

_{1}t_{2}) Q to have a similar shape as wp t_{1}(fun v ⇒ wp t_{2}Q)._{1}t_{2}) Q as wpgen t_{1}(fun v ⇒ wpgen t_{2}Q). The definition of wpgen thus gets refined as follows:Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_seq t

_{1}t_{2}⇒ wpgen t_{1}(fun v ⇒ wpgen t_{2}Q)...

### Definition of wpgen for Let-Bindings

Parameter wp_let : ∀ x t

wp t

_{1}t_{2}Q,wp t

_{1}(fun v ⇒ wp (subst x v t_{2}) Q) ==> wp (trm_let x t_{1}t_{2}) Q.
We fill in the dots as follows:

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_let x t

... One important observation to make at this point is that the function wpgen is no longer structurally recursive. Indeed, while the first recursive call to wpgen is invoked on t
It is technically possible to convince Coq that the function wpgen
terminates, yet with great effort. Alternatively, we can circumvent
the problem altogether by casting the function in a form that makes
it structurally recursive. Concretely, we will see further on how to
add as argument to wpgen a substitution context (written E) to
delay the computation of substitutions until the leaves of the recursion.

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_let x t

_{1}t_{2}⇒ wpgen t_{1}(fun v ⇒ wpgen (subst x v t_{2}) Q)... One important observation to make at this point is that the function wpgen is no longer structurally recursive. Indeed, while the first recursive call to wpgen is invoked on t

_{1}, which is a strict subterm of t, the second call is invoked on subst x v t_{2}, which is not a strict subterm of t.### Definition of wpgen for Variables

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_var x ⇒ \[False]

...

Lemma wp_var : ∀ x Q,

\[False] ==> wp (trm_var x) Q.

Proof using. intros. intros h Hh. destruct (hpure_inv Hh). false. Qed.

Lemma triple_var : ∀ x H Q,

False →

triple (trm_var x) H Q.

Proof using. intros. false. Qed.

Lemma triple_var' : ∀ x Q,

triple (trm_var x) \[False] Q.

Proof using. intros. rewrite <- wp_equiv. applys wp_var. Qed.

\[False] ==> wp (trm_var x) Q.

Proof using. intros. intros h Hh. destruct (hpure_inv Hh). false. Qed.

Lemma triple_var : ∀ x H Q,

False →

triple (trm_var x) H Q.

Proof using. intros. false. Qed.

Lemma triple_var' : ∀ x Q,

triple (trm_var x) \[False] Q.

Proof using. intros. rewrite <- wp_equiv. applys wp_var. Qed.

All these rules are correct, albeit totally useless.

### Definition of wpgen for Function Applications

_{1}v

_{2}.

_{1}) v

_{2}. However, if v

_{1}is an abstrat value (e.g., a Coq variable of type val), we have no reasoning rule at hand that applies.

_{1}v

_{2}) Q as wp (trm_app v

_{1}v

_{2}) Q. In other words, to define wpgen for a function application, we fall back to the semantic definition of wp. We thus extend the definition of wpgen as follows.

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_app v

_{1}v

_{2}⇒ wp (trm_app v

_{1}v

_{2}) Q

... As we carry out verification proofs in practice, when reaching an application we will face a goal of the form:

H ==> wpgen (trm_app v

_{1}v

_{2}) Q By revealing the definition of wpgen on applications, we get:

H ==> wp (trm_app v

_{1}v

_{2}) Q Then, by exploiting the equivalence with triples, we obtain:

triple (trm_app v

_{1}v

_{2}) H Q Such a proof obligation can be discharged by invoking a specification triple for the function v

_{1}.

_{1}t

_{2}where t

_{1}and t

_{2}are not both values, it is still correct to define wpgen (trm_app t

_{1}t

_{2})) as wp (trm_app t

_{1}t

_{2}). So, we need not bother checking in the definition of wpgen that the arguments of trm_app are actually values.

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_app t

_{1}t

_{2}⇒ wp t Q

...

### Definition of wpgen for Conditionals

Parameter wp_if : ∀ (b:bool) t

(if b then (wp t

_{1}t_{2}Q,(if b then (wp t

_{1}Q) else (wp t_{2}Q)) ==> wp (trm_if (val_bool b) t_{1}t_{2}) Q.
We need to define wpgen for all conditionals in A-normal form, i.e.,
all terms of the form trm_if (trm_val v
Yet, the rule wp_if only applies when the first argument of trm_if
is syntactically a boolean value b. To handle this mismatch, we
set up wpgen to pattern-match a conditional as trm_if t
This way, we delay the moment at which the argument of the conditional
needs to be shown to be a boolean value. The formal definition is:

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_if t

\∃ (b:bool), \[t

\* (if b then (wpgen t

...

_{0}) t_{1}t_{2}, where v_{0}could be a value of unknown shape. Typically, a program may feature a conditional trm_if (trm_var x) t_{1}t_{2}that, after substitution for x, becomes trm_if (trm_val v) t_{1}t_{2}, for some abstract v of type val that we might not yet know to be a boolean value._{0}t_{1}t_{2}, and then express using a Separation Logic existential quantifier that there should exist a boolean b such that t_{0}= trm_val (val_bool b).Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

...

| trm_if t

_{0}t_{1}t_{2}⇒\∃ (b:bool), \[t

_{0}= trm_val (val_bool b)]\* (if b then (wpgen t

_{1}) Q else (wpgen t_{2}) Q)...

### Summary of the Definition of wpgen for Term Rules

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

| trm_fun x t

_{1}⇒ Q (val_fun x t)

| trm_fix f x t

_{1}⇒ Q (val_fix f x t)

| trm_seq t

_{1}t

_{2}⇒ wpgen t

_{1}(fun v ⇒ wpgen t

_{2}Q)

| trm_let x t

_{1}t

_{2}⇒ wpgen t

_{1}(fun v ⇒ wpgen (subst x v t

_{2}) Q)

| trm_var x ⇒ \[False]

| trm_app v

_{1}v

_{2}⇒ wp t Q

| trm_if t

_{0}t

_{1}t

_{2}⇒

\∃ (b:bool), \[t

_{0}= trm_val (val_bool b)]

\* (if b then (wpgen t

_{1}) Q else (wpgen t

_{2}) Q)

end. As pointed out earlier, this definition is not structurally recursive and thus not accepted by Coq, due to the recursive call wpgen (subst x v t

_{2}) Q. Our next step is to fix this issue.

## Computing with wpgen

### Definition of Contexts and Operations on Them

Before we explain how to revisit the definition of wpgen using
contexts, we need to define the "iterated substitution" operation.
This operation, written isubst E t, describes the substitution
of all the bindings form E inside a term t.
The definition of iterated substitution is relatively standard:
we traverse the term recursively and, when reaching a variable,
we perform a lookup in the context E. We need to take care
to respect variable shadowing. To that end, when traversing a
binder that binds a variable x, we remove all occurrences of x
that might exist in E.
The formal definition of isubst involves two auxiliary functions:
lookup and removal on association lists.
The definition of the operation lookup x E on association lists
is standard. It returns an option on a value.

Fixpoint lookup (x:var) (E:ctx) : option val :=

match E with

| nil ⇒ None

| (y,v)::E

then Some v

else lookup x E

end.

match E with

| nil ⇒ None

| (y,v)::E

_{1}⇒ if var_eq x ythen Some v

else lookup x E

_{1}end.

The definition of the removal operation, written rem x E, is
also standard. It returns a filtered context.

Fixpoint rem (x:var) (E:ctx) : ctx :=

match E with

| nil ⇒ nil

| (y,v)::E

let E

if var_eq x y then E

end.

match E with

| nil ⇒ nil

| (y,v)::E

_{1}⇒let E

_{1}' := rem x E_{1}inif var_eq x y then E

_{1}' else (y,v)::E_{1}'end.

The definition of the operation isubst E t can then be expressed
as a recursive function over the term t. It invokes lookup x E
when reaching a variable x. It invokes rem x E when traversing
a binding on the name x.

Fixpoint isubst (E:ctx) (t:trm) : trm :=

match t with

| trm_val v ⇒

v

| trm_var x ⇒

match lookup x E with

| None ⇒ t

| Some v ⇒ v

end

| trm_fun x t

trm_fun x (isubst (rem x E) t

| trm_fix f x t

trm_fix f x (isubst (rem x (rem f E)) t

| trm_app t

trm_app (isubst E t

| trm_seq t

trm_seq (isubst E t

| trm_let x t

trm_let x (isubst E t

| trm_if t

trm_if (isubst E t

end.

match t with

| trm_val v ⇒

v

| trm_var x ⇒

match lookup x E with

| None ⇒ t

| Some v ⇒ v

end

| trm_fun x t

_{1}⇒trm_fun x (isubst (rem x E) t

_{1})| trm_fix f x t

_{1}⇒trm_fix f x (isubst (rem x (rem f E)) t

_{1})| trm_app t

_{1}t_{2}⇒trm_app (isubst E t

_{1}) (isubst E t_{2})| trm_seq t

_{1}t_{2}⇒trm_seq (isubst E t

_{1}) (isubst E t_{2})| trm_let x t

_{1}t_{2}⇒trm_let x (isubst E t

_{1}) (isubst (rem x E) t_{2})| trm_if t

_{0}t_{1}t_{2}⇒trm_if (isubst E t

_{0}) (isubst E t_{1}) (isubst E t_{2})end.

Remark: it is also possible to define the substitution by iterating
the unary substitution subst over the list of bindings from E.
However, this alternative approach yields a less efficient function
and leads to more complicated proofs.
In what follows, we present the definition of wpgen E t case by
case. Throughout these definitions, recall that wpgen E t is
interpreted as the weakest precondition of isubst E t.

### wpgen: the Let-Binding Case

_{1}t

_{2}) triggers a recursive call to wpgen ((x,v)::E) t

_{2}. The corresponding definition is:

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct (match t with

...

| trm_let x t

_{1}t

_{2}⇒ fun Q ⇒

(wpgen E t

_{1}) (fun v ⇒ wpgen ((x,v)::E) t

_{2})

...

) end.

### wpgen: the Variable Case

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct (match t with

...

| trm_var x ⇒ fun Q ⇒

match lookup x E with

| Some v ⇒ Q v

| None ⇒ \[False]

end

...

) end.

### wpgen: the Application Case

Fixpoint wpgen (t:trm) : formula :=

mkstruct (match t with

...

| trm_app v

_{1}v

_{2}⇒ wp (isubst E t)

..

### wpgen: the Function Definition Case

_{1}. Here again, the formula wpgen E t is interpreted as the weakest precondition of isubst E t.

_{1}, we obtain trm_fun x (isubst (rem x E) t

_{1}).

_{1}). The weakest precondition for that value is fun Q ⇒ Q (val_fun x (isubst (rem x E) t

_{1})).

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct (match t with

...

| trm_fun x t

_{1}⇒ fun Q ⇒ Q (val_fun x (isubst (rem x E) t

_{1}))

| trm_fix f x t

_{1}⇒ fun Q ⇒ Q (val_fix f x (isubst (rem x (rem f E)) t

_{1}))

...

) end.

At last, we arrive to a definition of wpgen that type-checks in Coq,
and that can be used to effectively compute weakest preconditions in
Separation Logic.

Fixpoint wpgen (E:ctx) (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

| trm_fun x t

| trm_fix f x t

| trm_seq t

| trm_let x t

| trm_var x ⇒

match lookup x E with

| Some v ⇒ Q v

| None ⇒ \[False]

end

| trm_app v

| trm_if t

\∃ (b:bool), \[t

\* (if b then (wpgen E t

end.

match t with

| trm_val v ⇒ Q v

| trm_fun x t

_{1}⇒ Q (val_fun x (isubst (rem x E) t_{1}))| trm_fix f x t

_{1}⇒ Q (val_fix f x (isubst (rem x (rem f E)) t_{1}))| trm_seq t

_{1}t_{2}⇒ wpgen E t_{1}(fun v ⇒ wpgen E t_{2}Q)| trm_let x t

_{1}t_{2}⇒ wpgen E t_{1}(fun v ⇒ wpgen ((x,v)::E) t_{2}Q)| trm_var x ⇒

match lookup x E with

| Some v ⇒ Q v

| None ⇒ \[False]

end

| trm_app v

_{1}v_{2}⇒ wp (isubst E t) Q| trm_if t

_{0}t_{1}t_{2}⇒\∃ (b:bool), \[t

_{0}= trm_val (val_bool b)]\* (if b then (wpgen E t

_{1}) Q else (wpgen E t_{2}) Q)end.

Compared with the presentation using the form wpgen t, the new
presentation using the form wpgen E t has the main benefits that
it is structurally recursive, thus easy to define in Coq.
Moreover, it is algorithmically more efficient in general, because
it performs substitutions lazily rather than eagerly.
Let us state the soundness theorem and its corollary for establishing
triples for functions.

The entailment above asserts in particular that if we can derive
triple t H Q by proving H ==> wpgen t Q.
A useful corrolary combines the soundness theorem with the rule
triple_app_fun, which allows establishing triples for functions.
Recall the rule triple_app_fun from Rules.

Parameter triple_app_fun : ∀ x v

v

triple (subst x v

triple (trm_app v

_{1}v_{2}t_{1}H Q,v

_{1}= val_fun x t_{1}→triple (subst x v

_{2}t_{1}) H Q →triple (trm_app v

_{1}v_{2}) H Q.
Reformulating the rule above into a rule for wpgen takes 3 steps.
First, we rewrite the premise triple (subst x v
Second, we observe that the term subst x v
Third, according to wpgen_sound, the predicate
wp (isubst ((x,v

_{2}t_{1}) H Q using wp. It becomes H ==> wp (subst x v_{2}t_{1}) Q._{2}t_{1}is equal to isubst ((x,v_{2})::nil) t_{1}. (This equality is captured by the lemma subst_eq_isubst_one proved in the bonus section of the chapter.) Thus, the heap predicate wp (subst x v_{2}t_{1}) Q is equivalent to wp (isubst ((x,v_{2})::nil) t_{1})._{2})::nil) t_{1}) is entailed by wpgen ((x,v_{2})::nil) t_{1}. Thus, we can use the latter as premise in place of the former. We thereby obtain the following lemma.
Parameter triple_app_fun_from_wpgen : ∀ v

v

H ==> wpgen ((x,v

triple (trm_app v

_{1}v_{2}x t_{1}H Q,v

_{1}= val_fun x t_{1}→H ==> wpgen ((x,v

_{2})::nil) t_{1}Q →triple (trm_app v

_{1}v_{2}) H Q.
Import ExamplePrograms.

Let us exploit triple_app_fun_from_wpgen to demonstrate the
computation of wpgen on a practical program.
Recall the function incr (defined in Rules), and its
specification, whose statement appears below.

Lemma triple_incr : ∀ (p:loc) (n:int),

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

intros. applys triple_app_fun_from_wpgen. { reflexivity. }

simpl. (* Read the goal here... *)

Abort.

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

intros. applys triple_app_fun_from_wpgen. { reflexivity. }

simpl. (* Read the goal here... *)

Abort.

The goal takes the form H ==> wpgen body Q, where H denotes
the precondition, Q the postcondition, and body the body of
the function incr.
Observe the invocations of wp on the application of primitive
operations.
Observe that the goal is nevertheless somewhat hard to relate
to the original program.
In what follows, we explain how to remedy the situation, and
set up wpgen is such a way that its output is human-readable,
moreover resembles the original source code.

## Optimizing the Readability of wpgen Output

- first, we modify the presentation of wpgen so that the fun (Q:val→hprop) ⇒ appears insides the branches of the match t with rather than around it,
- second, we introduce one auxiliary definition for each branch of the match t with,
- third, we introduce one piece of notation for each of these auxiliary definitions.

### Reability Step 1: Moving the Function below the Branches.

Fixpoint wpgen (E:ctx) (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

| trm_fun x t

_{1}⇒ Q (val_fun x (isubst (rem x E) t

_{1}))

...

end. to the equivalent form:

Fixpoint wpgen (E:ctx) (t:trm) : (val→hprop)->hprop :=

match t with

| trm_val v ⇒ fun (Q:val→hprop) ⇒ Q v

| trm_fun x t

_{1}⇒ fun (Q:val→hprop) ⇒ Q (val_fun x (isubst (rem x E) t

_{1}))

...

end.

### Readability Steps 2 and 3, Illustrated on the Case of Sequences

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

match t with

...

| trm_seq t

_{1}t

_{2}⇒ fun Q ⇒ (wpgen E t

_{1}) (fun v ⇒ wpgen E t

_{2}Q)

...

end. to the equivalent form:

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

match t with

...

| trm_seq t

_{1}t

_{2}⇒ wpgen_seq (wpgen E t

_{1}) (wpgen E t

_{2})

...

end. where wpgen_seq is defined as shown below.

Remark: above, F
With the above definitions, wgpen E (trm_seq t
Finally, we introduce a piece of notation for each case. In the case
of the sequence, we set up the notation defined next to so that any
formula of the form wpgen_seq F

_{1}and F_{2}denote the results of the recursive calls, wpgen E t_{1}and wpgen E t_{2}, respectively._{1}t_{2}) evaluates to wp_seq (wpgen E t_{1}) (wpgen E t_{2})._{1}F_{2}gets displayed as Seq F_{1}; F_{2}.
Notation "'Seq' F

((wpgen_seq F

(at level 68, right associativity,

format "'[v' 'Seq' '[' F

_{1}; F_{2}" :=((wpgen_seq F

_{1}F_{2}))(at level 68, right associativity,

format "'[v' 'Seq' '[' F

_{1}']' ';' '/' '[' F_{2}']' ']'").
Thanks to this notation, the wpgen of a sequence t

_{1}; t_{2}displays as Seq F_{1}; F_{2}where F_{1}and F_{2}denote the wpgen of t_{1}and t_{2}, respectively.### Readability Step 2: Auxiliary Definitions for other Constructs

Definition wpgen_val (v:val) : formula := fun Q ⇒

Q v.

Definition wpgen_let (F

F

Definition wpgen_if (t:trm) (F

\∃ (b:bool), \[t = trm_val (val_bool b)] \* (if b then F

Definition wpgen_fail : formula := fun Q ⇒

\[False].

Definition wpgen_var (E:ctx) (x:var) : formula :=

match lookup x E with

| None ⇒ wpgen_fail

| Some v ⇒ wpgen_val v

end.

Q v.

Definition wpgen_let (F

_{1}:formula) (F2of:val→formula) : formula := fun Q ⇒F

_{1}(fun v ⇒ F2of v Q).Definition wpgen_if (t:trm) (F

_{1}F_{2}:formula) : formula := fun Q ⇒\∃ (b:bool), \[t = trm_val (val_bool b)] \* (if b then F

_{1}Q else F_{2}Q).Definition wpgen_fail : formula := fun Q ⇒

\[False].

Definition wpgen_var (E:ctx) (x:var) : formula :=

match lookup x E with

| None ⇒ wpgen_fail

| Some v ⇒ wpgen_val v

end.

The new definition of wpgen reads as follows.

Module WpgenExec2.

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

match t with

| trm_val v ⇒ wpgen_val v

| trm_var x ⇒ wpgen_var E x

| trm_fun x t

| trm_fix f x t

| trm_app t

| trm_seq t

| trm_let x t

| trm_if t

end.

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

match t with

| trm_val v ⇒ wpgen_val v

| trm_var x ⇒ wpgen_var E x

| trm_fun x t

_{1}⇒ wpgen_val (val_fun x (isubst (rem x E) t_{1}))| trm_fix f x t

_{1}⇒ wpgen_val (val_fix f x (isubst (rem x (rem f E)) t_{1}))| trm_app t

_{1}t_{2}⇒ wp (isubst E t)| trm_seq t

_{1}t_{2}⇒ wpgen_seq (wpgen E t_{1}) (wpgen E t_{2})| trm_let x t

_{1}t_{2}⇒ wpgen_let (wpgen E t_{1}) (fun v ⇒ wpgen ((x,v)::E) t_{2})| trm_if t

_{0}t_{1}t_{2}⇒ wpgen_if (isubst E t_{0}) (wpgen E t_{1}) (wpgen E t_{2})end.

This definition is, up to unfolding of the new intermediate definitions,
totally equivalent to the previous one. We will prove the soundness
result and its corollary further on.

Parameter wpgen_sound : ∀ E t Q,

wpgen E t Q ==> wp (isubst E t) Q.

Parameter triple_app_fun_from_wpgen : ∀ v

v

H ==> wpgen ((x,v

triple (trm_app v

End WpgenExec2.

wpgen E t Q ==> wp (isubst E t) Q.

Parameter triple_app_fun_from_wpgen : ∀ v

_{1}v_{2}x t_{1}H Q,v

_{1}= val_fun x t_{1}→H ==> wpgen ((x,v

_{2})::nil) t_{1}Q →triple (trm_app v

_{1}v_{2}) H Q.End WpgenExec2.

### Readability Step 3: Notation for Auxiliary Definitions

Declare Scope wpgen_scope.

Notation "'Val' v" :=

((wpgen_val v))

(at level 69) : wpgen_scope.

Notation "'Let'' x ':=' F

((wpgen_let F

(at level 69, x ident, right associativity,

format "'[v' '[' 'Let'' x ':=' F

: wpgen_scope.

Notation "'If'' b 'Then' F

((wpgen_if b F

(at level 69) : wpgen_scope.

Notation "'Fail'" :=

((wpgen_fail))

(at level 69) : wpgen_scope.

Notation "'Val' v" :=

((wpgen_val v))

(at level 69) : wpgen_scope.

Notation "'Let'' x ':=' F

_{1}'in' F_{2}" :=((wpgen_let F

_{1}(fun x ⇒ F_{2})))(at level 69, x ident, right associativity,

format "'[v' '[' 'Let'' x ':=' F

_{1}'in' ']' '/' '[' F_{2}']' ']'"): wpgen_scope.

Notation "'If'' b 'Then' F

_{1}'Else' F_{2}" :=((wpgen_if b F

_{1}F_{2}))(at level 69) : wpgen_scope.

Notation "'Fail'" :=

((wpgen_fail))

(at level 69) : wpgen_scope.

In addition, we introduce handy notation of the result of wpgen t
where t denotes an application.

Notation "'App' f v

((wp (trm_app f v

(at level 68, f, v

_{1}" :=((wp (trm_app f v

_{1})))(at level 68, f, v

_{1}at level 0) : wpgen_scope.
Module WPgenWithNotation.

Import ExamplePrograms WpgenExec2.

Open Scope wpgen_scope.

Lemma triple_incr : ∀ (p:loc) (n:int),

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

intros. applys triple_app_fun_from_wpgen. { reflexivity. }

simpl. (* Read the goal here... It is of the form H ==> F Q,

where F vaguely looks like the code of the body of incr. *)

Abort.

Import ExamplePrograms WpgenExec2.

Open Scope wpgen_scope.

Lemma triple_incr : ∀ (p:loc) (n:int),

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

intros. applys triple_app_fun_from_wpgen. { reflexivity. }

simpl. (* Read the goal here... It is of the form H ==> F Q,

where F vaguely looks like the code of the body of incr. *)

Abort.

Up to proper tabulation, alpha-renaming, and removal of
parentheses (and dummy quotes after Let and If),
the formula F reads as:

Let n := App val_get p in

Let m := App (val_add n) 1 in

App (val_set p) m
With the introduction of intermediate definitions for wpgen and
the introduction of associated notations for each term construct,
what we achieved is that the output of wpgen is, for any input term
t, a human readable formula whose display closely resembles the
syntax source code of the term t.

Let n := App val_get p in

Let m := App (val_add n) 1 in

App (val_set p) m

## Extension of wpgen to Handle Structural Rules

- the frame rule, which asserts (wpgen t Q) \* H ==> wpgen t (Q \*+ H),
- and the rule of consequence, which asserts that Q
_{1}===> Q_{2}implies wpgen t Q_{1}==> wpgen t Q_{2}.

### Introduction of mkstruct in the Definition of wpgen

We would like wpgen to satisfy the same rule, so that we can
exploit the frame rule while reasoning about a program using
the heap predicate produced by wpgen.
With the definition of wpgen set up so far, it is possible
to prove, for any concrete term t, that the frame property
(wpgen t Q) \* H ==> wpgen t (Q \*+ H) holds.
However, establishing this result requires an induction over
the entire structure of the term t---a lot of tedious work.
Instead, we are going to tweak the definition of wpgen so as to
produce, at every step of the recursion, a special token to capture
the idea that whatever the details of the output predicate produced
by wpgen, this predicate does satisfy the frame property.
We achieve this magic by introducing a predicate called mkstruct,
and inserting it at the head of the output produced by wpgen
(and all of its recursive invocation) as follows:

Fixpoint wpgen (E:ctx) (t:trm) : (val→hprop)->hprop :=

mkstruct (

match t with

| trm_val v ⇒ wpgen_val v

...

end). The interest of the insertion of mkstruct above is that every result of a computation of wpgen t on a concrete term t is, by construction, of the form mkstruct F for some argument F.
There remains to investigate how mkstruct should be defined.

Fixpoint wpgen (E:ctx) (t:trm) : (val→hprop)->hprop :=

mkstruct (

match t with

| trm_val v ⇒ wpgen_val v

...

end). The interest of the insertion of mkstruct above is that every result of a computation of wpgen t on a concrete term t is, by construction, of the form mkstruct F for some argument F.

Let us state the properties that mkstruct should satisfy.
Because mkstruct appears between the prototype and the match
in the body of wpgen, the predicate mkstruct must have type
formula→formula.

There remains to find a suitable definition for mkstruct that enables
the frame property and the consequence property. These properties can
be stated by mimicking the rules wp_frame and wp_conseq.

Parameter mkstruct_frame : ∀ (F:formula) H Q,

(mkstruct F Q) \* H ==> mkstruct F (Q \*+ H).

Parameter mkstruct_conseq : ∀ (F:formula) Q

Q

mkstruct F Q

(mkstruct F Q) \* H ==> mkstruct F (Q \*+ H).

Parameter mkstruct_conseq : ∀ (F:formula) Q

_{1}Q_{2},Q

_{1}===> Q_{2}→mkstruct F Q

_{1}==> mkstruct F Q_{2}.
In addition, it should be possible to erase mkstruct from the head
of the output produced wpgen t when we do not need to apply any
structural rule. In other words, we need to be able to prove
H ==> mkstruct F Q by proving H ==> F Q, for any H.
This erasure property is captured by the following entailment.

Moreover, mkstruct should be monotone with respect to the formula:
if F

_{1}is stronger than F_{2}, then mkstruct F_{1}should be stronger then mkstruct F_{2}.
Parameter mkstruct_monotone : ∀ F

(∀ Q, F

mkstruct F

End MkstructProp.

_{1}F_{2}Q,(∀ Q, F

_{1}Q ==> F_{2}Q) →mkstruct F

_{1}Q ==> mkstruct F_{2}Q.End MkstructProp.

### Realization of mkstruct

Definition mkstruct (F:formula) : formula :=

fun (Q:val→hprop) ⇒ \∃ Q

fun (Q:val→hprop) ⇒ \∃ Q

_{1}H, F Q_{1}\* H \* \[Q_{1}\*+ H ===> Q].
We postpone to a bonus section the discussion of why it works and of how
one could have guessed this definition. Again, it really does not matter
the details of the definition of mkstruct. All that matters is that
mkstruct satisfies the three required properties: mkstruct_frame,
mkstruct_conseq, and mkstruct_erase. Let us establish these properties
for the definition considered. (Proof details can be skipped over.)

Lemma mkstruct_frame : ∀ F H Q,

(mkstruct F Q) \* H ==> mkstruct F (Q \*+ H).

Proof using.

intros. unfold mkstruct. xpull; intros Q' H' M. xsimpl. xchange M.

Qed.

Lemma mkstruct_conseq : ∀ F Q

Q

mkstruct F Q

Proof using.

introv WQ. unfold mkstruct. xpull; intros Q' H' M.

xsimpl. xchange M. xchange WQ.

Qed.

Lemma mkstruct_erase : ∀ F Q,

F Q ==> mkstruct F Q.

Proof using. intros. unfold mkstruct. xsimpl. xsimpl. Qed.

Lemma mkstruct_monotone : ∀ F

(∀ Q, F

mkstruct F

Proof using.

introv WF. unfolds mkstruct. xpull. intros Q' H M.

xchange WF. xsimpl Q'. applys M.

Qed.

(mkstruct F Q) \* H ==> mkstruct F (Q \*+ H).

Proof using.

intros. unfold mkstruct. xpull; intros Q' H' M. xsimpl. xchange M.

Qed.

Lemma mkstruct_conseq : ∀ F Q

_{1}Q_{2},Q

_{1}===> Q_{2}→mkstruct F Q

_{1}==> mkstruct F Q_{2}.Proof using.

introv WQ. unfold mkstruct. xpull; intros Q' H' M.

xsimpl. xchange M. xchange WQ.

Qed.

Lemma mkstruct_erase : ∀ F Q,

F Q ==> mkstruct F Q.

Proof using. intros. unfold mkstruct. xsimpl. xsimpl. Qed.

Lemma mkstruct_monotone : ∀ F

_{1}F_{2}Q,(∀ Q, F

_{1}Q ==> F_{2}Q) →mkstruct F

_{1}Q ==> mkstruct F_{2}Q.Proof using.

introv WF. unfolds mkstruct. xpull. intros Q' H M.

xchange WF. xsimpl Q'. applys M.

Qed.

An interesting property of mkstruct is it has no effect on a
formula of the form wp t. Intuitively, such a formula already
satisfies all the structural reasoning rules, hence adding
mkstruct to it does not increase its expressive power.

Lemma mkstruct_wp : ∀ t,

mkstruct (wp t) = (wp t).

Proof using.

intros. applys fun_ext_1. intros Q. applys himpl_antisym.

{ unfold mkstruct. xpull. intros H Q' M. applys wp_conseq_frame M. }

{ applys mkstruct_erase. }

Qed.

mkstruct (wp t) = (wp t).

Proof using.

intros. applys fun_ext_1. intros Q. applys himpl_antisym.

{ unfold mkstruct. xpull. intros H Q' M. applys wp_conseq_frame M. }

{ applys mkstruct_erase. }

Qed.

Another interesting property of mkstruct is its idempotence
property, that is, it is such that mkstruct (mkstruct F) = mkstruct F.
Idempotence asserts that applying the predicate mkstruct more than
once does not provide more expressiveness than applying it just once.
Intuitively, idempotence reflects in particular the fact that two nested
applications of the rule of consequence can always be combined into a
single application of that rule (due to the transitivity of entailment);
and that, similarly, two nested applications of the frame rule can always
be combined into a single application of that rule (framing on H

_{1}then framing on H_{2}is equivalent to framing on H_{1}\* H_{2}).#### Exercise: 3 stars, standard, especially useful (mkstruct_idempotent)

Complete the proof of the idempotence of mkstruct. Hint: leverage xpull and xsimpl.
Lemma mkstruct_idempotent : ∀ F,

mkstruct (mkstruct F) = mkstruct F.

Proof using.

intros. apply fun_ext_1. intros Q. applys himpl_antisym.

(* FILL IN HERE *) Admitted.

☐

mkstruct (mkstruct F) = mkstruct F.

Proof using.

intros. apply fun_ext_1. intros Q. applys himpl_antisym.

(* FILL IN HERE *) Admitted.

☐

### Definition of wpgen that Includes mkstruct

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct (match t with

| trm_val v ⇒ wpgen_val v

| trm_var x ⇒ wpgen_var E x

| trm_fun x t

| trm_fix f x t

| trm_app t

| trm_seq t

| trm_let x t

| trm_if t

end).

mkstruct (match t with

| trm_val v ⇒ wpgen_val v

| trm_var x ⇒ wpgen_var E x

| trm_fun x t

_{1}⇒ wpgen_val (val_fun x (isubst (rem x E) t_{1}))| trm_fix f x t

_{1}⇒ wpgen_val (val_fix f x (isubst (rem x (rem f E)) t_{1}))| trm_app t

_{1}t_{2}⇒ wp (isubst E t)| trm_seq t

_{1}t_{2}⇒ wpgen_seq (wpgen E t_{1}) (wpgen E t_{2})| trm_let x t

_{1}t_{2}⇒ wpgen_let (wpgen E t_{1}) (fun v ⇒ wpgen ((x,v)::E) t_{2})| trm_if t

_{0}t_{1}t_{2}⇒ wpgen_if (isubst E t_{0}) (wpgen E t_{1}) (wpgen E t_{2})end).

Again, we assert the soundness theorem and its corollary,
and we postpone the proof.

Parameter wpgen_sound : ∀ E t Q,

wpgen E t Q ==> wp (isubst E t) Q.

Parameter triple_app_fun_from_wpgen : ∀ v

v

H ==> wpgen ((x,v

triple (trm_app v

wpgen E t Q ==> wp (isubst E t) Q.

Parameter triple_app_fun_from_wpgen : ∀ v

_{1}v_{2}x t_{1}H Q,v

_{1}= val_fun x t_{1}→H ==> wpgen ((x,v

_{2})::nil) t_{1}Q →triple (trm_app v

_{1}v_{2}) H Q.### Notation for mkstruct and Test

Let us test again the readability of the output of wpgen on
a concrete example.

Module WPgenWithMkstruct.

Import ExamplePrograms.

Open Scope wpgen_scope.

Lemma triple_incr : ∀ (p:loc) (n:int),

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

intros. applys triple_app_fun_from_wpgen. { reflexivity. }

simpl.

Abort.

Import ExamplePrograms.

Open Scope wpgen_scope.

Lemma triple_incr : ∀ (p:loc) (n:int),

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

intros. applys triple_app_fun_from_wpgen. { reflexivity. }

simpl.

Abort.

Up to proper tabulation, alpha-renaming, and removal of
parentheses (and dummy quotes after Let and If),
F reads as:

`Let n := `(App val_get p) in

`Let m := `(App (val_add n) 1) in

`App (val_set p) m

`Let n := `(App val_get p) in

`Let m := `(App (val_add n) 1) in

`App (val_set p) m

## Lemmas for Handling wpgen Goals

Lemma xstruct_lemma : ∀ F H Q,

H ==> F Q →

H ==> mkstruct F Q.

Proof using. introv M. xchange M. applys mkstruct_erase. Qed.

H ==> F Q →

H ==> mkstruct F Q.

Proof using. introv M. xchange M. applys mkstruct_erase. Qed.

xval_lemma reformulates the definition of wpgen_val.
It just unfolds the definition.

xlet_lemma reformulates the definition of wpgen_let.
It just unfolds the definition.

Lemma xlet_lemma : ∀ H F

H ==> F

H ==> wpgen_let F

Proof using. introv M. xchange M. Qed.

_{1}F2of Q,H ==> F

_{1}(fun v ⇒ F2of v Q) →H ==> wpgen_let F

_{1}F2of Q.Proof using. introv M. xchange M. Qed.

Likewise, xseq_lemma reformulates wpgen_seq.

Lemma xseq_lemma : ∀ H F

H ==> F

H ==> wpgen_seq F

Proof using. introv M. xchange M. Qed.

_{1}F_{2}Q,H ==> F

_{1}(fun v ⇒ F_{2}Q) →H ==> wpgen_seq F

_{1}F_{2}Q.Proof using. introv M. xchange M. Qed.

xapp_lemma applies to goals produced by wpgen on an
application. In such cases, the proof obligation is of the form
H ==> wp t Q.
xapp_lemma reformulates the frame-consequence rule, and
states the premise of the rule using a triple, because
triples are used for stating specification lemmas.

Lemma xapp_lemma : ∀ t Q

triple t H

H ==> H

Q

H ==> wp t Q.

Proof using.

introv M WH WQ. rewrite wp_equiv. applys* triple_conseq_frame M.

Qed.

_{1}H_{1}H_{2}H Q,triple t H

_{1}Q_{1}→H ==> H

_{1}\* H_{2}→Q

_{1}\*+ H_{2}===> Q →H ==> wp t Q.

Proof using.

introv M WH WQ. rewrite wp_equiv. applys* triple_conseq_frame M.

Qed.

xwp_lemma is another name for triple_app_fun_from_wpgen.
It is used for establishing a triple for a function application.

Lemma xwp_lemma : ∀ v

v

H ==> wpgen ((x,v

triple (trm_app v

Proof using. introv M

_{1}v_{2}x t_{1}H Q,v

_{1}= val_fun x t_{1}→H ==> wpgen ((x,v

_{2})::nil) t_{1}Q →triple (trm_app v

_{1}v_{2}) H Q.Proof using. introv M

_{1}M_{2}. applys* triple_app_fun_from_wpgen. Qed.
Module ProofsWithXlemmas.

Import ExamplePrograms.

Open Scope wpgen_scope.

Lemma triple_incr : ∀ (p:loc) (n:int),

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

intros.

applys xwp_lemma. { reflexivity. }

(* Here the wpgen function computes. *)

simpl.

(* Observe how each node begin with mkstruct.

Observe how program variables are all eliminated. *)

applys xstruct_lemma.

applys xlet_lemma.

applys xstruct_lemma.

applys xapp_lemma. { apply triple_get. } { xsimpl. }

xpull; intros ? →.

applys xstruct_lemma.

applys xlet_lemma.

applys xstruct_lemma.

applys xapp_lemma. { apply triple_add. } { xsimpl. }

xpull; intros ? →.

applys xstruct_lemma.

applys xapp_lemma. { apply triple_set. } { xsimpl. }

xsimpl.

Qed.

Import ExamplePrograms.

Open Scope wpgen_scope.

Lemma triple_incr : ∀ (p:loc) (n:int),

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

intros.

applys xwp_lemma. { reflexivity. }

(* Here the wpgen function computes. *)

simpl.

(* Observe how each node begin with mkstruct.

Observe how program variables are all eliminated. *)

applys xstruct_lemma.

applys xlet_lemma.

applys xstruct_lemma.

applys xapp_lemma. { apply triple_get. } { xsimpl. }

xpull; intros ? →.

applys xstruct_lemma.

applys xlet_lemma.

applys xstruct_lemma.

applys xapp_lemma. { apply triple_add. } { xsimpl. }

xpull; intros ? →.

applys xstruct_lemma.

applys xapp_lemma. { apply triple_set. } { xsimpl. }

xsimpl.

Qed.

#### Exercise: 2 stars, standard, especially useful (triple_succ_using_incr_with_xlemmas)

Using x-lemmas, verify the proof of triple_succ_using_incr. (The proof was carried out using triples in chapter Rules.)
Lemma triple_succ_using_incr_with_xlemmas : ∀ (n:int),

triple (trm_app succ_using_incr n)

\[]

(fun v ⇒ \[v = n+1]).

Proof using. (* FILL IN HERE *) Admitted.

☐

triple (trm_app succ_using_incr n)

\[]

(fun v ⇒ \[v = n+1]).

Proof using. (* FILL IN HERE *) Admitted.

☐

## Making Proof Scripts More Concise

val, xseq and xlet invoke the corresponding x-lemmas,
after calling xstruct if a leading mkstruct is in the way.

Tactic Notation "xstruct_if_needed" :=

try match goal with ⊢ ?H ==> mkstruct ?F ?Q ⇒ xstruct end.

Tactic Notation "xval" :=

xstruct_if_needed; applys xval_lemma.

Tactic Notation "xlet" :=

xstruct_if_needed; applys xlet_lemma.

Tactic Notation "xseq" :=

xstruct_if_needed; applys xseq_lemma.

try match goal with ⊢ ?H ==> mkstruct ?F ?Q ⇒ xstruct end.

Tactic Notation "xval" :=

xstruct_if_needed; applys xval_lemma.

Tactic Notation "xlet" :=

xstruct_if_needed; applys xlet_lemma.

Tactic Notation "xseq" :=

xstruct_if_needed; applys xseq_lemma.

xapp_nosubst applys xapp_lemma, after calling xseq or xlet
if applicable. (We will subsequently define xapp as an enhanced version
of xapp_nosusbt that is able to automatically perform substitutions.

Tactic Notation "xseq_xlet_if_needed" :=

try match goal with ⊢ ?H ==> mkstruct ?F ?Q ⇒

match F with

| wpgen_seq ?F

| wpgen_let ?F

end end.

Tactic Notation "xapp_nosubst" constr(E) :=

xseq_xlet_if_needed; xstruct_if_needed;

applys xapp_lemma E; [ xsimpl | xpull ].

try match goal with ⊢ ?H ==> mkstruct ?F ?Q ⇒

match F with

| wpgen_seq ?F

_{1}?F_{2}⇒ xseq| wpgen_let ?F

_{1}?F2of ⇒ xletend end.

Tactic Notation "xapp_nosubst" constr(E) :=

xseq_xlet_if_needed; xstruct_if_needed;

applys xapp_lemma E; [ xsimpl | xpull ].

xwp applys xwp_lemma, then requests Coq to evaluate the
wpgen function. (For technical reasons, we need to explicitly
request the unfolding of wpgen_var.)

Tactic Notation "xwp" :=

intros; applys xwp_lemma;

[ reflexivity

| simpl; unfold wpgen_var; simpl ].

intros; applys xwp_lemma;

[ reflexivity

| simpl; unfold wpgen_var; simpl ].

Let us revisit the previous proof scripts using x-tactics
instead of x-lemmas. The reader may contemplate the gain
in conciseness.

Module ProofsWithXtactics.

Import ExamplePrograms.

Open Scope wpgen_scope.

Lemma triple_incr : ∀ (p:loc) (n:int),

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

xwp.

xapp_nosubst triple_get. intros ? →.

xapp_nosubst triple_add. intros ? →.

xapp_nosubst triple_set.

xsimpl.

Qed.

Import ExamplePrograms.

Open Scope wpgen_scope.

Lemma triple_incr : ∀ (p:loc) (n:int),

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

xwp.

xapp_nosubst triple_get. intros ? →.

xapp_nosubst triple_add. intros ? →.

xapp_nosubst triple_set.

xsimpl.

Qed.

#### Exercise: 2 stars, standard, especially useful (triple_succ_using_incr_with_xtactics)

Using x-tactics, verify the proof of succ_using_incr.
Lemma triple_succ_using_incr_with_xtactics : ∀ (n:int),

triple (trm_app succ_using_incr n)

\[]

(fun v ⇒ \[v = n+1]).

Proof using. (* FILL IN HERE *) Admitted.

☐

triple (trm_app succ_using_incr n)

\[]

(fun v ⇒ \[v = n+1]).

Proof using. (* FILL IN HERE *) Admitted.

☐

## Further Improvements to the xapp Tactic.

Tactic Notation "xapp_try_subst" := (* for internal use only *)

try match goal with

| ⊢ ∀ (r:val), (r = _) → _ ⇒ intros ? →

| ⊢ ∀ (r:val), ∀ x, (r = _) → _ ⇒

let y := fresh x in intros ? y ->; revert y

end.

Tactic Notation "xapp" constr(E) :=

xapp_nosubst E; xapp_try_subst.

try match goal with

| ⊢ ∀ (r:val), (r = _) → _ ⇒ intros ? →

| ⊢ ∀ (r:val), ∀ x, (r = _) → _ ⇒

let y := fresh x in intros ? y ->; revert y

end.

Tactic Notation "xapp" constr(E) :=

xapp_nosubst E; xapp_try_subst.

Explicitly providing arguments to xapp_nosubst or xapp
is very tedious. To avoid that effort, we can set up the tactics
to automatically look up for the relevant specification.
To that end, we instrument eauto to exploit a database of
already-established specification triples. This database, named
triple, can be populated using the Hint Resolve ... : triple
command, as illustrated below.

Hint Resolve triple_get triple_set triple_ref triple_free triple_add : triple.

The argument-free variants xapp_subst and xapp are implemented
by invoking eauto with triple to retrieve the relevant
specification.
The definition from Direct is slightly more powerful, in that
it is also able to pick up an induction hypothesis from the
context for instantiating the triple.
DISCLAIMER: the tactic xapp that leverages the triple database
is not able to automatically apply specifications that feature a
premise that eauto cannot solve. To exploit such specifications,
one need to provide the specification explicitly (using xapp E),
or to exploit a more complex hint mechanism (as done in CFML). (A
poor-man's workaround consists in moving all the premises inside
the precondition, however doing so harms readability.)

Tactic Notation "xapp_nosubst" :=

xseq_xlet_if_needed; xstruct_if_needed;

applys xapp_lemma; [ solve [ eauto with triple ] | xsimpl | xpull ].

Tactic Notation "xapp" :=

xapp_nosubst; xapp_try_subst.

xseq_xlet_if_needed; xstruct_if_needed;

applys xapp_lemma; [ solve [ eauto with triple ] | xsimpl | xpull ].

Tactic Notation "xapp" :=

xapp_nosubst; xapp_try_subst.

The proof script for the verification of incr using the tactic
xapps with implicit argument.

Lemma triple_incr : ∀ (p:loc) (n:int),

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

xwp. xapp. xapp. xapp. xsimpl.

Qed.

triple (trm_app incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

xwp. xapp. xapp. xapp. xsimpl.

Qed.

In order to enable automatically exploiting the specification
of triple in the verification of succ_using_incr, which
includes a function call to triple, we add it to the hint
database triple.

Hint Resolve triple_incr : triple.

#### Exercise: 2 stars, standard, especially useful (triple_succ_using_incr_with_xapps)

Using the improved x-tactics, verify the proof of succ_using_incr.
Lemma triple_succ_using_incr_with_xapps : ∀ (n:int),

triple (trm_app succ_using_incr n)

\[]

(fun v ⇒ \[v = n+1]).

Proof using. (* FILL IN HERE *) Admitted.

☐

triple (trm_app succ_using_incr n)

\[]

(fun v ⇒ \[v = n+1]).

Proof using. (* FILL IN HERE *) Admitted.

☐

## Tactics xconseq and xframe

#### Exercise: 1 star, standard, optional (xconseq_lemma)

Prove the xconseq_lemma.
Lemma xconseq_lemma : ∀ Q

H ==> mkstruct F Q

Q

H ==> mkstruct F Q

Proof using. (* FILL IN HERE *) Admitted.

☐

_{1}Q_{2}H F,H ==> mkstruct F Q

_{1}→Q

_{1}===> Q_{2}→H ==> mkstruct F Q

_{2}.Proof using. (* FILL IN HERE *) Admitted.

☐

Tactic Notation "xconseq" :=

applys xconseq_lemma.

Tactic Notation "xconseq" constr(Q) :=

applys xconseq_lemma Q.

applys xconseq_lemma.

Tactic Notation "xconseq" constr(Q) :=

applys xconseq_lemma Q.

The tactic xframe enables applying the frame rule on a formula
produced by wpgen. The syntax xframe H is used to specify
the heap predicate to keep, and the syntax xframe_out H is used
to specify the heap predicate to frame out---everything else is kept.

#### Exercise: 2 stars, standard, optional (xframe_lemma)

Prove the xframe_lemma. Exploit the properties of mkstruct; do not try to unfold the definition of mkstruct.
Lemma xframe_lemma : ∀ H

H ==> H

H

Q

H ==> mkstruct F Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

_{1}H_{2}H Q Q_{1}F,H ==> H

_{1}\* H_{2}→H

_{1}==> mkstruct F Q_{1}→Q

_{1}\*+ H_{2}===> Q →H ==> mkstruct F Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

Tactic Notation "xframe" constr(H) :=

eapply (@xframe_lemma H); [ xsimpl | | ].

Tactic Notation "xframe_out" constr(H) :=

eapply (@xframe_lemma _ H); [ xsimpl | | ].

eapply (@xframe_lemma H); [ xsimpl | | ].

Tactic Notation "xframe_out" constr(H) :=

eapply (@xframe_lemma _ H); [ xsimpl | | ].

Let's illustrate the use of xframe on an example.

Module ProofsWithStructuralXtactics.

Import ExamplePrograms.

Open Scope wpgen_scope.

Lemma triple_incr_frame : ∀ (p q:loc) (n m:int),

triple (trm_app incr p)

(p ~~> n \* q ~~> m)

(fun _ ⇒ (p ~~> (n+1)) \* (q ~~> m)).

Proof using.

xwp.

Import ExamplePrograms.

Open Scope wpgen_scope.

Lemma triple_incr_frame : ∀ (p q:loc) (n m:int),

triple (trm_app incr p)

(p ~~> n \* q ~~> m)

(fun _ ⇒ (p ~~> (n+1)) \* (q ~~> m)).

Proof using.

xwp.

Instead of calling xapp, we put aside q ~~> m and focus on p ~~> n.

Then we can work in a smaller state that mentions only p ~~> n.

xapp. xapp. xapp.

Finally we check the check that the current state augmented with
the framed predicate q ~~> m matches with the claimed postcondition.

### Introduction of the Predicate formula_sound

Parameter wpgen_sound : ∀ E t Q,

wpgen E t Q ==> wp (isubst E t) Q.

Using formula_sound, the soundness theorem for wpgen
reformulates as follows.

### Soundness for the Case of Sequences

_{1}t

_{2}) evaluates to wpgen_seq (wpgen E t

_{1}) (wpgen E t

_{2}).

Definition wpgen_seq (F

_{1}F

_{2}:formula) : formula := fun Q ⇒

F

_{1}(fun v ⇒ F

_{2}Q).

_{1}t

_{2}. The corresponding statement is:

Parameter wpgen_sound_seq : ∀ E t

formula_sound (isubst E (trm_seq t

_{1}t_{2},formula_sound (isubst E (trm_seq t

_{1}t_{2})) (wpgen E (trm_seq t_{1}t_{2})).
In that statement:
Moreover, by induction hypothesis, we will be able to assume
the soundness result to already hold for the subterms t
Thus, to establish the soundness of wpgen for sequences, we
have to prove the following result:

- wpgen E (trm_seq t
_{1}t_{2}) evaluates to wpgen_seq (wpgen E t_{1}) (wpgen E t_{2}). - isubst E (trm_seq t
_{1}t_{2}) evaluates to trm_seq (isubst E t_{1}) (isubst E t_{2}).

_{1}and t_{2}.
Parameter wpgen_sound_seq' : ∀ E t

formula_sound (isubst E t

formula_sound (isubst E t

formula_sound (trm_seq (isubst E t

(wpgen_seq (wpgen E t

_{1}t_{2},formula_sound (isubst E t

_{1}) (wpgen E t_{1}) →formula_sound (isubst E t

_{2}) (wpgen E t_{2}) →formula_sound (trm_seq (isubst E t

_{1}) (isubst E t_{2}))(wpgen_seq (wpgen E t

_{1}) (wpgen E t_{2})).
In the above statement, let us abstract isubst E t

_{1}as t_{1}' and wpgen t_{1}as F_{1}, and similarly isubst E t_{2}as t_{2}' and wpgen t_{2}as F_{2}. The statement reformulates as:
Lemma wpgen_seq_sound : ∀ t

formula_sound t

formula_sound t

formula_sound (trm_seq t

_{1}' t_{2}' F_{1}F_{2},formula_sound t

_{1}' F_{1}→formula_sound t

_{2}' F_{2}→formula_sound (trm_seq t

_{1}' t_{2}') (wpgen_seq F_{1}F_{2}).
This statement captures the essence of the correctness of
the definition of wpgen_seq. Let's prove it.

Proof using.

introv S

(* Reveal the soundness statement *)

unfolds formula_sound.

(* Consider a postcondition Q *)

intros Q.

(* Reveal wpgen_seq F

unfolds wpgen_seq.

(* By transitivity of entailment *)

applys himpl_trans.

(* Apply the soundness result for wp on sequences:

wp t

2:{ applys wp_seq. }

(* Exploit the induction hypotheses to conclude *)

{ applys himpl_trans.

{ applys S

{ applys wp_conseq. intros v. applys S

Qed.

introv S

_{1}S_{2}.(* Reveal the soundness statement *)

unfolds formula_sound.

(* Consider a postcondition Q *)

intros Q.

(* Reveal wpgen_seq F

_{1}F_{2}, which is defined as F_{1}(fun v ⇒ F_{2}Q). *)unfolds wpgen_seq.

(* By transitivity of entailment *)

applys himpl_trans.

(* Apply the soundness result for wp on sequences:

wp t

_{1}(fun v ⇒ wp t_{2}Q) ==> wp (trm_seq t_{1}t_{2}) Q. *)2:{ applys wp_seq. }

(* Exploit the induction hypotheses to conclude *)

{ applys himpl_trans.

{ applys S

_{1}. }{ applys wp_conseq. intros v. applys S

_{2}. } }Qed.

### Soundness of wpgen for the Other Term Constructs

Lemma wpgen_val_sound : ∀ v,

formula_sound (trm_val v) (wpgen_val v).

Proof using. intros. intros Q. unfolds wpgen_val. applys wp_val. Qed.

Lemma wpgen_fun_val_sound : ∀ x t,

formula_sound (trm_fun x t) (wpgen_val (val_fun x t)).

Proof using. intros. intros Q. unfolds wpgen_val. applys wp_fun. Qed.

Lemma wpgen_fix_val_sound : ∀ f x t,

formula_sound (trm_fix f x t) (wpgen_val (val_fix f x t)).

Proof using. intros. intros Q. unfolds wpgen_val. applys wp_fix. Qed.

Lemma wpgen_let_sound : ∀ F

formula_sound t

(∀ v, formula_sound (subst x v t

formula_sound (trm_let x t

Proof using.

introv S

applys himpl_trans S

Qed.

Lemma wpgen_if_sound : ∀ F

formula_sound t

formula_sound t

formula_sound (trm_if t

Proof using.

introv S

applys himpl_trans wp_if. case_if. { applys S

Qed.

formula_sound (trm_val v) (wpgen_val v).

Proof using. intros. intros Q. unfolds wpgen_val. applys wp_val. Qed.

Lemma wpgen_fun_val_sound : ∀ x t,

formula_sound (trm_fun x t) (wpgen_val (val_fun x t)).

Proof using. intros. intros Q. unfolds wpgen_val. applys wp_fun. Qed.

Lemma wpgen_fix_val_sound : ∀ f x t,

formula_sound (trm_fix f x t) (wpgen_val (val_fix f x t)).

Proof using. intros. intros Q. unfolds wpgen_val. applys wp_fix. Qed.

Lemma wpgen_let_sound : ∀ F

_{1}F2of x t_{1}t_{2},formula_sound t

_{1}F_{1}→(∀ v, formula_sound (subst x v t

_{2}) (F2of v)) →formula_sound (trm_let x t

_{1}t_{2}) (wpgen_let F_{1}F2of).Proof using.

introv S

_{1}S_{2}. intros Q. unfolds wpgen_let. applys himpl_trans wp_let.applys himpl_trans S

_{1}. applys wp_conseq. intros v. applys S_{2}.Qed.

Lemma wpgen_if_sound : ∀ F

_{1}F_{2}t_{0}t_{1}t_{2},formula_sound t

_{1}F_{1}→formula_sound t

_{2}F_{2}→formula_sound (trm_if t

_{0}t_{1}t_{2}) (wpgen_if t_{0}F_{1}F_{2}).Proof using.

introv S

_{1}S_{2}. intros Q. unfold wpgen_if. xpull. intros b →.applys himpl_trans wp_if. case_if. { applys S

_{1}. } { applys S_{2}. }Qed.

The formula wpgen_fail is a sound formula not just for a variable
trm_var x, but in fact for any term t. Indeed, the entailment
\[False] ==> wp t Q is always true. Hence the general statement
for wpgen_fail that appears next.

Lemma wpgen_fail_sound : ∀ t,

formula_sound t wpgen_fail.

Proof using. intros. intros Q. unfold wpgen_fail. xpull. Qed.

formula_sound t wpgen_fail.

Proof using. intros. intros Q. unfold wpgen_fail. xpull. Qed.

The formula wp t is a sound formula for a term t, not just when
t is an application, but for any term t. Hence the general
statement for wp that appears next.

Lemma wp_sound : ∀ t,

formula_sound t (wp t).

Proof using. intros. intros Q. applys himpl_refl. Qed.

formula_sound t (wp t).

Proof using. intros. intros Q. applys himpl_refl. Qed.

### Soundness of mkstruct

Lemma mkstruct_sound : ∀ t F,

formula_sound t F →

formula_sound t (mkstruct F).

Proof using.

introv M. unfolds formula_sound. intros Q.

rewrite <- mkstruct_wp. applys mkstruct_monotone. applys M.

Qed.

formula_sound t F →

formula_sound t (mkstruct F).

Proof using.

introv M. unfolds formula_sound. intros Q.

rewrite <- mkstruct_wp. applys mkstruct_monotone. applys M.

Qed.

Another, lower-level proof for the same result reveals the definition
of mkstruct and exploits the consequence-frame rule for wp.

Lemma mkstruct_sound' : ∀ t F,

formula_sound t F →

formula_sound t (mkstruct F).

Proof using.

introv M. unfolds formula_sound.

(* Consider a postcondition Q *)

intros Q.

(* Reveal the definition of mkstruct *)

unfolds mkstruct.

(* Extract the Q' quantified in the definition of mkstruct *)

xsimpl; intros Q' H N.

(* Instantiate the assumption on F with that Q', and exploit it. *)

lets M': M Q'. xchange M'.

(* Conclude using the structural rules for wp. *)

applys wp_conseq_frame. applys N.

Qed.

formula_sound t F →

formula_sound t (mkstruct F).

Proof using.

introv M. unfolds formula_sound.

(* Consider a postcondition Q *)

intros Q.

(* Reveal the definition of mkstruct *)

unfolds mkstruct.

(* Extract the Q' quantified in the definition of mkstruct *)

xsimpl; intros Q' H N.

(* Instantiate the assumption on F with that Q', and exploit it. *)

lets M': M Q'. xchange M'.

(* Conclude using the structural rules for wp. *)

applys wp_conseq_frame. applys N.

Qed.

### Lemmas Capturing Properties of Iterated Substitutions

The second property asserts that the substitution for a context
(x,v)::E is the same as the substitution for the context rem x E
followed with the substitution of x by v using the basic
substitution function subst. This second property is needed to
handle the case of let-bindings.

The proofs for these two lemmas is technical and of limited interest.
They can be found in appendix near the end of this chapter.

### Main Induction for the Soundness Proof of wpgen

- first, invoke the lemma mkstruct_sound to justify soundness of the leading mkstruct produced by wpgen,
- second, invoke the the soundness lemma specific to that term construct, e.g. wpgen_seq_sound for sequences.

Lemma wpgen_sound_induct : ∀ E t,

formula_sound (isubst E t) (wpgen E t).

Proof using.

intros. gen E. induction t; intros; simpl;

applys mkstruct_sound.

{ applys wpgen_val_sound. }

{ rename v into x. unfold wpgen_var. case_eq (lookup x E).

{ intros v EQ. applys wpgen_val_sound. }

{ intros N. applys wpgen_fail_sound. } }

{ applys wpgen_fun_val_sound. }

{ applys wpgen_fix_val_sound. }

{ applys wp_sound. }

{ applys wpgen_seq_sound. { applys IHt1. } { applys IHt2. } }

{ rename v into x. applys wpgen_let_sound.

{ applys IHt1. }

{ intros v. rewrite <- isubst_rem. applys IHt2. } }

{ applys wpgen_if_sound. { applys IHt2. } { applys IHt3. } }

Qed.

formula_sound (isubst E t) (wpgen E t).

Proof using.

intros. gen E. induction t; intros; simpl;

applys mkstruct_sound.

{ applys wpgen_val_sound. }

{ rename v into x. unfold wpgen_var. case_eq (lookup x E).

{ intros v EQ. applys wpgen_val_sound. }

{ intros N. applys wpgen_fail_sound. } }

{ applys wpgen_fun_val_sound. }

{ applys wpgen_fix_val_sound. }

{ applys wp_sound. }

{ applys wpgen_seq_sound. { applys IHt1. } { applys IHt2. } }

{ rename v into x. applys wpgen_let_sound.

{ applys IHt1. }

{ intros v. rewrite <- isubst_rem. applys IHt2. } }

{ applys wpgen_if_sound. { applys IHt2. } { applys IHt3. } }

Qed.

### Statement of Soundness of wpgen for Closed Terms

Lemma wpgen_sound : ∀ t Q,

wpgen nil t Q ==> wp t Q.

Proof using.

introv M. lets N: (wpgen_sound nil t). rewrite isubst_nil in N. applys* N.

Qed.

wpgen nil t Q ==> wp t Q.

Proof using.

introv M. lets N: (wpgen_sound nil t). rewrite isubst_nil in N. applys* N.

Qed.

A corollary can be derived for deriving a triple of the
form triple t H Q from wpgen nil t.

Lemma triple_of_wpgen : ∀ t H Q,

H ==> wpgen nil t Q →

triple t H Q.

Proof using.

introv M. rewrite <- wp_equiv. xchange M. applys wpgen_sound.

Qed.

H ==> wpgen nil t Q →

triple t H Q.

Proof using.

introv M. rewrite <- wp_equiv. xchange M. applys wpgen_sound.

Qed.

The lemma triple_app_fun_from_wpgen, used by the tactic xwp,
is a variant of wpgen_of_triple specialized for establishing
a triple for a function application. (Recall that, in essence,
this lemma is a reformulation of the rule triple_app_fun.)

Lemma triple_app_fun_from_wpgen : ∀ v

v

H ==> wpgen ((x,v

triple (trm_app v

Proof using.

introv M

asserts_rewrite (subst x v

{ rewrite isubst_rem. rewrite* isubst_nil. }

rewrite <- wp_equiv. xchange M

Qed.

_{1}v_{2}x t_{1}H Q,v

_{1}= val_fun x t_{1}→H ==> wpgen ((x,v

_{2})::nil) t_{1}Q →triple (trm_app v

_{1}v_{2}) H Q.Proof using.

introv M

_{1}M_{2}. applys triple_app_fun M_{1}.asserts_rewrite (subst x v

_{2}t_{1}= isubst ((x,v_{2})::nil) t_{1}).{ rewrite isubst_rem. rewrite* isubst_nil. }

rewrite <- wp_equiv. xchange M

_{2}. applys wpgen_sound_induct.Qed.

The lemma triple_app_fix_from_wpgen is a variant of the above
lemma suited for recursive functions. Note that the proof exploits a
lemma called isubst_rem_2 which is an immediate generalization of
the lemma isubst_rem. The proof of isubst_rem_2 appears near
the bottom of this file.

Lemma triple_app_fix_from_wpgen : ∀ v

v

H ==> wpgen ((f,v

triple (trm_app v

Proof using.

introv M

asserts_rewrite (subst x v

= isubst ((f,v

{ rewrite isubst_rem_2. rewrite* isubst_nil. }

rewrite <- wp_equiv. xchange M

Qed.

End WPgenSound.

_{1}v_{2}f x t_{1}H Q,v

_{1}= val_fix f x t_{1}→H ==> wpgen ((f,v

_{1})::(x,v_{2})::nil) t_{1}Q →triple (trm_app v

_{1}v_{2}) H Q.Proof using.

introv M

_{1}M_{2}. applys triple_app_fix M_{1}.asserts_rewrite (subst x v

_{2}(subst f v_{1}t_{1})= isubst ((f,v

_{1})::(x,v_{2})::nil) t_{1}).{ rewrite isubst_rem_2. rewrite* isubst_nil. }

rewrite <- wp_equiv. xchange M

_{2}. applys wpgen_sound_induct.Qed.

End WPgenSound.

How could we have possibly guessed the definition of mkstruct?
Recall that we observed, in an exercise, that the definition
of mkstruct satisfies the idempotence property:

Lemma mkstruct_idempotence : ∀ F

mkstruct (mkstruct F) = mkstruct F This idempotence property reflects in particular the fact that consecutive applications of the frame rule can be combined into into a single application of this rule, and likewise for the rule of consequence. Since it seems to make some sense for mkstruct to be idempotent, let us pretend that this property is a requirement for mkstruct.
In other words, assume that we are searching for a predicate satisfying
4 properties: mkstruct_frame, mkstruct_conseq, mkstruct_erase, and
mkstruct_idempotence.
The following reasoning steps can lead to figure out a definition of
mkstruct that satisfies these properties.
Recall the statement of mkstruct_frame and of mkstruct_conseq.

Lemma mkstruct_idempotence : ∀ F

mkstruct (mkstruct F) = mkstruct F This idempotence property reflects in particular the fact that consecutive applications of the frame rule can be combined into into a single application of this rule, and likewise for the rule of consequence. Since it seems to make some sense for mkstruct to be idempotent, let us pretend that this property is a requirement for mkstruct.

Parameter mkstruct_frame : ∀ F H Q,

(mkstruct F Q) \* H ==> mkstruct F (Q \*+ H).

Parameter mkstruct_conseq : ∀ F Q

Q

mkstruct F Q

(mkstruct F Q) \* H ==> mkstruct F (Q \*+ H).

Parameter mkstruct_conseq : ∀ F Q

_{1}Q_{2},Q

_{1}===> Q_{2}→mkstruct F Q

_{1}==> mkstruct F Q_{2}.
The two rules can be combined into a single one as follows
(similarly to the way it is done for wp_conseq_frame).

Parameter mkstruct_conseq_frame : ∀ F Q

Q

H \* (mkstruct F Q

_{1}Q_{2}H,Q

_{1}\*+ H ===> Q_{2}→H \* (mkstruct F Q

_{1}) ==> mkstruct F Q_{2}.
By the idempotence property mkstruct_idempotence,
mkstruct F should be equal to mkstruct (mkstruct F).
Let's exploit this equality for the second occurrence of mkstruct F.

Parameter mkstruct_conseq_idempotence : ∀ F Q

Q

H \* (mkstruct F Q

_{1}Q_{2}H,Q

_{1}\*+ H ===> Q_{2}→H \* (mkstruct F Q

_{1}) ==> mkstruct (mkstruct F) Q_{2}.
Now, let's replace mkstruct F with F'. Doing so results in the
statment shown below, which gives a sufficient condition for the
statement mkstruct_conseq_idempotence to hold.

Parameter mkstruct_conseq_idempotence_generalized : ∀ F' Q

Q

H \* (F' Q

_{1}Q_{2}H,Q

_{1}\*+ H ===> Q_{2}→H \* (F' Q

_{1}) ==> mkstruct F' Q_{2}.
We can reformulate the above statement as an introduction rule
by merging the hypothesis into the left-hand side of the entailment
from the conclusion. We thereby obtain an introduction lemma
for mkstruct.

Parameter mkstruct_introduction : ∀ F' Q

\∃ Q

_{2},\∃ Q

_{1}H, \[Q_{1}\*+ H ===> Q_{2}] \* H \* (F' Q_{1}) ==> mkstruct F' Q_{2}.
For this entailment to hold, because entailment is a reflexive relation,
it is sufficient to define mkstruct F' Q

_{2}, that is, the right-hand side of the entailment, as equal to the contents of the left-hand side.
Definition mkstruct (F':formula) : formula :=

fun (Q

fun (Q

_{2}:val→hprop) ⇒ \∃ Q_{1}H, \[Q_{1}\*+ H ===> Q_{2}] \* H \* (F' Q_{1}).
As we have proved earlier in this chapter, this definition indeed satisfies
the 4 desired properties: mkstruct_frame, mkstruct_conseq,
mkstruct_erase, and mkstruct_idempotence.

Recall that isubst E t denotes the multi-substitution
in the term t of all bindings form the association list E.
The soundness proof for wpgen and the proof of its corollary
triple_app_fun_from_wpgen rely on two key properties of
iterated substitutions, captured by the lemmas called isubst_nil
and isubst_rem, which we state and prove next.

isubst nil t = t

subst x v (isubst (rem x E) t) = isubst ((x,v)::E) t
The first lemma is straightforward by induction.

isubst nil t = t

subst x v (isubst (rem x E) t) = isubst ((x,v)::E) t

The second lemma is much more involved to prove.
We introduce the notion of "two equivalent contexts"
E
We then introduce the notion of "contexts with disjoint
domains", and argue that if E
Before we start, we describe the tactic case_var, which
helps with the case_analyses on variable equalities,
and we prove an auxiliary lemma that describes the
result of a lookup on a context from which a binding
has been removed. It is defined in file LibSepVar.v as:

Tactic Notation "case_var" :=

repeat rewrite var_eq_spec in *; repeat case_if. The tactic case_var* is a shorthand for case_var followed with automation (essentially, eauto).
On key auxiliary lemma relates subst and isubst.

_{1}and E_{2}, and argue that substitution for two equivalent contexts yields the same result._{1}and E_{2}are disjoint then isubst (E_{1}++ E_{2}) t = isubst E_{1}(isubst E_{2}t).Tactic Notation "case_var" :=

repeat rewrite var_eq_spec in *; repeat case_if. The tactic case_var* is a shorthand for case_var followed with automation (essentially, eauto).

Lemma subst_eq_isubst_one : ∀ x v t,

subst x v t = isubst ((x,v)::nil) t.

Proof using.

intros. induction t; simpl.

{ fequals. }

{ case_var*. }

{ fequals. case_var*. { rewrite* isubst_nil. } }

{ fequals. case_var; try case_var; simpl; try case_var;

try rewrite isubst_nil; auto. }

{ fequals*. }

{ fequals*. }

{ fequals*. case_var*. { rewrite* isubst_nil. } }

{ fequals*. }

Qed.

subst x v t = isubst ((x,v)::nil) t.

Proof using.

intros. induction t; simpl.

{ fequals. }

{ case_var*. }

{ fequals. case_var*. { rewrite* isubst_nil. } }

{ fequals. case_var; try case_var; simpl; try case_var;

try rewrite isubst_nil; auto. }

{ fequals*. }

{ fequals*. }

{ fequals*. case_var*. { rewrite* isubst_nil. } }

{ fequals*. }

Qed.

A lemma about the lookup in a removal.

Lemma lookup_rem : ∀ x y E,

lookup x (rem y E) = if var_eq x y then None else lookup x E.

Proof using.

intros. induction E as [|(z,v) E'].

{ simpl. case_var*. }

{ simpl. case_var*; simpl; case_var*. }

Qed.

lookup x (rem y E) = if var_eq x y then None else lookup x E.

Proof using.

intros. induction E as [|(z,v) E'].

{ simpl. case_var*. }

{ simpl. case_var*; simpl; case_var*. }

Qed.

A lemma about the removal over an append.

Lemma rem_app : ∀ x E

rem x (E

Proof using.

intros. induction E

{ case_var*. { rew_list. fequals. } }

Qed.

_{1}E_{2},rem x (E

_{1}++ E_{2}) = rem x E_{1}++ rem x E_{2}.Proof using.

intros. induction E

_{1}as [|(y,w) E_{1}']; rew_list; simpl. { auto. }{ case_var*. { rew_list. fequals. } }

Qed.

The definition of equivalent contexts.

The fact that removal preserves equivalence.

Lemma ctx_equiv_rem : ∀ x E

ctx_equiv E

ctx_equiv (rem x E

Proof using.

introv M. unfolds ctx_equiv. intros y.

do 2 rewrite lookup_rem. case_var*.

Qed.

_{1}E_{2},ctx_equiv E

_{1}E_{2}→ctx_equiv (rem x E

_{1}) (rem x E_{2}).Proof using.

introv M. unfolds ctx_equiv. intros y.

do 2 rewrite lookup_rem. case_var*.

Qed.

The fact that substitution for equivalent contexts
yields equal results.

Lemma isubst_ctx_equiv : ∀ t E

ctx_equiv E

isubst E

Proof using.

hint ctx_equiv_rem.

intros t. induction t; introv EQ; simpl; fequals*.

{ rewrite EQ. auto. }

Qed.

_{1}E_{2},ctx_equiv E

_{1}E_{2}→isubst E

_{1}t = isubst E_{2}t.Proof using.

hint ctx_equiv_rem.

intros t. induction t; introv EQ; simpl; fequals*.

{ rewrite EQ. auto. }

Qed.

The definition of disjoint contexts.

Definition ctx_disjoint E

∀ x v

_{1}E_{2}:=∀ x v

_{1}v_{2}, lookup x E_{1}= Some v_{1}→ lookup x E_{2}= Some v_{2}→ False.
Removal preserves disjointness.

Lemma ctx_disjoint_rem : ∀ x E

ctx_disjoint E

ctx_disjoint (rem x E

Proof using.

introv D. intros y v

case_var. applys* D K

Qed.

_{1}E_{2},ctx_disjoint E

_{1}E_{2}→ctx_disjoint (rem x E

_{1}) (rem x E_{2}).Proof using.

introv D. intros y v

_{1}v_{2}K_{1}K_{2}. rewrite lookup_rem in *.case_var. applys* D K

_{1}K_{2}.Qed.

Lookup in the concatenation of two disjoint contexts

Lemma lookup_app : ∀ x E

lookup x (E

| None ⇒ lookup x E

| Some v ⇒ Some v

end.

Proof using.

introv. induction E

{ auto. }

{ case_var*. }

Qed.

_{1}E_{2},lookup x (E

_{1}++ E_{2}) = match lookup x E_{1}with| None ⇒ lookup x E

_{2}| Some v ⇒ Some v

end.

Proof using.

introv. induction E

_{1}as [|(y,w) E_{1}']; rew_list; simpl; intros.{ auto. }

{ case_var*. }

Qed.

The key induction shows that isubst distributes over
context concatenation.

Lemma isubst_app : ∀ t E

isubst (E

Proof using.

hint ctx_disjoint_rem.

intros t. induction t; simpl; intros.

{ fequals. }

{ rename v into x. rewrite* lookup_app.

case_eq (lookup x E

{ simpl. rewrite* K

{ simpl. rewrite* K

{ fequals. rewrite* rem_app. }

{ fequals. do 2 rewrite* rem_app. }

{ fequals*. }

{ fequals*. }

{ fequals*. { rewrite* rem_app. } }

{ fequals*. }

Qed.

_{1}E_{2},isubst (E

_{1}++ E_{2}) t = isubst E_{2}(isubst E_{1}t).Proof using.

hint ctx_disjoint_rem.

intros t. induction t; simpl; intros.

{ fequals. }

{ rename v into x. rewrite* lookup_app.

case_eq (lookup x E

_{1}); introv K_{1}; case_eq (lookup x E_{2}); introv K_{2}; auto.{ simpl. rewrite* K

_{2}. }{ simpl. rewrite* K

_{2}. } }{ fequals. rewrite* rem_app. }

{ fequals. do 2 rewrite* rem_app. }

{ fequals*. }

{ fequals*. }

{ fequals*. { rewrite* rem_app. } }

{ fequals*. }

Qed.

The next lemma asserts that the concatenation order is irrelevant
in a substitution if the contexts have disjoint domains.

Lemma isubst_app_swap : ∀ t E

ctx_disjoint E

isubst (E

Proof using.

introv D. applys isubst_ctx_equiv. applys* ctx_disjoint_equiv_app.

Qed.

_{1}E_{2},ctx_disjoint E

_{1}E_{2}→isubst (E

_{1}++ E_{2}) t = isubst (E_{2}++ E_{1}) t.Proof using.

introv D. applys isubst_ctx_equiv. applys* ctx_disjoint_equiv_app.

Qed.

We are ready to derive the desired property of isubst.

Lemma isubst_rem : ∀ x v E t,

isubst ((x, v)::E) t = subst x v (isubst (rem x E) t).

Proof using.

intros. rewrite subst_eq_isubst_one. rewrite <- isubst_app.

rewrite isubst_app_swap.

{ applys isubst_ctx_equiv. intros y. rew_list. simpl. case_var*.

{ rewrite lookup_rem. case_var*. } }

{ intros y v

{ subst. rewrite lookup_rem in K

Qed.

isubst ((x, v)::E) t = subst x v (isubst (rem x E) t).

Proof using.

intros. rewrite subst_eq_isubst_one. rewrite <- isubst_app.

rewrite isubst_app_swap.

{ applys isubst_ctx_equiv. intros y. rew_list. simpl. case_var*.

{ rewrite lookup_rem. case_var*. } }

{ intros y v

_{1}v_{2}K_{1}K_{2}. simpls. case_var.{ subst. rewrite lookup_rem in K

_{1}. case_var*. } }Qed.

We also prove the variant lemma which is useful for handling recursive
functions.

Lemma isubst_rem_2 : ∀ f x vf vx E t,

isubst ((f,vf)::(x,vx)::E) t

= subst x vx (subst f vf (isubst (rem x (rem f E)) t)).

Proof using.

intros. do 2 rewrite subst_eq_isubst_one. do 2 rewrite <- isubst_app.

rewrite isubst_app_swap.

{ applys isubst_ctx_equiv. intros y. rew_list. simpl.

do 2 rewrite lookup_rem. case_var*. }

{ intros y v

do 2 rewrite lookup_rem in K

Qed.

End IsubstProp.

isubst ((f,vf)::(x,vx)::E) t

= subst x vx (subst f vf (isubst (rem x (rem f E)) t)).

Proof using.

intros. do 2 rewrite subst_eq_isubst_one. do 2 rewrite <- isubst_app.

rewrite isubst_app_swap.

{ applys isubst_ctx_equiv. intros y. rew_list. simpl.

do 2 rewrite lookup_rem. case_var*. }

{ intros y v

_{1}v_{2}K_{1}K_{2}. rew_listx in *. simpls.do 2 rewrite lookup_rem in K

_{1}. case_var. }Qed.

End IsubstProp.

## Historical Notes

(* 2021-05-25 15:27 *)