# HimplHeap Entailment

Set Implicit Arguments.

From SLF Require LibSepReference.

From SLF Require Export Hprop.

From SLF Require LibSepReference.

From SLF Require Export Hprop.

Implicit Types

Implicit Types P : Prop.

Implicit Types H : hprop.

Implicit Types Q : val→hprop.

Implicit Types H : hprop.

Implicit Types Q : val→hprop.

# First Pass

_{1}==> H

_{2}, asserts that any heap that satisfies H

_{1}also satisfies H

_{2}.

_{1}===> Q

_{2}to asserts that, for any result value v, the entailment Q

_{1}v ==> Q

_{2}v holds.

Lemma triple_conseq : ∀ t H Q H' Q',

triple t H' Q' →

H ==> H' →

Q' ===> Q →

triple t H Q.

- the formal definition of the entailment relations,
- the fundamental properties of the Separation Logic operators: these properties are expressed either as entailments, or as equalities, which denote symmetric entailments,
- the 4 structural rules of Separation Logic: the rule of consequence, the frame rule (which can be combined with the rule of consequence), and the extractions rules for pure facts and for quantifiers,
- the tactics xsimpl and xchange that are critically useful for manipulating entailments in practice,
- (optional) details on how to prove the fundamental properties and the structural rules.

## Definition of Entailment

_{1}==> H

_{2}asserts that any heap h that satisfies the heap predicate H

_{1}also satisfies the heap predicate H

_{2}.

Definition himpl (H

∀ (h:heap), H

Notation "H

_{1}H_{2}:hprop) : Prop :=∀ (h:heap), H

_{1}h → H_{2}h.Notation "H

_{1}==> H_{2}" := (himpl H_{1}H_{2}) (at level 55).
H
As we show next, the entailment relation is reflexive, transitive,
and antisymmetric. It thus forms an order relation on heap predicates.

_{1}==> H_{2}captures the fact that H_{1}is a stronger precondition than H_{2}, in the sense that it is more restrictive.
Lemma himpl_refl : ∀ H,

H ==> H.

Proof using. intros h. hnf. auto. Qed.

Lemma himpl_trans : ∀ H

(H

(H

(H

Proof using. introv M

H ==> H.

Proof using. intros h. hnf. auto. Qed.

Lemma himpl_trans : ∀ H

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

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

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

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

_{1}M_{2}. intros h H1h. eauto. Qed.#### Exercise: 1 star, standard, especially useful (himpl_antisym)

Prove the antisymmetry of entailment result shown below using extensionality for heap predicates, as captured by lemma predicate_extensionality (or lemma hprop_eq) introduced in the previous chapter (Hprop).
Lemma himpl_antisym : ∀ H

(H

(H

H

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

☐

_{1}H_{2},(H

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

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

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

☐

_{1}\* H

_{2}) = (H

_{2}\* H

_{1}) by proving that each side entails the other side, that is, by proving (H

_{1}\* H

_{2}) ==> (H

_{2}\* H

_{1}) and (H

_{2}\* H

_{1}) ==> (H

_{1}\* H

_{2}).

## Entailment for Postconditions

_{1}===> Q

_{2}, which asserts that for any value v, the heap predicate Q

_{1}v entails Q

_{2}v.

Definition qimpl (Q

∀ (v:val), Q

Notation "Q

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

_{1}v ==> Q_{2}v.Notation "Q

_{1}===> Q_{2}" := (qimpl Q_{1}Q_{2}) (at level 55).
Remark: equivalently, Q
Entailment on postconditions also forms an order relation:
it is reflexive, transitive, and antisymmetric.

_{1}===> Q_{2}holds if for any value v and any heap h, the proposition Q_{1}v h implies Q_{2}v h.
Lemma qimpl_refl : ∀ Q,

Q ===> Q.

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

Lemma qimpl_trans : ∀ Q

(Q

(Q

(Q

Proof using. introv M

Lemma qimpl_antisym : ∀ Q

(Q

(Q

(Q

Proof using.

introv M

intros v. applys himpl_antisym; eauto.

Qed.

Q ===> Q.

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

Lemma qimpl_trans : ∀ Q

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

_{1}===> Q_{2}) →(Q

_{2}===> Q_{3}) →(Q

_{1}===> Q_{3}).Proof using. introv M

_{1}M_{2}. intros v. applys himpl_trans; eauto. Qed.Lemma qimpl_antisym : ∀ Q

_{1}Q_{2},(Q

_{1}===> Q_{2}) →(Q

_{2}===> Q_{1}) →(Q

_{1}= Q_{2}).Proof using.

introv M

_{1}M_{2}. apply functional_extensionality.intros v. applys himpl_antisym; eauto.

Qed.

## Fundamental Properties of Separation Logic Operators

Parameter hstar_assoc : ∀ H

(H

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

_{1}\* H_{2}) \* H_{3}= H_{1}\* (H_{2}\* H_{3}).
(2) The star operator is commutative.

Parameter hstar_comm : ∀ H

H

_{1}H_{2},H

_{1}\* H_{2}= H_{2}\* H_{1}.
(3) The empty heap predicate is a neutral for the star.
Because star is commutative, it is equivalent to state that
hempty is a left or a right neutral for hstar.
We chose, arbitrarily, to state the left-neutral property.

Parameter hstar_hempty_l : ∀ H,

\[] \* H = H.

\[] \* H = H.

(4) Existentials can be "extruded" out of stars, that is:
(\∃ x, J x) \* H is equivalent to \∃ x, (J x \* H).

Parameter hstar_hexists : ∀ A (J:A→hprop) H,

(\∃ x, J x) \* H = \∃ x, (J x \* H).

(\∃ x, J x) \* H = \∃ x, (J x \* H).

(5) The star operator is "monotone" with respect to entailment, meaning
that if H
Viewed the other way around, if we have to prove the entailment relation
(H
Here again, due to commutativity of star, it only suffices to state
the left version of the monotonicity property.

_{1}==> H_{1}' then (H_{1}\* H_{2}) ==> (H_{1}' \* H_{2})._{1}\* H_{2}) ==> (H_{1}' \* H_{2}), we can "cancel out" H_{2}on both sides. In this view, the monotonicity property is a sort of "frame rule for the entailment relation".
Parameter himpl_frame_l : ∀ H

H

(H

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

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

_{1}\* H_{2}) ==> (H_{1}' \* H_{2}).#### Exercise: 1 star, standard, especially useful (hstar_comm_assoc)

The commutativity and associativity results combine into one result that is sometimes convenient to exploit in proofs.
Lemma hstar_comm_assoc : ∀ H

H

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

☐

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

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

☐

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

The monotonicity property of the star operator w.r.t. entailment can also be stated in a symmetric fashion, as shown next. Prove this result. Hint: exploit the transitivity of entailment (himpl_trans) and the asymmetric monotonicity result (himpl_frame_l).
Lemma himpl_frame_r : ∀ H

H

(H

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

☐

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

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

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

☐

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

The monotonicity property of the star operator w.r.t. entailment can also be stated in a symmetric fashion, as shown next. Prove this result. Hint: exploit the transitivity of entailment (himpl_trans) and the asymmetric monotonicity result (himpl_frame_l).
Lemma himpl_frame_lr : ∀ H

H

H

(H

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

☐

_{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. (* FILL IN HERE *) Admitted.

☐

## Introduction and Elimination Rules w.r.t. Entailments

#### Exercise: 2 stars, standard, especially useful (himpl_hstar_hpure_r).

Prove the rule himpl_hstar_hpure_r. Hint: recall from Hprop the lemma hstar_hpure_l, which asserts the equality (\[P] \* H) h = (P ∧ H h).
Lemma himpl_hstar_hpure_r : ∀ P H H',

P →

(H ==> H') →

H ==> (\[P] \* H').

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

☐

P →

(H ==> H') →

H ==> (\[P] \* H').

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

☐

#### Exercise: 2 stars, standard, especially useful (himpl_hstar_hpure_l).

Prove the rule himpl_hstar_hpure_l.
Lemma himpl_hstar_hpure_l : ∀ (P:Prop) (H H':hprop),

(P → H ==> H') →

(\[P] \* H) ==> H'.

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

☐

(P → H ==> H') →

(\[P] \* H) ==> H'.

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

☐

#### Exercise: 2 stars, standard, especially useful (himpl_hexists_r).

Prove the rule himpl_hexists_r.
Lemma himpl_hexists_r : ∀ A (x:A) H J,

(H ==> J x) →

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

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

☐

(H ==> J x) →

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

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

☐

#### Exercise: 2 stars, standard, especially useful (himpl_hexists_l).

Prove the rule himpl_hexists_l.
Lemma himpl_hexists_l : ∀ (A:Type) (H:hprop) (J:A→hprop),

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

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

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

☐

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

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

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

☐

## Extracting Information from Heap Predicates

_{1}) \* (p ~~> v

_{2}) describes two "disjoint" cells that are both "at location p", one can extract a contradiction.

Lemma hstar_hsingle_same_loc : ∀ (p:loc) (v

(p ~~> v

_{1}v_{2}:val),(p ~~> v

_{1}) \* (p ~~> v_{2}) ==> \[False].
The proof of this result exploits a result on finite maps.
Essentially, the domain of a single singleton map that binds
a location p to some value is the singleton set \{p}, thus
such a singleton map cannot be disjoint from another singleton
map that binds the same location p.

Check disjoint_single_single_same_inv : ∀ (p:loc) (v

Fmap.disjoint (Fmap.single p v

False.
Using this lemma, we can prove hstar_hsingle_same_loc
by unfolding the definition of hstar to reveal the
contradiction on the disjointness assumption.

Check disjoint_single_single_same_inv : ∀ (p:loc) (v

_{1}v_{2}:val),Fmap.disjoint (Fmap.single p v

_{1}) (Fmap.single p v_{2}) →False.

Proof using.

intros. unfold hsingle. intros h (h

subst. applys Fmap.disjoint_single_single_same_inv D.

Qed.

intros. unfold hsingle. intros h (h

_{1}&h_{2}&E_{1}&E_{2}&D&E). false.subst. applys Fmap.disjoint_single_single_same_inv D.

Qed.

More generally, a heap predicate of the form H \* H is generally
suspicious in Separation Logic. In (the simplest variant of) Separation
Logic, such a predicate can only be satisfied if H covers no memory
cell at all, that is, if H is a pure predicate of the form \[P]
for some proposition P.

## Consequence, Frame, and their Combination

Parameter triple_conseq : ∀ t H Q H' Q',

triple t H' Q' →

H ==> H' →

Q' ===> Q →

triple t H Q.

triple t H' Q' →

H ==> H' →

Q' ===> Q →

triple t H Q.

Recall the frame rule introduced in the previous chapter.

Parameter triple_frame : ∀ t H Q H',

triple t H Q →

triple t (H \* H') (Q \*+ H').

triple t H Q →

triple t (H \* H') (Q \*+ H').

Observe that, stated as such, it is very unlikely for the frame rule
to be applicable in practice, because the precondition must be exactly
of the form H \* H' and the postcondition exactly of the form
Q \*+ H', for some H'. For example, the frame rule would not apply
to a proof obligation of the form triple t (H' \* H) (Q \*+ H'),
simply because H' \* H does not match H \* H'.
This limitation of the frame rule can be addressed by combining the frame
rule with the rule of consequence into a single rule, called the
"consequence-frame rule". This rule, shown below, enables deriving
a triple from another triple, without any restriction on the exact
shape of the precondition and postcondition of the two triples involved.

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

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

Prove the combined consequence-frame rule.
Proof using. (* FILL IN HERE *) Admitted.

☐

☐

## The Extraction Rules for Triples

Parameter triple_hpure : ∀ t (P:Prop) H Q,

(P → triple t H Q) →

triple t (\[P] \* H) Q.

(P → triple t H Q) →

triple t (\[P] \* H) Q.

A judgment of the form triple t (\∃ x, J x) Q is equivalent
to ∀ x, triple t (J x) Q. This structural rule is called
triple_hexists and formalized as shown below. It captures the
extraction of an existential quantifier out of the precondition
of a triple, in a similar way as himpl_hexists_l for entailments.

Parameter triple_hexists : ∀ t (A:Type) (J:A→hprop) Q,

(∀ x, triple t (J x) Q) →

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

(∀ x, triple t (J x) Q) →

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

Module XsimplTactic.

Import LibSepReference.

Notation "'hprop''" := (Hprop.hprop).

Import LibSepReference.

Notation "'hprop''" := (Hprop.hprop).

Module CaseStudy.

Implicit Types p q : loc.

Implicit Types n m : int.

End CaseStudy.

Implicit Types p q : loc.

Implicit Types n m : int.

End CaseStudy.

Module EntailmentProofs.

Implicit Types p : loc.

Implicit Types n : int.

Implicit Types p : loc.

Implicit Types n : int.

Proving an entailment by hand is generally a tedious task. This is why
most Separation Logic based framework include an automated tactic for
simplifying entailments. In this course, the relevant tactic is named
xsimpl. Further in this chapter, we describe by means of examples the
behavior of this tactic. But in order to best appreciate what the tactic
provides and best understand how it works, it is very useful to complete
a few proofs by hand.

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

Prove the example entailment below. Hint: exploit hstar_comm, hstar_assoc, or hstar_comm_assoc which combines the two, and exploit himpl_frame_l or himpl_frame_r to cancel out matching pieces.
Lemma himpl_example_1 : ∀ p

p

==> p

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

☐

_{1}p_{2}p_{3}p_{4},p

_{1}~~> 6 \* p_{2}~~> 7 \* p_{3}~~> 8 \* p_{4}~~> 9==> p

_{4}~~> 9 \* p_{3}~~> 8 \* p_{2}~~> 7 \* p_{1}~~> 6.Proof using. (* FILL IN HERE *) Admitted.

☐

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

Prove the example entailment below. Hint: use himpl_hstar_hpure_r to extract pure facts, once they appear at the head of the left-hand side of the entailment.
Lemma himpl_example_2 : ∀ p

p

==> p

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

☐

_{1}p_{2}p_{3}n,p

_{1}~~> 6 \* \[n > 0] \* p_{2}~~> 7 \* \[n < 0]==> p

_{3}~~> 8.Proof using. (* FILL IN HERE *) Admitted.

☐

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

Prove the example entailment below. Hint: use lemmas among himpl_hexists_r, himpl_hexists_l, himpl_hstar_hpure_r and himpl_hstar_hpure_r to deal with pure facts and quantifiers.
Lemma himpl_example_3 : ∀ p,

\∃ n, p ~~> n \* \[n > 0]

==> \∃ n, \[n > 1] \* p ~~> (n-1).

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

☐

\∃ n, p ~~> n \* \[n > 0]

==> \∃ n, \[n > 1] \* p ~~> (n-1).

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

☐

End EntailmentProofs.

## The xsimpl Tactic

### xsimpl to Extract Pure Facts and Quantifiers in LHS

Lemma xsimpl_demo_lhs_hpure : ∀ H

H

Proof using.

intros. xsimpl. intros Hn.

Abort.

_{1}H_{2}H_{3}H_{4}(n:int),H

_{1}\* H_{2}\* \[n > 0] \* H_{3}==> H_{4}.Proof using.

intros. xsimpl. intros Hn.

Abort.

In case the LHS includes a contradiction, such as the pure fact
False, the goal gets solved immediately by xsimpl.

Lemma xsimpl_demo_lhs_hpure : ∀ H

H

Proof using.

intros. xsimpl.

Qed.

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

_{1}\* H_{2}\* \[False] \* H_{3}==> H_{4}.Proof using.

intros. xsimpl.

Qed.

The xsimpl tactic also extracts existential quantifier from the LHS.
It turns them into universally quantified variables outside of the
entailment relation, as illustrated through the following example.

Lemma xsimpl_demo_lhs_hexists : ∀ H

H

Proof using.

intros. xsimpl. intros n.

Abort.

_{1}H_{2}H_{3}H_{4}(p:loc),H

_{1}\* \∃ (n:int), (p ~~> n \* H_{2}) \* H_{3}==> H_{4}.Proof using.

intros. xsimpl. intros n.

Abort.

A call to xsimpl, or to its degraded version xpull, extract at once
all the pure facts and quantifiers from the LHS, as illustrated next.

Lemma xsimpl_demo_lhs_several : ∀ H

H

Proof using.

intros.

xsimpl. (* or xpull *)

intros n Hn Hp.

Abort.

_{1}H_{2}H_{3}H_{4}(p q:loc),H

_{1}\* \∃ (n:int), (p ~~> n \* \[n > 0] \* H_{2}) \* \[p ≠ q] \* H_{3}==> H_{4}.Proof using.

intros.

xsimpl. (* or xpull *)

intros n Hn Hp.

Abort.

### xsimpl to Cancel Out Heap Predicates from LHS and RHS

_{2}occurs on both sides, so it is canceled out by xsimpl.

Lemma xsimpl_demo_cancel_one : ∀ H

H

Proof using.

intros. xsimpl.

Abort.

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

_{1}\* H_{2}\* H_{3}\* H_{4}==> H_{5}\* H_{6}\* H_{2}\* H_{7}.Proof using.

intros. xsimpl.

Abort.

xsimpl actually cancels out at once all the heap predicates that it
can spot appearing on both sides. In the example below, H

_{2}, H_{3}, and H_{4}are canceled out.
Lemma xsimpl_demo_cancel_many : ∀ 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_{4}\* H_{3}\* H_{5}\* H_{2}.Proof using.

intros. xsimpl.

Abort.

If all the pieces of heap predicate get canceled out, the remaining
proof obligation is \[] ==> \[]. In this case, xsimpl automatically
solves the goal by invoking the reflexivity property of entailment.

Lemma xsimpl_demo_cancel_all : ∀ H

H

Proof using.

intros. xsimpl.

Qed.

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

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

intros. xsimpl.

Qed.

### xsimpl to Instantiate Pure Facts and Quantifiers in RHS

Lemma xsimpl_demo_rhs_hpure : ∀ H

H

Proof using.

intros. xsimpl.

Abort.

_{1}H_{2}H_{3}(n:int),H

_{1}==> H_{2}\* \[n > 0] \* H_{3}.Proof using.

intros. xsimpl.

Abort.

When it encounters an existential quantifier in the RHS, the xsimpl
tactic introduces a unification variable denoted by a question mark,
that is, an "evar", in Coq terminology. In the example below, the xsimpl
tactic turns \∃ n, .. p ~~> n .. into .. p ~~> ?x ...

Lemma xsimpl_demo_rhs_hexists : ∀ H

H

Proof using.

intros. xsimpl.

Abort.

_{1}H_{2}H_{3}H_{4}(p:loc),H

_{1}==> H_{2}\* \∃ (n:int), (p ~~> n \* H_{3}) \* H_{4}.Proof using.

intros. xsimpl.

Abort.

The "evar" often gets subsequently instantiated as a result of
a cancellation step. For example, in the example below, xsimpl
instantiates the existentially quantified variable n as ?x,
then cancels out p ~~> ?x from the LHS against p ~~> 3 on
the right-hand-side, thereby unifying ?x with 3.

Lemma xsimpl_demo_rhs_hexists_unify : ∀ H

H

Proof using.

intros. xsimpl.

Abort.

_{1}H_{2}H_{3}H_{4}(p:loc),H

_{1}\* (p ~~> 3) ==> H_{2}\* \∃ (n:int), (p ~~> n \* H_{3}) \* H_{4}.Proof using.

intros. xsimpl.

Abort.

The instantiation of the evar ?x can be observed if there is
another occurrence of the same variable in the entailment.
In the next example, which refines the previous one, observe how
n > 0 becomes 3 > 0.

Lemma xsimpl_demo_rhs_hexists_unify_view : ∀ H

H

Proof using.

intros. xsimpl.

Abort.

_{1}H_{2}H_{4}(p:loc),H

_{1}\* (p ~~> 3) ==> H_{2}\* \∃ (n:int), (p ~~> n \* \[n > 0]) \* H_{4}.Proof using.

intros. xsimpl.

Abort.

(Advanced.) In some cases, it is desirable to provide an explicit value
for instantiating an existential quantifier that occurs in the RHS.
The xsimpl tactic accepts arguments, which will be used to instantiate
the existentials (on a first-match basis). The syntax is xsimpl v

_{1}.. vn, or xsimpl (>> v_{1}.. vn) in the case n > 3.
Lemma xsimpl_demo_rhs_hints : ∀ H

H

Proof using.

intros. xsimpl 3 4.

Abort.

_{1}(p q:loc),H

_{1}==> \∃ (n m:int), (p ~~> n \* q ~~> m).Proof using.

intros. xsimpl 3 4.

Abort.

(Advanced.) If two existential quantifiers quantify variables of the same
type, it is possible to provide a value for only the second quantifier
by passing as first argument to xsimpl the special value __.
The following example shows how, on LHS of the form \∃ n m, ...,
the tactic xsimpl __ 4 instantiates m with 4 while leaving n
as an unresolved evar.

Lemma xsimpl_demo_rhs_hints_evar : ∀ H

H

Proof using.

intros. xsimpl __ 4.

Abort.

_{1}(p q:loc),H

_{1}==> \∃ (n m:int), (p ~~> n \* q ~~> m).Proof using.

intros. xsimpl __ 4.

Abort.

### xsimpl on Entailments Between Postconditions

_{1}===> Q

_{2}.

Lemma qimpl_example_1 : ∀ (Q

Q

Proof using. intros. xsimpl. intros r. Abort.

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

_{1}\*+ H_{2}===> Q_{2}\*+ H_{2}\*+ H_{3}.Proof using. intros. xsimpl. intros r. Abort.

Lemma himpl_example_1 : ∀ (p:loc),

p ~~> 3 ==>

\∃ (n:int), p ~~> n.

Proof using. xsimpl. Qed.

Lemma himpl_example_2 : ∀ (p q:loc),

p ~~> 3 \* q ~~> 3 ==>

\∃ (n:int), p ~~> n \* q ~~> n.

Proof using. xsimpl. Qed.

Lemma himpl_example_4 : ∀ (p:loc),

\∃ (n:int), p ~~> n ==>

\∃ (m:int), p ~~> (m + 1).

Proof using.

intros. (* observe that xsimpl here does not work well. *)

xpull. intros n. xsimpl (n-1).

replace (n-1+1) with n. { auto. } { math. }

(* variant for the last line:

applys_eq himpl_refl. fequal. math. *)

Qed.

Lemma himpl_example_5 : ∀ (H:hprop),

\[False] ==> H.

Proof using. xsimpl. Qed.

p ~~> 3 ==>

\∃ (n:int), p ~~> n.

Proof using. xsimpl. Qed.

Lemma himpl_example_2 : ∀ (p q:loc),

p ~~> 3 \* q ~~> 3 ==>

\∃ (n:int), p ~~> n \* q ~~> n.

Proof using. xsimpl. Qed.

Lemma himpl_example_4 : ∀ (p:loc),

\∃ (n:int), p ~~> n ==>

\∃ (m:int), p ~~> (m + 1).

Proof using.

intros. (* observe that xsimpl here does not work well. *)

xpull. intros n. xsimpl (n-1).

replace (n-1+1) with n. { auto. } { math. }

(* variant for the last line:

applys_eq himpl_refl. fequal. math. *)

Qed.

Lemma himpl_example_5 : ∀ (H:hprop),

\[False] ==> H.

Proof using. xsimpl. Qed.

## The xchange Tactic

_{1}\* H

_{2}\* H

_{3}==> H

_{4}. Assume an entailment assumption M, say H

_{2}==> H

_{2}'. Then xchange M turns the goal into H

_{1}\* H

_{2}' \* H

_{3}==> H

_{4}, effectively replacing H

_{2}with H

_{2}'.

Lemma xchange_demo_base : ∀ H

H

H

Proof using.

introv M. xchange M.

(* Note that freshly produced items appear to the front *)

Abort.

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

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

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

introv M. xchange M.

(* Note that freshly produced items appear to the front *)

Abort.

The tactic xchange can also take as argument equalities.
The tactic xchange M exploits the left-to-right direction of an
equality M, whereas xchange <- M exploits the right-to-left
direction .

Lemma xchange_demo_eq : ∀ H

H

H

Proof using.

introv M. xchange M.

xchange <- M.

Abort.

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

_{1}\* H_{3}= H_{5}→H

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

introv M. xchange M.

xchange <- M.

Abort.

The tactic xchange M does accept a lemma or hypothesis M
featuring universal quantifiers, as long as its conclusion
is an equality or an entailment. In such case, xchange M
instantiates M before attemting to perform a replacement.

Lemma xchange_demo_inst : ∀ H

(∀ n, J n = J' (n+1)) →

H

Proof using.

introv M. xchange M.

(* Note that freshly produced items appear to the front *)

Abort.

_{1}(J J':int→hprop) H_{3}H_{4},(∀ n, J n = J' (n+1)) →

H

_{1}\* J 3 \* H_{3}==> H_{4}.Proof using.

introv M. xchange M.

(* Note that freshly produced items appear to the front *)

Abort.

How does the xchange tactic work? Consider a goal of the form H ==> H'
and assume xchange is invoked with an hypothesis of type H

_{1}==> H_{1}' as argument. The tactic xchange should attempt to decompose H as the star of H_{1}and the rest of H, call it H_{2}. If it succeeds, then the goal H ==> H' can be rewritten as H_{1}\* H_{2}==> H'. To exploit the hypothesis H_{1}==> H_{1}', the tactic should replace the goal with the entailment H_{1}' \* H_{2}==> H'. The lemma shown below captures this piece of reasoning implemented by the tactic xchange.#### Exercise: 2 stars, standard, especially useful (xchange_lemma)

Prove, without using the tactic xchange, the following lemma which captures the internal working of xchange.
Lemma xchange_lemma : ∀ H

H

H ==> H

H

H ==> H'.

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

☐

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

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

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

_{1}' \* H_{2}==> H' →H ==> H'.

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

☐

End XsimplTactic.

Module FundamentalProofs.

We next show the details of the proofs establishing the fundamental
properties of the Separation Logic operators.
Note that all these results must be proved without help of the tactic
xsimpl, because the implementation of the tactic xsimpl itself
depends on these fundamental properties.
We begin with the frame property, which is the simplest to prove.

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

Prove the frame property for entailment. Hint: unfold the definition of hstar.
Lemma himpl_frame_l : ∀ H

H

(H

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

☐

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

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

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

☐

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

Prove the lemma himpl_frame_r, symmetric to himpl_frame_l.
Lemma himpl_frame_r : ∀ H

H

(H

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

☐

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

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

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

☐

_{1}\* \∃ x, H

_{2}and \∃ x, H

_{1}\* H

_{2}.

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

(\∃ x, J x) \* H = \∃ x, (J x \* H).

Proof using.

intros. applys himpl_antisym.

{ intros h (h

{ intros h (x&M). destruct M as (h

splits¬. ∃* x. }

Qed.

(\∃ x, J x) \* H = \∃ x, (J x \* H).

Proof using.

intros. applys himpl_antisym.

{ intros h (h

_{1}&h_{2}&M_{1}&M_{2}&D&U). destruct M_{1}as (x&M_{1}). ∃* x h_{1}h_{2}. }{ intros h (x&M). destruct M as (h

_{1}&h_{2}&M_{1}&M_{2}&D&U). ∃ h_{1}h_{2}.splits¬. ∃* x. }

Qed.

There remains to establish the commutativity and associativity of the star
operator, and the fact that the empty heap predicate is its neutral element.
To establish these properties, we need to exploit a few basic facts about
finite maps. We introduce them as we go along.
To prove the commutativity of the star operator, i.e. H

_{1}\* H_{2}= H_{2}\* H_{1}, it is sufficient to prove the entailement in one direction, e.g., H_{1}\* H_{2}==> H_{2}\* H_{1}. Indeed, the other other direction is symmetrical. The symmetry argument is captured by the following lemma, which we will exploit in the proof of hstar_comm.
Lemma hprop_op_comm : ∀ (op:hprop→hprop→hprop),

(∀ H

(∀ H

Proof using. introv M. intros. applys himpl_antisym; applys M. Qed.

(∀ H

_{1}H_{2}, op H_{1}H_{2}==> op H_{2}H_{1}) →(∀ H

_{1}H_{2}, op H_{1}H_{2}= op H_{2}H_{1}).Proof using. introv M. intros. applys himpl_antisym; applys M. Qed.

To prove commutativity of star, we need to exploit the fact that the union
of two finite maps with disjoint domains commutes. This fact is captured
by the following lemma.

Check Fmap.union_comm_of_disjoint : ∀ h

Fmap.disjoint h

h
The commutativity result is then proved as follows. Observe the use of
the lemma hprop_op_comm, which allows establishing the entailment in
only one of the two directions.

Check Fmap.union_comm_of_disjoint : ∀ h

_{1}h_{2},Fmap.disjoint h

_{1}h_{2}→h

_{1}\u h_{2}= h_{2}\u h_{1}.
Lemma hstar_comm : ∀ H

H

Proof using.

applys hprop_op_comm. intros. intros h (h

subst. splits¬. { rewrite Fmap.union_comm_of_disjoint; auto. }

Qed.

_{1}H_{2},H

_{1}\* H_{2}= H_{2}\* H_{1}.Proof using.

applys hprop_op_comm. intros. intros h (h

_{1}&h_{2}&M_{1}&M_{2}&D&U). ∃ h_{2}h_{1}.subst. splits¬. { rewrite Fmap.union_comm_of_disjoint; auto. }

Qed.

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

Prove that the empty heap predicate is a neutral element for the star. You will need to exploit the fact that the union with an empty map is the identity, as captured by lemma Fmap.union_empty_l.Check Fmap.union_empty_l : ∀ h,

Fmap.empty \u h = h.

Lemma hstar_hempty_l : ∀ H,

\[] \* H = H.

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

☐

\[] \* H = H.

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

☐

Lemma hstar_hempty_r : ∀ H,

H \* \[] = H.

Proof using.

intros. rewrite hstar_comm. rewrite hstar_hempty_l. auto.

Qed.

H \* \[] = H.

Proof using.

intros. rewrite hstar_comm. rewrite hstar_hempty_l. auto.

Qed.

Associativity of star is the most tedious result to derive.
We need to exploit the associativity of union on finite maps,
as well as lemmas about the disjointness of a map with the
result of the union of two maps.

Check Fmap.union_assoc : ∀ h

(h

Check Fmap.disjoint_union_eq_l : ∀ h

Fmap.disjoint (h

= (Fmap.disjoint h

Check Fmap.disjoint_union_eq_r : ∀ h

Fmap.disjoint h

= (Fmap.disjoint h

Check Fmap.union_assoc : ∀ h

_{1}h_{2}h_{3},(h

_{1}\u h_{2}) \u h_{3}= h_{1}\u (h_{2}\u h_{3}).Check Fmap.disjoint_union_eq_l : ∀ h

_{1}h_{2}h_{3},Fmap.disjoint (h

_{2}\u h_{3}) h_{1}= (Fmap.disjoint h

_{1}h_{2}∧ Fmap.disjoint h_{1}h_{3}).Check Fmap.disjoint_union_eq_r : ∀ h

_{1}h_{2}h_{3},Fmap.disjoint h

_{1}(h_{2}\u h_{3})= (Fmap.disjoint h

_{1}h_{2}∧ Fmap.disjoint h_{1}h_{3}).#### Exercise: 1 star, standard, optional (hstar_assoc)

Complete the right-to-left part of the proof of associativity of the star operator.
Lemma hstar_assoc : ∀ H

(H

Proof using.

intros. applys himpl_antisym.

{ intros h (h'&h

subst h'. rewrite Fmap.disjoint_union_eq_l in D.

∃ h

{ applys M

{ ∃* h

{ rewrite* @Fmap.disjoint_union_eq_r. }

{ rewrite* @Fmap.union_assoc in U. } }

(* FILL IN HERE *) Admitted.

☐

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

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

intros. applys himpl_antisym.

{ intros h (h'&h

_{3}&M_{1}&M_{2}&D&U). destruct M_{1}as (h_{1}&h_{2}&M_{3}&M_{4}&D'&U').subst h'. rewrite Fmap.disjoint_union_eq_l in D.

∃ h

_{1}(h_{2}\u h_{3}). splits.{ applys M

_{3}. }{ ∃* h

_{2}h_{3}. }{ rewrite* @Fmap.disjoint_union_eq_r. }

{ rewrite* @Fmap.union_assoc in U. } }

(* FILL IN HERE *) Admitted.

☐

End FundamentalProofs.

Module ProveConsequenceRules.

Recall the statement of the rule of consequence.

Lemma triple_conseq' : ∀ t H Q H' Q',

triple t H' Q' →

H ==> H' →

Q' ===> Q →

triple t H Q.

triple t H' Q' →

H ==> H' →

Q' ===> Q →

triple t H Q.

A direct proof of triple_conseq goes through the low-level
interpretation of Separation Logic triples in terms of heaps.

Proof using.

(* No need to follow through this low-level proof. *)

introv M WH WQ. rewrite triple_iff_triple_lowlevel in *.

intros h

∃ v h

Qed.

(* No need to follow through this low-level proof. *)

introv M WH WQ. rewrite triple_iff_triple_lowlevel in *.

intros h

_{1}h_{2}D HH. forwards (v&h_{1}'&D'&R&HQ): M D. applys WH HH.∃ v h

_{1}'. splits¬. applys WQ HQ.Qed.

An alternative proof consists of first establishing the consequence
rule for the hoare judgment, then derive its generalization to
the triple judgment of Separation Logic.

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

Prove the consequence rule for Hoare triples.
Lemma hoare_conseq : ∀ t H Q H' Q',

hoare t H' Q' →

H ==> H' →

Q' ===> Q →

hoare t H Q.

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

☐

hoare t H' Q' →

H ==> H' →

Q' ===> Q →

hoare t H Q.

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

☐

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

Prove the consequence rule by leveraging the lemma hoare_conseq. Hint: unfold the definition of triple, apply the lemma hoare_conseq with the appropriate arguments, then exploit himpl_frame_l to prove the entailment relations.
Lemma triple_conseq : ∀ t H Q H' Q',

triple t H' Q' →

H ==> H' →

Q' ===> Q →

triple t H Q.

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

☐

triple t H' Q' →

H ==> H' →

Q' ===> Q →

triple t H Q.

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

☐

End ProveConsequenceRules.

Module ProveExtractionRules.

Recall the extraction rule for pure facts.

Parameter triple_hpure' : ∀ t (P:Prop) H Q,

(P → triple t H Q) →

triple t (\[P] \* H) Q.

(P → triple t H Q) →

triple t (\[P] \* H) Q.

To prove this lemma, we first the establish corresponding
result on hoare, then derive its version for triple.

Lemma hoare_hpure : ∀ t (P:Prop) H Q,

(P → hoare t H Q) →

hoare t (\[P] \* H) Q.

Proof using.

introv M. intros h (h

subst. rewrite Fmap.union_empty_l. applys M HP M

Qed.

Lemma triple_hpure : ∀ t (P:Prop) H Q,

(P → triple t H Q) →

triple t (\[P] \* H) Q.

Proof using.

introv M. unfold triple. intros H'.

rewrite hstar_assoc. applys hoare_hpure.

intros HP. applys M HP.

Qed.

(P → hoare t H Q) →

hoare t (\[P] \* H) Q.

Proof using.

introv M. intros h (h

_{1}&h_{2}&M_{1}&M_{2}&D&U). destruct M_{1}as (M_{1}&HP).subst. rewrite Fmap.union_empty_l. applys M HP M

_{2}.Qed.

Lemma triple_hpure : ∀ t (P:Prop) H Q,

(P → triple t H Q) →

triple t (\[P] \* H) Q.

Proof using.

introv M. unfold triple. intros H'.

rewrite hstar_assoc. applys hoare_hpure.

intros HP. applys M HP.

Qed.

Similarly, the extraction rule for existentials for
triple can be derived from that for hoare.

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

Prove the extraction rule triple_hexists. Hint: start by stating and proving the corresponding lemma for hoare triples.
Lemma hoare_hexists : ∀ t (A:Type) (J:A→hprop) Q,

(∀ x, hoare t (J x) Q) →

hoare t (\∃ x, J x) Q.

Proof using. introv M. intros h (x&Hh). applys M Hh. Qed.

Lemma triple_hexists : ∀ t (A:Type) (J:A→hprop) Q,

(∀ x, triple t (J x) Q) →

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

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

☐

(∀ x, hoare t (J x) Q) →

hoare t (\∃ x, J x) Q.

Proof using. introv M. intros h (x&Hh). applys M Hh. Qed.

Lemma triple_hexists : ∀ t (A:Type) (J:A→hprop) Q,

(∀ x, triple t (J x) Q) →

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

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

☐

Parameter hstar_hexists' : ∀ A (J:A→hprop) H,

(hexists J) \* H = hexists (J \*+ H).

Parameter triple_hexists' : ∀ t (A:Type) (J:A→hprop) Q,

(∀ x, triple t (J x) Q) →

triple t (hexists J) Q.

(hexists J) \* H = hexists (J \*+ H).

Parameter triple_hexists' : ∀ t (A:Type) (J:A→hprop) Q,

(∀ x, triple t (J x) Q) →

triple t (hexists J) Q.

Remark: in chapter Hprop, we observed that \[P] can be
encoded as \∃ (p:P), \[]. When this encoding is used,
the rule triple_hpure turns out to be a particular instance
of the rule triple_hexists, as we prove next.

Parameter hpure_encoding : ∀ P,

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

Lemma triple_hpure_from_triple_hexists : ∀ t (P:Prop) H Q,

(P → triple t H Q) →

triple t (\[P] \* H) Q.

Proof using.

introv M. rewrite hpure_encoding.

rewrite hstar_hexists. (* disable notation printing to see the effect *)

applys triple_hexists. (* ∀ (p:P), ... is the same as P → ... *)

rewrite hstar_hempty_l. applys M.

Qed.

End ProveExtractionRules.

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

Lemma triple_hpure_from_triple_hexists : ∀ t (P:Prop) H Q,

(P → triple t H Q) →

triple t (\[P] \* H) Q.

Proof using.

introv M. rewrite hpure_encoding.

rewrite hstar_hexists. (* disable notation printing to see the effect *)

applys triple_hexists. (* ∀ (p:P), ... is the same as P → ... *)

rewrite hstar_hempty_l. applys M.

Qed.

End ProveExtractionRules.

### Rules for Naming Heaps

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

Prove that a heap predicate H is equivalent to the heap predicate which asserts that the heap is, for a heap h such that H h, exactly equal to H.
Lemma hexists_named_eq : ∀ H,

H = (\∃ h, \[H h] \* (= h)).

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

☐

H = (\∃ h, \[H h] \* (= h)).

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

☐

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

Prove that the proposition hoare t H Q is equivalent to: for any heap h satisfying the precondition H, the Hoare triple whose precondition requires the input heap to be exactly equal to h, and whose postcondition is Q holds.
Lemma hoare_named_heap : ∀ t H Q,

(∀ h, H h → hoare t (= h) Q) →

hoare t H Q.

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

☐

(∀ h, H h → hoare t (= h) Q) →

hoare t H Q.

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

☐

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

Prove the counterpart of hoare_named_heap for Separation Logic triples.
Lemma triple_named_heap : ∀ t H Q,

(∀ h, H h → triple t (= h) Q) →

triple t H Q.

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

☐

(∀ h, H h → triple t (= h) Q) →

triple t H Q.

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

☐

Module AlternativeExistentialRule.

Traditional papers on Separation Logic do not include triple_hexists,
but instead a rule called triple_hexists2 that includes an existential
quantifier both in the precondition and the postcondition.
As we show next, in the presence of the consequence rule,
the two rules are equivalent.
The formulation of triple_hexists is not only more concise, it is
also better suited for practical applications.

Lemma triple_hexists2 : ∀ A (Hof:A→hprop) (Qof:A→val→hprop) t,

(∀ x, triple t (Hof x) (Qof x)) →

triple t (\∃ x, Hof x) (fun v ⇒ \∃ x, Qof x v).

Proof using.

introv M.

applys triple_hexists. intros x.

applys triple_conseq (M x).

{ applys himpl_refl. }

{ intros v. applys himpl_hexists_r x. applys himpl_refl. }

Qed.

Lemma triple_hexists_of_triple_hexists2 : ∀ t (A:Type) (Hof:A→hprop) Q,

(∀ x, triple t (Hof x) Q) →

triple t (\∃ x, Hof x) Q.

Proof using.

introv M.

applys triple_conseq (\∃ x, Hof x) (fun (v:val) ⇒ \∃ (x:A), Q v).

{ applys triple_hexists2. intros x. applys M. }

{ applys himpl_refl. }

{ intros v. applys himpl_hexists_l. intros _. applys himpl_refl. }

Qed.

End AlternativeExistentialRule.

(∀ x, triple t (Hof x) (Qof x)) →

triple t (\∃ x, Hof x) (fun v ⇒ \∃ x, Qof x v).

Proof using.

introv M.

applys triple_hexists. intros x.

applys triple_conseq (M x).

{ applys himpl_refl. }

{ intros v. applys himpl_hexists_r x. applys himpl_refl. }

Qed.

Lemma triple_hexists_of_triple_hexists2 : ∀ t (A:Type) (Hof:A→hprop) Q,

(∀ x, triple t (Hof x) Q) →

triple t (\∃ x, Hof x) Q.

Proof using.

introv M.

applys triple_conseq (\∃ x, Hof x) (fun (v:val) ⇒ \∃ (x:A), Q v).

{ applys triple_hexists2. intros x. applys M. }

{ applys himpl_refl. }

{ intros v. applys himpl_hexists_l. intros _. applys himpl_refl. }

Qed.

End AlternativeExistentialRule.

## Historical Notes

(* 2021-01-25 13:22 *)