# HimplHeap Entailment

Implicit Types

# First Pass

_{1}\* H

_{2}, Q

_{1}\*+ H

_{2}, and \∃ x, H.

_{1}==> H

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

_{1}also satisfies H

_{2}. We also need to extend the entailment relation to postconditions. We write Q

_{1}===> Q

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

_{1}v ==> Q

_{2}v holds.

_{1}Q

_{1}. There are two requirements: First, the precondition H must decompose into H

_{1}, which denotes the precondition expected by the specification, and the remaining part, called H

_{2}. Second, the targeted postcondition Q must be a consequence of the conjunction of Q

_{1}, which denotes the postcondition asserted by the specification, and H

_{2}, which denotes the remaining part that has not been affected during the evaluation of the term t. The formal statement is as follows.

Lemma triple_conseq_frame : ∀ H

_{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 chapter presents:

- the formal definition of the entailment relations, for heap predicates and for postconditions,
- the lemmas capturing the interaction of entailment with the star operator,
- the tactics xsimpl and xchange that are critically useful for manipulating entailments in practice.

## 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).
As we show next, the entailment relation is reflexive, transitive, and
antisymmetric. It thus forms an order relation on heap predicates.

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. Hint: use predicate_extensionality.
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.

☐

## 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).
In other words, Q
Entailment on postconditions also forms an order relation: it is reflexive,
transitive, and antisymmetric.

_{1}===> Q_{2}holds if and only 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. apply himpl_refl. Qed.

Lemma qimpl_trans : ∀ Q

(Q

(Q

(Q

Proof using. introv M

Q ===> Q.

Proof using. intros Q v. apply 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. eapply himpl_trans; eauto. Qed.#### Exercise: 1 star, standard, especially useful (qimpl_antisym)

Prove the antisymmetry of entailment on postconditions. Hint: exploit functional_extensionality.
Lemma qimpl_antisym : ∀ Q

(Q

(Q

(Q

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

☐

_{1}Q_{2},(Q

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

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

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

☐

## Frame Rule for Entailment

_{1}==> H

_{1}' then (H

_{1}\* H

_{2}) ==> (H

_{1}' \* H

_{2}). In other words, an arbitrary heap predicate H

_{2}can be "framed" on both sides of an entailment.

_{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}).## 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. Indeed, such a state cannot exist. The underlying contraction is formally captured by the following entailment relation, which concludes False.

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. eapply Fmap.disjoint_single_single_same_inv. eapply D.

Qed.

intros. unfold hsingle. intros h (h

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

Qed.

More generally, a heap predicate of the form H \* H is generally
suspicious in Separation Logic. In the simple variant of Separation Logic
that we consider in this course, there are only 3 typical situations where
H \* H makes sense: (1) if H is the empty heap predicate \[], (2) If
H is a pure heap predicate of the form \P], (3) if H of the form
\∃ H

_{0}, H_{0}, which will be written \GC in chapter Affine.### Rules for Naming Heaps

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

Prove that a heap predicate H is equivalent to \∃ h, \[H h] \* (= h)). Hint: use hstar_hpure_l and hexists_intro , as well as the extraction rules himpl_hexists_l and himpl_hstar_hpure_l.
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.

☐

## Identifying True and False Entailments

Module XsimplTactic.

Import LibSepReference.

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

Module CaseStudy.

Implicit Types p q : loc.

Implicit Types n m : int.

Import LibSepReference.

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

Module CaseStudy.

Implicit Types p q : loc.

Implicit Types n m : int.

Quiz: For each entailment relation, indicate (without a Coq proof) whether
it is true or false. Solutions appear further on.

Parameter case_study_1 : ∀ p q,

p ~~> 3 \* q ~~> 4

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

Parameter case_study_2 : ∀ p q,

p ~~> 3

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

Parameter case_study_3 : ∀ p q,

q ~~> 4 \* p ~~> 3

==> p ~~> 4.

Parameter case_study_4 : ∀ p q,

q ~~> 4 \* p ~~> 3

==> p ~~> 3.

Parameter case_study_5 : ∀ p q,

\[False] \* p ~~> 3

==> p ~~> 4 \* q ~~> 4.

Parameter case_study_6 : ∀ p q,

p ~~> 3 \* q ~~> 4

==> \[False].

Parameter case_study_7 : ∀ p,

p ~~> 3 \* p ~~> 4

==> \[False].

Parameter case_study_8 : ∀ p,

p ~~> 3 \* p ~~> 3

==> \[False].

Parameter case_study_9 : ∀ p,

p ~~> 3

==> \∃ n, p ~~> n.

Parameter case_study_10 : ∀ p,

∃ n, p ~~> n

==> p ~~> 3.

Parameter case_study_11 : ∀ p,

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

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

Parameter case_study_12 : ∀ p q,

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

==> \∃ n, p ~~> n \* q ~~> n.

Parameter case_study_13 : ∀ p n,

p ~~> n \* \[n > 0] \* \[n < 0] ==> p ~~> n \* p ~~> n.

End CaseStudy.

Module CaseStudyAnswers.

p ~~> 3 \* q ~~> 4

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

Parameter case_study_2 : ∀ p q,

p ~~> 3

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

Parameter case_study_3 : ∀ p q,

q ~~> 4 \* p ~~> 3

==> p ~~> 4.

Parameter case_study_4 : ∀ p q,

q ~~> 4 \* p ~~> 3

==> p ~~> 3.

Parameter case_study_5 : ∀ p q,

\[False] \* p ~~> 3

==> p ~~> 4 \* q ~~> 4.

Parameter case_study_6 : ∀ p q,

p ~~> 3 \* q ~~> 4

==> \[False].

Parameter case_study_7 : ∀ p,

p ~~> 3 \* p ~~> 4

==> \[False].

Parameter case_study_8 : ∀ p,

p ~~> 3 \* p ~~> 3

==> \[False].

Parameter case_study_9 : ∀ p,

p ~~> 3

==> \∃ n, p ~~> n.

Parameter case_study_10 : ∀ p,

∃ n, p ~~> n

==> p ~~> 3.

Parameter case_study_11 : ∀ p,

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

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

Parameter case_study_12 : ∀ p q,

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

==> \∃ n, p ~~> n \* q ~~> n.

Parameter case_study_13 : ∀ p n,

p ~~> n \* \[n > 0] \* \[n < 0] ==> p ~~> n \* p ~~> n.

End CaseStudy.

Module CaseStudyAnswers.

The answers to the quiz are as follows.
1. True, by commutativity.
2. False, because one cell does not entail two cells.
3. False, because two cells do not entail one cell.
4. False, because two cells do not entail one cell.
5. True, because \False entails anything.
6. False, because a satisfiable heap predicate does not entail \False.
7. True, because a cell cannot be starred with itself.
8. True, because a cell cannot be starred with itself.
9. True, by instantiating n with 3.
10. False, because n could be something else than 3.
11. True, by instantiating n in RHS with n+1 for the n of the LHS.
12. True, by instantiating n with 3.
13. True, because it is equivalent to \[False] ==> \[False].
Proofs for the true results appear below.

Implicit Types p q : loc.

Implicit Types n m : int.

Lemma case_study_1 : ∀ p q,

p ~~> 3 \* q ~~> 4

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

Proof using. xsimpl. Qed.

Lemma case_study_5 : ∀ p q,

\[False] \* p ~~> 3

==> p ~~> 4 \* q ~~> 4.

Proof using. xsimpl. Qed.

Lemma case_study_7 : ∀ p,

p ~~> 3 \* p ~~> 4

==> \[False].

Proof using. intros. xchange (hstar_hsingle_same_loc p). Qed.

Lemma case_study_8 : ∀ p,

p ~~> 3 \* p ~~> 3

==> \[False].

Proof using. intros. xchange (hstar_hsingle_same_loc p). Qed.

Lemma case_study_9 : ∀ p,

p ~~> 3

==> \∃ n, p ~~> n.

Proof using. xsimpl. Qed.

Lemma case_study_11 : ∀ p,

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

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

Proof using.

intros. xpull. intros n Hn. xsimpl (n+1).

math. math.

Qed.

Lemma case_study_12 : ∀ p q,

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

==> \∃ n, p ~~> n \* q ~~> n.

Proof using. xsimpl. Qed.

Lemma case_study_13 : ∀ p n,

p ~~> n \* \[n > 0] \* \[n < 0] ==> p ~~> n \* p ~~> n.

Proof using. intros. xsimpl. intros Hn

End CaseStudyAnswers.

Implicit Types n m : int.

Lemma case_study_1 : ∀ p q,

p ~~> 3 \* q ~~> 4

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

Proof using. xsimpl. Qed.

Lemma case_study_5 : ∀ p q,

\[False] \* p ~~> 3

==> p ~~> 4 \* q ~~> 4.

Proof using. xsimpl. Qed.

Lemma case_study_7 : ∀ p,

p ~~> 3 \* p ~~> 4

==> \[False].

Proof using. intros. xchange (hstar_hsingle_same_loc p). Qed.

Lemma case_study_8 : ∀ p,

p ~~> 3 \* p ~~> 3

==> \[False].

Proof using. intros. xchange (hstar_hsingle_same_loc p). Qed.

Lemma case_study_9 : ∀ p,

p ~~> 3

==> \∃ n, p ~~> n.

Proof using. xsimpl. Qed.

Lemma case_study_11 : ∀ p,

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

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

Proof using.

intros. xpull. intros n Hn. xsimpl (n+1).

math. math.

Qed.

Lemma case_study_12 : ∀ p q,

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

==> \∃ n, p ~~> n \* q ~~> n.

Proof using. xsimpl. Qed.

Lemma case_study_13 : ∀ p n,

p ~~> n \* \[n > 0] \* \[n < 0] ==> p ~~> n \* p ~~> n.

Proof using. intros. xsimpl. intros Hn

_{1}Hn_{2}. false. math. Qed.End CaseStudyAnswers.

Proving an entailment by hand is generally a tedious task. This is why most
frameworks based on Separation Logic 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. In order to best appreciate what a simplification
tactic provides and best understand how it works, it is very useful to first
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_l to extract pure facts, once they appear at the head of the left-hand side of the entailment. For arithmetic inequalities, use the math tactic.
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.

☐

## The xsimpl Tactic

- extract pure facts and existential quantifiers from the LHS,
- cancel out equal predicates occurring both in the LHS and RHS,
- generate subgoals for the pure facts occurring in the RHS, and instantiate the existential quantifiers from the RHS (using either unification variables or user-provided hints).

### 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 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. 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. 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 certain situations, it may be 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 8 9.

Abort.

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

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

intros. xsimpl 8 9.

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 __ 9 instantiates m with 9 while leaving n as an unresolved
evar.

Lemma xsimpl_demo_rhs_hints_evar : ∀ H

H

Proof using.

intros. xsimpl __ 9.

Abort.

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

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

intros. xsimpl __ 9.

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.

### Example of Entailment Proofs using xpull and xsimpl

Lemma xpull_example_1 : ∀ (p:loc),

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

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

Proof using.

intros. xpull.

Abort.

Lemma xpull_example_2 : ∀ (H:hprop),

\[False] ==> H.

Proof using. xpull. Qed.

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

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

Proof using.

intros. xpull.

Abort.

Lemma xpull_example_2 : ∀ (H:hprop),

\[False] ==> H.

Proof using. xpull. Qed.

xsimpl first invokes xpull to simplify the left-hand side, then attempts
to cancel out items from the right-hand side with items from the
left-hand-side.

Lemma xsimpl_example_1 : ∀ (p:loc),

p ~~> 3 ==>

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

Proof using. xsimpl. Qed.

Lemma xsimpl_example_2 : ∀ (p q:loc),

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

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

Proof using. xsimpl. Qed.

Lemma xsimpl_example_3 : ∀ (p:loc),

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

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

Proof using.

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

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

Qed.

p ~~> 3 ==>

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

Proof using. xsimpl. Qed.

Lemma xsimpl_example_2 : ∀ (p q:loc),

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

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

Proof using. xsimpl. Qed.

Lemma xsimpl_example_3 : ∀ (p:loc),

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

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

Proof using.

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

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

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.

☐

We next show the details of the proofs establishing the fundamental
properties of the Separation Logic operators. 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 himpl_frame_r, which is the symmetric of 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.

☐

## Historical Notes

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