# SLFRules

Set Implicit Arguments.

This file imports SLFDirect.v instead of SLFHprop.v and SLFHimpl.v.
The file SLFDirect.v contains definitions that are essentially similar
to those from SLFHprop.v and SLFHimpl.v, yet with one main difference:
SLFDirect makes the definition of Separation Logic operators opaque.
As a result, one cannot unfold the definition of hstar, hpure, etc.
To carry out reasoning, one must use the introduction and elimination
lemmas (e.g. hstar_intro, hstar_elim). These lemmas enforce
abstraction: they ensure that the proofs do not depend on the particular
choice of the definitions used for constructing Separation Logic.

From SLF (* Sep *) Require Export SLFDirect SLFExtra.

# Chapter in a rush

- introduced the key heap predicate operators,
- introduced the notion of Separation Logic triple,
- introduced the entailment relation,
- introduced the structural rules of Separation Logic.

- definition of the syntax of the language,
- definition of the semantics of the language,
- statements of the reasoning rules associated with each of the term constructions from the language,
- specification of the primitive operations of the language, in particular those associated with memory operations,
- review of the 4 structural rules introduced in prior chapters,
- examples of practical verification proofs.

- proofs of the reasoning rules associated with each term construct,
- proofs of the specification of the primitive operations.

### Syntax

Inductive val : Type :=

| val_unit : val

| val_bool : bool → val

| val_int : int → val

| val_loc : loc → val

| val_fun : var → trm → val

| val_fix : var → var → trm → val

| val_ref : val

| val_get : val

| val_set : val

| val_free : val

| val_add : val

| val_div : val

The grammar for terms includes values, variables, function definitions,
recursive function definitions, function applications, sequences,
let-bindings, and conditionals.

with trm : Type :=

| trm_val : val → trm

| trm_var : var → trm

| trm_fun : var → trm → trm

| trm_fix : var → var → trm → trm

| trm_app : trm → trm → trm

| trm_seq : trm → trm → trm

| trm_let : var → trm → trm → trm

| trm_if : trm → trm → trm → trm.

Note that trm_fun and trm_fix denote functions that may feature free
variables, unlike val_fun and val_fix which denote closed values.
The intention is that the evaluation of a trm_fun in the empty context
produces a val_fun value. Likewise, a trm_fix eventually evaluates to
a val_fix.
Several value constructors are declared as coercions, to enable more
concise statements. For example, val_loc is declared as a coercion,
so that a location p of type loc can be viewed as the value
val_loc p where an expression of type val is expected. Likewise,
a boolean b may be viewed as the value val_bool b, and an integer
n may be viewed as the value val_int n.

### State

For technical reasons related to the internal representation of finite
maps, to enable reading in a state, we need to justify that the grammar
of values is inhabited. This property is captured by the following
command, whose details are not relevant for understanding the rest of
the chapter.

### Substitution

_{1}t

_{2}) is defined as trm_let x (subst y w t

_{1}) (if var_eq x y then t

_{2}else (subst y w t

_{2})).

Fixpoint subst (y:var) (w:val) (t:trm) : trm :=

let aux t := subst y w t in

let if_y_eq x t

_{1}t

_{2}:= if var_eq x y then t

_{1}else t

_{2}in

match t with

| trm_val v ⇒ trm_val v

| trm_var x ⇒ if_y_eq x (trm_val w) t

| trm_fun x t

_{1}⇒ trm_fun x (if_y_eq x t

_{1}(aux t

_{1}))

| trm_fix f x t

_{1}⇒ trm_fix f x (if_y_eq f t

_{1}(if_y_eq x t

_{1}(aux t

_{1})))

| trm_app t

_{1}t

_{2}⇒ trm_app (aux t

_{1}) (aux t

_{2})

| trm_seq t

_{1}t

_{2}⇒ trm_seq (aux t

_{1}) (aux t

_{2})

| trm_let x t

_{1}t

_{2}⇒ trm_let x (aux t

_{1}) (if_y_eq x t

_{2}(aux t

_{2}))

| trm_if t

_{0}t

_{1}t

_{2}⇒ trm_if (aux t

_{0}) (aux t

_{1}) (aux t

_{2})

end.

### Implicit Types and coercions

Implicit Types b : bool.

Implicit Types v r : val.

Implicit Types t : trm.

Implicit Types s : state.

We next introduce two key coercions. First, we declare
trm_val as a coercion, so that, instead of writing trm_val v,
we may write simply v wherever a term is expected.

Second, we declare trm_app as a "Funclass" coercion. This piece
of magic enables us to write t

_{1}t_{2}as a shorthand for trm_app t_{1}t_{2}. The idea of associating trm_app as the "Funclass" coercion for the type trm is that if a term t_{1}of type trm is applied like a function to an argument, then t_{1}should be interpreted as trm_app t_{1}.
Interestingly, the "Funclass" coercion for trm_app can be iterated.
The expression t

_{1}t_{2}t_{3}is parsed by Coq as (t_{1}t_{2}) t_{3}. The first application t_{1}t_{2}is interpreted as trm_app t_{1}t_{2}. This expression, which itself has type trm, is applied to t_{3}. Hence, it is interpreted as trm_app (trm_app t_{1}t_{2}) t_{3}, which indeed corresponds to a function applied to two arguments.### Big-step semantics

_{0}t

_{1}t

_{2}, then it is required that t

_{0}be either a variable or a value. This is not a real restriction, because trm_if t

_{0}t

_{1}t

_{2}can always be encoded as let x = t

_{0}in if x then t

_{1}else t

_{2}.

1. eval for values and function definitions.
A value evaluates to itself.
A term function evaluates to a value function.
Likewise for a recursive function.

| eval_val : ∀ s v,

eval s (trm_val v) s v

| eval_fun : ∀ s x t

_{1},

eval s (trm_fun x t

_{1}) s (val_fun x t

_{1})

| eval_fix : ∀ s f x t

_{1},

eval s (trm_fix f x t

_{1}) s (val_fix f x t

_{1})

2. eval for function applications.
The beta reduction rule asserts that (val_fun x t
In the recursive case, (val_fix f x t

_{1}) v_{2}evaluates to the same result as subst x v_{2}t_{1}._{1}) v_{2}evaluates to subst x v_{2}(subst f v_{1}t_{1}), where v_{1}denotes the recursive function itself, that is, val_fix f x t_{1}.| eval_app_fun : ∀ s

_{1}s

_{2}v

_{1}v

_{2}x t

_{1}v,

v

_{1}= val_fun x t

_{1}→

eval s

_{1}(subst x v

_{2}t

_{1}) s

_{2}v →

eval s

_{1}(trm_app v

_{1}v

_{2}) s

_{2}v

| eval_app_fix : ∀ s

_{1}s

_{2}v

_{1}v

_{2}f x t

_{1}v,

v

_{1}= val_fix f x t

_{1}→

eval s

_{1}(subst x v

_{2}(subst f v

_{1}t

_{1})) s

_{2}v →

eval s

_{1}(trm_app v

_{1}v

_{2}) s

_{2}v

3. eval for structural constructs.
A sequence trm_seq t
The let-binding trm_let x t

_{1}t_{2}first evaluates t_{1}, taking the state from s_{1}to s_{2}, drops the result of t_{1}, then evaluates t_{2}, taking the state from s_{2}to s_{3}._{1}t_{2}is similar, except that the variable x gets substituted for the result of t_{1}inside t_{2}.| eval_seq : ∀ s

_{1}s

_{2}s

_{3}t

_{1}t

_{2}v

_{1}v,

eval s

_{1}t

_{1}s

_{2}v

_{1}→

eval s

_{2}t

_{2}s

_{3}v →

eval s

_{1}(trm_seq t

_{1}t

_{2}) s

_{3}v

| eval_let : ∀ s

_{1}s

_{2}s

_{3}x t

_{1}t

_{2}v

_{1}r,

eval s

_{1}t

_{1}s

_{2}v

_{1}→

eval s

_{2}(subst x v

_{1}t

_{2}) s

_{3}r →

eval s

_{1}(trm_let x t

_{1}t

_{2}) s

_{3}r

4. eval for conditionals.
A conditional in a source program is assumed to be of the form
if t
The term trm_if (val_bool true) t

_{0}then t_{1}else t_{2}, where t_{0}is either a variable or a value. If it is a variable, then by the time it reaches an evaluation position, the variable must have been substituted by a value. Thus, the evaluation rule only considers the form if v_{0}then t_{1}else t_{2}. The value v_{0}must be a boolean value, otherwise evaluation gets stuck._{1}t_{2}behaves like t_{1}, whereas the term trm_if (val_bool false) t_{1}t_{2}behaves like t_{2}. This behavior is described by a single rule, leveraging Coq's "if" constructor to factor out the two cases.| eval_if : ∀ s

_{1}s

_{2}b v t

_{1}t

_{2},

eval s

_{1}(if b then t

_{1}else t

_{2}) s

_{2}v →

eval s

_{1}(trm_if (val_bool b) t

_{1}t

_{2}) s

_{2}v

5. eval for primitive stateless operations.
For similar reasons as explained above, the behavior of applied
primitive functions only need to be described for the case of value
arguments.
An arithmetic operation expects integer arguments. The addition
of val_int n
The division operation, on the same arguments, produces the
quotient n

_{1}and val_int n_{2}produces val_int (n_{1}+ n_{2})._{1}/ n_{2}, under the assumption that the dividor n_{2}is non-zero. In other words, if a program performs a division by zero, then it cannot satisfy the eval judgment.| eval_add : ∀ s n

_{1}n

_{2},

eval s (val_add (val_int n

_{1}) (val_int n

_{2})) s (val_int (n

_{1}+ n

_{2}))

| eval_div : ∀ s n

_{1}n

_{2},

n

_{2}≠ 0 →

eval s (val_div (val_int n

_{1}) (val_int n

_{2})) s (val_int (Z.quot n

_{1}n

_{2}))

6. eval for primitive operations on memory.
There remains to describe operations that act on the mutable store.
val_ref v allocates a fresh cell with contents v. The operation
returns the location, written p, of the new cell. This location
must not be previously in the domain of the store s.
val_get (val_loc p) reads the value in the store s at location p.
The location must be bound to a value in the store, else evaluation
is stuck.
val_set (val_loc p) v updates the store at a location p assumed to
be bound in the store s. The operation modifies the store and returns
the unit value.
val_free (val_loc p) deallocates the cell at location p.

| eval_ref : ∀ s v p,

¬ Fmap.indom s p →

eval s (val_ref v) (Fmap.update s p v) (val_loc p)

| eval_get : ∀ s p,

Fmap.indom s p →

eval s (val_get (val_loc p)) s (Fmap.read s p)

| eval_set : ∀ s p v,

Fmap.indom s p →

eval s (val_set (val_loc p) v) (Fmap.update s p v) val_unit

| eval_free : ∀ s p,

Fmap.indom s p →

eval s (val_free (val_loc p)) (Fmap.remove s p) val_unit.

End SyntaxAndSemantics.

### Loading of definitions from SLFDirecŧ

Implicit Types x f : var.

Implicit Types b : bool.

Implicit Types p : loc.

Implicit Types n : int.

Implicit Types v w r : val.

Implicit Types t : trm.

Implicit Types h : heap.

Implicit Types s : state.

Implicit Types H : hprop.

Implicit Types Q : val→hprop.

## Rules for terms

### Reasoning rule for sequences

_{1};t

_{2}is essentially the same as that from Hoare logic. The rule is:

{H} t

_{1}{fun v ⇒ H

_{1}} {H

_{1}} t

_{2}{Q}

------------------------------------

{H} (t

_{1};t

_{2}) {Q}

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

Remark: the variable v denotes the result of the evaluation
of t

_{1}. For well-typed programs, this result would always be val_unit. Yet, because we here consider an untyped language, we do not bother adding the constraint v = val_unit. Instead, we simply treat the result of t_{1}as a value irrelevant to the remaining of the evaluation.### Reasoning rule for let-bindings

_{1}in t

_{2}could be stated, in informal writing, in the form:

{H} t

_{1}{Q

_{1}} (∀ x, {Q

_{1}x} t

_{2}{Q})

-----------------------------------------

{H} (let x = t

_{1}in t

_{2}) {Q}

_{1}in t

_{2}, and the x that denotes a value when quantified as ∀ x.

{H} t

_{1}{Q

_{1}} (∀ v, {Q

_{1}v} (subst x v t

_{2}) {Q})

-----------------------------------------------------

{H} (let x = t

_{1}in t

_{2}) {Q}

Parameter triple_let : ∀ x t

_{1}t

_{2}H Q Q

_{1},

triple t

_{1}H Q

_{1}→

(∀ v, triple (subst x v t

_{2}) (Q

_{1}v) Q) →

triple (trm_let x t

_{1}t

_{2}) H Q.

### Reasoning rule for conditionals

b = true → {H} t

_{1}{Q} b = false → {H} t

_{2}{Q}

--------------------------------------------------

{H} (if b then t

_{1}in t

_{2}) {Q}

Parameter triple_if_case : ∀ b t

_{1}t

_{2}H Q,

(b = true → triple t

_{1}H Q) →

(b = false → triple t

_{2}H Q) →

triple (trm_if (val_bool b) t

_{1}t

_{2}) H Q.

Remark: the two premises may be factorized into a single one
using Coq's conditional construct. Such an alternative
statement is discussed further in this chapter.

### Reasoning rule for values

----------------------------

{\[]} v {fun r ⇒ \[r = v]}

H ==> Q v

---------

{H} v {Q}

### Reasoning rule for functions

_{1}, expressed as a subterm in a program, evaluates to a value, more precisely to val_fun x t

_{1}. Again, we could consider a rule with an empty precondition:

------------------------------------------------------

{\[]} (trm_fun x t

_{1}) {fun r ⇒ \[r = val_fun x t

_{1}]}

_{1}) {Q}. We thus consider the following rule, very similar to triple_val.

The rule for recursive functions is similar. It is presented
further in the file.
Last but not least, we need a reasoning rule to reason about a
function application. Consider an application trm_app v

semantics of trm_app v

v

---------------------------------------------

{H} (trm_app v
The corresponding Coq statement is as shown below.

_{1}v_{2}. Assume v_{1}to be a function, that is, to be of the form (* val_fun x t_{1}. Then, according to the beta-reduction rule, the *)semantics of trm_app v

_{1}v_{2}is the same as that of subst x v_{2}t_{1}. This reasoning rule is thus:v

_{1}= val_fun x t_{1}{H} (subst x v_{2}t_{1}) {Q}---------------------------------------------

{H} (trm_app v

_{1}v_{2}) {Q}Parameter triple_app_fun : ∀ x v

_{1}v

_{2}t

_{1}H Q,

v

_{1}= val_fun x t

_{1}→

triple (subst x v

_{2}t

_{1}) H Q →

triple (trm_app v

_{1}v

_{2}) H Q.

The generalization to the application of recursive functions is
straightforward. It is discussed further in this chapter.

## Specification of primitive operations

### Specification of arithmetic primitive operations

_{1}n

_{2}, which is short for trm_app (trm_app (trm_val val_add) (val_int n

_{1})) (val_int n

_{2}). Indeed, recall that val_int is declared as a coercion.

_{1}+n

_{2}).

_{1}+n

_{2}).

Parameter triple_add : ∀ n

_{1}n

_{2},

triple (val_add n

_{1}n

_{2})

\[]

(fun r ⇒ \[r = val_int (n

_{1}+ n

_{2})]).

The specification of the division operation val_div n

_{1}n_{2}is similar, yet with the extra requirement that the argument n_{2}must be nonzero. This requirement n_{2}≠ 0 is a pure fact, which can be asserted as part of the precondition, as follows.Parameter triple_div : ∀ n

_{1}n

_{2},

triple (val_div n

_{1}n

_{2})

\[n

_{2}≠ 0]

(fun r ⇒ \[r = val_int (Z.quot n

_{1}n

_{2})]).

Equivalently, the requirement n

_{2}≠ 0 may be asserted as an hypothesis to the front of the triple judgment, in the form of a standard Coq hypothesis, as shown below.Parameter triple_div' : ∀ n

_{1}n

_{2},

n

_{2}≠ 0 →

triple (val_div n

_{1}n

_{2})

\[]

(fun r ⇒ \[r = val_int (Z.quot n

_{1}n

_{2})]).

This latter presentation with pure facts such as n

_{2}≠ 0 placed to the front of the triple turns out to be more practical to exploit in proofs. Hence, we always follow this style of presentation, and reserve the precondition for describing pieces of mutable state.### Specification of primitive operations acting on memory

Parameter triple_get : ∀ v p,

triple (val_get (val_loc p))

(p ~~> v)

(fun r ⇒ \[r = v] \* (p ~~> v)).

Remark: val_loc is registered as a coercion, so val_get (val_loc p)
could be written simply as val_get p, where p has type loc.
We here chose to write val_loc explicitly for clarity.
Recall that val_set denotes the operation for writing a memory cell.
A call of the form val_set v' w executes safely if v' is of the
form val_loc p for some location p, in a state p ~~> v.
The write operation updates this state to p ~~> w, and returns
the unit value, which can be ignored. Hence, val_set is specified
as follows.

Recall that val_ref denotes the operation for allocating a cell
with a given contents. A call to val_ref v does not depend on
the contents of the existing state. It extends the state with a fresh
singleton cell, at some location p, assigning it v as contents.
The fresh cell is then described by the heap predicate p ~~> v.
The evaluation of val_ref v produces the value val_loc p. Thus,
if r denotes the result value, we have r = val_loc p for some p.
In the corresponding specification shown below, observe how the
location p is existentially quantified in the postcondition.

Parameter triple_ref : ∀ v,

triple (val_ref v)

\[]

(fun (r:val) ⇒ \∃ (p:loc), \[r = val_loc p] \* p ~~> v).

Using the notation funloc p ⇒ H as a shorthand for
fun (r:val) ⇒ \∃ (p:loc), \[r = val_loc p] \* H,
the specification for val_ref becomes more concise.

Recall that val_free denotes the operation for deallocating a cell
at a given address. A call of the form val_free p executes safely
in a state p ~~> v. The operation leaves an empty state, and
asserts that the return value, named r, is equal to unit.

## Review of the structural rules

The consequence rule allows to strengthen the precondition and
weaken the postcondition.

In practice, it is most convenient to exploit a rule that combines
both frame and consequence into a single rule, as stated next.
(Remark: this "combined structural rule" was proved as an exercise
in chapter SLFHimpl.)

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

The two extraction rules enable to extract pure facts and existentially
quantified variables, from the precondition into the Coq context.

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

(P → triple t H Q) →

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

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

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

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

## Verification proof in Separation Logic

### Proof of incr

let incr p =

p := !p + 1

let incr p =

let n = !p in

let m = n+1 in

p := m

Definition incr : val :=

val_fun "p" (

trm_let "n" (trm_app val_get (trm_var "p")) (

trm_let "m" (trm_app (trm_app val_add

(trm_var "n")) (val_int 1)) (

trm_app (trm_app val_set (trm_var "p")) (trm_var "m")))).

Alternatively, using notation and coercions, the same program can be
written as shown below.

Let us check that the two definitions are indeed the same.

Recall from the first chapter the specification of the increment function.
Its precondition requires a singleton state of the form p ~~> n.
Its postcondition describes a state of the form p ~~> (n+1).

We next show a detailed proof for this specification. It exploits:

- the structural reasoning rules,
- the reasoning rules for terms,
- the specification of the primitive functions,
- the xsimpl tactic for simplifying entailments.

Proof using.

(* initialize the proof *)

intros. applys triple_app_fun. { reflexivity. } simpl.

(* reason about let n = .. *)

applys triple_let.

(* reason about !p *)

{ apply triple_get. }

(* name n' the result of !p *)

intros n'. simpl.

(* substitute away the equality n' = n *)

apply triple_hpure. intros →.

(* reason about let m = .. *)

applys triple_let.

(* apply the frame rule to put aside p ~~> n *)

{ applys triple_conseq_frame.

(* reason about n+1 in the empty state *)

{ applys triple_add. }

{ xsimpl. }

{ xsimpl. } }

(* name m' the result of n+1 *)

intros m'. simpl.

(* substitute away the equality m' = m *)

apply triple_hpure. intros →.

(* reason about p := m *)

{ applys triple_set. }

Qed.

### Proof of succ_using_incr

let succ_using_incr n =

let r = ref n in

incr r;

let x = !r in

free r;

x

Definition succ_using_incr : val :=

Fun 'n :=

Let 'r := val_ref 'n in

incr 'r ';

Let 'x := '! 'r in

val_free 'r ';

'x.

Recall the specification of succ_using_incr.

Lemma triple_succ_using_incr : ∀ (n:int),

triple (trm_app succ_using_incr n)

\[]

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

#### Exercise: 3 stars, standard, recommended (triple_succ_using_incr)

Verify the function triple_succ_using_incr. Hint: follow the pattern of triple_incr. Hint: use applys triple_seq for reasoning about a sequence. Hint: use applys triple_val for reasoning about the final return value, namely x.Proof using. (* FILL IN HERE *) Admitted.

☐

The matter of the next chapter is to introduce additional
technology to streamline the proof process, notably by:
The rest of this chapter is concerned with alternative statements
for the reasoning rules, and with the proofs of the reasoning rules.

- automating the application of the frame rule
- eliminating the need to manipulate program variables and substitutions during the verification proof.

Recall the specification for division.

Parameter triple_div : ∀ n

_{1}n

_{2},

n

_{2}≠ 0 →

triple (val_div n

_{1}n

_{2})

\[]

(fun r ⇒ \[r = val_int (Z.quot n

_{1}n

_{2})]).

Equivalently, we could place the requirement n

_{2}≠ 0 in the precondition:Parameter triple_div' : ∀ n

_{1}n

_{2},

triple (val_div n

_{1}n

_{2})

\[n

_{2}≠ 0]

(fun r ⇒ \[r = val_int (Z.quot n

_{1}n

_{2})]).

Let us formally prove that the two presentations are equivalent.

#### Exercise: 1 star, standard, recommended (triple_div_from_triple_div')

Prove triple_div by exploiting triple_div'. Hint: the key proof step is applys triple_conseqLemma triple_div_from_triple_div' : ∀ n

_{1}n

_{2},

n

_{2}≠ 0 →

triple (val_div n

_{1}n

_{2})

\[]

(fun r ⇒ \[r = val_int (Z.quot n

_{1}n

_{2})]).

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

☐

#### Exercise: 2 stars, standard, recommended (triple_div'_from_triple_div)

Prove triple_div' by exploiting triple_div. Hint: the first key proof step is applys triple_hpure. Yet some preliminary rewriting is required for this tactic to apply. Hint: the second key proof step is applys triple_conseq.Lemma triple_div'_from_triple_div : ∀ n

_{1}n

_{2},

triple (val_div n

_{1}n

_{2})

\[n

_{2}≠ 0]

(fun r ⇒ \[r = val_int (Z.quot n

_{1}n

_{2})]).

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

☐

Recall the Separation Logic let rule.

Parameter triple_let : ∀ x t

_{1}t

_{2}H Q Q

_{1},

triple t

_{1}H Q

_{1}→

(∀ v, triple (subst x v t

_{2}) (Q

_{1}v) Q) →

triple (trm_let x t

_{1}t

_{2}) H Q.

At first sight, it seems that, to reason about let x = t
The "let-frame" rule combines the rule for let-bindings with the
frame rule to make it more explicit that the precondition H
may be decomposed in the form H
The corresponding statement is as follows.

_{1}in t_{2}in a state described by precondition H, we need to first reason about t_{1}in that same state. Yet, t_{1}may well require only a subset of the state H to evaluate, and not all of H._{1}\* H_{2}, where H_{1}is the part needed by t_{1}, and H_{2}denotes the rest of the state. The part of the state covered by H_{2}remains unmodified during the evaluation of t_{1}, and appears as part of the precondition of t_{2}.Lemma triple_let_frame : ∀ x t

_{1}t

_{2}H H

_{1}H

_{2}Q Q

_{1},

triple t

_{1}H

_{1}Q

_{1}→

H ==> H

_{1}\* H

_{2}→

(∀ v, triple (subst x v t

_{2}) (Q

_{1}v \* H

_{2}) Q) →

triple (trm_let x t

_{1}t

_{2}) H Q.

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

☐

The proofs for the Separation Logic reasoning rules all follow
a similar pattern: first establish a corresponding rule for
Hoare triples, then generalize it to a Separation Logic triple.
To establish a reasoning rule w.r.t. a Hoare triple, we reveal
the definition expressed in terms of the big-step semantics.

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

∀ s, H s →

∃ s' v, eval s t s' v ∧ Q v s'.
Concretely, we consider a given initial state s satisfying the
precondition, and we have to provide witnesses for the output
value v and output state s' such that the reduction holds and
the postcondition holds.
Then, to lift the reasoning rule from Hoare logic to Separation
Logic, we reveal the definition of a Separation Logic triple.

Definition triple t H Q :=

∀ H', hoare t (H \* H') (Q \*+ H').
Recall that we already employed this two-step scheme in the
previous chapter, e.g., to establish the consequence rule
(rule_conseq).

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

∀ s, H s →

∃ s' v, eval s t s' v ∧ Q v s'.

Definition triple t H Q :=

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

### Proof of triple_val

The Hoare version of the reasoning rule for values is as follows.

Lemma hoare_val : ∀ v H Q,

H ==> Q v →

hoare (trm_val v) H Q.

Proof using.

(* 1. We unfold the definition of hoare. *)

introv M. intros s K

_{0}.

(* 2. We provide the witnesses for the output value and heap.

These witnesses are dictated by the statement of eval_val. *)

∃ s v. splits.

{ (* 3. We invoke the big-step rule eval_val *)

applys eval_val. }

{ (* 4. We establish the postcondition, exploiting the entailment hypothesis. *)

applys M. auto. }

Qed.

The Separation Logic version of the rule then follows.

Lemma triple_val : ∀ v H Q,

H ==> Q v →

triple (trm_val v) H Q.

Proof using.

(* 1. We unfold the definition of triple to reveal a hoare judgment. *)

introv M. intros H'.

(* 2. We invoke the reasoning rule hoare_val that we have just established. *)

applys hoare_val.

(* 3. We exploit the assumption and conclude using xsimpl. *)

xchange M.

Qed.

Parameter eval_seq : ∀ s

_{1}s

_{2}s

_{3}t

_{1}t

_{2}v

_{1}v,

eval s

_{1}t

_{1}s

_{2}v

_{1}→

eval s

_{2}t

_{2}s

_{3}v →

eval s

_{1}(trm_seq t

_{1}t

_{2}) s

_{3}v.

The Hoare triple version of the reasoning rule is proved as follows.
This lemma, called hoare_seq, has the same statement as triple_seq,
except with occurrences of triple replaced with hoare.

Lemma hoare_seq : ∀ t

_{1}t

_{2}H Q H

_{1},

hoare t

_{1}H (fun v ⇒ H

_{1}) →

hoare t

_{2}H

_{1}Q →

hoare (trm_seq t

_{1}t

_{2}) H Q.

Proof using.

(* 1. We unfold the definition of hoare.

Let K

_{0}describe the initial state. *)

introv M

_{1}M

_{2}. intros s K

_{0}. (* optional: *) unfolds hoare.

(* 2. We exploit the first hypothesis to obtain information about

the evaluation of the first subterm t

_{1}.

The state before t

_{1}executes is described by K

_{0}.

The state after t

_{1}executes is described by K

_{1}. *)

forwards (s

_{1}'&v

_{1}&R

_{1}&K

_{1}): (rm M

_{1}) K

_{0}.

(* 3. We exploit the second hypothesis to obtain information about

the evaluation of the first subterm t

_{2}.

The state before t

_{2}executes is described by K

_{1}.

The state after t

_{2}executes is described by K

_{2}. *)

forwards (s

_{2}'&v

_{2}&R

_{2}&K

_{2}): (rm M

_{2}) K

_{1}.

(* 4. We provide witness for the output value and heap.

They correspond to those produced by the evaluation of t

_{2}. *)

∃ s

_{2}' v

_{2}. split.

{ (* 5. We invoke the big-step rule. *)

applys eval_seq R

_{1}R

_{2}. }

{ (* 6. We establish the final postcondition, which is directly

inherited from the reasoning on t

_{2}. *)

apply K

_{2}. }

Qed.

The Separation Logic reasoning rule is proved as follows.

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.

(* 1. We unfold the definition of triple to reveal a hoare judgment. *)

introv M

_{1}M

_{2}. intros H'. (* optional: *) unfolds triple.

(* 2. We invoke the reasoning rule hoare_seq that we have just

established. *)

applys hoare_seq.

{ (* 3. For the hypothesis on the first subterm t

_{1},

we can invoke directly our first hypothesis. *)

applys M

_{1}. }

{ applys M

_{2}. }

Qed.

Parameter eval_let : ∀ s

_{1}s

_{2}s

_{3}x t

_{1}t

_{2}v

_{1}v,

eval s

_{1}t

_{1}s

_{2}v

_{1}→

eval s

_{2}(subst x v

_{1}t

_{2}) s

_{3}v →

eval s

_{1}(trm_let x t

_{1}t

_{2}) s

_{3}v.

#### Exercise: 2 stars, standard, recommended (triple_let)

Following the same proof scheme as for triple_seq, establish the reasoning rule for triple_let, whose statement appears earlier in this file. Make sure to first state and prove the lemma hoare_let, which has the same statement as triple_let yet with occurrences of triple replaced with hoare.(* FILL IN HERE *)

☐

Parameter eval_add : ∀ s n

_{1}n

_{2},

eval s (val_add (val_int n

_{1}) (val_int n

_{2})) s (val_int (n

_{1}+ n

_{2})).

In the proof, we will need to use the following result,
established in the first chapter.

As usual, we first establish a Hoare triple.

Lemma hoare_add : ∀ H n

_{1}n

_{2},

hoare (val_add n

_{1}n

_{2})

H

(fun r ⇒ \[r = val_int (n

_{1}+ n

_{2})] \* H).

Proof using.

intros. intros s K

_{0}. ∃ s (val_int (n

_{1}+ n

_{2})). split.

{ applys eval_add. }

{ rewrite hstar_hpure_l. split.

{ auto. }

{ applys K

_{0}. } }

Qed.

Deriving triple_add is then straightforward.

Lemma triple_add : ∀ n

_{1}n

_{2},

triple (val_add n

_{1}n

_{2})

\[]

(fun r ⇒ \[r = val_int (n

_{1}+ n

_{2})]).

Proof using.

intros. intros H'. applys hoare_conseq.

{ applys hoare_add. } { xsimpl. } { xsimpl. auto. }

Qed.

Parameter eval_div' : ∀ s n

_{1}n

_{2},

n

_{2}≠ 0 →

eval s (val_div (val_int n

_{1}) (val_int n

_{2})) s (val_int (Z.quot n

_{1}n

_{2})).

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

Following the same proof scheme as for triple_add, establish the reasoning rule for triple_div. Make sure to first state and prove hoare_div, which is like triple_div except with hoare instead of triple.(* FILL IN HERE *)

☐

## Proofs for primitive operations operating on the state

Inductive hval : Type :=

| hval_val : val → hval.

### Read in a reference

Parameter eval_get : ∀ v s p,

Fmap.indom s p →

Fmap.read s p = v →

eval s (val_get (val_loc p)) s v.

We reformulate this rule by isolating from the current state s
the singleton heap made of the cell at location p, and let s

_{2}denote the rest of the heap. When the singleton heap is described as Fmap.single p v, then v is the result value returned by get p.Lemma eval_get_sep : ∀ s s

_{2}p v,

s = Fmap.union (Fmap.single p v) s

_{2}→

eval s (val_get (val_loc p)) s v.

The proof of this lemma is of little interest. We show it only to
demonstrate that it relies only a few basic facts related to finite
maps.

Proof using.

introv →. forwards Dv: Fmap.indom_single p v.

applys eval_get.

{ applys× Fmap.indom_union_l. }

{ rewrite× Fmap.read_union_l. rewrite× Fmap.read_single. }

Qed.

Our goal is to establish the triple:

triple (val_get p)

(p ~~> v)

(fun r ⇒ \[r = v] \* (p ~~> v)).
Establishing this lemma requires us to reason about propositions
of the form (\[P] \* H) h and (p ~~> v) h. To that end,
recall from the first chapter the following two lemmas.
The first one was already used in the proof of triple_add.
The second one in the inversion lemma for the singleton heap
predicate.

triple (val_get p)

(p ~~> v)

(fun r ⇒ \[r = v] \* (p ~~> v)).

Parameter hstar_hpure_l' : ∀ P H h,

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

Parameter hsingle_inv: ∀ p v h,

(p ~~> v) h →

h = Fmap.single p v.

We establish the specification of get first w.r.t. to
the hoare judgment.

Lemma hoare_get : ∀ H v p,

hoare (val_get p)

((p ~~> v) \* H)

(fun r ⇒ \[r = v] \* (p ~~> v) \* H).

Proof using.

(* 1. We unfold the definition of hoare. *)

intros. intros s K

_{0}.

(* 2. We provide the witnesses for the reduction,

as dictated by eval_get_sep. *)

∃ s v. split.

{ (* 3. To justify the reduction using eval_get_sep, we need to

argue that the state s decomposes as a singleton heap

Fmap.single p v and the rest of the state s

_{2}. This is

obtained by eliminating the star in hypothesis K

_{0}. *)

destruct K

_{0}as (s

_{1}&s

_{2}&P

_{1}&P

_{2}&D&U).

(* 4. Inverting (p ~~> v) h

_{1}simplifies the goal. *)

lets E

_{1}: hsingle_inv P

_{1}. subst s

_{1}.

(* 5. At this point, the goal matches exactly eval_get_sep. *)

applys eval_get_sep U. }

{ (* 6. To establish the postcondition, we reuse justify the

pure fact \v = v, and check that the state, which

has not changed, satisfy the same heap predicate as

in the precondition. *)

rewrite hstar_hpure_l. auto. }

Qed.

Deriving the Separation Logic triple follows the usual pattern.

Lemma triple_get : ∀ v p,

triple (val_get p)

(p ~~> v)

(fun r ⇒ \[r = v] \* (p ~~> v)).

Proof using.

intros. intros H'. applys hoare_conseq.

{ applys hoare_get. }

{ xsimpl. }

{ xsimpl. auto. }

Qed.

### Allocation of a reference

Parameter eval_ref : ∀ s v p,

¬ Fmap.indom s p →

eval s (val_ref v) (Fmap.update s p v) (val_loc p).

Let us reformulate eval_ref to replace references to Fmap.indom
and Fmap.update with references to Fmap.single and Fmap.disjoint.
Concretely, ref v extends the state from s

_{1}to s_{1}\u s_{2}, where s_{2}denotes the singleton heap Fmap.single p v, and with the requirement that Fmap.disjoint s_{2}s_{1}, to capture freshness.Lemma eval_ref_sep : ∀ s

_{1}s

_{2}v p,

s

_{2}= Fmap.single p v →

Fmap.disjoint s

_{2}s

_{1}→

eval s

_{1}(val_ref v) (Fmap.union s

_{2}s

_{1}) (val_loc p).

Proof using.

It is not needed to follow through this proof.

introv → D. forwards Dv: Fmap.indom_single p v.

rewrite <- Fmap.update_eq_union_single. applys× eval_ref.

{ intros N. applys× Fmap.disjoint_inv_not_indom_both D N. }

Qed.

rewrite <- Fmap.update_eq_union_single. applys× eval_ref.

{ intros N. applys× Fmap.disjoint_inv_not_indom_both D N. }

Qed.

In order to apply the rules eval_ref or eval_ref_sep, we need
to be able to synthetize fresh locations. The following lemma
(from Fmap.v) captures the existence, for any state s, of
a non-null location p not already bound in s.

We reformulate the lemma above in a way that better matches
the premise of the lemma eval_ref_sep, which we need to apply
for establishing the specification of ref.
This reformulation, shown below, asserts that, for any h,
there existence a non-null location p such that the singleton
heap Fmap.single p v is disjoint from h.

It is not needed to follow through this proof.

The proof of the Hoare triple for ref is as follows.

Lemma hoare_ref : ∀ H v,

hoare (val_ref v)

H

(fun r ⇒ (\∃ p, \[r = val_loc p] \* p ~~> v) \* H).

Proof using.

(* 1. We unfold the definition of hoare. *)

intros. intros s

_{1}K

_{0}.

(* 2. We claim the disjointness relation

Fmap.disjoint (Fmap.single p v) s

_{1}. *)

forwards× (p&D): (single_fresh s

_{1}v).

(* 3. We provide the witnesses for the reduction,

as dictated by eval_ref_sep. *)

∃ ((Fmap.single p v) \u s

_{1}) (val_loc p). split.

{ (* 4. We exploit eval_ref_sep, which has exactly the desired shape! *)

applys eval_ref_sep D. auto. }

{ (* 5. We establish the postcondition

(\∃ p, \[r = val_loc p] \* p ~~> v) \* H

by providing p and the relevant pieces of heap. *)

applys hstar_intro.

{ ∃ p. rewrite hstar_hpure_l.

split. { auto. } { applys¬hsingle_intro. } }

{ applys K

_{0}. }

{ applys D. } }

Qed.

We then derive the Separation Logic triple as usual.

Lemma triple_ref : ∀ v,

triple (val_ref v)

\[]

(funloc p ⇒ p ~~> v).

Proof using.

intros. intros H'. applys hoare_conseq.

{ applys hoare_ref. }

{ xsimpl. }

{ xsimpl. auto. }

Qed.

End Proofs.

## Alternative rule for values

----------------------------

{\[]} v {fun r ⇒ \[r = v]}

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

Prove that the alternative rule for values derivable from triple_val. Hint: use the tactic xsimpl to conclude the proof.Lemma triple_val_minimal : ∀ v,

triple (trm_val v) \[] (fun r ⇒ \[r = v]).

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

☐

#### Exercise: 2 stars, standard, recommended (triple_val_minimal)

More interestingly, prove that triple_val is derivable from triple_val_minimal. Hint: you will need to exploit the appropriate structural rule(s).Lemma triple_val' : ∀ v H Q,

H ==> Q v →

triple (trm_val v) H Q.

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

☐

## Reasoning rules for recursive functions

_{1}, and the corresponding value is written val_fix f x t

_{1}.

Parameter triple_fix : ∀ f x t

_{1}H Q,

H ==> Q (val_fix f x t

_{1}) →

triple (trm_fix f x t

_{1}) H Q.

The reasoning rule that corresponds to beta-reduction for
a recursive function involves two substitutions: a first
substitution for recursive occurrences of the function,
followed with a second substitution for the argument
provided to the call.

Parameter triple_app_fix : ∀ v

_{1}v

_{2}f x t

_{1}H Q,

v

_{1}= val_fix f x t

_{1}→

triple (subst x v

_{2}(subst f v

_{1}t

_{1})) H Q →

triple (trm_app v

_{1}v

_{2}) H Q.

### Proof of triple_fun and triple_fix

### Proof of triple_if

Lemma eval_if : ∀ s

_{1}s

_{2}b v t

_{1}t

_{2},

eval s

_{1}(if b then t

_{1}else t

_{2}) s

_{2}v →

eval s

_{1}(trm_if b t

_{1}t

_{2}) s

_{2}v.

Proof using.

intros. case_if; applys eval_if; auto_false.

Qed.

The reasoning rule for conditional w.r.t. Hoare triples is as follows.

Lemma hoare_if_case : ∀ b t

_{1}t

_{2}H Q,

(b = true → hoare t

_{1}H Q) →

(b = false → hoare t

_{2}H Q) →

hoare (trm_if b t

_{1}t

_{2}) H Q.

Proof using.

introv M

_{1}M

_{2}. intros s K

_{0}. destruct b.

{ forwards× (s

_{1}'&v

_{1}&R

_{1}&K

_{1}): (rm M

_{1}) K

_{0}.

∃ s

_{1}' v

_{1}. split×. { applys× eval_if. } }

{ forwards× (s

_{1}'&v

_{1}&R

_{1}&K

_{1}): (rm M

_{2}) K

_{0}.

∃ s

_{1}' v

_{1}. split×. { applys× eval_if. } }

Qed.

The corresponding Separation Logic reasoning rule is as follows.

Lemma triple_if_case : ∀ b t

_{1}t

_{2}H Q,

(b = true → triple t

_{1}H Q) →

(b = false → triple t

_{2}H Q) →

triple (trm_if (val_bool b) t

_{1}t

_{2}) H Q.

Proof using.

unfold triple. introv M

_{1}M

_{2}. intros H'.

applys hoare_if_case; intros Eb.

{ applys× M

_{1}. }

{ applys× M

_{2}. }

Qed.

Observe that the above proofs contain a fair amount of duplication,
due to the symmetry between the b = true and b = false branches.
If we state the reasoning rules using Coq's conditional just like
it appears in the evaluation rule eval_if, we can better factorize
the proof script.

Lemma hoare_if : ∀ (b:bool) t

_{1}t

_{2}H Q,

hoare (if b then t

_{1}else t

_{2}) H Q →

hoare (trm_if b t

_{1}t

_{2}) H Q.

Proof using.

introv M

_{1}. intros s K

_{0}.

forwards (s'&v&R

_{1}&K

_{1}): (rm M

_{1}) K

_{0}.

∃ s' v. split. { applys eval_if R

_{1}. } { applys K

_{1}. }

Qed.

Lemma triple_if : ∀ b t

_{1}t

_{2}H Q,

triple (if b then t

_{1}else t

_{2}) H Q →

triple (trm_if (val_bool b) t

_{1}t

_{2}) H Q.

Proof using.

unfold triple. introv M

_{1}. intros H'. applys hoare_if. applys M

_{1}.

Qed.

### Proof of triple_app_fun

_{1}) v

_{2}provided that they hold for the term subst x v

_{2}t

_{1}.

Parameter eval_app_fun : ∀ s

_{1}s

_{2}v

_{1}v

_{2}x t

_{1}v,

v

_{1}= val_fun x t

_{1}→

eval s

_{1}(subst x v

_{2}t

_{1}) s

_{2}v →

eval s

_{1}(trm_app v

_{1}v

_{2}) s

_{2}v.

Lemma hoare_app_fun : ∀ v

_{1}v

_{2}x t

_{1}H Q,

v

_{1}= val_fun x t

_{1}→

hoare (subst x v

_{2}t

_{1}) H Q →

hoare (trm_app v

_{1}v

_{2}) H Q.

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

☐

Lemma triple_app_fun : ∀ x v

_{1}v

_{2}t

_{1}H Q,

v

_{1}= val_fun x t

_{1}→

triple (subst x v

_{2}t

_{1}) H Q →

triple (trm_app v

_{1}v

_{2}) H Q.

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

☐

### Write in a reference

Parameter eval_set : ∀ m p v,

Fmap.indom m p →

eval m (val_set (val_loc p) v) (Fmap.update m p v) val_unit.

As for get, we first reformulate this lemma, to replace
references to Fmap.indom and Fmap.update with references
to Fmap.union, Fmap.single, and Fmap.disjoint, to
prepare for the introduction of separating conjunctions.

Lemma eval_set_sep : ∀ s

_{1}s

_{2}h

_{2}p v

_{1}v

_{2},

s

_{1}= Fmap.union (Fmap.single p v

_{1}) h

_{2}→

s

_{2}= Fmap.union (Fmap.single p v

_{2}) h

_{2}→

Fmap.disjoint (Fmap.single p v

_{1}) h

_{2}→

eval s

_{1}(val_set (val_loc p) v

_{2}) s

_{2}val_unit.

Proof using.

It is not needed to follow through this proof.

introv → → D. forwards Dv: Fmap.indom_single p v

applys_eq eval_set.

{ rewrite× Fmap.update_union_l. fequals.

rewrite× Fmap.update_single. }

{ applys× Fmap.indom_union_l. }

Qed.

_{1}.applys_eq eval_set.

{ rewrite× Fmap.update_union_l. fequals.

rewrite× Fmap.update_single. }

{ applys× Fmap.indom_union_l. }

Qed.

The proof of the Hoare rule for set makes use of the following
fact (from Fmap.v) about Fmap.disjoint: when one of its argument is
a singleton map, the value stored in that singleton map is irrelevant.

Check Fmap.disjoint_single_set : ∀ p v

Fmap.disjoint (Fmap.single p v

Fmap.disjoint (Fmap.single p v
We will make use of three lemmas, all introduced in the first chapter:
Let's now dive in the proof of the Hoare triple for set.

Check Fmap.disjoint_single_set : ∀ p v

_{1}v_{2}h_{2},Fmap.disjoint (Fmap.single p v

_{1}) h_{2}→Fmap.disjoint (Fmap.single p v

_{2}) h_{2}.- the lemma hstar_hpure_l, already used earlier in this chapter to reformulate (\[P] \* H) h as P ∧ H h,
- the lemma hsingle_intro, to prove (p ~~> v) (Fmap.single p v),
- and the lemma hstar_intro, to prove (H
_{1}\* H_{2}) (h_{1}\u h_{2}).

Lemma hoare_set : ∀ H v p v',

hoare (val_set (val_loc p) v)

((p ~~> v') \* H)

(fun _ ⇒ (p ~~> v) \* H).

Proof using.

(* 1. We unfold the definition of hoare. *)

intros. intros s

_{1}K

_{0}.

(* 2. We decompose the star from the precondition. *)

destruct K

_{0}as (h

_{1}&h

_{2}&P

_{1}&P

_{2}&D&U).

(* 3. We also decompose the singleton heap predicate from it. *)

lets E

_{1}: hsingle_inv P

_{1}.

(* 4. We provide the witnesses as guided by eval_set_sep. *)

∃ ((Fmap.single p v) \u h

_{2}) val_unit. split.

{ (* 5. The evaluation subgoal matches the statement of eval_set_sep. *)

subst h

_{1}. applys eval_set_sep U D. auto. }

{ (* 7. Then establish the star. *)

applys hstar_intro.

{ (* 8. We establish the heap predicate p ~~> w *)

applys hsingle_intro. }

{ applys P

_{2}. }

{ (* 9. Finally, we justify disjointness using the lemma

Fmap.disjoint_single_set introduced earlier. *)

subst h

_{1}. applys Fmap.disjoint_single_set D. } }

Qed.

We then derive the Separation Logic triple as usual.

Lemma triple_set : ∀ w p v,

triple (val_set (val_loc p) w)

(p ~~> v)

(fun _ ⇒ p ~~> w).

Proof using.

intros. intros H'. applys hoare_conseq.

{ applys hoare_set. }

{ xsimpl. }

{ xsimpl. }

Qed.

### Deallocation of a reference

Parameter eval_free : ∀ s p,

Fmap.indom s p →

eval s (val_set (val_loc p)) (Fmap.remove s p) val_unit.

Let us reformulate eval_free to replace references to Fmap.indom
and Fmap.remove with references to Fmap.single and Fmap.union
and Fmap.disjoint. The details are not essential, thus omitted.

Parameter eval_free_sep : ∀ s

_{1}s

_{2}v p,

s

_{1}= Fmap.union (Fmap.single p v) s

_{2}→

Fmap.disjoint (Fmap.single p v) s

_{2}→

eval s

_{1}(val_free p) s

_{2}val_unit.

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

Prove the Hoare triple for the operation free. Hint: adapt the proof of lemma hoare_set.Lemma hoare_free : ∀ H p v,

hoare (val_free (val_loc p))

((p ~~> v) \* H)

(fun _ ⇒ H).

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

☐

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

Derive from the Hoare triple for the operation free the corresponding Separation Logic triple. Hint: adapt the proof of lemma triple_set.Lemma triple_free : ∀ p v,

triple (val_free (val_loc p))

(p ~~> v)

(fun _ ⇒ \[]).

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

☐

The proof that, e.g., triple_add is a consequence of
hoare_add follows the same pattern as many other similar
proofs, each time invoking the lemma hoare_conseq.
Thus, we could attempt at factorizing this proof pattern.
The following lemma corresponds to such an attempt.

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

Prove the lemma triple_of_hoare stated below.Lemma triple_of_hoare : ∀ t H Q,

(∀ H', ∃ Q', hoare t (H \* H') Q'

∧ Q' ===> Q \*+ H') →

triple t H Q.

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

☐

#### Exercise: 2 stars, standard, optional (triple_add')

Prove that triple_add is a consequence of hoare_add by exploiting triple_of_hoare.Lemma triple_add' : ∀ n

_{1}n

_{2},

triple (val_add n

_{1}n

_{2})

\[]

(fun r ⇒ \[r = val_int (n

_{1}+ n

_{2})]).

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

☐

A general principle is that if t
Let us formalize this principle.
Two (closed) terms are semantically equivalent, written
trm_equiv t

_{1}has the same semantics as t_{2}(w.r.t. the big-step evaluation judgment eval), then t_{1}and t_{2}satisfy the same triples._{1}t_{2}, if two terms, when evaluated in the same state, produce the same output.
Two terms that are equivalent satisfy the same Separation Logic
triples (and the same Hoare triples).
Indeed, the definition of a Separation Logic triple directly depends
on the notion of Hoare triple, and the latter directly depends
on the semantics captured by the predicate eval.
Let us formalize the result in three steps.
eval_like t

_{1}t_{2}asserts that t_{2}evaluates like t_{1}. In particular, this relation hold whenever t_{2}reduces in small-step to t_{1}.
For example eval_like t (trm_let x t x) holds, reflecting the
fact that let x = t in x reduces in small-step to t.

Lemma eval_like_eta_reduction : ∀ (t:trm) (x:var),

eval_like t (trm_let x t x).

Proof using.

introv R. applys eval_let R.

simpl. rewrite var_eq_spec. case_if. applys eval_val.

Qed.

It turns out that the symmetric relation eval_like (trm_let x t x) t
also holds: the term t does not exhibit more behaviors than those
of let x = t in x.

Lemma eval_like_eta_expansion : ∀ (t:trm) (x:var),

eval_like (trm_let x t x) t.

Proof using.

introv R. inverts R as. introv R

_{1}R

_{2}.

simpl in R

_{2}. rewrite var_eq_spec in R

_{2}. case_if.

inverts R

_{2}. auto.

Qed.

We deduce that a term t denotes a program equivalent to
the program let x = t in x.

Lemma trm_equiv_eta : ∀ (t:trm) (x:var),

trm_equiv t (trm_let x t x).

Proof using.

intros. intros s s' v. iff M.

{ applys eval_like_eta_reduction M. }

{ applys eval_like_eta_expansion M. }

Qed.

If eval_like t

_{1}t_{2}, then any triple that holds for t_{1}also holds for t_{2}.Lemma hoare_eval_like : ∀ t

_{1}t

_{2}H Q,

eval_like t

_{1}t

_{2}→

hoare t

_{1}H Q →

hoare t

_{2}H Q.

Proof using.

introv E M

_{1}K

_{0}. forwards (s'&v&R

_{1}&K

_{1}): M

_{1}K

_{0}.

∃ s' v. split. { applys E R

_{1}. } { applys K

_{1}. }

Qed.

Lemma triple_eval_like : ∀ t

_{1}t

_{2}H Q,

eval_like t

_{1}t

_{2}→

triple t

_{1}H Q →

triple t

_{2}H Q.

Proof using.

introv E M

_{1}. intros H'. applys hoare_eval_like E. applys M

_{1}.

Qed.

It follows that if two terms are equivalent, then they admit
the same triples.

Lemma triple_trm_equiv : ∀ t

_{1}t

_{2}H Q,

trm_equiv t

_{1}t

_{2}→

triple t

_{1}H Q ↔ triple t

_{2}H Q.

Proof using.

introv E. unfolds trm_equiv. iff M.

{ applys triple_eval_like M. introv R. applys× E. }

{ applys triple_eval_like M. introv R. applys× E. }

Qed.

The reasoning rule triple_eval_like has a number of practical applications.
One, show below, is to revisit the proof of triple_app_fun in a
much more succint way, by arguing that trm_app (val_fun x t

_{1}) and subst x v_{2}t_{1}are equivalent terms, hence they admit the same behavior.Lemma triple_app_fun : ∀ x v

_{1}v

_{2}t

_{1}H Q,

v

_{1}= val_fun x t

_{1}→

triple (subst x v

_{2}t

_{1}) H Q →

triple (trm_app v

_{1}v

_{2}) H Q.

Proof using.

introv E M

_{1}. applys triple_eval_like M

_{1}.

introv R. applys eval_app_fun E R.

Qed.

Another application is the following rule, which allows to modify the
parenthesis structure of a sequence, from t

_{1}; (t_{2}; t_{3}) to (t_{1};t_{2}); t_{3}.Lemma triple_trm_seq_assoc : ∀ t

_{1}t

_{2}t

_{3}H Q,

triple (trm_seq (trm_seq t

_{1}t

_{2}) t

_{3}) H Q →

triple (trm_seq t

_{1}(trm_seq t

_{2}t

_{3})) H Q.

Proof using.

introv M. applys triple_eval_like M. clear M.

introv R. inverts R as. introv R

_{1}R

_{3}. inverts R

_{1}as. introv R

_{1}R

_{2}.

applys eval_seq R

_{1}. applys eval_seq R

_{2}R

_{3}.

Qed.

Such a change in the parenthesis structure of a sequence can be helfpul
to apply the frame rule around t
Another useful application of the lemma triple_eval_like appears in
chapter SLFAffine, for proving the equivalence of two versions of the
garbage collection rule.

_{1};t_{2}, for example.
Recall the specification for the function ref.

Its postcondition could be equivalently stated by using, instead
of an existential quantifier \∃, a pattern matching.

Parameter triple_ref' : ∀ v,

triple (val_ref v)

\[]

(fun r ⇒ match r with

| val_loc p ⇒ (p ~~> v)

| _ ⇒ \[False]

end).

However, the pattern-matching presentation is less readable and
would be fairly cumbersome to work with in practice. Thus, we
systematically prefer using existentials.