# WandThe Magic Wand and Other Operators

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

- the disjunction, written hor H
_{1}H_{2}, - the non-separating conjunction, written hand H
_{1}H_{2}, - the "forall", named hforall, and written \∀ x, H,
- the "magic wand", named hwand, and written H
_{1}\−∗ H_{2}, - the "magic wand for postconditions", named qwand, and written
Q
_{1}\−−∗ Q_{2}.

- it is key to formulate the "ramified frame rule", a more practical rule for exploiting the frame and consequence properties,
- it will be used in the chapter WPgen to define a weakest-precondition generator,
- it can be useful to state the specifications for certain data structures.

- definition and properties of hand, hor, and hforall,
- definition and properties of the magic wand operator,
- generalization of the magic wand to postconditions,
- extension of the xsimpl tactic to handle the magic wand,
- statement and benefits of the ramified frame rule.

The heap predicate \∀ x, H holds of a heap h that, for any possibly
value of x, satisfies H. It may be puzzling at first what could possibly
be the use case for such a universal quantification. We will see several
examples through this chapter, in particular the encoding of the
non-separating conjunction (hand) and of the magic wand on postconditions
(qwand).
The predicate \∀ x, H stands for hforall (fun x ⇒ H), where the
definition of hforall follows the exact same pattern as for hexists.

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 ']'").
To follow through the rest of this chapter, it suffices to have in mind the
introduction and elimination rules for hforall.

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.

The lemma hforall_specialize 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 in a similar fashion as universal quantifiers appearing on 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.

End Hforall.

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.

End Hforall.

The heap predicate hor H
The disjunction operator does not appeared critically useful in practice,
because it can be encoded using Coq conditional construct, or using Coq
pattern matching. Nevertheless, there are situations where it proves handy.
The heap disjunction predicate admits a direct definition as a function over
heaps, written hor'.

_{1}H_{2}describes a heap that satisfies H_{1}or satifies H_{2}(possibly both). In other words, the heap predicate hor H_{1}H_{2}lifts the disjunction operator P_{1}∨ P_{2}from Prop to hprop .
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'._{1}holds, then hor H

_{1}H

_{2}holds; and, symmetrically, if H

_{2}holds, then hor H

_{1}H

_{2}holds.

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 asserts that if hor H

_{1}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 hor H_{1}H_{2}entails a heap predicate H_{3}, one must show both that H_{1}entails H_{3}, and that H_{2}entails H_{3}.
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 useful
to exploit the following lemma, called if_neg, for swapping the two
branches of a conditional by negating its 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.

☐

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

Prove that the representation predicate MList introduced in chapter Repr can be equivalently characterized using the predicate hor, as shown below. Hint: to prove this equivalence, do not attempt to unfold MList, but instead work using the equalities MList_nil and MList_cons.
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.

☐

The heap predicate hand H

_{1}H_{2}describes a heap that satisfies H_{1}and at the same time satifies H_{2}. In other words, the heap predicate hand H_{1}H_{2}lifts the disjunction operator P_{1}∧ P_{2}from Prop to hprop. The heap predicate hand admits a direct definition as a function over heaps.
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.

☐

### Definition of hwand

_{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 thinks 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}.

_{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}. The operator hwand, which implements the notation H

_{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 established further in this file, hwand and hwand' both 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, thereby conducting all the reasoning
at the level of hprop, rather than having to work with concrete heaps.

### Characteristic Equivalence for hwand

_{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 is provably equal to hwand._{1}\−∗ H_{2}from a state H_{0}. To establish that H_{0}entails H_{1}\−∗ H_{2}, one has to show that the conjunction of H_{0}and 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.

### Other 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.

Let's now study the interaction of hwand with hempty and hpure.
The heap predicate \[] \−∗ H is equivalent to H. Intuitively, one can
rewrite -0+H as +H.

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:

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

Prove hwand_hpure_l, whose statement appears below._{2}, it suffices to prove that this heap satisfies H

_{2}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.

☐

_{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

_{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}). One way to read this: "if you own H_{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.

The reciprocal entailment is false: H

_{1}\−∗ (H_{2}\* H_{3}) does not entail (H_{1}\−∗ H_{2}) \* H_{3}. To see why, instantiate H_{1}with \[False]. The predicate H_{1}\−∗ (H_{2}\* H_{3}) is equivalent to True, hence imposes no restriction on the heap. Yet, to establish (H_{1}\−∗ H_{2}) \* H_{3}, one would need to exhibit a piece of heap satisfiying H_{3}.#### 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: use xsimpl.

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.

☐

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

Prove the following inversion lemma for hwand. This lemma essentially captures the fact that hwand entails the alternative definition named 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.

☐

In what follows, we generalize the magic wand to operate on postconditions,
introducing a heap predicate of the form Q
The first possibility is to follow the same pattern as for hwand, that is,
to quantify some heap predicate H

_{1}\−−∗ Q_{2}, of type hprop. Note that the magic wand between two postconditions produces a heap predicate, and not a postcondition. There are two ways to define the operator qwand._{0}such that H_{0}starred with Q_{1}yields Q_{2}.
Definition qwand' (Q

\∃ H

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

_{0}, H_{0}\* \[ Q_{1}\*+ H_{0}===> Q_{2}].
The second possibility is to define qwand on top of hwand, by means of
the hforall quantifier.

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).
As established further on in this chapter, qwand and qwand' both define
the same operator. We prefer taking qwand as definition because in
practice instantiating the universal quantifier is the most useful way to
exploit a magic wand between postconditions. This specialization operation
is formalized next. This result is a direct consequence of the
specialization result for \∀.

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.

The predicate qwand satisfies numerous properties that are the direct
counterpart of the properties on hwand. First, qwand satisfies a
characteristic equivalence rule.

Lemma qwand_equiv : ∀ H Q

H ==> (Q

↔ (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.

Second, qwand satisfies a cancellation rule.

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.

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

Fourht 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.

☐

## Automation with xsimpl for hwand Expressions

The tactic 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 simplified into 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 simplified into (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 simplify the conjunction of Q

_{1}\−−∗ Q_{2}and Q_{1}v into 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.

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 in terms of the core operators
defined above.

Module ReaminingOperatorsDerived.

Definition hpure (P:Prop) : hprop :=

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

Definition hand (H

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

Definition hor (H

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

Definition hwand (H

\∃ H

Definition qwand (Q

\∀ v, (Q

End ReaminingOperatorsDerived.

Definition hpure (P:Prop) : hprop :=

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

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}.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).End ReaminingOperatorsDerived.

Note: these derived operators could also be defined directly as predicate
over heaps. The definitions are shown below. Establishing properties of such
low-level definitions requires more effort than establishing properties for
the derived definitions shown above. Indeed, when operators are defined as
derived operations, their properties may be established with help of the
powerful entailment simplification tactic xsimpl.

Module ReaminingOperatorsDirect.

Definition hpure (P:Prop) : hprop :=

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

Definition hor (H

fun h ⇒ H

Definition hand (H

fun h ⇒ H

Definition hwand (H

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

Definition qwand (Q

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

End ReaminingOperatorsDirect.

End SummaryHprop.

Definition hpure (P:Prop) : hprop :=

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

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.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').End ReaminingOperatorsDirect.

End SummaryHprop.

Recall the consequence-frame rule, which is pervasively used for example by
the tactic xapp for reasoning about applications.

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

_{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}. This replacement premise is H ==> H_{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). This merge of the two entailments leads us to the statement of the "ramified frame rule" shown below.
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.

## Benefits of the Ramified 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, once again, 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

_{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}. 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.
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 RamifiedFrame.

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 RamifiedFrame.

The entailment \[] ==> (H \−∗ H) holds for any H. However, the
symmetrical entailement (H \−∗ H) ==> \[] is false. For a counterexample,
instantiate H as \[False]. Any heap satisfies \[False] \−∗ \[False].
Yet, only the empty heap satisfies \[].

Lemma himpl_hwand_same_hempty_counterexample :

¬ (∀ H, (H \−∗ H) ==> \[]).

Proof using.

rew_logic. (* rewrite "not forall" as "exists not" *)

∃ \[False]. intros M.

lets (h,Hh): (@Fmap.exists_not_empty val _).

forwards K: M h.

{ applys* himpl_hwand_r (fun h ⇒ h ≠ Fmap.empty). unfolds loc. xsimpl*. }

lets: hempty_inv K. unfolds loc. false.

Qed.

¬ (∀ H, (H \−∗ H) ==> \[]).

Proof using.

rew_logic. (* rewrite "not forall" as "exists not" *)

∃ \[False]. intros M.

lets (h,Hh): (@Fmap.exists_not_empty val _).

forwards K: M h.

{ applys* himpl_hwand_r (fun h ⇒ h ≠ Fmap.empty). unfolds loc. xsimpl*. }

lets: hempty_inv K. unfolds loc. false.

Qed.

As another tempting yet false property of the magic wand, consider the
reciprocal entailment to the cancellation lemma, that is,
H

_{2}==> H_{1}\* (H_{1}\−∗ H_{2}). It does not hold in general. As counter-example, consider H_{2}= \[] and H_{1}= \[False]. The empty heap satisfies the left-hand side of the entailment, yet it does does not satisfy \[False] \* (\[False] \−∗ \[]), because there is no way to establish False out of thin air.
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

_{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". On the contrary, the reciprocal entailment (H_{1}\−∗ H_{3}) ==> (H_{1}\−∗ H_{2}) \* (H_{2}\−∗ H_{3}) is false. Intuitively, from H_{1}≤ H_{3}there is no way to justify H_{1}≤ H_{2}nor H_{2}≤ H_{3}.
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. The reader needs not
follow through the details of these proofs.

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

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})).
Here again, we show proofs for the reference, but the reader needs not
follow through the details.

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.

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.

## Historical Notes

(* 2024-01-03 14:19 *)