HpropHeap Predicates
First Pass
- \[] denotes the empty heap predicate,
- \[P] denotes a pure fact,
- p ~~> v denotes a predicate that characterizes a singleton heap,
- H1 \* H2 denotes the separating conjunction,
- Q1 \*+ H2 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
By convention, we use the type state describes a "full" state of memory,
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 the
following:
Note that the union operation is commutative only when its two 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 h1 h2 denotes the union of the two states h1 and h2.
- Fmap.disjoint h1 h2 asserts that h1 and h2 have disjoint domains.
Heap Predicates
Thereafter, let H range 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 H1 \* H2, characterizes a state that
can be decomposed in two disjoint parts, one that satisfies H1, and
another that satisfies H2. In the definition below, the two parts are
named h1 and h2.
Definition hstar (H1 H2 : hprop) : hprop :=
fun (h:heap) ⇒ ∃ h1 h2, H1 h1
∧ H2 h2
∧ Fmap.disjoint h1 h2
∧ h = Fmap.union h1 h2.
Notation "H1 '\*' H2" := (hstar H1 H2) (at level 41, right associativity).
fun (h:heap) ⇒ ∃ h1 h2, H1 h1
∧ H2 h2
∧ Fmap.disjoint h1 h2
∧ h = Fmap.union h1 h2.
Notation "H1 '\*' H2" := (hstar H1 H2) (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 type A.
The notation \∃ x, H stands for hexists (fun x ⇒ H). The
generalized notation \∃ x1 ... xn, H is also available.
The definition of hexists is a bit technical. It is not essential to
master it at this point. Additional explanations are provided near the end
of this chapter.
Definition hexists (A:Type) (J:A→hprop) : hprop :=
fun (h:heap) ⇒ ∃ x, J x h.
Notation "'\exists' x1 .. xn , H" :=
(hexists (fun x1 ⇒ .. (hexists (fun xn ⇒ H)) ..))
(at level 39, x1 binder, H at level 50, right associativity,
format "'[' '\exists' '/ ' x1 .. xn , '/ ' H ']'").
fun (h:heap) ⇒ ∃ x, J x h.
Notation "'\exists' x1 .. xn , H" :=
(hexists (fun x1 ⇒ .. (hexists (fun xn ⇒ H)) ..))
(at level 39, x1 binder, H at level 50, right associativity,
format "'[' '\exists' '/ ' x1 .. xn , '/ ' H ']'").
Universal quantification in hprop is only useful for more advanced
features of Separation Logic. We postpone its introduction to chapter
Wand.
All the definitions above are eventually turned Opaque, after the
appropriate introduction and elimination lemmas are established for them.
Thus, at some point it is no longer possible to execute, say, unfold hstar
. Opacity is essential to ensures that proofs do not depend on the details
of how the definitions of heap predicates are set up.
Extensionality for Heap Predicates
How can we prove a goal of the form H1 = H2 when H1 and H2 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), H1 h ↔ H2 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".
By specializing P and Q above to the type hprop, we obtain exactly the
desired extensionality principle.
Lemma hprop_eq : ∀ (H1 H2:hprop),
(∀ (h:heap), H1 h ↔ H2 h) →
H1 = H2.
Proof using. apply predicate_extensionality. Qed.
(∀ (h:heap), H1 h ↔ H2 h) →
H1 = H2.
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 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.
(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 to augment a postcondition with a piece of state.
This operation is described by the operator 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 Q1 and Q2 are
equal, it suffices to show that the heap predicates Q1 v and Q2 v (both
of type hprop) are equal for any value v.
Again, the extensionality property that we need is not built-in to Coq. We
need another axiom called "functional extensionality".
The desired equality property for postconditions follows directly from that
axiom.
Lemma qprop_eq : ∀ (Q1 Q2:val→hprop),
(∀ (v:val), Q1 v = Q2 v) →
Q1 = Q2.
Proof using. apply functional_extensionality. Qed.
(∀ (v:val), Q1 v = Q2 v) →
Q1 = Q2.
Proof using. apply functional_extensionality. Qed.
Introduction and Inversion Lemmas for Basic Operators
Notation "h1 \u h2" := (Fmap.union h1 h2) (at level 37, right associativity).
Implicit Types P : Prop.
Implicit Types v : val.
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 : ∀ H1 H2 h1 h2,
H1 h1 →
H2 h2 →
Fmap.disjoint h1 h2 →
(H1 \* H2) (h1 \u h2).
Proof using. intros. ∃* h1 h2. 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.
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 : ∀ H1 H2 h1 h2,
H1 h1 →
H2 h2 →
Fmap.disjoint h1 h2 →
(H1 \* H2) (h1 \u h2).
Proof using. intros. ∃* h1 h2. 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 : ∀ H1 H2 h,
(H1 \* H2) h →
∃ h1 h2, H1 h1 ∧ H2 h2 ∧ Fmap.disjoint h1 h2 ∧ h = h1 \u h2.
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 : ∀ H1 H2 h,
(H1 \* H2) h →
∃ h1 h2, H1 h1 ∧ H2 h2 ∧ Fmap.disjoint h1 h2 ∧ h = h1 \u h2.
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 (h1&h2&M1&M2&D&U). destruct M1 as (x&M1). ∃* x h1 h2. }
{ intros (x&M). destruct M as (h1&h2&M1&M2&D&U). ∃ h1 h2.
splits¬. ∃* x. }
Qed.
{ intros (x&M). destruct M as (h1&h2&M1&M2&D&U). ∃ h1 h2.
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
Lemma hprop_op_comm : ∀ (op:hprop→hprop→hprop),
(∀ H1 H2 h, op H1 H2 h → op H2 H1 h) →
(∀ H1 H2, op H1 H2 = op H2 H1).
Proof using. introv M. intros. applys hprop_eq. split; applys M. Qed.
(∀ H1 H2 h, op H1 H2 h → op H2 H1 h) →
(∀ H1 H2, op H1 H2 = op H2 H1).
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 : ∀ h1 h2,
Fmap.disjoint h1 h2 →
h1 \u h2 = h2 \u h1. The commutativity result is then proved as follows.
Check Fmap.union_comm_of_disjoint : ∀ h1 h2,
Fmap.disjoint h1 h2 →
h1 \u h2 = h2 \u h1. The commutativity result is then proved as follows.
Lemma hstar_comm : ∀ H1 H2,
H1 \* H2 = H2 \* H1.
Proof using.
(* Exploit symmetry. *)
applys hprop_op_comm.
H1 \* H2 = H2 \* H1.
Proof using.
(* Exploit symmetry. *)
applys hprop_op_comm.
Unfold the defnition of star.
introv (h1&h2&M1&M2&D&U).
∃ h2 h1. subst. splits¬.
(* Exploit commutativity of disjoint union *)
{ rewrite Fmap.union_comm_of_disjoint; auto. }
Qed.
∃ h2 h1. subst. splits¬.
(* Exploit commutativity of disjoint union *)
{ rewrite Fmap.union_comm_of_disjoint; auto. }
Qed.
Associativity of Separating Conjunction
Check Fmap.union_assoc : ∀ h1 h2 h3,
(h1 \u h2) \u h3 = h1 \u (h2 \u h3).
Check Fmap.disjoint_union_eq_l : ∀ h1 h2 h3,
Fmap.disjoint (h2 \u h3) h1
= (Fmap.disjoint h1 h2 ∧ Fmap.disjoint h1 h3).
Check Fmap.disjoint_union_eq_r : ∀ h1 h2 h3,
Fmap.disjoint h1 (h2 \u h3)
= (Fmap.disjoint h1 h2 ∧ Fmap.disjoint h1 h3).
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 : ∀ H1 H2 H3,
(H1 \* H2) \* H3 = H1 \* (H2 \* H3).
Proof using.
intros. applys hprop_eq. split.
{ intros (h'&h3&M1&M2&D&U). destruct M1 as (h1&h2&M3&M4&D'&U').
subst h'. rewrite Fmap.disjoint_union_eq_l in D.
∃ h1 (h2 \u h3). splits.
{ applys M3. }
{ ∃* h2 h3. }
{ rewrite* @Fmap.disjoint_union_eq_r. }
{ rewrite* @Fmap.union_assoc in U. } }
(* FILL IN HERE *) Admitted.
☐
(H1 \* H2) \* H3 = H1 \* (H2 \* H3).
Proof using.
intros. applys hprop_eq. split.
{ intros (h'&h3&M1&M2&D&U). destruct M1 as (h1&h2&M3&M4&D'&U').
subst h'. rewrite Fmap.disjoint_union_eq_l in D.
∃ h1 (h2 \u h3). splits.
{ applys M3. }
{ ∃* h2 h3. }
{ 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 : ∀ H1 H2 H3,
H1 \* H2 \* H3 = H2 \* H1 \* H3.
Proof using. (* FILL IN HERE *) Admitted.
☐
H1 \* H2 \* H3 = H2 \* H1 \* H3.
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
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 the 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, like 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' x1 .. xn , p" := (ex (fun x1 ⇒ .. (ex (fun xn ⇒ p)) ..))
(at level 200, x1 binder, right associativity,
format "'[' 'exists' '/ ' x1 .. xn , '/ ' p ']'").
Notation "'\exists' x1 .. xn , H" :=
(hexists (fun x1 ⇒ .. (hexists (fun xn ⇒ H)) ..))
(at level 39, x1 binder, right associativity, H at level 50,
format "'[' '\exists' '/ ' x1 .. 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" asserts that two functions are
equal if they provide equal result for every argument.
Exercise: 1 star, standard, especially useful (predicate_extensionality_derived)
Using the two axioms propositional_extensionality and functional_extensionality, show how 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
(* 2023-11-29 09:22 *)