# SLFAffine

Set Implicit Arguments.

From SLF (* Sep *) Require SLFRules.

From SLF (* Sep *) Require Export SLFDirect.

Implicit Types f : var.

Implicit Types b : bool.

Implicit Types v : val.

Implicit Types h : heap.

Implicit Types P : Prop.

Implicit Types H : hprop.

Implicit Types Q : val→hprop.

# Chapter in a rush

- first, we recall the example illustrating the limitation of a logic without a discard rule, for a garbage-collected language;
- second, we present several versions of the "discard rule";
- third, we show how to refine the definition of Separation Logic triples in such a way that the discard rules are satisfied.

Let us recall the example of the function succ_using_incr_attempt
from chapter SLFBasic. This function allocates a reference with
contents n, then increments that reference, and finally returning
its contents, that is, n+1. Let us revisit this example, with
this time the intention of establishing for it a postcondition that
does not leak the existence of a left-over reference cell.

let succ_using_incr n =

let p = ref n in

incr p;

!p

let succ_using_incr n =

let p = ref n in

incr p;

!p

In the framework developed so far, the heap predicate describing the
reference cell allocated by the function cannot be discarded, because
the code considered does not include a deallocation operation. Thus,
we are forced to include in the postcondition the description of a
left-over reference with a heap predicate, e.g., \∃ p, p ~~> (n+1),
or \∃ p m, p ~~> m.

Lemma triple_succ_using_incr : ∀ (n:int),

triple (succ_using_incr n)

\[]

(fun r ⇒ \[r = n+1] \* \∃ p, (p ~~> (n+1))).

Proof using.

xwp. xapp. intros p. xapp. xapp. xsimpl. auto.

Qed.

If we try to prove a specification that does not mention the left-over
reference, then we get stuck with a proof obligation of the form
p ~~> (n+1) ==> \[].

Lemma triple_succ_using_incr' : ∀ (n:int),

triple (succ_using_incr n)

\[]

(fun r ⇒ \[r = n+1]).

Proof using.

xwp. xapp. intros p. xapp. xapp. xsimpl. { auto. } (* stuck here *)

Abort.

This situation is desirable in a programming language with explicit
deallocation, because it ensures that the code written by the
programmer is not missing any deallocation operation. However, it is
ill-suited for a programming language equipped with a garbage collector
that deallocates data automatically.
In this chapter, we present an "affine" version of Separation Logic,
where the above function succ_using_incr does admits the simple
postcondition fun r ⇒ \[r = n+1], i.e., that needs not mention the
left-over reference in the postcondition.

## Statement of the discard rule

Let us show that, using the rule triple_hany_post, we can derive
the desired specification for the motivating example from the
specification that mentions the left-over postcondition.

Module MotivatingExampleSolved.

Export MotivatingExample.

Lemma triple_succ_using_incr' : ∀ (n:int),

triple (succ_using_incr n)

\[]

(fun r ⇒ \[r = n+1]).

Proof using.

intros. applys triple_hany_post. applys triple_succ_using_incr.

Qed.

End MotivatingExampleSolved.

A symmetric rule, named triple_hany_pre, asserts that an arbitrary
heap predicate H' can be dropped from the precondition, simplifying
it from H \* H' to H.

Observe the difference between the two rules. In triple_hany_post,
the discarded predicate H' appears in the premise, reflecting the
fact that we discard it after the evaluation of the term t. On the
contrary, in triple_hany_pre, the discarded predicate H' appears
in the conclusion, reflecting the fact that we discard it before the
evaluation of t.
The two rules triple_hany_pre and triple_hany_post can be derived from
each other. As we will establish further on, the rule triple_hany_pre is
derivable from triple_hany_post, by a simple application of the frame rule.
Reciprocally, triple_hany_post is derivable from triple_hany_post,
however the proof is more involved (it appears in the bonus section).

## Fine-grained control on collectable predicates

Module Preview.

Parameter haffine : hprop → Prop.

Parameter triple_haffine_post : ∀ t H H' Q,

haffine H' →

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

triple t H Q.

Parameter triple_haffine_pre : ∀ t H H' Q,

haffine H' →

triple t H Q →

triple t (H \* H') Q.

End Preview.

To constraint the discard rule and allow fine-tuning of which heap
predicates may be thrown away, we introduce the notions of "affine
heap" and of "affine heap predicates", captured by the judgments
heap_affine h and haffine H, respectively.
The definition of heap_affine h is left abstract for the moment.
We will show two extreme instantiations: one that leads to a logic
where all predicates are affine (i.e. can be freely discarded),
one one that leads to a logic where all predicates are linear
(i.e. none can be freely discarded, like in our previous set up).

## Definition of heap_affine and of haffine

This predicate heap_affine is assumed to satisfy two properties:
it holds of the empty heap, and it is stable by (disjoint) union of heaps.

Parameter heap_affine_empty :

heap_affine Fmap.empty.

Parameter heap_affine_union : ∀ h

_{1}h

_{2},

heap_affine h

_{1}→

heap_affine h

_{2}→

Fmap.disjoint h

_{1}h

_{2}→

heap_affine (Fmap.union h

_{1}h

_{2}).

The predicate haffine H captures the notion of "affine heap predicate".
A heap predicate is affine iff it only holds of affine heaps.

The predicate haffine distributes in a natural way on each of the
operators of Separation Logic: the combination of affine heap predicates
yields affine heap predicates. In particular:

- \[] and \[P], which describes empty heaps, can always be discarded;
- H
_{1}\* H_{2}can be discarded if both H_{1}and H_{2}can be discarded; - \∃ x, H and \∀ x, H can be discarded if H can be discarded for any x.

Lemma haffine_hempty :

haffine \[].

Proof using.

introv K. lets E: hempty_inv K. subst. applys heap_affine_empty.

Qed.

Lemma haffine_hpure : ∀ P,

haffine \[P].

Proof using.

intros. intros h K. lets (HP&M): hpure_inv K.

subst. applys heap_affine_empty.

Qed.

Lemma haffine_hstar : ∀ H

_{1}H

_{2},

haffine H

_{1}→

haffine H

_{2}→

haffine (H

_{1}\* H

_{2}).

Proof using.

introv M

_{1}M

_{2}K. lets (h

_{1}&h

_{2}&K

_{1}&K

_{2}&D&U): hstar_inv K.

subst. applys× heap_affine_union.

Qed.

Lemma haffine_hexists : ∀ A (J:A→hprop),

(∀ x, haffine (J x)) →

haffine (\∃ x, (J x)).

Proof using. introv F

_{1}(x&Hx). applys× F

_{1}. Qed.

Lemma haffine_hforall : ∀ A `{Inhab A} (J:A→hprop),

(∀ x, haffine (J x)) →

haffine (\∀ x, (J x)).

Proof using. introv IA F

_{1}Hx. lets N: hforall_inv Hx. applys× F

_{1}arbitrary. Qed.

Remark: in the last rule above, that the type A must be inhabited
for this rule to make sense. In practice, the \∀ quantifier
is always invoked on inhabited types, so this is a benign restriction.
In addition, haffine (\[P] \* H) should simplify to haffine H
under the hypothesis P. Indeed, if a heap h satisfies \[P] \* H,
then it must be the case that the proposition P is true. Formally:

Lemma haffine_hstar_hpure_l : ∀ P H,

(P → haffine H) →

haffine (\[P] \* H).

Proof using. introv M. intros h K. rewrite hstar_hpure_l in K. applys× M. Qed.

## Definition of the "affine top" heap predicates

Definition hgc : hprop :=

\∃ H, \[haffine H] \* H.

Notation "\GC" := (hgc) : hgc_scope.

Open Scope hgc_scope.

The introduction lemmas asserts that \GC h holds when h
satisfies heap_affine.

#### Exercise: 1 star, standard, recommended (triple_frame)

Prove that the affine heap predicate holds of any affine heap.
The elimination lemma asserts the reciprocal.

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

Prove the elimination lemma for \GC expressed using heap_affine.
Together, the introduction and the elimination rule justify
the fact that hgc could equivalently have been defined as
fun h ⇒ heap_affine h.

Definition hgc' : hprop :=

fun h ⇒ heap_affine h.

Lemma hgc_eq_hgc' :

hgc = hgc'.

Proof using.

intros. applys himpl_antisym.

{ intros h M. applys× hgc_inv. }

{ intros h M. applys× hgc_intro. }

Qed.

## Properties of the \GC predicate

Lemma hstar_hgc_hgc :

(\GC \* \GC) = \GC.

Proof using.

unfold hgc. applys himpl_antisym.

{ xpull. intros H

_{1}K

_{1}H

_{2}K

_{2}. xsimpl (H

_{1}\* H

_{2}). applys× haffine_hstar. }

{ xpull. intros H K. xsimpl H \[]. auto. applys haffine_hempty. }

Qed.

Another useful property is that the heap predicate \GC itself
satisifes haffine. Indeed, \GC denotes some heap H such that
H is affine; Thus, by essence, it denotes an affine heap predicate.

Lemma haffine_hgc :

haffine \GC.

Proof using.

applys haffine_hexists. intros H. applys haffine_hstar_hpure_l. auto.

Qed.

The process of exploiting the \GC to "absorb" affine heap predicates
is captured by the following lemma, which asserts that a heap predicate
H entails \GC whenever H is affine.

Lemma himpl_hgc_r : ∀ H,

haffine H →

H ==> \GC.

Proof using. introv M. intros h K. applys hgc_intro. applys M K. Qed.

In particular, the empty heap predicate \[] entails \GC, because the
empty heap predicate is affine (recall lemma haffine_hempty).

Using the predicate \GC, we can reformulate the constrained
discard rule triple_haffine_post as follows.

Not only is this rule more concise than triple_haffine_post, it
also has the benefits that the piece of heap discarded, previously
described by H', no longer needs to be provided upfront at the
moment of applying the rule. It may be provided further on in the
reasoning, for example in an entailment, by instantiating the
existential quantifier carried into the definition of \GC.

To set up a fully-affine logic, we consider a definition of
heap_affine that holds of any heap.

It is trivial to check that heap_affine satisfies the required
distribution properties on the empty heap and the union of heaps.

Lemma heap_affine_empty :

heap_affine Fmap.empty.

Proof using. rewrite× heap_affine_def. Qed.

Lemma heap_affine_union : ∀ h

_{1}h

_{2},

heap_affine h

_{1}→

heap_affine h

_{2}→

Fmap.disjoint h

_{1}h

_{2}→

heap_affine (Fmap.union h

_{1}h

_{2}).

Proof using. intros. rewrite× heap_affine_def. Qed.

With that instantiation, haffine holds of any heap predicate.

Lemma haffine_equiv : ∀ H,

(haffine H) ↔ True.

Proof using.

intros. iff M.

{ auto. }

{ unfold haffine. intros. rewrite× heap_affine_def. }

Qed.

With that instantiation, the affine top predicate \GC is equivalent
to the top predicate htop, defined as fun h ⇒ True or, equivalently,
as \∃ H, H.

Definition htop : hprop :=

\∃ H, H.

Lemma hgc_eq_htop : hgc = htop.

Proof using.

unfold hgc, htop. applys himpl_antisym.

{ xsimpl. }

{ xsimpl. intros. rewrite× haffine_equiv. }

Qed.

End FullyAffineLogic.

To set up a fully-affine logic, we consider a definition of
heap_affine that holds only of empty heaps.

Again, it is not hard to check that heap_affine satisfies the
required distributivity properties.

Lemma heap_affine_empty :

heap_affine Fmap.empty.

Proof using. rewrite× heap_affine_def. Qed.

Lemma heap_affine_union : ∀ h

_{1}h

_{2},

heap_affine h

_{1}→

heap_affine h

_{2}→

Fmap.disjoint h

_{1}h

_{2}→

heap_affine (Fmap.union h

_{1}h

_{2}).

Proof using.

introv K

_{1}K

_{2}D. rewrite heap_affine_def in ×.

subst. rewrite× Fmap.union_empty_r.

Qed.

The predicate haffine H is equivalent to H ==> \[],
that is, it characterizes heap predicates that hold of the
empty heap.

Lemma haffine_equiv : ∀ H,

haffine H ↔ (H ==> \[]).

Proof using.

intros. unfold haffine. iff M.

{ intros h K. specializes M K. rewrite heap_affine_def in M.

subst. applys hempty_intro. }

{ intros h K. specializes M K. rewrite heap_affine_def.

applys hempty_inv M. }

Qed.

With that instantiation, the affine top predicate \GC is equivalent
to the empty heap predicate hempty.

Lemma hgc_eq_hempty : hgc = hempty.

Proof using.

unfold hgc. applys himpl_antisym.

{ xpull. introv N. rewrite× haffine_equiv in N. }

{ xsimpl \[]. applys haffine_hempty. }

Qed.

End FullyLinearLogic.

Thereafter, we purposely leave the definition of haffine
abstract, for the sake of generality.
In what follows, we explain how to refine the notion of Separation
Logic triple so as to accomodate the discard rule.
Recall the definition of triple for a linear logic.

Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ (H':hprop), hoare t (H \* H') (Q \*+ H').
The discard rule triple_htop_post asserts that postconditions
may be freely extended with the \GC predicate. To support
this rule, it suffices to modify the definition of triple to
include the predicate \GC in the postcondition of the underlying
Hoare triple, as follows.

Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ (H':hprop), hoare t (H \* H') (Q \*+ H').

Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ (H':hprop), hoare t (H \* H') (Q \*+ H' \*+ \GC).

Observe that this definition of triple is strictly more general than
the previous one. Indeed, as explained earlier on, when considering the
fully-linear instantiation of haffine, the predicate \GC is equivalent
to the empty predicate \[]. In this case, the occurence of \GC that
appears in the definition of triple can be replaced with \[], yielding
a definition equivalent to our original definition of triple.
For the updated definition of triple using \GC, one can prove that:

- all the existing reasoning rules of Separation Logic remain sound;
- the discard rules triple_htop_post, triple_haffine_hpost and triple_haffine_hpre can be proved sound.

## Soundness of the existing rules

#### Exercise: 2 stars, standard, optional (triple_frame)

Prove the frame rule for the definition of triple that includes \GC. Hint: unfold the definition of triple but not that of hoare, then exploit lemma hoare_conseq and conclude using the tactic xsimpl.Lemma triple_frame : ∀ t H Q H',

triple t H Q →

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

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

(* *)

#### Exercise: 2 stars, standard, optional (triple_conseq)

Prove the frame rule for the definition of triple that includes \GC. Hint: follow the same approach as in the proof of triple_frame, and leverage the tactic xchange to conclude.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.

(* *)

The extraction rules remain valid as well.

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

(P → triple t H Q) →

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

Proof using.

introv M. unfolds triple. intros H'.

rewrite hstar_assoc. applys× hoare_hpure.

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.

introv M. unfolds triple. intros H'.

rewrite hstar_hexists. applys× hoare_hexists.

Qed.

The standard reasoning rules of Separation Logic can be derived
for the revised notion of Separation Logic triple, the one which
includes \GC, following essentially the same proofs as for the
original Separation Logic triples. The main difference is that one
sometimes needs to invoke the lemma hstar_hgc_hgc for collapsing
two \GC into a single one.
In what follows, we present just one representative example of
such proofs, namely the reasoning rule for sequences. This proof
is similar to that of lemma triple_seq from chapter SLFRules.

Lemma triple_seq : ∀ t

_{1}t

_{2}H Q H

_{1},

triple t

_{1}H (fun v ⇒ H

_{1}) →

triple t

_{2}H

_{1}Q →

triple (trm_seq t

_{1}t

_{2}) H Q.

Proof using.

introv M

_{1}M

_{2}. intros H'. unfolds triple.

applys hoare_seq.

{ applys M

_{1}. }

{ applys hoare_conseq. { applys M

_{2}. } { xsimpl. }

{ xchanges hstar_hgc_hgc. } }

Qed.

Let us first establish the soundness of the discard rule
triple_htop_post.

#### Exercise: 2 stars, standard, recommended (triple_hgc_post')

Prove triple_htop_post with respect to the refined definition of triple that includes \GC in the postcondition. Hint: exploit hoare_conseq, then exploit hstar_hgc_hgc, with help of the tactics xchange and xsimpl.Lemma triple_hgc_post : ∀ t H Q,

triple t H (Q \*+ \GC) →

triple t H Q.

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

(* *)

EX1! (triple_haffine_post)
Prove that triple_haffine_post is derivable from triple_hgc_post.
Hint: unfold the definition of \GC using unfold hgc.

Lemma triple_haffine_post : ∀ t H H' Q,

haffine H' →

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

triple t H Q.

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

(* *)

EX1? (triple_hgc_post_from_triple_haffine_post)
Reciprocally, prove that triple_hgc_post is derivable from
triple_haffine_post.

Lemma triple_hgc_post_from_triple_haffine_post : ∀ t H Q,

triple t H (Q \*+ \GC) →

triple t H Q.

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

(* *)

EX1? (triple_haffine_pre)
Prove that triple_haffine_pre is derivable from triple_hgc_post.
Hint: exploit the frame rule.

Lemma triple_haffine_pre : ∀ t H H' Q,

haffine H' →

triple t H Q →

triple t (H \* H') Q.

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

(* *)

EX1? (triple_conseq_frame_hgc)
Prove the combined structural rule triple_conseq_frame_hgc, which
extends triple_conseq_frame with the discard rule, replacing
Q

_{1}\*+ H_{2}===> Q with Q_{1}\*+ H_{2}===> Q \*+ \GC. Hint: invoke triple_conseq, triple_frame and triple_hgc_post in the appropriate order.Lemma triple_conseq_frame_hgc : ∀ 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 \*+ \GC →

triple t H Q.

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

(* *)

EX1? (triple_ramified_frame_hgc)
Prove the following generalization of the ramified frame rule
that includes the discard rule.
Hint: it is a corollary of triple_conseq_frame_hgc. Take inspiration
from the proof of triple_ramified_frame in chapter SLFWand.

Lemma triple_ramified_frame_hgc : ∀ H

_{1}Q

_{1}t H Q,

triple t H

_{1}Q

_{1}→

H ==> H

_{1}\* (Q

_{1}\--* (Q \*+ \GC)) →

triple t H Q.

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

(* *)

End GCRules.

Recall the characteristic equivalence of wp.

Lemma wp_equiv : ∀ t H Q,

(H ==> wp t Q) ↔ (triple t H Q).

Proof using.

unfold wp. iff M.

{ applys× triple_conseq Q M.

applys triple_hexists. intros H'.

rewrite hstar_comm. applys× triple_hpure. }

{ xsimpl× H. }

Qed.

In weakest precondition style, the discard rule triple_hgc_post
translates into the entailment wp t (Q \*+ \GC) ==> wp t Q,
as we prove next.
EX

_{1}? (wp_hgc_post) Prove the discard rule in wp-style. Hint: exploit wp_equiv and triple_hgc_post.Lemma wp_hgc_post : ∀ t H Q,

wp t (Q \*+ \GC) ==> wp t Q.

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

(* *)

Likewise, the wp-style presentation of the rule triple_hgc_pre
takes the following form.

Lemma wp_haffine_pre : ∀ t H Q,

haffine H →

(wp t Q) \* H ==> wp t Q.

Proof using.

introv K. rewrite wp_equiv. applys triple_haffine_pre.

{ applys K. } { rewrite× <- wp_equiv. }

Qed.

The revised presentation of the wp-style ramified frame rule includes
an extra \GC predicate. This rule captures at once all the structural
properties of Separation Logic, including the discard rule.

For a change, let us present below a direct proof for this lemma,
that is, not reusing the structural rules associated with triples.

Proof using.

intros. unfold wp. xpull ;=> H M.

xsimpl (H \* (Q

_{1}\--* Q

_{2}\*+ \GC)).

unfolds triple. intros H'.

applys hoare_conseq (M ((Q

_{1}\--* Q

_{2}\*+ \GC) \* H')).

{ xsimpl. } { xchange hstar_hgc_hgc. xsimpl. }

Qed.

## Exploiting the discard rule in proofs

- either by invoking triple_haffine_pre to remove a specific predicate from the current state, i.e., the precondition;
- or by invoking triple_htop_post to add a \GC into the current postcondition and allow subsequent removal of any predicate that may be left-over in the final entailment justifying that the final state satisfies the postcondition.

Parameter xwp_lemma : ∀ v

_{1}v

_{2}x t

_{1}H Q,

v

_{1}= val_fun x t

_{1}→

H ==> wpgen ((x,v

_{2})::nil) t

_{1}Q →

triple (trm_app v

_{1}v

_{2}) H Q.

Its generalized form extends the postcondition to which the formula
computed by wpgen is applied from Q to Q \*+ \GC, as shown below.

Lemma xwp_lemma' : ∀ v

_{1}v

_{2}x t

_{1}H Q,

v

_{1}= val_fun x t

_{1}→

H ==> wpgen ((x,v

_{2})::nil) t

_{1}(Q \*+ \GC) →

triple (trm_app v

_{1}v

_{2}) H Q.

Proof using. introv E M. applys triple_hgc_post. applys× xwp_lemma. Qed.

Let us update the tactic xwp to exploit the lemma xwp_lemma'
instead of xwp_lemma.

Tactic Notation "xwp" :=

intros; applys xwp_lemma';

[ reflexivity | simpl; unfold wpgen_var; simpl ].

## Example proof involving discarded heap predicates

Assume a fully-affine logic.

Observe in the proof below the \GC introduced in the postcondition
by the call to xwp.

Lemma triple_succ_using_incr : ∀ (n:int),

triple (succ_using_incr n)

\[]

(fun r ⇒ \[r = n+1]).

Proof using.

xwp. xapp. intros r. xapp. xapp. xsimpl. { auto. }

(* There remains to absorb the left-over reference into the \GC predicate *)

applys himpl_hgc_r. applys haffine_hany.

Qed.

We will show further on how to automate the work from the last line
of the proof above, by setting up xsimpl to automatically resolve
goals of the form H ==> \GC.

## Revised definition of mkstruct

Definition mkstruct (F:formula) : formula :=

fun Q ⇒ \∃ Q', (F Q') \* (Q' \--* Q).

Let us prove that this revised definition of mkstruct does sastisfy
the wp-style statement of the discard rule, which is stated
in a way similar to wp_hgc_post.

Lemma mkstruct_hgc : ∀ Q F,

mkstruct F (Q \*+ \GC) ==> mkstruct F Q.

Proof using.

intros. unfold mkstruct. set (X := hgc) at 3. replace X with (\GC \* \GC).

{ xsimpl. } { subst X. apply hstar_hgc_hgc. }

Qed.

Besides, let us prove that the revised definition of mkstruct still
satisfies the three originally-required properties: erasure, consequence,
and frame.
Remark: the proofs shown below exploit a version of xsimpl that handles
the magic wand but provides no built-in support for the \GC predicate.

Lemma mkstruct_erase : ∀ F Q,

F Q ==> mkstruct F Q.

Proof using.

intros. unfold mkstruct. xsimpl Q. apply himpl_hgc_r. apply haffine_hempty.

Qed.

Lemma mkstruct_conseq : ∀ F Q

_{1}Q

_{2},

Q

_{1}===> Q

_{2}→

mkstruct F Q

_{1}==> mkstruct F Q

_{2}.

Proof using.

introv WQ. unfold mkstruct. xpull. intros Q'. xsimpl Q'. xchange WQ.

Qed.

Lemma mkstruct_frame : ∀ F H Q,

(mkstruct F Q) \* H ==> mkstruct F (Q \*+ H).

Proof using.

intros. unfold mkstruct. xpull. intros Q'. xsimpl Q'.

Qed.

EX2? (mkstruct_haffine_post)
Prove the reformulation of triple_haffine_post adapted to mkstruct,
for discarding an affine piece of postcondition.

Lemma mkstruct_haffine_post : ∀ H Q F,

haffine H →

mkstruct F (Q \*+ H) ==> mkstruct F Q.

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

(* *)

EX2? (mkstruct_haffine_pre)
Prove the reformulation of triple_haffine_pre adapted to mkstruct,
for discarding an affine piece of postcondition.

Lemma mkstruct_haffine_pre : ∀ H Q F,

haffine H →

(mkstruct F Q) \* H ==> mkstruct F Q.

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

(* *)

End NewTriples.

The tactic xaffine applys to a goal of the form haffine H.
The tactic simplifies the goal using all the distributivity rules
associated with haffine. Ultimately, it invokes eauto with haffine,
which can leverage knowledge specific to the definition of haffine
from the Separation Logic set up at hand.

Create HintDb haffine.

Tactic Notation "xaffine" :=

repeat match goal with ⊢ haffine ?H ⇒

match H with

| (hempty) ⇒ apply haffine_hempty

| (hpure _) ⇒ apply haffine_hpure

| (hstar _ _) ⇒ apply haffine_hstar

| (hexists _) ⇒ apply haffine_hexists

| (hforall _) ⇒ apply haffine_hforall

| (hgc) ⇒ apply haffine_hgc

| _ ⇒ eauto with haffine

end

end.

Lemma xaffine_demo : ∀ H

_{1}H

_{2}H

_{3},

haffine H

_{1}→

haffine H

_{3}→

haffine (H

_{1}\* H

_{2}\* H

_{3}).

Proof using. introv K

_{1}KJ. xaffine. (* remains haffine H

_{2}*) Abort.

End Xaffine.

Module XsimplExtended.

Import SLFDirect SLFExtra.

The tactic xsimpl is extended with support for simplifying goals
of the form H ==> \GC into haffine H, using lemma himpl_hgc_r.
For example, xsimpl can simplify the goal H

_{1}\* H_{2}==> H_{2}\* \GC into just haffine H_{1}.Lemma xsimpl_xgc_demo : ∀ H

_{1}H

_{2},

H

_{1}\* H

_{2}==> H

_{2}\* \GC.

Proof using. intros. xsimpl. Abort.

In addition, xsimpl invokes the tactic xaffine to simplify
side-conditions of the form haffine H. For example, xsimpl
can prove the following lemma.

Lemma xsimpl_xaffine_demo : ∀ H

_{1}H

_{2},

haffine H

_{1}→

H

_{1}\* H

_{2}==> H

_{2}\* \GC.

Proof using. introv K

_{1}. xsimpl. Qed.

End XsimplExtended.

To present the discard tactics xgc, xc_keep and xgc_post,
we import the definitions from SLFDirect but assume that the
definition of mkstruct is like the one presented in the present
file, that is, including the \GC when defining mkstruct F
as fun Q ⇒ \∃ Q', F Q' \* (Q' \--* (Q \*+ \GC)).
As argued earlier on, with this definition, [mkstruct] satisfies the
following discard rule.

The tactic xgc H removes H from the precondition (i.e. from the
current state), in the course of a proof exploiting a formula produced
by wpgen.
More precisely, the tactic invokes the following variant of the rule
triple_haffine_pre, which allows to leverage xsimpl for computing
the heap predicate H

_{2}that remains after a predicate H_{1}is removed from a precondition H, through the entailment H ==> H_{1}\* H_{2}.Lemma xgc_lemma: ∀ H

_{1}H

_{2}H F Q,

H ==> H

_{1}\* H

_{2}→

haffine H

_{1}→

H

_{2}==> mkstruct F Q →

H ==> mkstruct F Q.

Proof using.

introv WH K M. xchange WH. xchange M.

applys himpl_trans mkstruct_frame.

applys himpl_trans mkstruct_hgc.

applys mkstruct_conseq. xsimpl.

Qed.

Tactic Notation "xgc" constr(H) :=

eapply (@xgc_lemma H); [ xsimpl | xaffine | ].

Lemma xgc_demo : ∀ H

_{1}H

_{2}H

_{3}F Q,

haffine H

_{2}→

(H

_{1}\* H

_{2}\* H

_{3}) ==> mkstruct F Q.

Proof using. introv K

_{2}. xgc H

_{2}. (* clears H

_{2}*) Abort.

The tactic xgc_keep H is a variant of xgc that enables to discard
everything but H from the precondition.
The implementation of the tactic leverages the same lemma xgc_lemma,
only providing H

_{2}instead of H_{1}.Tactic Notation "xgc_keep" constr(H) :=

eapply (@xgc_lemma _ H); [ xsimpl | xaffine | ].

Lemma xgc_keep_demo : ∀ H

_{1}H

_{2}H

_{3}F Q,

haffine H

_{1}→

haffine H

_{3}→

(H

_{1}\* H

_{2}\* H

_{3}) ==> mkstruct F Q.

Proof using. introv K

_{1}K

_{3}. xgc_keep H

_{2}. Abort.

The tactic xgc_post simply extends the postcondition with a \GC,
to enable subsequent discarding of heap predicates in the final entailment.

Lemma xgc_post_lemma : ∀ H Q F,

H ==> mkstruct F (Q \*+ \GC) →

H ==> mkstruct F Q.

Proof using. introv M. xchange M. applys mkstruct_hgc. Qed.

Tactic Notation "xgc_post" :=

apply xgc_post_lemma.

Lemma xgc_keep_demo : ∀ H

_{1}H

_{2}H

_{3}F Q,

haffine H

_{1}→

haffine H

_{3}→

H

_{1}==> mkstruct F (Q \*+ H

_{2}\*+ H

_{3}) →

H

_{1}==> mkstruct F Q.

Proof using.

introv K

_{1}K

_{3}M. xgc_post. xchange M. applys mkstruct_conseq. xsimpl.

(* Check out how the end proof fails without the call to xgc_post. *)

Abort.

End XGC.

Recall the lemmas haffine_hexists and haffine_hforall.

Lemma haffine_hexists : ∀ A (J:A→hprop),

(∀ x, haffine (J x)) →

haffine (\∃ x, (J x)).

Lemma haffine_hforall : ∀ A `{Inhab A} (J:A→hprop),

(∀ x, haffine (J x)) →

haffine (\∀ x, (J x)).
They can be reformulated in a more concise way, as explained next.
First, to smoothly handle the distribution on the quantifiers, let us
extend the notion of "affinity" to postconditions. The predicate
haffine_post J asserts that haffine holds of J x for any x.

Lemma haffine_hexists : ∀ A (J:A→hprop),

(∀ x, haffine (J x)) →

haffine (\∃ x, (J x)).

Lemma haffine_hforall : ∀ A `{Inhab A} (J:A→hprop),

(∀ x, haffine (J x)) →

haffine (\∀ x, (J x)).

The rules then reformulate as follows.

Lemma haffine_hexists : ∀ A (J:A→hprop),

haffine_post J →

haffine (hexists J).

Proof using. introv F

_{1}(x&Hx). applys× F

_{1}. Qed.

Lemma haffine_hforall : ∀ A `{Inhab A} (J:A→hprop),

haffine_post J →

haffine (hforall J).

Proof using. introv IA F

_{1}Hx. lets N: hforall_inv Hx. applys× F

_{1}arbitrary. Qed.

End HaffineQuantifiers.

Earlier on, we proved that triple_hgc_pre is derivable from
triple_hgc_post, through a simple application of the frame rule.
We wrote that, reciprocally, the rule triple_hgc_post is derivable
from triple_hgc_pre, yet with a slightly more involved proof.
Let us present this proof.
In other word, assume triple_hgc_pre, and let us prove triple_hgc_post.

Parameter triple_hgc_pre : ∀ t H Q,

triple t H Q →

triple t (H \* \GC) Q.

Lemma triple_hgc_post : ∀ t H Q,

triple t H (Q \*+ \GC) →

triple t H Q.

The key idea of the proof is that a term t admits the same behavior
as let x = t in x. Thus, to simulate discarding a predicate from
the postcondition of t, one can invoke the discard rule on the
precondition of the variable x that appears at the end of
let x = t in x.
To formalize this idea, recall from SLFRules the lemma
eval_like_eta_expansion which asserts the equivalence of
t and let x = t in x, and recall the lemma triple_eval_like,
which asserts that two equivalent terms satisfy the same triples.

Proof using.

introv M. lets E: eval_like_eta_expansion t "x".

applys triple_eval_like E. applys triple_let.

{ applys M. }

{ intros v. simpl. applys triple_hgc_pre. applys triple_val. auto. }

Qed.

End FromPreToPostGC.

Consider the updated definition of triple introduced in this chapter.

Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ (H':hprop), hoare t (H \* H') (Q \*+ H' \*+ \GC).

In chapter SLFHprop, we presented an alternative definition for
Separation Logic triples, called triple_lowlevel, expressed directly
in terms of heaps.

Definition triple_lowlevel (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ h

Fmap.disjoint h

H h

∃ h

Fmap.disjoint h

∧ eval (h

∧ Q v h
In what follows, we explain how to generalize this definition to match
our revised definition of triple, and thereby obtain a direct definition
expressed in terms of heap, that does not depend on the definition of
hstar nor that of \GC.
Let us aim instead for a direct definition, entirely expressed in terms
of union of heaps. To that end, we need to introduce an additional piece of
state to describe the piece of the final heap covered by the \GC predicate.
We will need to describe the disjointness of the 3 pieces of heap that
describe the final state. To that end, we exploit the auxiliary definition
Fmap.disjoint_3 h

Definition disjoint_3 (h

disjoint h

∧ disjoint h

∧ disjoint h
We then formulate triple_lowlevel using a final state of the from
h

Definition triple_lowlevel (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ h

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

_{1}h_{2}→H h

_{1}→∃ h

_{1}' v,Fmap.disjoint h

_{1}' h_{2}∧ eval (h

_{1}\u h_{2}) t (h_{1}' \u h_{2}) v∧ Q v h

_{1}'._{1}h_{2}h_{3}, which asserts that the three arguments denote pairwise disjoint heaps. It is defined in the module Fmap as follows.Definition disjoint_3 (h

_{1}h_{2}h_{3}:heap) : Prop :=disjoint h

_{1}h_{2}∧ disjoint h

_{2}h_{3}∧ disjoint h

_{1}h_{3}._{1}' \u h_{2}\u h_{3}' instead of just h_{1}' \u h_{2}. There, h_{3}' denotes the piece of the final state covered by the \GC heap predicate. This piece of state is an affine heap, as captured by heap_affine h_{3}'.Definition triple_lowlevel (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ h

_{1}h

_{2},

Fmap.disjoint h

_{1}h

_{2}→

H h

_{1}→

∃ h

_{1}' h

_{3}' v,

Fmap.disjoint_3 h

_{1}' h

_{2}h

_{3}'

∧ heap_affine h

_{3}'

∧ eval (h

_{1}\u h

_{2}) t (h

_{1}' \u h

_{2}\u h

_{3}') v

∧ Q v h

_{1}'.

One can prove the equivalence of triple and triple_lowlevel
following a similar proof pattern as previously.

Lemma triple_eq_triple_lowlevel :

triple = triple_lowlevel.

Proof using.

applys pred_ext_3. intros t H Q.

unfold triple, triple_lowlevel, hoare. iff M.

{ introv D P

_{1}.

forwards¬(h'&v&R

_{1}&R

_{2}): M (=h

_{2}) (h

_{1}\u h

_{2}). { apply× hstar_intro. }

destruct R

_{2}as (h

_{2}'&h

_{1}''&N

_{0}&N

_{1}&N

_{2}&N

_{3}).

destruct N

_{0}as (h

_{1}'&h

_{3}'&T

_{0}&T

_{1}&T

_{2}&T

_{3}). subst.

∃ h

_{1}' h

_{1}'' v. splits×.

{ rew_disjoint. auto. }

{ applys hgc_inv N

_{1}. }

{ applys_eq× R

_{1}. } }

{ introv (h

_{1}&h

_{2}&N

_{1}&N

_{2}&D&U).

forwards¬(h

_{1}'&h

_{3}'&v&R

_{1}&R

_{2}&R

_{3}&R

_{4}): M h

_{1}h

_{2}.

∃ (h

_{1}' \u h

_{3}' \u h

_{2}) v. splits×.

{ applys_eq× R

_{3}. }

{ subst. rewrite hstar_assoc. apply× hstar_intro.

rewrite hstar_comm. applys× hstar_intro. applys× hgc_intro. } }

Qed.

End LowLevel.

(* 2020-03-23 08:37:52 (UTC+01) *)