# WandThe Magic Wand Operator

Set Implicit Arguments.

From SLF Require Import LibSepReference.

From SLF Require Repr.

Close Scope trm_scope.

Implicit Types h : heap.

Implicit Types P : Prop.

Implicit Types H : hprop.

Implicit Types Q : val→hprop.

From SLF Require Import LibSepReference.

From SLF Require Repr.

Close Scope trm_scope.

Implicit Types h : heap.

Implicit Types P : Prop.

Implicit Types H : hprop.

Implicit Types Q : val→hprop.

# First Pass

_{1}\−∗ H

_{2}.

- it helps reformulate the consequence-frame rule in an improved manner, through a rule called the "ramified frame rule",
- it helps stating the weakest-preconditions of a number of languages constructs in a concise manner,
- it can be useful to state specification for certain data structures.

- definition and properties of the magic wand operator,
- generalization of the magic wand to postconditions,
- statement and benefits of the ramified frame rule,
- statement of the ramified frame rule in weakest-precondition style,
- generalized definition of wpgen that recurses in local functions.

- presentation of alternative, equivalent definitions of the magic wand,
- statement and proofs of additional properties of the magic wand,
- a revised definition of mkstruct using the magic wand.
- "Texan triples", which express function specifications using the magic wand instead of using triples,
- two other operators, disjunction and non-separating conjunction, so as to complete the presentation of all Separation Logic operators.

## Intuition for the Magic Wand

_{1}\−∗ H

_{2}, to be read "H

_{1}wand H

_{2}", defines a heap predicate such that, if we extend it with H

_{1}, we obtain H

_{2}. Formally, the following entailment holds:

H

_{1}\* (H

_{1}\−∗ H

_{2}) ==> H

_{2}. Intuitively, if one can think of the star H

_{1}\* H

_{2}as the addition H

_{1}+ H

_{2}, then one can think of H

_{1}\−∗ H

_{2}as the subtraction -H

_{1}+ H

_{2}. The entailment stated above essentially captures the idea that (-H

_{1}+ H

_{2}) + H

_{1}simplifies to H

_{2}.

_{1}\−∗ H

_{2}only makes sense if H

_{1}describes a piece of heap that "can" be subtracted from H

_{2}. Otherwise, the predicate H

_{1}\−∗ H

_{2}characterizes a heap that cannot possibly exist. Informally speaking, H

_{1}must somehow be a subset of H

_{2}for the subtraction -H

_{1}+ H

_{2}to make sense.

_{1}and P

_{2}were propositions (of type Prop), then P

_{1}\* P

_{2}would mean P

_{1}∧ P

_{2}and P

_{1}\−∗ P

_{2}would mean P

_{1}→ P

_{2}. The entailment P

_{1}\* (P

_{1}\−∗ P

_{2}) ==> P

_{2}then corresponds to the tautology (P

_{1}∧ (P

_{1}→ P

_{2})) → P

_{2}.

Technically, H
The operator hwand, which implements the notation H

_{1}\−∗ H_{2}holds of a heap h if, for any heap h' disjoint from h and that satisfies H_{1}, the union of h and h' satisfies H_{2}._{1}\−∗ H_{2}, may thus be defined as follows.
Definition hwand' (H

fun h ⇒ ∀ h', Fmap.disjoint h h' → H

_{1}H_{2}:hprop) : hprop :=fun h ⇒ ∀ h', Fmap.disjoint h h' → H

_{1}h' → H_{2}(h \u h').
The definition above is perfectly fine, however it is more practical
to use an alternative, equivalent definition of hwand, expressed
in terms of previously introduced Separation Logic operators.
The alternative definition asserts that H

_{1}\−∗ H_{2}corresponds to some heap predicate, called H_{0}, such that H_{0}starred with H_{1}yields H_{2}. In other words, H_{0}is such that (H_{1}\* H_{0}) ==> H_{2}. In the definition of hwand shown below, observe how H_{0}is existentially quantified.
Definition hwand (H

\∃ H

Notation "H

_{1}H_{2}:hprop) : hprop :=\∃ H

_{0}, H_{0}\* \[ H_{1}\* H_{0}==> H_{2}].Notation "H

_{1}\−∗ H_{2}" := (hwand H_{1}H_{2}) (at level 43, right associativity).
As we establish further in this file, one can prove that hwand
and hwand' define the same operator.
The reason we prefer taking hwand as definition rather than hwand'
is that it enables us to establish all the properties of the magic wand
by exploiting the tactic xsimpl, conducting all the reasoning at the
level of hprop rather than having to work with explicit heaps of type
heap.

## Characteristic Property of the Magic Wand

_{1}\−∗ H

_{2}satisfies the following equivalence. Informally speaking, think of H

_{0}= -H

_{1}+H

_{2}and H

_{1}+H

_{0}= H

_{2}being equivalent.

Lemma hwand_equiv : ∀ H

(H

Proof using.

unfold hwand. iff M.

{ xchange M. intros H N. xchange N. }

{ xsimpl H

Qed.

_{0}H_{1}H_{2},(H

_{0}==> H_{1}\−∗ H_{2}) ↔ (H_{1}\* H_{0}==> H_{2}).Proof using.

unfold hwand. iff M.

{ xchange M. intros H N. xchange N. }

{ xsimpl H

_{0}. xchange M. }Qed.

It turns out that the magic wand operator is uniquely defined by the
equivalence (H
The right-to-left direction of the equivalence is an introduction rule:
it tells what needs to be proved for constructing a magic wand H

_{0}==> H_{1}\−∗ H_{2}) ↔ (H_{1}\* H_{0}==> H_{2}). In other words, as we establish further on, any operator that satisfies the above equivalence for all arguments is provably equal to hwand._{1}\−∗ H_{2}from a state H_{0}. What needs to be proved to establish H_{0}==> (H_{1}\−∗ H_{2}) is that H_{0}, when starred with H_{1}, yields H_{2}.
Lemma himpl_hwand_r : ∀ H

(H

H

Proof using. introv M. applys hwand_equiv. applys M. Qed.

_{0}H_{1}H_{2},(H

_{1}\* H_{0}) ==> H_{2}→H

_{0}==> (H_{1}\−∗ H_{2}).Proof using. introv M. applys hwand_equiv. applys M. Qed.

The left-to-right direction of the equivalence is an elimination rule:
it tells what can be deduced from an entailment H

_{0}==> (H_{1}\−∗ H_{2}). What can be deduced from this entailment is that if H_{0}is starred with H_{1}, then H_{2}can be recovered.
Lemma himpl_hwand_r_inv : ∀ H

H

(H

Proof using. introv M. applys hwand_equiv. applys M. Qed.

_{0}H_{1}H_{2},H

_{0}==> (H_{1}\−∗ H_{2}) →(H

_{1}\* H_{0}) ==> H_{2}.Proof using. introv M. applys hwand_equiv. applys M. Qed.

This elimination rule can be equivalently reformulated in the following
form, which makes clearer that H

_{1}\−∗ H_{2}, when starred with H_{1}, yields H_{2}.
Lemma hwand_cancel : ∀ H

H

Proof using. intros. applys himpl_hwand_r_inv. applys himpl_refl. Qed.

Arguments hwand_cancel : clear implicits.

_{1}H_{2},H

_{1}\* (H_{1}\−∗ H_{2}) ==> H_{2}.Proof using. intros. applys himpl_hwand_r_inv. applys himpl_refl. Qed.

Arguments hwand_cancel : clear implicits.

#### Exercise: 3 stars, standard, especially useful (hwand_inv)

Prove the following inversion lemma for hwand. This lemma essentially captures the fact that hwand entails its alternative definition hwand'.
Lemma hwand_inv : ∀ h

(H

H

Fmap.disjoint h

H

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

☐

_{1}h_{2}H_{1}H_{2},(H

_{1}\−∗ H_{2}) h_{2}→H

_{1}h_{1}→Fmap.disjoint h

_{1}h_{2}→H

_{2}(h_{1}\u h_{2}).Proof using. (* FILL IN HERE *) Admitted.

☐

## Magic Wand for Postconditions

_{1}\−−∗ Q

_{2}, of type hprop. Note that the magic wand between two postconditions produces a heap predicate, and not a postcondition.

_{0}such that H

_{0}starred with Q

_{1}yields Q

_{2}.

Definition qwand (Q

\∃ H

Notation "Q

_{1}Q_{2}:val→hprop) : hprop :=\∃ H

_{0}, H_{0}\* \[ Q_{1}\*+ H_{0}===> Q_{2}].Notation "Q

_{1}\−−∗ Q_{2}" := (qwand Q_{1}Q_{2}) (at level 43).
The operator qwand satisfies essentially the same properties as hwand.
Let us begin with the associated equivalence rule, which captures both
the introduction and the elimination rule.

Lemma qwand_equiv : ∀ H Q

H ==> (Q

Proof using.

unfold qwand. iff M.

{ intros v. xchange M. intros H

{ xsimpl H. xchange M. }

Qed.

_{1}Q_{2},H ==> (Q

_{1}\−−∗ Q_{2}) ↔ (Q_{1}\*+ H) ===> Q_{2}.Proof using.

unfold qwand. iff M.

{ intros v. xchange M. intros H

_{4}N. xchange N. }{ xsimpl H. xchange M. }

Qed.

The cancellation rule follows.

Lemma qwand_cancel : ∀ Q

Q

Proof using. intros. rewrite <- qwand_equiv. applys qimpl_refl. Qed.

_{1}Q_{2},Q

_{1}\*+ (Q_{1}\−−∗ Q_{2}) ===> Q_{2}.Proof using. intros. rewrite <- qwand_equiv. applys qimpl_refl. Qed.

An interesting property of qwand is the fact that we can specialize
Q

_{1}\−−∗ Q_{2}to (Q_{1}v) \−∗ (Q_{2}v), for any value v.
Lemma qwand_specialize : ∀ (v:val) (Q

(Q

Proof using.

intros. unfold qwand, hwand. xpull. intros H

xsimpl H

Qed.

_{1}Q_{2}:val→hprop),(Q

_{1}\−−∗ Q_{2}) ==> (Q_{1}v \−∗ Q_{2}v).Proof using.

intros. unfold qwand, hwand. xpull. intros H

_{0}M.xsimpl H

_{0}. xchange M.Qed.

## Frame Expressed with hwand: the Ramified Frame Rule

Parameter triple_conseq_frame : ∀ H

triple t H

H ==> H

Q

triple t H Q.

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

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

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

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

This rule suffers from a practical issue, which we illustrate in
details on a concrete example further on. For now, let us just
attempt to describe the issue at a high-level.
In short, the problem stems from the fact that we need to instantiate
H
The "ramified frame rule" exploits the magic wand operator to circumvent
the problem, by merging the two premises H ==> H
This replacement premise is H ==> H
This merging of the two entailments leads us to the statement of the
"ramified frame rule" shown below.

_{2}for applying the rule. Providing H_{2}by hand is not practical, thus we need to infer it. The value of H_{2}can be computed as the subtraction of H minus H_{1}. The resulting value may then exploited in the last premise for constructing Q_{1}\*+ H_{2}. This transfer of information via H_{2}from one subgoal to another can be obtained by introducing an "evar" (Coq unification variable) for H_{2}. However this approach does not work well in the cases where H contains existential quantifiers. Indeed, such existential quantifiers are typically first extracted out of the entailment H ==> H_{1}\* H_{2}by the tactic xsimpl. However, these existentially quantified variables are not in the scope of H_{2}, hence the instantiation of the evar associated with H_{2}typically fails._{1}\* H_{2}and Q_{1}\*+ H_{2}===> Q into a single premise that no longer mentions H_{2}._{1}\* (Q_{1}\−−∗ Q). To understand where it comes from, observe first that the second premise Q_{1}\*+ H_{2}===> Q is equivalent to H_{2}==> (Q_{1}\−−∗ Q). By replacing H_{2}with Q_{1}\−−∗ Q inside the first premise H ==> H_{1}\* H_{2}, we obtain the new premise H ==> H_{1}\* (Q_{1}\−−∗ Q).
Lemma triple_ramified_frame : ∀ H

triple t H

H ==> H

triple t H Q.

Proof using.

introv M W. applys triple_conseq_frame (Q

{ applys W. } { applys qwand_cancel. }

Qed.

_{1}Q_{1}t H Q,triple t H

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

_{1}\* (Q_{1}\−−∗ Q) →triple t H Q.

Proof using.

introv M W. applys triple_conseq_frame (Q

_{1}\−−∗ Q) M.{ applys W. } { applys qwand_cancel. }

Qed.

Reciprocally, we can prove that the ramified frame rule entails
the consequence-frame rule. Hence, the ramified frame rule has
the same expressive power as the consequence-frame rule.

Lemma triple_conseq_frame_of_ramified_frame : ∀ H

triple t H

H ==> H

Q

triple t H Q.

Proof using.

introv M WH WQ. applys triple_ramified_frame M.

xchange WH. xsimpl. rewrite qwand_equiv. applys WQ.

Qed.

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

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

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

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

Proof using.

introv M WH WQ. applys triple_ramified_frame M.

xchange WH. xsimpl. rewrite qwand_equiv. applys WQ.

Qed.

## Ramified Frame Rule in Weakest-Precondition Style

(wp t Q

_{1}) \* (Q

_{1}\−−∗ Q

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

_{2}).

Parameter wp_conseq_frame : ∀ t H Q

Q

(wp t Q

_{1}Q_{2},Q

_{1}\*+ H ===> Q_{2}→(wp t Q

_{1}) \* H ==> (wp t Q_{2}).
Let us reformulate this rule using a magic wand. The premise
Q

_{1}\*+ H ===> Q_{2}can be rewritten as H ==> (Q_{1}\−−∗ Q_{2}). By replacing H with Q_{1}\−−∗ Q_{2}in the conclusion of wp_conseq_frame, we obtain the ramified rule for wp.
Lemma wp_ramified : ∀ t Q

(wp t Q

Proof using. intros. applys wp_conseq_frame. applys qwand_cancel. Qed.

_{1}Q_{2},(wp t Q

_{1}) \* (Q_{1}\−−∗ Q_{2}) ==> (wp t Q_{2}).Proof using. intros. applys wp_conseq_frame. applys qwand_cancel. Qed.

#### Exercise: 3 stars, standard, especially useful (wp_conseq_frame_of_wp_ramified)

Prove that wp_conseq_frame is derivable from wp_ramified. To that end, prove the statement of wp_conseq_frame by using only wp_ramified, the characteristic property of the magic wand qwand_equiv, and properties of the entailment relation.
Lemma wp_conseq_frame_of_wp_ramified : ∀ t H Q

Q

(wp t Q

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

☐

_{1}Q_{2},Q

_{1}\*+ H ===> Q_{2}→(wp t Q

_{1}) \* H ==> (wp t Q_{2}).Proof using. (* FILL IN HERE *) Admitted.

☐

Lemma wp_ramified_trans : ∀ t H Q

H ==> (wp t Q

H ==> (wp t Q

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

End WandDef.

_{1}Q_{2},H ==> (wp t Q

_{1}) \* (Q_{1}\−−∗ Q_{2}) →H ==> (wp t Q

_{2}).Proof using. introv M. xchange M. applys wp_ramified. Qed.

End WandDef.

## Automation with xsimpl for hwand Expressions

xsimpl is able to spot a magic wand that cancels out.
For example, if an iterated separating conjunction includes
both H

_{2}\−∗ H_{3}and H_{2}, then these two heap predicates can be merged, leaving just H_{3}.
Lemma xsimpl_demo_hwand_cancel : ∀ H

H

Proof using. intros. xsimpl. Abort.

_{1}H_{2}H_{3}H_{4}H_{5},H

_{1}\* (H_{2}\−∗ H_{3}) \* H_{4}\* H_{2}==> H_{5}.Proof using. intros. xsimpl. Abort.

xsimpl is able to simplify uncurried magic wands.
For example, if an iterated separating conjunction includes
(H

_{1}\* H_{2}\* H_{3}) \−∗ H_{4}and H_{2}, the two predicates can be merged, leaving (H_{1}\* H_{3}) \−∗ H_{4}.
Lemma xsimpl_demo_hwand_cancel_partial : ∀ H

((H

Proof using. intros. xsimpl. Abort.

_{1}H_{2}H_{3}H_{4}H_{5}H_{6},((H

_{1}\* H_{2}\* H_{3}) \−∗ H_{4}) \* H_{5}\* H_{2}==> H_{6}.Proof using. intros. xsimpl. Abort.

xsimpl automatically applies the introduction rule himpl_hwand_r
when the right-hand-side, after prior simplification, reduces to
just a magic wand. In the example below, H

_{1}is first cancelled out from both sides, then H_{3}is moved from the RHS to the LHS.
Lemma xsimpl_demo_himpl_hwand_r : ∀ H

H

Proof using. intros. xsimpl. Abort.

_{1}H_{2}H_{3}H_{4}H_{5},H

_{1}\* H_{2}==> H_{1}\* (H_{3}\−∗ (H_{4}\* H_{5})).Proof using. intros. xsimpl. Abort.

xsimpl can iterate a number of simplifications involving
different magic wands.

Lemma xsimpl_demo_hwand_iter : ∀ H

H

Proof using. intros. xsimpl. Qed.

_{1}H_{2}H_{3}H_{4}H_{5},H

_{1}\* H_{2}\* ((H_{1}\* H_{3}) \−∗ (H_{4}\−∗ H_{5})) \* H_{4}==> ((H_{2}\−∗ H_{3}) \−∗ H_{5}).Proof using. intros. xsimpl. Qed.

xsimpl is also able to deal with the magic wand for postconditions.
In particular, it is able to merge Q

_{1}\−−∗ Q_{2}with Q_{1}v, leaving Q_{2}v.
Lemma xsimpl_demo_qwand_cancel : ∀ v (Q

(Q

Proof using. intros. xsimpl. Abort.

_{1}Q_{2}:val→hprop) H_{1}H_{2},(Q

_{1}\−−∗ Q_{2}) \* H_{1}\* (Q_{1}v) ==> H_{2}.Proof using. intros. xsimpl. Abort.

xsimpl is able to prove entailments whose right-hand side is
a magic wand.

Lemma xsimpl_hwand_frame : ∀ H

(H

Proof using.

intros. xsimpl.

(* xsimpl first step is to turn the goal into:

(H

Qed.

End XsimplDemo.

_{1}H_{2}H_{3},(H

_{1}\−∗ H_{2}) ==> ((H_{1}\* H_{3}) \−∗ (H_{2}\* H_{3})).Proof using.

intros. xsimpl.

(* xsimpl first step is to turn the goal into:

(H

_{1}\−∗ H_{2}) \* (H_{1}\* H_{3}) ==> (H_{2}\* H_{3}). *)Qed.

End XsimplDemo.

Recall from chapter WPgen the original definition of wpgen,
that is, before numerous refactoring. It admitted the following shape.

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

match t with

| trm_val v ⇒ Q v

| trm_fun x t

| trm_fix f x t

...

end. This definition of wpgen t Q does not recurse inside the body of functions that occur in the argument t. Instead, it treats such locally defined functions just like values.
Not processing local functions does not limit expressiveness, because
it is always possible for the user to manually invoke wpgen
for each locally defined function, during the verification proof.
Nevertheless, it is much more satisfying and much more practical
to set up wpgen so that it recursively computes the weakest
precondition of all the local functions that it encounters during
its evaluation.
In what follows, we show how such a version of wpgen can be set up.
We begin with the case of non-recursive functions of the form
trm_fun x t
The new definition of wpgen will take the shape shown below, for
well-suited definitions of wpgen_fun and wpgen_fix yet to be
introduced. In the code snippet below, vx denotes a value to
which the function may be applied, and vf denotes the value
associated with the function itself, this value being used in particular
in the case of recursive calls.

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

mkstruct match t with

| trm_val v ⇒ wpgen_val v

| trm_fun x t

| trm_fix f x t

...

end.

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_{1})| trm_fix f x t

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

end. This definition of wpgen t Q does not recurse inside the body of functions that occur in the argument t. Instead, it treats such locally defined functions just like values.

_{1}, then generalize the definition to the slightly more complex case of recursive functions of the form trm_fix f x t_{1}. In both cases, the function wpgen will get recursively invoked on the body t_{1}of the function, in a context extended with the appropriate bindings.Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct match t with

| trm_val v ⇒ wpgen_val v

| trm_fun x t

_{1}⇒ wpgen_fun (fun vx ⇒ wpgen ((x,vx)::E) t_{1})| trm_fix f x t

_{1}⇒ wpgen_fix (fun vf vx ⇒ wpgen ((f,vf)::(x,vx)::E) t_{1})...

end.

### 1. Treatment of Non-Recursive Functions

_{1}) Q, expressed in terms of wpgen t

_{1}.

_{1}, which the term trm_fun x t

_{1}evaluates to. The heap predicate wpgen (trm_fun x t

_{1}) Q should assert that that the postcondition Q holds of the result value vf, i.e., that Q vf should hold.

_{1}as we were doing previously, we would like to specify that vf denotes a function whose body admits wpgen t

_{1}as weakest precondition. This information no longer exposes the syntax of the term t

_{1}, and is nevertheless sufficient for the user to reason about the behavior of the function vf.

_{1}) Q to be of the form \∀ vf, \[P vf] \−∗ Q vf for a carefully crafted predicate P that describes the behavior of the function by means of its weakest precondition. P is defined further on.

_{1}. It would be correct to replace \∀ vf, ... with let vf := val_fun x t

_{1}in ..., yet we are purposely trying to abstract away from the syntax of t

_{1}, hence the universal quantification of vf.

_{1}of the function, in such a way that the user is able to derive the specification aimed for the local function vf.

Parameter triple_app_fun_from_wpgen : ∀ vf vx x t

vf = val_fun x t

H' ==> wpgen ((x,vx)::nil) t

triple (trm_app vf vx) H' Q'.

_{1}H' Q',vf = val_fun x t

_{1}→H' ==> wpgen ((x,vx)::nil) t

_{1}Q' →triple (trm_app vf vx) H' Q'.

The lemma above enables establishing a triple for an application
trm_app vf vx with precondition H' and postcondition Q',
from the premise H' ==> wgen ((x,vx)::nil) t
It therefore makes sense, in our definition of the predicate
wpgen (trm_fun x t

∀ vx H' Q', (H' ==> wpgen ((x,vx)::nil) t

triple (trm_app vf vx) H' Q' This proposition can be slightly simplified, by using wp instead of triple, allowing to eliminate H'. We thus define P vf as:

∀ vx H', wpgen ((x,vx)::nil) t
Overall, the definition of wpgen E t is as follows. Note that
the occurence of nil is replaced with E to account for the
case of a nonempty context.

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

mkstruct match t with

...

| trm_fun x t

let P vf :=

(∀ vx H', wpgen ((x,vx)::nil) t

\∀ vf, \[P vf] \−∗ Q vf

...

end.
The actual definition of wpgen exploits an intermediate definition
called wpgen_fun, as shown below:

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

mkstruct match t with

...

| trm_fun x t

...

end. where wpgen_fun is defined as follows:

_{1}Q'._{1}) Q, which we said would take the form \∀ vf, \[P vf] \−∗ Q vf, to define P vf as:∀ vx H' Q', (H' ==> wpgen ((x,vx)::nil) t

_{1}Q') →triple (trm_app vf vx) H' Q' This proposition can be slightly simplified, by using wp instead of triple, allowing to eliminate H'. We thus define P vf as:

∀ vx H', wpgen ((x,vx)::nil) t

_{1}Q' ==> wp (trm_app vf vx) Q'Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct match t with

...

| trm_fun x t

_{1}⇒ fun Q ⇒let P vf :=

(∀ vx H', wpgen ((x,vx)::nil) t

_{1}Q' ==> wp (trm_app vf vx) Q') in\∀ vf, \[P vf] \−∗ Q vf

...

end.

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

mkstruct match t with

...

| trm_fun x t

_{1}⇒ wpgen_fun (fun vx ⇒ wpgen ((x,vx)::E) t_{1})...

end. where wpgen_fun is defined as follows:

Definition wpgen_fun (Fof:val→formula) : formula := fun Q ⇒

\∀ vf, \[∀ vx Q', Fof vx Q' ==> wp (trm_app vf vx) Q'] \−∗ Q vf.

\∀ vf, \[∀ vx Q', Fof vx Q' ==> wp (trm_app vf vx) Q'] \−∗ Q vf.

The soundness lemma for this construct follows from the wp-style
reasoning rule for applications, called wp_app_fun, introduced in
chapter WPsem. It is not needed to follow at this stage through
the details of the proof. (The proof involves lemmas about \∀
and about \−∗ that are stated and proved only further on in this
chapter.)

Lemma wpgen_fun_sound : ∀ x t

(∀ vx, formula_sound (subst x vx t

formula_sound (trm_fun x t

Proof using.

introv M. intros Q. unfolds wpgen_fun. applys himpl_hforall_l (val_fun x t

xchange hwand_hpure_l.

{ intros. applys himpl_trans_r. { applys* wp_app_fun. } { applys* M. } }

{ applys wp_fun. }

Qed.

_{1}Fof,(∀ vx, formula_sound (subst x vx t

_{1}) (Fof vx)) →formula_sound (trm_fun x t

_{1}) (wpgen_fun Fof).Proof using.

introv M. intros Q. unfolds wpgen_fun. applys himpl_hforall_l (val_fun x t

_{1}).xchange hwand_hpure_l.

{ intros. applys himpl_trans_r. { applys* wp_app_fun. } { applys* M. } }

{ applys wp_fun. }

Qed.

When we carry out the proof of soundness for the new version of wpgen
that features wpgen_fun, we obtain the following new proof obligation.
(To see it, play the proof of lemma wpgen_sound,
in file LibSepDirect.v.)

Lemma wpgen_fun_proof_obligation : ∀ E x t

(∀ E, formula_sound (isubst E t

formula_sound (trm_fun x (isubst (rem x E) t

(wpgen_fun (fun v ⇒ wpgen ((x,v)::E) t

_{1},(∀ E, formula_sound (isubst E t

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

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

_{1})).
The proof exploits the lemma wpgen_fun_sound that we just established,
as well as a substitution lemma, the same as the one used to justify the
soundness of the wpgen of a let-binding.

Proof using.

introv IH. applys wpgen_fun_sound.

{ intros vx. rewrite <- isubst_rem. applys IH. }

Qed.

introv IH. applys wpgen_fun_sound.

{ intros vx. rewrite <- isubst_rem. applys IH. }

Qed.

Like for other auxiliary functions associated with wpgen, we introduce
a custom notation for wpgen_fun. Here, we let Fun x := F stand for
wpgen_fun (fun x ⇒ F).

Notation "'Fun' x ':=' F

((wpgen_fun (fun x ⇒ F

(at level 69, x name, right associativity,

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

_{1}" :=((wpgen_fun (fun x ⇒ F

_{1})))(at level 69, x name, right associativity,

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

_{1}']' ']'").### 2. Treatment of Recursive Functions

_{1}is almost the same as for a non-recursive function, the main difference being that we need to add a binding in the context to associate the name f of the recursive function with the value vf that corresponds to the recursive function.

_{1}) Q will be of the form \∀ vf, \[P vf] \−∗ Q vf.

Parameter triple_app_fix_from_wpgen : ∀ vf vx f x t

vf = val_fix f x t

H' ==> wpgen ((f,vf)::(x,vx)::nil) t

triple (trm_app vf vx) H' Q'.

_{1}H' Q',vf = val_fix f x t

_{1}→H' ==> wpgen ((f,vf)::(x,vx)::nil) t

_{1}Q' →triple (trm_app vf vx) H' Q'.

It therefore makes sense to define P vf as:

∀ vx H' Q', (H' ==> wpgen ((f,vf)::(x,vx)::nil) t

triple (trm_app vf vx) H' Q' which can be rewritten as:

∀ vx H', wpgen ((f,vf)::(x,vx)::nil) t

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

mkstruct match t with

| ..

| trm_fix f x t

| ..

end with the following definition for wpgen_fix.

∀ vx H' Q', (H' ==> wpgen ((f,vf)::(x,vx)::nil) t

_{1}Q') →triple (trm_app vf vx) H' Q' which can be rewritten as:

∀ vx H', wpgen ((f,vf)::(x,vx)::nil) t

_{1}Q' ==> wp (trm_app vf vx) Q' We thus consider:Fixpoint wpgen (E:ctx) (t:trm) : formula :=

mkstruct match t with

| ..

| trm_fix f x t

_{1}⇒ wpgen_fix (fun vf v ⇒ wpgen ((f,vf)::(x,v)::E) t_{1})| ..

end with the following definition for wpgen_fix.

Definition wpgen_fix (Fof:val→val→formula) : formula := fun Q ⇒

\∀ vf, \[∀ vx Q', Fof vf vx Q' ==> wp (trm_app vf vx) Q'] \−∗ Q vf.

\∀ vf, \[∀ vx Q', Fof vf vx Q' ==> wp (trm_app vf vx) Q'] \−∗ Q vf.

The soundness lemma for wpgen_fix is very similar to that of wpgen_fun.
Again, it is not needed to follow through the details of this proof.

Lemma wpgen_fix_sound : ∀ f x t

(∀ vf vx, formula_sound (subst x vx (subst f vf t

formula_sound (trm_fix f x t

Proof using.

introv M. intros Q. unfolds wpgen_fix.

applys himpl_hforall_l (val_fix f x t

{ intros. applys himpl_trans_r. { applys* wp_app_fix. } { applys* M. } }

{ applys wp_fix. }

Qed.

_{1}Fof,(∀ vf vx, formula_sound (subst x vx (subst f vf t

_{1})) (Fof vf vx)) →formula_sound (trm_fix f x t

_{1}) (wpgen_fix Fof).Proof using.

introv M. intros Q. unfolds wpgen_fix.

applys himpl_hforall_l (val_fix f x t

_{1}). xchange hwand_hpure_l.{ intros. applys himpl_trans_r. { applys* wp_app_fix. } { applys* M. } }

{ applys wp_fix. }

Qed.

The proof of soundness of wpgen involves the following proof obligation
to handle the case of recursive functions. (To see it, play the proof of
lemma wpgen_sound, in file LibSepDirect.v.)

Lemma wpgen_fix_proof_obligation : ∀ E f x t

(∀ E, formula_sound (isubst E t

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

(wpgen_fix (fun vf vx ⇒ wpgen ((f,vf)::(x,vx)::E) t

Proof using.

introv IH. applys wpgen_fix_sound.

{ intros vf vx. rewrite <- isubst_rem_2. applys IH. }

Qed.

_{1},(∀ E, formula_sound (isubst E t

_{1}) (wpgen E t_{1})) →formula_sound (trm_fix f x (isubst (rem x (rem f E)) t

_{1}))(wpgen_fix (fun vf vx ⇒ wpgen ((f,vf)::(x,vx)::E) t

_{1})).Proof using.

introv IH. applys wpgen_fix_sound.

{ intros vf vx. rewrite <- isubst_rem_2. applys IH. }

Qed.

Here again, we introduce a piece of notation for wpgen_fix. We let
Fix f x := F stand for wpgen_fix (fun f x ⇒ F).

Notation "'Fix' f x ':=' F

((wpgen_fix (fun f x ⇒ F

(at level 69, f name, x name, right associativity,

format "'[v' '[' 'Fix' f x ':=' F

_{1}" :=((wpgen_fix (fun f x ⇒ F

_{1})))(at level 69, f name, x name, right associativity,

format "'[v' '[' 'Fix' f x ':=' F

_{1}']' ']'").
Remark: similarly to xfun, one could devise a xfix tactic.
We omit the details.

### 3. Final Definition of wpgen, with Processing a Local Functions

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_if t

| trm_seq t

| trm_let x t

| trm_app 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_fun (fun v ⇒ wpgen ((x,v)::E) t_{1})| trm_fix f x t

_{1}⇒ wpgen_fix (fun vf v ⇒ wpgen ((f,vf)::(x,v)::E) t_{1})| trm_if t

_{0}t_{1}t_{2}⇒ wpgen_if t_{0}(wpgen E t_{1}) (wpgen E t_{2})| 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_app t

_{1}t_{2}⇒ wp (isubst E t)end.

The full soundness proof appears in file LibSepDirect, lemma
wpgen_sound.

### 4. Tactic to Reason About Functions

Lemma xfun_spec_lemma : ∀ (S:val→Prop) H Q Fof,

(∀ vf,

(∀ vx H' Q', (H' ==> Fof vx Q') → triple (trm_app vf vx) H' Q') →

S vf) →

(∀ vf, S vf → (H ==> Q vf)) →

H ==> wpgen_fun Fof Q.

Proof using.

introv M

applys M

Qed.

Tactic Notation "xfun" constr(S) :=

xseq_xlet_if_needed; xstruct_if_needed; applys xfun_spec_lemma S.

(∀ vf,

(∀ vx H' Q', (H' ==> Fof vx Q') → triple (trm_app vf vx) H' Q') →

S vf) →

(∀ vf, S vf → (H ==> Q vf)) →

H ==> wpgen_fun Fof Q.

Proof using.

introv M

_{1}M_{2}. unfold wpgen_fun. xsimpl. intros vf N.applys M

_{2}. applys M_{1}. introv K. rewrite <- wp_equiv. xchange K. applys N.Qed.

Tactic Notation "xfun" constr(S) :=

xseq_xlet_if_needed; xstruct_if_needed; applys xfun_spec_lemma S.

Second, we describe the tactic xfun without argument. It applies to a goal
of the form H ==> wpgen_fun Fof Q. The tactic xfun simply makes
available an hypothesis about the local function. The user may subsequently
exploit this hypothesis for reasoning about a call to that function, just
like if the code of the function was inlined at its call site. The use of
xfun without argument is usually relevant only for local functions that
are invoked exactly once (as is often the case for functions passed to
higher-order iterators). Again, an example use case appears further on.

Lemma xfun_nospec_lemma : ∀ H Q Fof,

(∀ vf,

(∀ vx H' Q', (H' ==> Fof vx Q') → triple (trm_app vf vx) H' Q') →

(H ==> Q vf)) →

H ==> wpgen_fun Fof Q.

Proof using.

introv M. unfold wpgen_fun. xsimpl. intros vf N. applys M.

introv K. rewrite <- wp_equiv. xchange K. applys N.

Qed.

Tactic Notation "xfun" :=

xseq_xlet_if_needed; xstruct_if_needed; applys xfun_nospec_lemma.

(∀ vf,

(∀ vx H' Q', (H' ==> Fof vx Q') → triple (trm_app vf vx) H' Q') →

(H ==> Q vf)) →

H ==> wpgen_fun Fof Q.

Proof using.

introv M. unfold wpgen_fun. xsimpl. intros vf N. applys M.

introv K. rewrite <- wp_equiv. xchange K. applys N.

Qed.

Tactic Notation "xfun" :=

xseq_xlet_if_needed; xstruct_if_needed; applys xfun_nospec_lemma.

A generalization of xfun that handles recursive functions may be defined
following exactly the same pattern.
This completes our presentation of a version of wpgen that recursively
processes the local definition of non-recursive functions. An practical
example is presented next.

### 5. Example Computation of wpgen in Presence of a Local Function

Consider the following example program, which involves a local function
definition, then two successive calls to that local function.

We first illustrate a call to xfun with an explicit specification.
Here, the function f is specified as incrementing the reference p.
Observe that the body function of the function f is verified only
once. The reasoning about the two calls to the function f that appears
in the code are done with respect to the specification that we provide
as argument to xfun at the moment of the definition of f.

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

triple (trm_app myfun p)

(p ~~> n)

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

Proof using.

xwp.

xfun (fun (f:val) ⇒ ∀ (m:int),

triple (f())

(p ~~> m)

(fun _ ⇒ p ~~> (m+1))); intros f Hf.

{ intros. applys Hf. clear Hf. xapp. (* exploits triple_incr *) xsimpl. }

xapp. (* exploits Hf. *)

xapp. (* exploits Hf. *)

replace (n+1+1) with (n+2); [|math]. xsimpl.

Qed.

triple (trm_app myfun p)

(p ~~> n)

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

Proof using.

xwp.

xfun (fun (f:val) ⇒ ∀ (m:int),

triple (f())

(p ~~> m)

(fun _ ⇒ p ~~> (m+1))); intros f Hf.

{ intros. applys Hf. clear Hf. xapp. (* exploits triple_incr *) xsimpl. }

xapp. (* exploits Hf. *)

xapp. (* exploits Hf. *)

replace (n+1+1) with (n+2); [|math]. xsimpl.

Qed.

We next illustrate a call to xfun without argument. The "generic
specification" that comes as hypothesis about the local function
is a proposition that describes the behavior of the function in terms
of the weakest-precondition of its body.
When reasoning about a call to the function, one can invoke this
generic specification. The effect is equivalent to that of inlining
the code of the function at its call site.
Here, there are two calls to the function. We will thus have to exploit
twice the generic specification of f, which corresponds to its body
incr p. We will therefore have to reason twice about the increment
function.

Lemma triple_myfun' : ∀ (p:loc) (n:int),

triple (trm_app myfun p)

(p ~~> n)

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

Proof using.

xwp.

xfun; intros f Hf.

xapp. (* exploits Hf *)

xapp. (* exploits triple_incr *)

xapp. (* exploits Hf *)

xapp. (* exploits triple_incr *)

replace (n+1+1) with (n+2); [|math]. xsimpl.

Qed.

End WPgenRec.

triple (trm_app myfun p)

(p ~~> n)

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

Proof using.

xwp.

xfun; intros f Hf.

xapp. (* exploits Hf *)

xapp. (* exploits triple_incr *)

xapp. (* exploits Hf *)

xapp. (* exploits triple_incr *)

replace (n+1+1) with (n+2); [|math]. xsimpl.

Qed.

End WPgenRec.

## Benefits of the Ramified Rule over the Consequence-Frame Rule

_{2}in the rule. Let us come back to this point and describe the issue in depth on a concrete example, and show how the ramified frame rule smoothly handles that same example.

Recall the consequence-frame rule.

Parameter triple_conseq_frame : ∀ H

triple t H

H ==> H

Q

triple t H Q.

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

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

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

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

One practical caveat with this rule is that we must resolve H
This approach works in simple cases, but fails in particular in
the case where H contains an existential quantifier.
For a concrete example, consider the specification of the
function ref, which allocates a reference.

_{2}, which corresponds to the difference between H and H_{1}. In practice, providing H_{2}explicitly is extremely tedious. The alternative is to leave H_{2}as an evar, and count on the fact that the tactic xsimpl, when applied to H ==> H_{1}\* H_{2}, will correctly instantiate H_{2}.
Assume that wish to derive the following triple, which extends
both the precondition and the postcondition of the above specification
triple_ref with the heap predicate \∃ l' v', l' ~~> v'.
This predicate describes the existence of some, totally unspecified,
reference cell. It is a bit artificial but illustrates well the issue.

Lemma triple_ref_extended : ∀ (v:val),

triple (val_ref v)

(\∃ l' v', l' ~~> v')

(funloc p ⇒ p ~~> v \* \∃ l' v', l' ~~> v').

triple (val_ref v)

(\∃ l' v', l' ~~> v')

(funloc p ⇒ p ~~> v \* \∃ l' v', l' ~~> v').

Let us prove that this specification is derivable from the
original one, namely triple_ref.

Proof using.

intros. applys triple_conseq_frame.

(* observe the evar ?H

{ applys triple_ref. }

{ (* here, ?H

but xsimpl strategy is to first extract the quantifiers

from the LHS. After that, the instantiation of ?H

because the LHS contains variables that are not defined in

the scope of the evar ?H

xsimpl.

Abort.

intros. applys triple_conseq_frame.

(* observe the evar ?H

_{2}that appears in the second and third subgoals *){ applys triple_ref. }

{ (* here, ?H

_{2}should be in theory instantiated with the LHS.but xsimpl strategy is to first extract the quantifiers

from the LHS. After that, the instantiation of ?H

_{2}fails,because the LHS contains variables that are not defined in

the scope of the evar ?H

_{2}at the time it was introduced. *)xsimpl.

Abort.

Now, let us apply the ramified frame rule to carry out the same
proof, and observe how the problem does not show up.

Lemma triple_ref_extended' : ∀ (v:val),

triple (val_ref v)

(\∃ l' v', l' ~~> v')

(funloc p ⇒ p ~~> v \* \∃ l' v', l' ~~> v').

Proof using.

intros. applys triple_ramified_frame.

{ applys triple_ref. }

{ xsimpl.

(* Here again, xsimpl strategy works on the LHS, and pulls out

the existentially quantified variables. But it works here

because the remaining of the reasoning takes place in the

same subgoal, in the scope of the extended Coq context. *)

intros l' v'. rewrite qwand_equiv. xsimpl. auto. }

Qed.

End WandBenefits.

triple (val_ref v)

(\∃ l' v', l' ~~> v')

(funloc p ⇒ p ~~> v \* \∃ l' v', l' ~~> v').

Proof using.

intros. applys triple_ramified_frame.

{ applys triple_ref. }

{ xsimpl.

(* Here again, xsimpl strategy works on the LHS, and pulls out

the existentially quantified variables. But it works here

because the remaining of the reasoning takes place in the

same subgoal, in the scope of the extended Coq context. *)

intros l' v'. rewrite qwand_equiv. xsimpl. auto. }

Qed.

End WandBenefits.

We next present the most important properties of H
Thereafter, the tactic xsimpl is accessible, but in a form
that does not provide support for the magic wand.
The actual tactic would trivially solve many of these lemmas,
but using it would be cheating because the implementation of
xsimpl relies on several of these lemmas.

_{1}\−∗ H_{2}.### Structural Properties of hwand

_{1}\−∗ H

_{2}is contravariant in H

_{1}and covariant in H

_{2}, similarly to the implication operator →.

Lemma hwand_himpl : ∀ H

H

H

(H

Proof using.

introv M

xchange (hwand_cancel H

Qed.

_{1}H_{1}' H_{2}H_{2}',H

_{1}' ==> H_{1}→H

_{2}==> H_{2}' →(H

_{1}\−∗ H_{2}) ==> (H_{1}' \−∗ H_{2}').Proof using.

introv M

_{1}M_{2}. applys himpl_hwand_r. xchange M_{1}.xchange (hwand_cancel H

_{1}H_{2}). applys M_{2}.Qed.

Two predicates H

_{1}\−∗ H_{2}ans H_{2}\−∗ H_{3}may simplify to H_{1}\−∗ H_{3}. This simplification is reminiscent of the arithmetic operation (-H_{1}+ H_{2}) + (-H_{2}+ H_{3}) = (-H_{1}+ H_{3}).
Lemma hwand_trans_elim : ∀ H

(H

Proof using.

intros. applys himpl_hwand_r. xchange (hwand_cancel H

Qed.

_{1}H_{2}H_{3},(H

_{1}\−∗ H_{2}) \* (H_{2}\−∗ H_{3}) ==> (H_{1}\−∗ H_{3}).Proof using.

intros. applys himpl_hwand_r. xchange (hwand_cancel H

_{1}H_{2}).Qed.

The predicate H \−∗ H holds of the empty heap.
Intuitively, one can rewrite 0 as -H + H.

Lemma himpl_hempty_hwand_same : ∀ H,

\[] ==> (H \−∗ H).

Proof using. intros. apply himpl_hwand_r. xsimpl. Qed.

\[] ==> (H \−∗ H).

Proof using. intros. apply himpl_hwand_r. xsimpl. Qed.

### Tempting Yet False Properties for hwand

Lemma himpl_hwand_same_hempty_counterexample : ∀ p v,

let H := (\∃ H', H') in

(p ~~> v) ==> (H \−∗ H).

Proof using. intros. subst H. rewrite hwand_equiv. xsimpl. Qed.

let H := (\∃ H', H') in

(p ~~> v) ==> (H \−∗ H).

Proof using. intros. subst H. rewrite hwand_equiv. xsimpl. Qed.

In technical terms, H \−∗ H characterizes the empty heap only
in the case where H is "precise", that is, when it describes
a heap of a specific shape. In the above counterexample, H is
clearly not precise, because it is satisfied by heaps of any shape.
The notion of "preciseness" can be defined formally, yet it is
out of the scope of this course.
As another tempting yet false property of the magic wand,
consider the reciprocal entailment to the cancellation lemma,
that is, H
As counter-example, consider H

_{2}==> H_{1}\* (H_{1}\−∗ H_{2}). It does not hold in general._{2}= \[] and H_{1}= \[False]. We can prove that the empty heap does not satisfies \[False] \* (\[False] \−∗ \[]).
Lemma not_himpl_hwand_r_inv_reciprocal : ∃ H

¬ (H

Proof using.

∃ \[False] \[]. intros N. forwards K: N (Fmap.empty:heap).

applys hempty_intro. rewrite hstar_hpure_l in K. destruct K. auto.

Qed.

_{1}H_{2},¬ (H

_{2}==> H_{1}\* (H_{1}\−∗ H_{2})).Proof using.

∃ \[False] \[]. intros N. forwards K: N (Fmap.empty:heap).

applys hempty_intro. rewrite hstar_hpure_l in K. destruct K. auto.

Qed.

More generally, one has to be suspicious of any entailment
that introduces wands "out of nowhere".
The entailment hwand_trans_elim:
(H
On the contrary, the reciprocal entailment
(H

_{1}\−∗ H_{2}) \* (H_{2}\−∗ H_{3}) ==> (H_{1}\−∗ H_{3}) is correct because, intuitively, the left-hand-side captures that H_{1}≤ H_{2}and that H_{2}≤ H_{3}for some vaguely defined notion of ≤ as "being a subset of". From that, we can derive H_{1}≤ H_{3}, and justify that the right-hand-side makes sense._{1}\−∗ H_{3}) ==> (H_{1}\−∗ H_{2}) \* (H_{2}\−∗ H_{3}) is certainly false, because from H_{1}≤ H_{3}there is no way to justify H_{1}≤ H_{2}nor H_{2}≤ H_{3}.
Lemma hwand_hempty_l : ∀ H,

(\[] \−∗ H) = H.

Proof using.

intros. unfold hwand. xsimpl.

{ intros H

{ xsimpl. }

Qed.

(\[] \−∗ H) = H.

Proof using.

intros. unfold hwand. xsimpl.

{ intros H

_{0}M. xchange M. }{ xsimpl. }

Qed.

The lemma above shows that the empty predicate \[] can
be removed from the LHS of a magic wand.
More generally, a pure predicate \[P] can be removed from
the LHS of a magic wand, as long as P is true. Formally:

Lemma hwand_hpure_l : ∀ P H,

P →

(\[P] \−∗ H) = H.

Proof using.

introv HP. unfold hwand. xsimpl.

{ intros H

{ xpull. auto. }

Qed.

P →

(\[P] \−∗ H) = H.

Proof using.

introv HP. unfold hwand. xsimpl.

{ intros H

_{0}M. xchange M. applys HP. }{ xpull. auto. }

Qed.

Reciprocally, to prove that a heap satisfies \[P] \−∗ H,
it suffices to prove that this heap satisfies H under the
assumption that P is true. Formally:

Lemma himpl_hwand_hpure_r : ∀ H

(P → H

H

Proof using. introv M. applys himpl_hwand_r. xsimpl. applys M. Qed.

_{1}H_{2}P,(P → H

_{1}==> H_{2}) →H

_{1}==> (\[P] \−∗ H_{2}).Proof using. introv M. applys himpl_hwand_r. xsimpl. applys M. Qed.

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

Prove that \[P_{1}→ P

_{2}] entails \[P

_{1}] \−∗ \[P

_{2}].

Lemma himpl_hwand_hpure_lr : ∀ (P

\[P

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

☐

_{1}P_{2}:Prop),\[P

_{1}→ P_{2}] ==> (\[P_{1}] \−∗ \[P_{2}]).Proof using. (* FILL IN HERE *) Admitted.

☐

### Interaction of hwand with hstar

_{1}\* H

_{2}) \−∗ H

_{3}and H

_{1}\−∗ (H

_{2}\−∗ H

_{3}) and H

_{2}\−∗ (H

_{1}\−∗ H

_{3}) are all equivalent. Intuitively, they all describe the predicate H

_{3}with the missing pieces H

_{1}and H

_{2}.

_{1}\* H

_{2}) \−∗ H

_{3}and the curried form H

_{1}\−∗ (H

_{2}\−∗ H

_{3}) is formalized by the lemma shown below. The third form, H

_{2}\−∗ (H

_{1}\−∗ H

_{3}), follows from the commutativity property H

_{1}\* H

_{2}= H

_{2}\* H

_{1}.

Lemma hwand_curry_eq : ∀ H

(H

Proof using.

intros. applys himpl_antisym.

{ apply himpl_hwand_r. apply himpl_hwand_r.

xchange (hwand_cancel (H

{ apply himpl_hwand_r. xchange (hwand_cancel H

xchange (hwand_cancel H

Qed.

_{1}H_{2}H_{3},(H

_{1}\* H_{2}) \−∗ H_{3}= H_{1}\−∗ (H_{2}\−∗ H_{3}).Proof using.

intros. applys himpl_antisym.

{ apply himpl_hwand_r. apply himpl_hwand_r.

xchange (hwand_cancel (H

_{1}\* H_{2}) H_{3}). }{ apply himpl_hwand_r. xchange (hwand_cancel H

_{1}(H_{2}\−∗ H_{3})).xchange (hwand_cancel H

_{2}H_{3}). }Qed.

Another interesting property is that the RHS of a magic wand
can absorb resources that the magic wand is starred with.
Concretely, from (H
One way to read this: "if you own H

_{1}\−∗ H_{2}) \* H_{3}, one can get the predicate H_{3}to be absorbed by the H_{2}in the magic wand, yielding H_{1}\−∗ (H_{2}\* H_{3})._{3}and, when given H_{1}you own H_{2}, then, when given H_{1}, you own both H_{2}and H_{3}."
Lemma hstar_hwand : ∀ H

(H

Proof using.

intros. applys himpl_hwand_r. xsimpl. xchange (hwand_cancel H

Qed.

_{1}H_{2}H_{3},(H

_{1}\−∗ H_{2}) \* H_{3}==> H_{1}\−∗ (H_{2}\* H_{3}).Proof using.

intros. applys himpl_hwand_r. xsimpl. xchange (hwand_cancel H

_{1}H_{2}).Qed.

Remark: the reciprocal entailment is false: it is not possible
to extract a heap predicate out of the LHS of an entailment.
Indeed, that heap predicate might not exist if it is mentioned
in the RHS of the magic wand.

#### Exercise: 1 star, standard, especially useful (himpl_hwand_hstar_same_r)

Prove that H_{1}entails H_{2}\−∗ (H_{2}\* H_{1}).
Lemma himpl_hwand_hstar_same_r : ∀ H

H

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

☐

_{1}H_{2},H

_{1}==> (H_{2}\−∗ (H_{2}\* H_{1})).Proof using. (* FILL IN HERE *) Admitted.

☐

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

Prove that H_{1}\* ((H

_{1}\* H

_{2}) \−∗ H

_{3}) simplifies to H

_{2}\−∗ H

_{3}.

Lemma hwand_cancel_part : ∀ H

H

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

☐

_{1}H_{2}H_{3},H

_{1}\* ((H_{1}\* H_{2}) \−∗ H_{3}) ==> (H_{2}\−∗ H_{3}).Proof using. (* FILL IN HERE *) Admitted.

☐

#### Exercise: 3 stars, standard, optional (hwand_frame)

Prove that H_{1}\−∗ H

_{2}entails to (H

_{1}\* H

_{3}) \−∗ (H

_{2}\* H

_{3}). Hint: you can use xsimpl during the proof.

Lemma hwand_frame : ∀ H

H

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

☐

_{1}H_{2}H_{3},H

_{1}\−∗ H_{2}==> (H_{1}\* H_{3}) \−∗ (H_{2}\* H_{3}).Proof using. (* FILL IN HERE *) Admitted.

☐

In what follows we prove the equivalence between the three
characterizations of hwand H
1. The definition hwand', expressed directly in terms of heaps:
fun h ⇒ ∀ h', Fmap.disjoint h h' → H
2. The definition hwand, expressed in terms of existing operators:
\∃ H
3. The characterization via the equivalence hwand_equiv:
∀ H
4. The characterization via the pair of the introduction rule
himpl_hwand_r and the elimination rule hwand_cancel.
To prove the 4-way equivalence, we first prove the equivalence
between (1) and (2), then prove the equivalence between (2) and (3),
and finally the equivalence between (3) and (4).

_{1}H_{2}that we have presented:_{1}h' → H_{2}(h' \u h)_{0}, H_{0}\* \[ (H_{1}\* H_{0}) ==> H_{2}]_{0}H_{1}H_{2}, (H_{0}==> H_{1}\−∗ H_{2}) ↔ (H_{1}\* H_{0}==> H_{2}).
Definition hwand_characterization_1 (op:hprop→hprop→hprop) :=

op = (fun H

(fun h ⇒ ∀ h', Fmap.disjoint h h' → H

Definition hwand_characterization_2 (op:hprop→hprop→hprop) :=

op = (fun H

Definition hwand_characterization_3 (op:hprop→hprop→hprop) :=

∀ H

Definition hwand_characterization_4 (op:hprop→hprop→hprop) :=

(∀ H

∧ (∀ H

op = (fun H

_{1}H_{2}⇒(fun h ⇒ ∀ h', Fmap.disjoint h h' → H

_{1}h' → H_{2}(h' \u h))).Definition hwand_characterization_2 (op:hprop→hprop→hprop) :=

op = (fun H

_{1}H_{2}⇒ \∃ H_{0}, H_{0}\* \[ H_{1}\* H_{0}==> H_{2}]).Definition hwand_characterization_3 (op:hprop→hprop→hprop) :=

∀ H

_{0}H_{1}H_{2}, (H_{0}==> op H_{1}H_{2}) ↔ (H_{1}\* H_{0}==> H_{2}).Definition hwand_characterization_4 (op:hprop→hprop→hprop) :=

(∀ H

_{0}H_{1}H_{2}, (H_{1}\* H_{0}==> H_{2}) → (H_{0}==> op H_{1}H_{2}))∧ (∀ H

_{1}H_{2}, (H_{1}\* (op H_{1}H_{2}) ==> H_{2})).
The equivalence proofs are given here for reference. It is not needed
to follow through the technical details.

Lemma hwand_characterization_1_eq_2 :

hwand_characterization_1 = hwand_characterization_2.

Proof using.

applys pred_ext_1. intros op.

unfold hwand_characterization_1, hwand_characterization_2.

asserts K: (∀ A B, A = B → (op = A ↔ op = B)).

{ intros. iff; subst*. } apply K; clear K.

apply pred_ext_3. intros H

{ ∃ (=h). rewrite hstar_hpure_r. split.

{ auto. }

{ intros h

destruct K

rewrites (>> union_comm_of_disjoint D). applys M D K

{ (* This direction reproduces the proof of hwand_inv. *)

intros h

destruct M as (h

lets (N&E): hpure_inv (rm K

rewrite Fmap.union_empty_r in *.

applys N. applys hstar_intro K

Qed.

Lemma hwand_characterization_2_eq_3 :

hwand_characterization_2 = hwand_characterization_3.

Proof using.

applys pred_ext_1. intros op.

unfold hwand_characterization_2, hwand_characterization_3. iff K.

{ subst. intros. (* apply hwand_equiv. *) iff M.

{ xchange M. intros H

{ xsimpl H

{ apply fun_ext_2. intros H

{ lets (M&_): (K (op H

applys M. applys himpl_refl. }

{ xsimpl. intros H

Qed.

Lemma hwand_characterization_3_eq_4 :

hwand_characterization_3 = hwand_characterization_4.

Proof using.

applys pred_ext_1. intros op.

unfold hwand_characterization_3, hwand_characterization_4. iff K.

{ split.

{ introv M. apply <- K. apply M. }

{ intros. apply K. auto. } }

{ destruct K as (K

{ introv M. xchange M. xchange (K

{ introv M. applys K

Qed.

End HwandEquiv.

hwand_characterization_1 = hwand_characterization_2.

Proof using.

applys pred_ext_1. intros op.

unfold hwand_characterization_1, hwand_characterization_2.

asserts K: (∀ A B, A = B → (op = A ↔ op = B)).

{ intros. iff; subst*. } apply K; clear K.

apply pred_ext_3. intros H

_{1}H_{2}h. iff M.{ ∃ (=h). rewrite hstar_hpure_r. split.

{ auto. }

{ intros h

_{3}K_{3}. rewrite hstar_comm in K_{3}.destruct K

_{3}as (h_{1}&h_{2}&K_{1}&K_{2}&D&U). subst h_{1}h_{3}.rewrites (>> union_comm_of_disjoint D). applys M D K

_{2}. } }{ (* This direction reproduces the proof of hwand_inv. *)

intros h

_{1}D K_{1}. destruct M as (H_{0}&M).destruct M as (h

_{0}&h_{2}&K_{0}&K_{2}&D'&U).lets (N&E): hpure_inv (rm K

_{2}). subst h h_{2}.rewrite Fmap.union_empty_r in *.

applys N. applys hstar_intro K

_{1}K_{0}. applys disjoint_sym D. }Qed.

Lemma hwand_characterization_2_eq_3 :

hwand_characterization_2 = hwand_characterization_3.

Proof using.

applys pred_ext_1. intros op.

unfold hwand_characterization_2, hwand_characterization_3. iff K.

{ subst. intros. (* apply hwand_equiv. *) iff M.

{ xchange M. intros H

_{3}N. xchange N. }{ xsimpl H

_{0}. xchange M. } }{ apply fun_ext_2. intros H

_{1}H_{2}. apply himpl_antisym.{ lets (M&_): (K (op H

_{1}H_{2}) H_{1}H_{2}). xsimpl (op H_{1}H_{2}).applys M. applys himpl_refl. }

{ xsimpl. intros H

_{0}M. rewrite K. applys M. } }Qed.

Lemma hwand_characterization_3_eq_4 :

hwand_characterization_3 = hwand_characterization_4.

Proof using.

applys pred_ext_1. intros op.

unfold hwand_characterization_3, hwand_characterization_4. iff K.

{ split.

{ introv M. apply <- K. apply M. }

{ intros. apply K. auto. } }

{ destruct K as (K

_{1}&K_{2}). intros. split.{ introv M. xchange M. xchange (K

_{2}H_{1}H_{2}). }{ introv M. applys K

_{1}. applys M. } }Qed.

End HwandEquiv.

In the beginning of this chapter, we defined qwand following the pattern
of hwand, as \∃ H
This alternative definition involves the universal quantifier for heap
predicates, written \∀ x, H. The universal quantifier is the
counterpart of the existential quantifier \∃ x, H.
Using the \∀ quantifier, we may define Q
Let us first formalize the definition of the universal quantifier on
hprop. Technically, a heap predicate of the form \∀ x, H stands for
hforall (fun x ⇒ H), where the definition of hforall follows the
exact same pattern as for hexists. The definition shown below is somewhat
technical---details may be safely skipped over.

_{0}, H_{0}\* \[ Q_{1}\*+ H_{0}==> Q_{2}] . An alternative approach consists of defining qwand in terms of hwand._{1}\−−∗ Q_{2}as the heap predicate \∀ v, (Q_{1}v) \−∗ (Q_{2}v).
Definition hforall (A : Type) (J : A → hprop) : hprop :=

fun h ⇒ ∀ x, J x h.

Notation "'\forall' x

(hforall (fun x

(at level 39, x

format "'[' '\forall' '/ ' x

fun h ⇒ ∀ x, J x h.

Notation "'\forall' x

_{1}.. xn , H" :=(hforall (fun x

_{1}⇒ .. (hforall (fun xn ⇒ H)) ..))(at level 39, x

_{1}binder, H at level 50, right associativity,format "'[' '\forall' '/ ' x

_{1}.. xn , '/ ' H ']'").
The introduction and elimination rule for hforall are as follows.

Lemma hforall_intro : ∀ A (J:A→hprop) h,

(∀ x, J x h) →

(hforall J) h.

Proof using. introv M. applys* M. Qed.

Lemma hforall_inv : ∀ A (J:A→hprop) h,

(hforall J) h →

∀ x, J x h.

Proof using. introv M. applys* M. Qed.

(∀ x, J x h) →

(hforall J) h.

Proof using. introv M. applys* M. Qed.

Lemma hforall_inv : ∀ A (J:A→hprop) h,

(hforall J) h →

∀ x, J x h.

Proof using. introv M. applys* M. Qed.

The introduction rule in an entailement for \∀ appears below.
To prove that a heap satisfies \∀ x, J x, one must show that,
for any x, this heap satisfies J x.

Lemma himpl_hforall_r : ∀ A (J:A→hprop) H,

(∀ x, H ==> J x) →

H ==> (\∀ x, J x).

Proof using. introv M. intros h K x. apply¬M. Qed.

(∀ x, H ==> J x) →

H ==> (\∀ x, J x).

Proof using. introv M. intros h K x. apply¬M. Qed.

The elimination rule in an entailment for \∀ appears below.
Assuming a heap satisfies \∀ x, J x, one can derive that the
same heap satisfies J v for any desired value v.

Lemma hforall_specialize : ∀ A (v:A) (J:A→hprop),

(\∀ x, J x) ==> (J v).

Proof using. intros. intros h K. apply* K. Qed.

(\∀ x, J x) ==> (J v).

Proof using. intros. intros h K. apply* K. Qed.

This last lemma can equivalently be formulated in the following way,
which makes it easier to apply in some cases.

Lemma himpl_hforall_l : ∀ A (v:A) (J:A→hprop) H,

J v ==> H →

(\∀ x, J x) ==> H.

Proof using. introv M. applys himpl_trans M. applys hforall_specialize. Qed.

J v ==> H →

(\∀ x, J x) ==> H.

Proof using. introv M. applys himpl_trans M. applys hforall_specialize. Qed.

Universal quantifers that appear in the precondition of a triple
may be specialized, just like those in the left-hand side of an
entailment.

Lemma triple_hforall : ∀ A (v:A) t (J:A→hprop) Q,

triple t (J v) Q →

triple t (\∀ x, J x) Q.

Proof.

introv M. applys triple_conseq M.

{ applys hforall_specialize. }

{ applys qimpl_refl. }

Qed.

triple t (J v) Q →

triple t (\∀ x, J x) Q.

Proof.

introv M. applys triple_conseq M.

{ applys hforall_specialize. }

{ applys qimpl_refl. }

Qed.

Declare Scope qwand_scope.

Open Scope qwand_scope.

Open Scope qwand_scope.

We are now read to state the alternative definition of Q

_{1}\−−∗ Q_{2}, as the heap predicate \∀ v, (Q_{1}v) \−∗ (Q_{2}v).
Definition qwand (Q

\∀ v, (Q

Notation "Q

_{1}Q_{2}:val→hprop) : hprop :=\∀ v, (Q

_{1}v) \−∗ (Q_{2}v).Notation "Q

_{1}\−−∗ Q_{2}" := (qwand Q_{1}Q_{2}) (at level 43) : qwand_scope.
Let us establish the properties of the new definition of qwand.
We begin by the specialization lemma, which asserts that Q

_{1}\−−∗ Q_{2}can be specialized to (Q_{1}v) \−∗ (Q_{2}v) for any value v. This result is a direct consequence of the corresponding specialization property of \∀.
Lemma qwand_specialize : ∀ (v:val) (Q

(Q

Proof using.

intros. unfold qwand. applys himpl_hforall_l v. xsimpl.

Qed.

_{1}Q_{2}:val→hprop),(Q

_{1}\−−∗ Q_{2}) ==> (Q_{1}v \−∗ Q_{2}v).Proof using.

intros. unfold qwand. applys himpl_hforall_l v. xsimpl.

Qed.

We next prove the equivalence rule.

Lemma qwand_equiv : ∀ H Q

H ==> (Q

Proof using.

intros. iff M.

{ intros x. xchange M. xchange (qwand_specialize x).

xchange (hwand_cancel (Q

{ applys himpl_hforall_r. intros x. applys himpl_hwand_r.

xchange (M x). }

Qed.

_{1}Q_{2},H ==> (Q

_{1}\−−∗ Q_{2}) ↔ (Q_{1}\*+ H) ===> Q_{2}.Proof using.

intros. iff M.

{ intros x. xchange M. xchange (qwand_specialize x).

xchange (hwand_cancel (Q

_{1}x)). }{ applys himpl_hforall_r. intros x. applys himpl_hwand_r.

xchange (M x). }

Qed.

The cancellation rule follows.

Lemma qwand_cancel : ∀ Q

Q

Proof using. intros. rewrite <- qwand_equiv. applys qimpl_refl. Qed.

_{1}Q_{2},Q

_{1}\*+ (Q_{1}\−−∗ Q_{2}) ===> Q_{2}.Proof using. intros. rewrite <- qwand_equiv. applys qimpl_refl. Qed.

Like H

_{1}\−∗ H_{2}, the operation Q_{1}\−−∗ Q_{2}is contravariant in Q_{1}and covariant in Q_{2}.
Lemma qwand_himpl : ∀ Q

Q

Q

(Q

Proof using.

introv M

xchange (qwand_specialize x). xchange M

xchange (hwand_cancel (Q

Qed.

_{1}Q_{1}' Q_{2}Q_{2}',Q

_{1}' ===> Q_{1}→Q

_{2}===> Q_{2}' →(Q

_{1}\−−∗ Q_{2}) ==> (Q_{1}' \−−∗ Q_{2}').Proof using.

introv M

_{1}M_{2}. rewrite qwand_equiv. intros x.xchange (qwand_specialize x). xchange M

_{1}.xchange (hwand_cancel (Q

_{1}x)). xchange M_{2}.Qed.

Like H

_{1}\−∗ H_{2}, the operation Q_{1}\−−∗ Q_{2}can absorb in its RHS resources to which it is starred.
Lemma hstar_qwand : ∀ Q

(Q

Proof using.

intros. rewrite qwand_equiv. xchange (@qwand_cancel Q

Qed.

_{1}Q_{2}H,(Q

_{1}\−−∗ Q_{2}) \* H ==> Q_{1}\−−∗ (Q_{2}\*+ H).Proof using.

intros. rewrite qwand_equiv. xchange (@qwand_cancel Q

_{1}).Qed.

#### Exercise: 1 star, standard, especially useful (himpl_qwand_hstar_same_r)

Prove that H entails Q \−−∗ (Q \*+ H).
Lemma himpl_qwand_hstar_same_r : ∀ H Q,

H ==> Q \−−∗ (Q \*+ H).

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

☐

H ==> Q \−−∗ (Q \*+ H).

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

☐

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

Prove that H \* ((Q_{1}\*+ H) \−−∗ Q

_{2}) simplifies to Q

_{1}\−−∗ Q

_{2}. Hint: use xchange.

Lemma qwand_cancel_part : ∀ H Q

H \* ((Q

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

☐

_{1}Q_{2},H \* ((Q

_{1}\*+ H) \−−∗ Q_{2}) ==> (Q_{1}\−−∗ Q_{2}).Proof using. (* FILL IN HERE *) Admitted.

☐

In what follows we prove the equivalence between five equivalent
characterizations of qwand H
1. The definition expressed directly in terms of heaps:
fun h ⇒ ∀ v h', Fmap.disjoint h h' → Q
2. The definition qwand, expressed in terms of existing operators:
\∃ H
3. The definition expressed using the universal quantifier:
\∀ v, (Q
4. The characterization via the equivalence hwand_equiv:
∀ H
5. The characterization via the pair of the introduction rule
himpl_qwand_r and the elimination rule qwand_cancel.
The proof are essentially identical to the equivalence proofs for hwand,
except for definition (3), which is specific to qwand.

_{1}H_{2}:_{1}v h' → Q_{2}v (h \u h')_{0}, H_{0}\* \[ (Q_{1}\*+ H_{0}) ===> Q_{2}]_{1}v) \−∗ (Q_{2}v)_{0}H_{1}H_{2}, (H_{0}==> H_{1}\−∗ H_{2}) ↔ (H_{1}\* H_{0}==> H_{2}).
Definition qwand_characterization_1 op :=

op = (fun Q

Q

Definition qwand_characterization_2 op :=

op = (fun Q

Definition qwand_characterization_3 op :=

op = (fun Q

Definition qwand_characterization_4 op :=

∀ H

Definition qwand_characterization_5 op :=

(∀ H

∧ (∀ Q

Lemma hwand_characterization_1_eq_2 :

qwand_characterization_1 = qwand_characterization_2.

Proof using.

applys pred_ext_1. intros op.

unfold qwand_characterization_1, qwand_characterization_2.

asserts K: (∀ A B, A = B → (op = A ↔ op = B)).

{ intros. iff; subst*. } apply K; clear K.

apply pred_ext_3. intros Q

{ ∃ (=h). rewrite hstar_hpure_r. split.

{ auto. }

{ intros v h

destruct K

{ intros v h

destruct M as (h

lets (N&E): hpure_inv (rm K

rewrite Fmap.union_empty_r in *.

applys N. rewrite hstar_comm. applys hstar_intro K

Qed.

Lemma qwand_characterization_2_eq_3 :

qwand_characterization_2 = qwand_characterization_3.

Proof using.

applys pred_ext_1. intros op.

unfold qwand_characterization_2, qwand_characterization_3.

asserts K: (∀ A B, A = B → (op = A ↔ op = B)).

{ intros. iff; subst*. } apply K; clear K.

apply fun_ext_2. intros Q

{ xpull. intros H

rewrite hwand_equiv. xchange M. }

{ xsimpl (qwand Q

Qed.

Lemma qwand_characterization_2_eq_4 :

qwand_characterization_2 = qwand_characterization_4.

Proof using.

applys pred_ext_1. intros op.

unfold qwand_characterization_2, qwand_characterization_4. iff K.

{ subst. intros. iff M.

{ xchange M. intros v H

{ xsimpl H

{ apply fun_ext_2. intros H

{ lets (M&_): (K (op H

applys M. applys himpl_refl. }

{ xsimpl. intros H

Qed.

Lemma qwand_characterization_4_eq_5 :

qwand_characterization_4 = qwand_characterization_5.

Proof using.

applys pred_ext_1. intros op.

unfold qwand_characterization_4, qwand_characterization_5. iff K.

{ split.

{ introv M. apply <- K. apply M. }

{ intros. apply K. auto. } }

{ destruct K as (K

{ introv M. xchange M. xchange (K

{ introv M. applys K

Qed.

End QwandEquiv.

op = (fun Q

_{1}Q_{2}⇒ (fun h ⇒ ∀ v h', Fmap.disjoint h h' →Q

_{1}v h' → Q_{2}v (h \u h'))).Definition qwand_characterization_2 op :=

op = (fun Q

_{1}Q_{2}⇒ \∃ H_{0}, H_{0}\* \[ Q_{1}\*+ H_{0}===> Q_{2}]).Definition qwand_characterization_3 op :=

op = (fun Q

_{1}Q_{2}⇒ \∀ v, (Q_{1}v) \−∗ (Q_{2}v)).Definition qwand_characterization_4 op :=

∀ H

_{0}Q_{1}Q_{2}, (H_{0}==> op Q_{1}Q_{2}) ↔ (Q_{1}\*+ H_{0}===> Q_{2}).Definition qwand_characterization_5 op :=

(∀ H

_{0}Q_{1}Q_{2}, (Q_{1}\*+ H_{0}===> Q_{2}) → (H_{0}==> op Q_{1}Q_{2}))∧ (∀ Q

_{1}Q_{2}, (Q_{1}\*+ (op Q_{1}Q_{2}) ===> Q_{2})).Lemma hwand_characterization_1_eq_2 :

qwand_characterization_1 = qwand_characterization_2.

Proof using.

applys pred_ext_1. intros op.

unfold qwand_characterization_1, qwand_characterization_2.

asserts K: (∀ A B, A = B → (op = A ↔ op = B)).

{ intros. iff; subst*. } apply K; clear K.

apply pred_ext_3. intros Q

_{1}Q_{2}h. iff M.{ ∃ (=h). rewrite hstar_hpure_r. split.

{ auto. }

{ intros v h

_{3}K_{3}. rewrite hstar_comm in K_{3}.destruct K

_{3}as (h_{1}&h_{2}&K_{1}&K_{2}&D&U). subst h_{1}h_{3}. applys M D K_{2}. } }{ intros v h

_{1}D K_{1}. destruct M as (H_{0}&M).destruct M as (h

_{0}&h_{2}&K_{0}&K_{2}&D'&U).lets (N&E): hpure_inv (rm K

_{2}). subst h h_{2}.rewrite Fmap.union_empty_r in *.

applys N. rewrite hstar_comm. applys hstar_intro K

_{0}K_{1}D. }Qed.

Lemma qwand_characterization_2_eq_3 :

qwand_characterization_2 = qwand_characterization_3.

Proof using.

applys pred_ext_1. intros op.

unfold qwand_characterization_2, qwand_characterization_3.

asserts K: (∀ A B, A = B → (op = A ↔ op = B)).

{ intros. iff; subst*. } apply K; clear K.

apply fun_ext_2. intros Q

_{1}Q_{2}. apply himpl_antisym.{ xpull. intros H

_{0}M. applys himpl_hforall_r. intros v.rewrite hwand_equiv. xchange M. }

{ xsimpl (qwand Q

_{1}Q_{2}). applys qwand_cancel. }Qed.

Lemma qwand_characterization_2_eq_4 :

qwand_characterization_2 = qwand_characterization_4.

Proof using.

applys pred_ext_1. intros op.

unfold qwand_characterization_2, qwand_characterization_4. iff K.

{ subst. intros. iff M.

{ xchange M. intros v H

_{3}N. xchange N. }{ xsimpl H

_{0}. xchange M. } }{ apply fun_ext_2. intros H

_{1}H_{2}. apply himpl_antisym.{ lets (M&_): (K (op H

_{1}H_{2}) H_{1}H_{2}). xsimpl (op H_{1}H_{2}).applys M. applys himpl_refl. }

{ xsimpl. intros H

_{0}M. rewrite K. applys M. } }Qed.

Lemma qwand_characterization_4_eq_5 :

qwand_characterization_4 = qwand_characterization_5.

Proof using.

applys pred_ext_1. intros op.

unfold qwand_characterization_4, qwand_characterization_5. iff K.

{ split.

{ introv M. apply <- K. apply M. }

{ intros. apply K. auto. } }

{ destruct K as (K

_{1}&K_{2}). intros. split.{ introv M. xchange M. xchange (K

_{2}Q_{1}Q_{2}). }{ introv M. applys K

_{1}. applys M. } }Qed.

End QwandEquiv.

## Simplified Definition 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].
Observe that the fragment \∃ H, H \* \[Q

_{1}\*+ H ===> Q] is equivalent to Q_{1}\−−∗ Q. This observation leads to the following more concise reformulation of the definition of mkstruct.
Let us prove, for this revised definition, that mkstruct satisfies
the three required properties (recall WPgen): mkstruct_erase,
mkstruct_frame, and mkstruct_conseq. In these proofs, we assume
the revised definition of qwand expressed in terms of hwand
and hforall.

Lemma mkstruct_erase : ∀ F Q,

F Q ==> mkstruct F Q.

Proof using.

intros. unfold mkstruct. xsimpl Q. rewrite qwand_equiv. xsimpl.

Qed.

Lemma mkstruct_conseq : ∀ F Q

Q

mkstruct F Q

Proof using.

introv WQ. unfold mkstruct. xpull. intros Q'. xsimpl Q'.

rewrite qwand_equiv. xchange qwand_cancel. xchange WQ.

Qed.

Lemma mkstruct_frame : ∀ F H Q,

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

Proof using.

intros. unfold mkstruct. xpull. intros Q'. xsimpl Q'.

rewrite qwand_equiv. xchange qwand_cancel.

Qed.

End NewQwand.

F Q ==> mkstruct F Q.

Proof using.

intros. unfold mkstruct. xsimpl Q. rewrite qwand_equiv. xsimpl.

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'. xsimpl Q'.

rewrite qwand_equiv. xchange qwand_cancel. xchange WQ.

Qed.

Lemma mkstruct_frame : ∀ F H Q,

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

Proof using.

intros. unfold mkstruct. xpull. intros Q'. xsimpl Q'.

rewrite qwand_equiv. xchange qwand_cancel.

Qed.

End NewQwand.

In this section, we assume a version of xsimpl that handles
the magic wand. Note that hforall and other operators are
set "Opaque", their definitions cannot be unfolded.

### 1. Example of Texan Triples

This specification can be equivalently reformulated in the following
form.

Above, we purposely left the empty heap predicate to the front to
indicate where the precondition, if it were not empty, would go in
the reformulation.
In what follows, we describe the chain of transformation that can take us
from the triple form to the wp form, and establish the reciprocal.
We then formalize the general pattern for translating a triple
into a "texan triple" (i.e., the wp-based specification).
By replacing triple t H Q with H ==> wp t Q, the specification
triple_ref can be reformulated as follows.

Lemma wp_ref_0 : ∀ v,

\[] ==> wp (val_ref v) (funloc p ⇒ p ~~> v).

Proof using. intros. rewrite wp_equiv. applys triple_ref. Qed.

\[] ==> wp (val_ref v) (funloc p ⇒ p ~~> v).

Proof using. intros. rewrite wp_equiv. applys triple_ref. Qed.

We wish to cast the RHS in the form wp (val_ref v) Q for an abstract
variable Q. To that end, we reformulate the above statement by including
a magic wand relating the current postcondition, which is
(funloc p ⇒ p ~~> v), and Q.

Lemma wp_ref_1 : ∀ Q v,

((funloc p ⇒ p ~~> v) \−−∗ Q) ==> wp (val_ref v) Q.

Proof using. intros. xchange (wp_ref_0 v). applys wp_ramified. Qed.

((funloc p ⇒ p ~~> v) \−−∗ Q) ==> wp (val_ref v) Q.

Proof using. intros. xchange (wp_ref_0 v). applys wp_ramified. Qed.

This statement can be made slightly more readable by unfolding the
definition of the magic wand for postconditions, as shown next.

Lemma wp_ref_2 : ∀ Q v,

(\∀ r, (\∃ p, \[r = val_loc p] \* p ~~> v) \−∗ Q r)

==> wp (val_ref v) Q.

Proof using. intros. applys himpl_trans wp_ref_1. xsimpl. Qed.

(\∀ r, (\∃ p, \[r = val_loc p] \* p ~~> v) \−∗ Q r)

==> wp (val_ref v) Q.

Proof using. intros. applys himpl_trans wp_ref_1. xsimpl. Qed.

Interestingly, the variable r, which is equal to val_loc p,
can now be substituted away, further increasing readability.
We obtain the specificaiton of val_ref in "Texan triple style".

Lemma wp_ref_3 : ∀ Q v,

(\∀ p, (p ~~> v) \−∗ Q (val_loc p)) ==> wp (val_ref v) Q.

Proof using.

intros. applys himpl_trans wp_ref_2. xsimpl. intros ? p →.

xchange (hforall_specialize p).

Qed.

(\∀ p, (p ~~> v) \−∗ Q (val_loc p)) ==> wp (val_ref v) Q.

Proof using.

intros. applys himpl_trans wp_ref_2. xsimpl. intros ? p →.

xchange (hforall_specialize p).

Qed.

### 2. The General Pattern

_{1}x

_{2}, \[r = v] \* H'). In such a specification:

- the value v may depend on the xi,
- the heap predicate H' may depend on r and the xi,
- the number of existentials xi may vary, possibly be zero,
- the equality \[r = v] may be removed if no pure fact is needed about r.

_{1}x

_{2}, \[r = v] \* H' can be be reformulated as the Texan triple: (\∀ x

_{1}x

_{2}, H \−∗ Q v) ==> wp t Q.

Lemma texan_triple_equiv : ∀ t H A (Hof:val→A→hprop) (vof:A→val),

(triple t H (fun r ⇒ \∃ x, \[r = vof x] \* Hof r x))

↔ (∀ Q, H \* (\∀ x, Hof (vof x) x \−∗ Q (vof x)) ==> wp t Q).

Proof using.

intros. rewrite <- wp_equiv. iff M.

{ intros Q. xchange M. applys wp_ramified_trans.

xsimpl. intros r x →.

xchange (hforall_specialize x). }

{ applys himpl_trans M. xsimpl¬. }

Qed.

(triple t H (fun r ⇒ \∃ x, \[r = vof x] \* Hof r x))

↔ (∀ Q, H \* (\∀ x, Hof (vof x) x \−∗ Q (vof x)) ==> wp t Q).

Proof using.

intros. rewrite <- wp_equiv. iff M.

{ intros Q. xchange M. applys wp_ramified_trans.

xsimpl. intros r x →.

xchange (hforall_specialize x). }

{ applys himpl_trans M. xsimpl¬. }

Qed.

The wp-style specification of ref, get and set follow.

Lemma wp_get : ∀ v p Q,

(p ~~> v) \* (p ~~> v \−∗ Q v) ==> wp (val_get p) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_get. } { applys himpl_refl. } { xsimpl. intros ? →. auto. }

Qed.

Lemma wp_set : ∀ v w p Q,

(p ~~> v) \* (\∀ r, p ~~> w \−∗ Q r) ==> wp (val_set p w) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_set. } { applys himpl_refl. }

{ intros r. xchange (hforall_specialize r). }

Qed.

Lemma wp_free : ∀ v p Q,

(p ~~> v) \* (\∀ r, Q r) ==> wp (val_free p) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_free. } { applys himpl_refl. }

{ intros r. xchange (hforall_specialize r). }

Qed.

(p ~~> v) \* (p ~~> v \−∗ Q v) ==> wp (val_get p) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_get. } { applys himpl_refl. } { xsimpl. intros ? →. auto. }

Qed.

Lemma wp_set : ∀ v w p Q,

(p ~~> v) \* (\∀ r, p ~~> w \−∗ Q r) ==> wp (val_set p w) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_set. } { applys himpl_refl. }

{ intros r. xchange (hforall_specialize r). }

Qed.

Lemma wp_free : ∀ v p Q,

(p ~~> v) \* (\∀ r, Q r) ==> wp (val_free p) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_free. } { applys himpl_refl. }

{ intros r. xchange (hforall_specialize r). }

Qed.

Alternatively, we can advertize that set and free output the unit
value.

Parameter triple_set' : ∀ w p v,

triple (val_set p w)

(p ~~> v)

(fun r ⇒ \[r = val_unit] \* p ~~> w).

Parameter triple_free' : ∀ p v,

triple (val_free p)

(p ~~> v)

(fun r ⇒ \[r = val_unit]).

Lemma wp_set' : ∀ v w p Q,

(p ~~> v) \* (p ~~> w \−∗ Q val_unit) ==> wp (val_set p w) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_set'. }

{ applys himpl_refl. }

{ xsimpl. intros ? →. auto. }

Qed.

Lemma wp_free' : ∀ v w p Q,

(p ~~> v) \* (Q val_unit) ==> wp (val_free p) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_free'. }

{ applys himpl_refl. }

{ xsimpl. intros ? →. auto. }

Qed.

End WpSpecRef.

triple (val_set p w)

(p ~~> v)

(fun r ⇒ \[r = val_unit] \* p ~~> w).

Parameter triple_free' : ∀ p v,

triple (val_free p)

(p ~~> v)

(fun r ⇒ \[r = val_unit]).

Lemma wp_set' : ∀ v w p Q,

(p ~~> v) \* (p ~~> w \−∗ Q val_unit) ==> wp (val_set p w) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_set'. }

{ applys himpl_refl. }

{ xsimpl. intros ? →. auto. }

Qed.

Lemma wp_free' : ∀ v w p Q,

(p ~~> v) \* (Q val_unit) ==> wp (val_free p) Q.

Proof using.

intros. rewrite wp_equiv. applys triple_conseq_frame.

{ applys triple_free'. }

{ applys himpl_refl. }

{ xsimpl. intros ? →. auto. }

Qed.

End WpSpecRef.

### 4. Equivalent expressiveness

Lemma triple_ref_of_wp_ref_3 : ∀ v,

triple (val_ref v)

\[]

(funloc p ⇒ p ~~> v).

Proof using.

intros. rewrite <- wp_equiv.

applys himpl_trans; [| applys wp_ref_3 ].

xsimpl*.

Qed.

triple (val_ref v)

\[]

(funloc p ⇒ p ~~> v).

Proof using.

intros. rewrite <- wp_equiv.

applys himpl_trans; [| applys wp_ref_3 ].

xsimpl*.

Qed.

Likewise for the other three operations: the triple-based specification
is derivable from the wp-based specification.

Lemma triple_get_of_wp_get : ∀ v p,

triple (val_get p)

(p ~~> v)

(fun r ⇒ \[r = v] \* (p ~~> v)).

Proof using.

intros. rewrite <- wp_equiv.

applys himpl_trans; [| applys wp_get ].

xsimpl*.

Qed.

Lemma triple_set : ∀ w p v,

triple (val_set (val_loc p) v)

(p ~~> w)

(fun _ ⇒ p ~~> v).

Proof using.

intros. rewrite <- wp_equiv.

applys himpl_trans; [| applys wp_set ].

xsimpl*.

Qed.

Lemma triple_free : ∀ p v,

triple (val_free (val_loc p))

(p ~~> v)

(fun _ ⇒ \[]).

Proof using.

intros. rewrite <- wp_equiv.

applys himpl_trans; [| applys wp_free ].

xsimpl*.

Qed.

triple (val_get p)

(p ~~> v)

(fun r ⇒ \[r = v] \* (p ~~> v)).

Proof using.

intros. rewrite <- wp_equiv.

applys himpl_trans; [| applys wp_get ].

xsimpl*.

Qed.

Lemma triple_set : ∀ w p v,

triple (val_set (val_loc p) v)

(p ~~> w)

(fun _ ⇒ p ~~> v).

Proof using.

intros. rewrite <- wp_equiv.

applys himpl_trans; [| applys wp_set ].

xsimpl*.

Qed.

Lemma triple_free : ∀ p v,

triple (val_free (val_loc p))

(p ~~> v)

(fun _ ⇒ \[]).

Proof using.

intros. rewrite <- wp_equiv.

applys himpl_trans; [| applys wp_free ].

xsimpl*.

Qed.

### 5. Exercise

Parameter incr : val.

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

triple (incr p)

(p ~~> n)

(fun v ⇒ \[v = val_unit] \* (p ~~> (n+1))).

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

triple (incr p)

(p ~~> n)

(fun v ⇒ \[v = val_unit] \* (p ~~> (n+1))).

#### Exercise: 3 stars, standard, especially useful (wp_incr)

State a Texan triple for incr as a lemma called wp_incr, then prove this lemma from triple_incr.
(* FILL IN HERE *)

☐

☐

Recall from the last section of the chapter WPsem that it can
be interesting to define wp-style rules directly from the hoare
rules, so as to bypass the statements and proofs of rules for triples.
In the first part of this chapter, we proved that the rule
wp_ramified is derivable from the consequence-frame rule for triples.
Let us now show how to prove the rule wp_ramified directly from
the rules of Hoare logic.

Lemma wp_ramified : ∀ t Q

(wp t Q

Proof using.

intros. unfold wp. xpull. intros H M.

xsimpl (H \* (Q

applys hoare_conseq M. { xsimpl. }

intros r. xchange (qwand_specialize r). xsimpl.

rewrite hstar_comm. applys hwand_cancel.

Qed.

End WpFromHoare.

_{1}Q_{2},(wp t Q

_{1}) \* (Q_{1}\−−∗ Q_{2}) ==> (wp t Q_{2}).Proof using.

intros. unfold wp. xpull. intros H M.

xsimpl (H \* (Q

_{1}\−−∗ Q_{2})). intros H'.applys hoare_conseq M. { xsimpl. }

intros r. xchange (qwand_specialize r). xsimpl.

rewrite hstar_comm. applys hwand_cancel.

Qed.

End WpFromHoare.

## Conjunction and Disjunction Operators on hprop

### Definition of hor

_{1}H

_{2}lifts the disjunction operator P

_{1}∨ P

_{2}from Prop to hprop.

_{1}H

_{2}describes a heap that satisfies H

_{1}or satifies H

_{2}(possibly both).

An alternative definition leverages the \∃ quantifier.
The definition, shown below, reads as follows: "there exists
an unspecified boolean value b such that if b is true
then H
The benefits of this definition is that the proof of its properties
can be established without manipulating heaps explicitly.

_{1}holds, else if b is false then H_{2}holds".#### Exercise: 3 stars, standard, optional (hor_eq_hor')

Prove the equivalence of the definitions hor and hor'.- If H
_{1}holds, then "H_{1}or H_{2}" holds. - Symmetrically, if H
_{2}holds, then "H_{1}or H_{2}" holds. - Reciprocally, if "H
_{1}or H_{2}" holds, then one can perform a case analysis on whether it is H_{1}or H_{2}that holds. Concretely, to show that "H_{1}or H_{2}" entails H_{3}, one must show both that H_{1}entails H_{3}and that H_{2}entails H_{3}.

Lemma himpl_hor_r_l : ∀ H

H

Proof using. intros. unfolds hor. ∃* true. Qed.

Lemma himpl_hor_r_r : ∀ H

H

Proof using. intros. unfolds hor. ∃* false. Qed.

_{1}H_{2},H

_{1}==> hor H_{1}H_{2}.Proof using. intros. unfolds hor. ∃* true. Qed.

Lemma himpl_hor_r_r : ∀ H

_{1}H_{2},H

_{2}==> hor H_{1}H_{2}.Proof using. intros. unfolds hor. ∃* false. Qed.

In practice, these two rules are easier to exploit when combined with a
transitivity step.

Lemma himpl_hor_r_l_trans : ∀ H

H

H

Proof using. introv W. applys himpl_trans W. applys himpl_hor_r_l. Qed.

Lemma himpl_hor_r_r_trans : ∀ H

H

H

Proof using. introv W. applys himpl_trans W. applys himpl_hor_r_r. Qed.

_{1}H_{2}H_{3},H

_{3}==> H_{1}→H

_{3}==> hor H_{1}H_{2}.Proof using. introv W. applys himpl_trans W. applys himpl_hor_r_l. Qed.

Lemma himpl_hor_r_r_trans : ∀ H

_{1}H_{2}H_{3},H

_{3}==> H_{2}→H

_{3}==> hor H_{1}H_{2}.Proof using. introv W. applys himpl_trans W. applys himpl_hor_r_r. Qed.

The elimination rule is stated as follows.

Lemma himpl_hor_l : ∀ H

H

H

hor H

Proof using.

introv M

Qed.

_{1}H_{2}H_{3},H

_{1}==> H_{3}→H

_{2}==> H_{3}→hor H

_{1}H_{2}==> H_{3}.Proof using.

introv M

_{1}M_{2}. unfolds hor. applys himpl_hexists_l. intros b. case_if*.Qed.

The operator hor is commutative. To establish this property, it is
handy to exploit the following lemma, called if_neg, which swaps the
two branches of a conditional by negating the boolean condition.

Lemma if_neg : ∀ (b:bool) A (X Y:A),

(if b then X else Y) = (if neg b then Y else X).

Proof using. intros. case_if*. Qed.

(if b then X else Y) = (if neg b then Y else X).

Proof using. intros. case_if*. Qed.

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

Prove that hor is a symmetric operator. Hint: exploit if_neg and hprop_op_comm (from chapter Himpl).
Lemma hor_comm : ∀ H

hor H

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

☐

_{1}H_{2},hor H

_{1}H_{2}= hor H_{2}H_{1}.Proof using. (* FILL IN HERE *) Admitted.

☐

Recall from chapter Repr the definition of MList, and the two
lemmas MList_nil and MList_cons that reformulates that definition.

#### Exercise: 4 stars, standard, especially useful (hor_comm)

Prove that MList can be characterized by a disjunction expressed using hor as shown below.
Lemma MList_using_hor : ∀ L p,

MList L p =

hor (\[L = nil ∧ p = null])

(\∃ x q L', \[L = x::L']

\* (p ~~~>`{ head := x; tail := q})

\* (MList L' q)).

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

☐

MList L p =

hor (\[L = nil ∧ p = null])

(\∃ x q L', \[L = x::L']

\* (p ~~~>`{ head := x; tail := q})

\* (MList L' q)).

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

☐

### Definition of hand

_{1}H

_{2}lifts the disjunction operator P

_{1}∧ P

_{2}from Prop to hprop.

_{1}H

_{2}describes a heap that satisfies H

_{1}and at the same time satifies H

_{2}.

An alternative definition leverages the \∀ quantifier.
The definition, shown below, reads as follows: "for any
boolean value b, if b is true then H

_{1}should hold, and if b is false then H_{2}should hold".#### Exercise: 2 stars, standard, especially useful (hand_eq_hand')

Prove the equivalence of the definitions hand and hand'.- If "H
_{1}and H_{2}" holds, then in particular H_{1}holds. - Symmetrically, if "H
_{1}and H_{2}" holds, then in particular H_{2}holds. - Reciprocally, to prove that a heap predicate H
_{3}entails "H_{1}and H_{2}", one must prove that H_{3}entails H_{1}, and that H_{3}satisfies H_{2}.

Lemma himpl_hand_l_r : ∀ H

hand H

Proof using. intros. unfolds hand. applys* himpl_hforall_l true. Qed.

Lemma himpl_hand_l_l : ∀ H

hand H

Proof using. intros. unfolds hand. applys* himpl_hforall_l false. Qed.

Lemma himpl_hand_r : ∀ H

H

H

H

Proof using. introv M

_{1}H_{2},hand H

_{1}H_{2}==> H_{1}.Proof using. intros. unfolds hand. applys* himpl_hforall_l true. Qed.

Lemma himpl_hand_l_l : ∀ H

_{1}H_{2},hand H

_{1}H_{2}==> H_{2}.Proof using. intros. unfolds hand. applys* himpl_hforall_l false. Qed.

Lemma himpl_hand_r : ∀ H

_{1}H_{2}H_{3},H

_{3}==> H_{1}→H

_{3}==> H_{2}→H

_{3}==> hand H_{1}H_{2}.Proof using. introv M

_{1}M_{2}Hh. intros b. case_if*. Qed.#### Exercise: 1 star, standard, especially useful (hand_comm)

Prove that hand is a symmetric operator. Hint: use hprop_op_comm, and rewrite if_neg (or a case analysis on the boolean value coming from hand).
Lemma hand_comm : ∀ H

hand H

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

☐

_{1}H_{2},hand H

_{1}H_{2}= hand H_{2}H_{1}.Proof using. (* FILL IN HERE *) Admitted.

☐

The core operators are defined as functions over heaps.

Definition hempty : hprop :=

fun h ⇒ (h = Fmap.empty).

Definition hsingle (p:loc) (v:val) : hprop :=

fun h ⇒ (h = Fmap.single p v).

Definition hstar (H

fun h ⇒ ∃ h

∧ H

∧ Fmap.disjoint h

∧ h = Fmap.union h

Definition hexists A (J:A→hprop) : hprop :=

fun h ⇒ ∃ x, J x h.

Definition hforall (A : Type) (J : A → hprop) : hprop :=

fun h ⇒ ∀ x, J x h.

fun h ⇒ (h = Fmap.empty).

Definition hsingle (p:loc) (v:val) : hprop :=

fun h ⇒ (h = Fmap.single p v).

Definition hstar (H

_{1}H_{2}: hprop) : hprop :=fun h ⇒ ∃ h

_{1}h_{2}, H_{1}h_{1}∧ H

_{2}h_{2}∧ Fmap.disjoint h

_{1}h_{2}∧ h = Fmap.union h

_{1}h_{2}.Definition hexists A (J:A→hprop) : hprop :=

fun h ⇒ ∃ x, J x h.

Definition hforall (A : Type) (J : A → hprop) : hprop :=

fun h ⇒ ∀ x, J x h.

The remaining operators can be defined either as functions over
heaps, or as derived definitions expressed in terms of the core
operators defined above.
Direct definition for the remaining operators.

Module ReaminingOperatorsDirect.

Definition hpure (P:Prop) : hprop :=

fun h ⇒ (h = Fmap.empty) ∧ P.

Definition hwand (H

fun h ⇒ ∀ h', Fmap.disjoint h h' → H

Definition qwand (Q

fun h ⇒ ∀ v h', Fmap.disjoint h h' → Q

Definition hor (H

fun h ⇒ H

Definition hand (H

fun h ⇒ H

End ReaminingOperatorsDirect.

Definition hpure (P:Prop) : hprop :=

fun h ⇒ (h = Fmap.empty) ∧ P.

Definition hwand (H

_{1}H_{2}:hprop) : hprop :=fun h ⇒ ∀ h', Fmap.disjoint h h' → H

_{1}h' → H_{2}(h \u h').Definition qwand (Q

_{1}Q_{2}:val→hprop) : hprop :=fun h ⇒ ∀ v h', Fmap.disjoint h h' → Q

_{1}v h' → Q_{2}v (h \u h').Definition hor (H

_{1}H_{2}: hprop) : hprop :=fun h ⇒ H

_{1}h ∨ H_{2}h.Definition hand (H

_{1}H_{2}: hprop) : hprop :=fun h ⇒ H

_{1}h ∧ H_{2}h.End ReaminingOperatorsDirect.

Alternative definitions for the same operators, expressed in terms
of the core operators.

Module ReaminingOperatorsDerived.

Definition hpure (P:Prop) : hprop :=

\∃ (p:P), \[].

Definition hwand (H

\∃ H

Definition qwand (Q

\∀ v, (Q

Definition qwand' (Q

\∃ H

Definition hand (H

\∀ (b:bool), if b then H

Definition hor (H

\∃ (b:bool), if b then H

End ReaminingOperatorsDerived.

Definition hpure (P:Prop) : hprop :=

\∃ (p:P), \[].

Definition hwand (H

_{1}H_{2}: hprop) : hprop :=\∃ H

_{0}, H_{0}\* \[ (H_{1}\* H_{0}) ==> H_{2}].Definition qwand (Q

_{1}Q_{2}: val→hprop) : hprop :=\∀ v, (Q

_{1}v) \−∗ (Q_{2}v).Definition qwand' (Q

_{1}Q_{2}: val→hprop) : hprop := (* alternative *)\∃ H

_{0}, H_{0}\* \[ (Q_{1}\*+ H_{0}) ===> Q_{2}].Definition hand (H

_{1}H_{2}: hprop) : hprop :=\∀ (b:bool), if b then H

_{1}else H_{2}.Definition hor (H

_{1}H_{2}: hprop) : hprop :=\∃ (b:bool), if b then H

_{1}else H_{2}.End ReaminingOperatorsDerived.

In practice, it saves a lot of effort to use the derived definitions,
because using derived definitions all the properties of these definitions
can be established with the help of the xsimpl tactic, through reasoning
taking place exclusively at the level of hprop.

## Historical Notes

(* 2023-08-23 12:58 *)