# HpropHeap Predicates

# First Pass

- \[] denotes the empty heap predicate,
- \[P] denotes a pure fact,
- p ~~> v denotes a predicate that characterizes a singleton heap,
- H
_{1}\* H_{2}denotes the separating conjunction, - Q
_{1}\*+ H_{2}denotes the separating conjunction between a postcondition and a heap predicate, - \∃ x, H denotes an existential quantifier.

- H denotes a heap predicate of type hprop; it describes a piece of state,
- Q denotes a postcondition, of type val→hprop; it describes both a result value and a piece of state.

## Description of Memory States

_{1}\* H

_{2}admit the type state → Prop, where the type state corresponds to a finite map used to describe the contents of the memory. In what follows, we give the formal definition of state and of the type of heap predicates.

By convention, we use the type state to describe a "full" memory state,
and we use an alias, the type heap, to describe a "piece of" state.

The file LibSepReference introduces the module name Fmap as a shorthand
for LibSepFmap. The key operations associated with finite maps are:
Note that the union operation is commutative only when its arguments
have disjoint domains. Throughout the course, we only consider disjoint
unions, for which commutativity holds.

- Fmap.empty denotes the empty state,
- Fmap.single p v denotes a singleton state, that is, a unique cell at location p with contents v,
- Fmap.union h
_{1}h_{2}denotes the union of the two states h_{1}and h_{2}. - Fmap.disjoint h
_{1}h_{2}asserts that h_{1}and h_{2}have disjoint domains.

## Heap Predicates

H ranges over heap predicates.

An essential aspect of Separation Logic is that all heap predicates defined
and used in practice are built using a few basic combinators. In other
words, except for the definition of the combinators themselves, we will
never define a custom heap predicate directly as a function of the state.
We next describe the most important combinators, which were pervasively used
throughout the first two chapters.
The hempty predicate, usually written \[], characterizes an empty
state.

Definition hempty : hprop :=

fun (h:heap) ⇒ (h = Fmap.empty).

Notation "\[]" := (hempty) (at level 0).

fun (h:heap) ⇒ (h = Fmap.empty).

Notation "\[]" := (hempty) (at level 0).

The pure fact predicate, written \[P], characterizes an empty state and
moreover asserts that the proposition P is true.

Definition hpure (P:Prop) : hprop :=

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

Notation "\[ P ]" := (hpure P) (at level 0, format "\[ P ]").

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

Notation "\[ P ]" := (hpure P) (at level 0, format "\[ P ]").

The singleton heap predicate, written p ~~> v, characterizes a state with
a single allocated cell, at location p, storing the value v.

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

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

Notation "p '~~>' v" := (hsingle p v) (at level 32).

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

Notation "p '~~>' v" := (hsingle p v) (at level 32).

The "separating conjunction", written H

_{1}\* H_{2}, characterizes a state that can be decomposed in two disjoint parts, one that satisfies H_{1}and another that satisfies H_{2}. In the definition below, the two parts are named h_{1}and h_{2}.
Definition hstar (H

fun (h:heap) ⇒ ∃ h

∧ H

∧ Fmap.disjoint h

∧ h = Fmap.union h

Notation "H

_{1}H_{2}: hprop) : hprop :=fun (h:heap) ⇒ ∃ 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}.Notation "H

_{1}'\*' H_{2}" := (hstar H_{1}H_{2}) (at level 41, right associativity).
The existential quantifier for heap predicates, written \∃ x, H
characterizes a heap that satisfies H for some x. The variable x has
type A, for some arbitrary A.
The notation \∃ x, H stands for hexists (fun x ⇒ H). The
generalized notation \∃ x
The definition of hexists is a bit technical, and it is not essential to
master it at this point. Additional explanations are provided near the end
of this chapter.

_{1}... xn, H is also available.
Definition hexists (A:Type) (J:A→hprop) : hprop :=

fun (h:heap) ⇒ ∃ x, J x h.

Notation "'\exists' x

(hexists (fun x

(at level 39, x

format "'[' '\exists' '/ ' x

fun (h:heap) ⇒ ∃ x, J x h.

Notation "'\exists' x

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

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

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

_{1}.. xn , '/ ' H ']'").
Universal quantification in hprop is also possible, but it is only
useful for more advanced features of Separation Logic. We postpone its
introduction to chapter Wand.
All the definitions above will eventually be made Opaque, after the
appropriate introduction and elimination lemmas have been established,
making it no longer possible to execute, say, unfold hstar. Opacity is
essential to ensure that proofs do not depend on the details of the
definitions.

## Extensionality for Heap Predicates

Parameter hstar_assoc_statement : ∀ H

((H

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

_{1}\* H_{2}) \* H_{3}) = (H_{1}\* (H_{2}\* H_{3})).
How can we prove a goal of the form H
This reasoning principle, a specific form of extensionality property, is not
available by default in Coq. But we can safely assume it if we extend the
logic of Coq with a standard axiom called "predicate extensionality".

_{1}= H_{2}when H_{1}and H_{2}have type hprop, that is, heap→Prop? Intuitively, H and H' are equal if and only if they characterize exactly the same set of heaps, that is, if ∀ (h:heap), H_{1}h ↔ H_{2}h.
By specializing P and Q above to the type hprop, we obtain exactly the
desired extensionality principle.

Lemma hprop_eq : ∀ (H

(∀ (h:heap), H

H

Proof using. apply predicate_extensionality. Qed.

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

_{1}h ↔ H_{2}h) →H

_{1}= H_{2}.Proof using. apply predicate_extensionality. Qed.

More information about extensionality axioms may be found near the end of
this chapter.

## Statement of Fundamental Properties

(2) The star operator is commutative.

(3) The empty heap predicate is a neutral element for the star. Because star
is commutative, it is equivalent to state that hempty is a left or a right
neutral element for hstar. We choose, arbitrarily, to state the
left-neutrality property.

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

(5) Pure facts can be extruded out stars.

## Postconditions: Type, Syntax, and Extensionality

One common operation is augmenting a postcondition with a description of
another piece of state. This operation is written as Q \*+ H, which is
just a convenient notation for fun x ⇒ (Q x \* H). We will use this
operator in particular in the statement of the frame rule in the next
chapter.

Intuitively, in order to prove that two postconditions Q
Again, the extensionality property that we need is not built into Coq. We
need another axiom called "functional extensionality".

_{1}and Q_{2}are equal, it suffices to show that the heap predicates Q_{1}v and Q_{2}v are equal for any value v.
The desired equality property for postconditions follows directly from this
axiom.

Lemma qprop_eq : ∀ (Q

(∀ (v:val), Q

Q

Proof using. apply functional_extensionality. Qed.

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

_{1}v = Q_{2}v) →Q

_{1}= Q_{2}.Proof using. apply functional_extensionality. Qed.

## Introduction and Inversion Lemmas for Basic Operators

Notation "h

Implicit Types P : Prop.

Implicit Types v : val.

_{1}\u h_{2}" := (Fmap.union h_{1}h_{2}) (at level 37, right associativity).Implicit Types P : Prop.

Implicit Types v : val.

The introduction lemmas show how to prove goals of the form H h, for
various forms of the heap predicate H.

The tactic hnf, for "head normal form", unfolds the head constants.

hnf. auto.

Qed.

Lemma hpure_intro : ∀ P,

P →

\[P] Fmap.empty.

Proof using. introv M. hnf. auto. Qed.

Lemma hsingle_intro : ∀ p v,

(p ~~> v) (Fmap.single p v).

Proof using. intros. hnf. auto. Qed.

Lemma hstar_intro : ∀ H

H

H

Fmap.disjoint h

(H

Proof using. intros. ∃* h

Lemma hexists_intro : ∀ A (x:A) (J:A→hprop) h,

J x h →

(\∃ x, J x) h.

Proof using. introv M. hnf. eauto. Qed.

Qed.

Lemma hpure_intro : ∀ P,

P →

\[P] Fmap.empty.

Proof using. introv M. hnf. auto. Qed.

Lemma hsingle_intro : ∀ p v,

(p ~~> v) (Fmap.single p v).

Proof using. intros. hnf. auto. Qed.

Lemma hstar_intro : ∀ H

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

_{1}h_{1}→H

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

_{1}h_{2}→(H

_{1}\* H_{2}) (h_{1}\u h_{2}).Proof using. intros. ∃* h

_{1}h_{2}. Qed.Lemma hexists_intro : ∀ A (x:A) (J:A→hprop) h,

J x h →

(\∃ x, J x) h.

Proof using. introv M. hnf. eauto. Qed.

The inversion lemmas show how to extract information from hypotheses of the
form H h, for various forms of the heap predicate H.

Lemma hempty_inv : ∀ h,

\[] h →

h = Fmap.empty.

Proof using. introv M. hnf in M. auto. Qed.

Lemma hpure_inv : ∀ P h,

\[P] h →

P ∧ h = Fmap.empty.

Proof using. introv M. hnf in M. autos*. Qed.

Lemma hsingle_inv: ∀ p v h,

(p ~~> v) h →

h = Fmap.single p v.

Proof using. introv M. hnf in M. auto. Qed.

Lemma hstar_inv : ∀ H

(H

∃ h

Proof using. introv M. hnf in M. eauto. Qed.

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

(\∃ x, J x) h →

∃ x, J x h.

Proof using. introv M. hnf in M. eauto. Qed.

\[] h →

h = Fmap.empty.

Proof using. introv M. hnf in M. auto. Qed.

Lemma hpure_inv : ∀ P h,

\[P] h →

P ∧ h = Fmap.empty.

Proof using. introv M. hnf in M. autos*. Qed.

Lemma hsingle_inv: ∀ p v h,

(p ~~> v) h →

h = Fmap.single p v.

Proof using. introv M. hnf in M. auto. Qed.

Lemma hstar_inv : ∀ H

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

_{1}\* H_{2}) h →∃ h

_{1}h_{2}, H_{1}h_{1}∧ H_{2}h_{2}∧ Fmap.disjoint h_{1}h_{2}∧ h = h_{1}\u h_{2}.Proof using. introv M. hnf in M. eauto. Qed.

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

(\∃ x, J x) h →

∃ x, J x h.

Proof using. introv M. hnf in M. eauto. Qed.

## Extraction of Existentials

First, we exploit extensionality, using hprop_eq or himpl_antisym.

Then we reveal the definitions of ==>, hexists and hstar.

{ intros (h

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

splits¬. ∃* x. }

Qed.

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

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

Qed.

## Neutral of Separating Conjunction

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

## Commutativity of Separating Conjunction

_{1}\* H

_{2}is equivalent to H

_{2}\* H

_{1}. By symmetry, it suffices to prove the entailement in one direction, e.g., H

_{1}\* H

_{2}==> H

_{2}\* H

_{1}. The symmetry argument for any binary operator on heap predicates is captured by the lemma hprop_op_comm shown below.

Lemma hprop_op_comm : ∀ (op:hprop→hprop→hprop),

(∀ H

(∀ H

Proof using. introv M. intros. applys hprop_eq. split; applys M. Qed.

(∀ H

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

_{1}H_{2}, op H_{1}H_{2}= op H_{2}H_{1}).Proof using. introv M. intros. applys hprop_eq. split; 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
a lemma coming from the finite map library.

Check Fmap.union_comm_of_disjoint : ∀ h

Fmap.disjoint h

h

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}. The commutativity result is then proved as follows.
Lemma hstar_comm : ∀ H

H

Proof using.

(* Exploit symmetry. *)

applys hprop_op_comm.

_{1}H_{2},H

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

(* Exploit symmetry. *)

applys hprop_op_comm.

Unfold the defnition of star.

introv (h

∃ h

(* Exploit commutativity of disjoint union *)

{ rewrite Fmap.union_comm_of_disjoint; auto. }

Qed.

_{1}&h_{2}&M_{1}&M_{2}&D&U).∃ h

_{2}h_{1}. subst. splits¬.(* Exploit commutativity of disjoint union *)

{ rewrite Fmap.union_comm_of_disjoint; auto. }

Qed.

## Associativity of Separating Conjunction

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 hprop_eq. split.

{ intros (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 hprop_eq. split.

{ intros (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.

☐

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.

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

☐

## Extract Pure Facts from Separating Conjunctions

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

Check Fmap.union_empty_l : ∀ h,

Fmap.empty \u h = h.

Check Fmap.disjoint_empty_l : ∀ h,

Fmap.disjoint Fmap.empty h. Note that auto can apply Fmap.disjoint_empty_l automatically. Hint: begin the proof by appyling propositional_extensionality.

Lemma hstar_hpure_l : ∀ P H h,

(\[P] \* H) h = (P ∧ H h).

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

☐

(\[P] \* H) h = (P ∧ H h).

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

☐

## Alternative Definitions for Heap Predicates

_{1}= H

_{2}. Recall that the lemma hprop_eq enables deriving such equalities by invoking predicate extensionality.

Lemma hempty_eq_hpure_true :

\[] = \[True].

Proof using.

unfold hempty, hpure. apply hprop_eq. intros h. iff Hh.

{ auto. }

{ destruct Hh. auto. }

Qed.

\[] = \[True].

Proof using.

unfold hempty, hpure. apply hprop_eq. intros h. iff Hh.

{ auto. }

{ destruct Hh. auto. }

Qed.

Thus, hempty could be defined in terms of hpure, as hpure True,
written \[True].

The pure fact predicate [\P] is equivalent to the existential
quantification over a proof of P in the empty heap, that is, to the heap
predicate \∃ (p:P), \[].

Lemma hpure_eq_hexists_proof : ∀ P,

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

Proof using.

unfold hempty, hpure, hexists. intros P.

apply hprop_eq. intros h. iff Hh.

{ destruct Hh as (E&p). ∃ p. auto. }

{ destruct Hh as (p&E). auto. }

Qed.

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

Proof using.

unfold hempty, hpure, hexists. intros P.

apply hprop_eq. intros h. iff Hh.

{ destruct Hh as (E&p). ∃ p. auto. }

{ destruct Hh as (p&E). auto. }

Qed.

Thus, hpure could be defined in terms of hexists and hempty, as
hexists (fun (p:P) ⇒ hempty), also written \∃ (p:P), \[]. In fact,
this is how hpure is defined in the rest of the course.

It is useful to minimize the number of combinators, both for elegance and to
reduce proof effort. We cannot do without hexists, thus there remains
a choice between considering either hpure or hempty as primitive, and
the other one as derived. The predicate hempty is simpler and appears as
more fundamental. Hence, in the subsequent chapters (and in the CFML tool),
we define hpure in terms of hexists and hempty, as in the definition
of hpure' shown above. In other words, we assume the definition:

Definition hpure (P:Prop) : hprop :=

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

Definition hpure (P:Prop) : hprop :=

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

## Additional Explanations for the Definition of \∃

Parameter (p:loc).

Check (\∃ (n:int), p ~~> (val_int n)) : hprop. The type of \∃, which operates on hprop,is very similar to that of ∃, which operates on Prop. The key difference is that a witness for a \∃ can depend on the current heap, whereas a witness for a ∃ cannot.

Check ex : ∀ A : Type, (A → Prop) → Prop. Likewise, \∃ x, H stands for hexists (fun x ⇒ H), where hexists has the following type:

Check hexists : ∀ A : Type, (A → hprop) → hprop.

Notation "'exists' x

_{1}.. xn , p" := (ex (fun x

_{1}⇒ .. (ex (fun xn ⇒ p)) ..))

(at level 200, x

_{1}binder, right associativity,

format "'[' 'exists' '/ ' x

_{1}.. xn , '/ ' p ']'").

Notation "'\exists' x

_{1}.. xn , H" :=

(hexists (fun x

_{1}⇒ .. (hexists (fun xn ⇒ H)) ..))

(at level 39, x

_{1}binder, right associativity, H at level 50,

format "'[' '\exists' '/ ' x

_{1}.. xn , '/ ' H ']'").

To establish extensionality of entailment, we have used the predicate
extensionality axiom. In fact, this axiom can be derived by combining the
axiom of "functional extensionality" with another one called "propositional
extensionality". The axiom of "propositional extensionality" asserts that
two propositions that are logically equivalent, in the sense that they imply
each other, can be considered equal.

The axiom of "functional extensionality", as we saw above, asserts that two
functions are equal if they provide equal result for every argument.

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

Use propositional_extensionality and functional_extensionality to derive predicate_extensionality.
Lemma predicate_extensionality_derived : ∀ A (P Q:A→Prop),

(∀ x, P x ↔ Q x) →

P = Q.

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

☐

(∀ x, P x ↔ Q x) →

P = Q.

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

☐

## Historical Notes

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