LibSepMinimalAppendix - Minimalistic Soundness Proof

This file contains a stand-alone, minimalistic formalization of the soundness of Separation Logic reasoning rules with respect to an omni-big-step semantics. For a development grounded with respect to a small-step semantics, see the two approaches described in chapter Triples.

Source Language

Syntax

Set Implicit Arguments.
From SLF Require Export LibString LibCore.
From SLF Require Export LibSepTLCbuffer LibSepFmap.
Module Fmap := LibSepFmap.
Variables are defined as strings, var_eq denotes boolean comparison.
Definition var : Type := string.
Definition var_eq := String.string_dec.
Locations are defined as natural numbers.
Definition loc : Type := nat.
Primitive operations include memory operations, as well as addition and division to illustrate a total and a partial arithmetic operations.
Inductive prim : Type :=
  | val_ref : prim
  | val_get : prim
  | val_set : prim
  | val_free : prim
  | val_add : prim
  | val_div : prim
  | val_rand : prim.
The grammar of closed values (assumed to contain no free variables) includes values of ground types, primitive operations, and closures.
Inductive val : Type :=
  | val_unit : val
  | val_bool : bool → val
  | val_int : int → val
  | val_loc : loc → val
  | val_prim : prim → val
  | val_fix : var → var → trm → val

The grammar of terms includes closed values, variables, functions, applications, let-binding and conditional.

with trm : Type :=
  | trm_val : val → trm
  | trm_var : var → trm
  | trm_fix : var → var → trm → trm
  | trm_app : trm → trm → trm
  | trm_let : var → trm → trm → trm
  | trm_if : trm → trm → trm → trm.
Coercions are used to improve conciseness in the statment of evaluation rules.
Coercion val_bool : bool >-> val.
Coercion val_int : Z >-> val.
Coercion val_loc : loc >-> val.
Coercion val_prim : prim >-> val.
Coercion trm_val : val >-> trm.
Coercion trm_var : var >-> trm.
Coercion trm_app : trm >-> Funclass.
The type of values is inhabited (useful for finite map operations).
Global Instance Inhab_val : Inhab val.
Proof. apply (Inhab_of_val val_unit). Qed.
A heap, a.k.a. heap, consists of a finite map from location to values. Finite maps are formalized in the file LibSepFmap.v. (We purposely do not use TLC's finite map library to avoid complications with typeclasses.)
Definition heap : Type := fmap loc val.
Implicit types associate meta-variable with types.
Implicit Types 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 s h : heap.

Semantics

The standard capture-avoiding substitution is written subst y w t.
Fixpoint subst (y:var) (w:val) (t:trm) : trm :=
  let aux t := subst y w t in
  let if_y_eq x t1 t2 := if var_eq x y then t1 else t2 in
  match t with
  | trm_val v ⇒ trm_val v
  | trm_var x ⇒ if_y_eq x (trm_val w) t
  | trm_fix f x t1 ⇒ trm_fix f x (if_y_eq f t1 (if_y_eq x t1 (aux t1)))
  | trm_app t1 t2 ⇒ trm_app (aux t1) (aux t2)
  | trm_let x t1 t2 ⇒ trm_let x (aux t1) (if_y_eq x t2 (aux t2))
  | trm_if t0 t1 t2 ⇒ trm_if (aux t0) (aux t1) (aux t2)
  end.

Definition of Omni-Big-Step Semantics

Implicit Types Q : val→heap→Prop.
Inductive eval : heap → trm → (val→heap→Prop) → Prop :=
  | eval_val : ∀ s v Q,
      Q v s →
      eval s (trm_val v) Q
  | eval_fix : ∀ s f x t1 Q,
      Q (val_fix f x t1) s →
      eval s (trm_fix f x t1) Q
  | eval_app_fix : ∀ s v1 v2 f x t1 Q,
      v1 = val_fix f x t1 →
      eval s (subst x v2 (subst f v1 t1)) Q →
      eval s (trm_app v1 v2) Q
  | eval_let : ∀ Q1 s x t1 t2 Q,
      eval s t1 Q1 →
      (∀ v1 s2, Q1 v1 s2 → eval s2 (subst x v1 t2) Q) →
      eval s (trm_let x t1 t2) Q
  | eval_if : ∀ s (b:bool) t1 t2 Q,
      eval s (if b then t1 else t2) Q →
      eval s (trm_if (val_bool b) t1 t2) Q
  | eval_add : ∀ s n1 n2 Q,
      Q (val_int (n1 + n2)) s →
      eval s (val_add (val_int n1) (val_int n2)) Q
  | eval_div : ∀ s n1 n2 Q,
      n2 ≠ 0 →
      Q (val_int (Z.quot n1 n2)) s →
      eval s (val_div (val_int n1) (val_int n2)) Q
  | eval_rand : ∀ s n Q,
      n > 0 →
      (∀ n1, 0 ≤ n1 < n → Q n1 s) →
      eval s (val_rand (val_int n)) Q
  | eval_ref : ∀ s v Q,
      (∀ p, ¬ Fmap.indom s p →
          Q (val_loc p) (Fmap.update s p v)) →
      eval s (val_ref v) Q
  | eval_get : ∀ s p Q,
      Fmap.indom s p →
      Q (Fmap.read s p) s →
      eval s (val_get (val_loc p)) Q
  | eval_set : ∀ s p v Q,
      Fmap.indom s p →
      Q val_unit (Fmap.update s p v) →
      eval s (val_set (val_loc p) v) Q
  | eval_free : ∀ s p Q,
      Fmap.indom s p →
      Q val_unit (Fmap.remove s p) →
      eval s (val_free (val_loc p)) Q.

Automation for Heap Equality and Heap Disjointness

For goals asserting equalities between heaps, i.e., of the form h1 = h2, we set up automation so that it performs some tidying: substitution, removal of empty heaps, normalization with respect to associativity.
#[global] Hint Rewrite union_assoc union_empty_l union_empty_r : fmap.
#[global] Hint Extern 1 (_ = _ :> heap) ⇒ subst; autorewrite with fmap.
For goals asserting disjointness between heaps, i.e., of the form Fmap.disjoint h1 h2, we set up automation to perform simplifications: substitution, exploit distributivity of the disjointness predicate over unions of heaps, and exploit disjointness with empty heaps. The tactic jauto_set used here comes from the TLC library; essentially, it destructs conjunctions and existentials.
#[global] Hint Resolve Fmap.disjoint_empty_l Fmap.disjoint_empty_r.
#[global] Hint Rewrite disjoint_union_eq_l disjoint_union_eq_r : disjoint.
#[global] Hint Extern 1 (Fmap.disjoint _ _) ⇒
  subst; autorewrite with rew_disjoint in *; jauto_set.

Heap Predicates and Entailment

Extensionality Axioms

Extensionality axioms are essential to assert equalities between heap predicates of type hprop, and between postconditions, of type val→hprop.
Axiom functional_extensionality : ∀ A B (f g:A→B),
  (∀ x, f x = g x) →
  f = g.
Axiom propositional_extensionality : ∀ (P Q:Prop),
  (P ↔ Q) →
  P = Q.

Core Heap Predicates

The type of heap predicates is named hprop.
Definition hprop := heap → Prop.
We bind a few more meta-variables.
Implicit Types P : Prop.
Implicit Types H : hprop.
Core heap predicates, and their associated notations:
  • \[] denotes the empty heap predicate
  • \[P] denotes a pure fact
  • p ~~> v denotes a singleton heap
  • H1 \* H2 denotes the separating conjunction
  • Q1 \*+ H2 denotes the separating conjunction extending a postcondition
  • \∃ x, H denotes an existential
  • \∀ x, H denotes a universal.
Definition hempty : hprop :=
  fun h ⇒ (h = Fmap.empty).
Definition hsingle (p:loc) (v:val) : hprop :=
  fun h ⇒ (h = Fmap.single p v).
Definition hstar (H1 H2 : hprop) : hprop :=
  fun h ⇒ ∃ h1 h2, H1 h1
                              ∧ H2 h2
                              ∧ Fmap.disjoint h1 h2
                              ∧ h = Fmap.union h1 h2.
Definition hexists A (J:A→hprop) : hprop :=
  fun h ⇒ ∃ x, J x h.
Definition hforall (A : Type) (J : A → hprop) : hprop :=
  fun h ⇒ ∀ x, J x h.
Definition hpure (P:Prop) : hprop := (* encoded as \∃ (p:P), \[] *)
  hexists (fun (p:P) ⇒ hempty).
Declare Scope hprop_scope.
Notation "\[]" := (hempty)
  (at level 0) : hprop_scope.
Notation "\[ P ]" := (hpure P)
  (at level 0, format "\[ P ]") : hprop_scope.
Notation "p '~~>' v" := (hsingle p v) (at level 32) : hprop_scope.
Notation "H1 '\*' H2" := (hstar H1 H2)
  (at level 41, right associativity) : hprop_scope.
Notation "Q \*+ H" := (fun x ⇒ hstar (Q x) H)
  (at level 40) : hprop_scope.
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 ']'") : hprop_scope.
Notation "'\forall' x1 .. xn , H" :=
  (hforall (fun x1 ⇒ .. (hforall (fun xn ⇒ H)) ..))
  (at level 39, x1 binder, H at level 50, right associativity,
   format "'[' '\forall' '/ ' x1 .. xn , '/ ' H ']'") : hprop_scope.

Entailment

Declare Scope hprop_scope.
Open Scope hprop_scope.
Entailment for heap predicates, written H1 ==> H2.
Definition himpl (H1 H2:hprop) : Prop :=
  ∀ h, H1 h → H2 h.
Notation "H1 ==> H2" := (himpl H1 H2) (at level 55) : hprop_scope.
Entailment between postconditions, written Q1 ===> Q2
Definition qimpl A (Q1 Q2:A→hprop) : Prop :=
  ∀ (v:A), Q1 v ==> Q2 v.
Notation "Q1 ===> Q2" := (qimpl Q1 Q2) (at level 55) : hprop_scope.
Entailment defines an order on heap predicates
Lemma himpl_refl : ∀ H,
  H ==> H.
Proof. introv M. auto. Qed.
Lemma himpl_trans : ∀ H2 H1 H3,
  (H1 ==> H2) →
  (H2 ==> H3) →
  (H1 ==> H3).
Proof. introv M1 M2. unfolds* himpl. Qed.
Lemma himpl_antisym : ∀ H1 H2,
  (H1 ==> H2) →
  (H2 ==> H1) →
  (H1 = H2).
Proof. introv M1 M2. applys pred_ext_1. intros h. iff*. Qed.
Lemma qimpl_refl : ∀ Q,
  Q ===> Q.
Proof. intros Q v. applys himpl_refl. Qed.
#[global] Hint Resolve himpl_refl qimpl_refl.

Properties of hstar

Lemma hstar_intro : ∀ H1 H2 h1 h2,
  H1 h1 →
  H2 h2 →
  Fmap.disjoint h1 h2 →
  (H1 \* H2) (Fmap.union h1 h2).
Proof. intros. ∃* h1 h2. Qed.
Lemma hstar_comm : ∀ H1 H2,
   H1 \* H2 = H2 \* H1.
Proof.
  unfold hprop, hstar. intros H1 H2. applys himpl_antisym.
  { intros h (h1&h2&M1&M2&D&U).
    rewrite* Fmap.union_comm_of_disjoint in U. ∃* h2 h1. }
  { intros h (h1&h2&M1&M2&D&U).
    rewrite* Fmap.union_comm_of_disjoint in U. ∃* h2 h1. }
Qed.
Lemma hstar_assoc : ∀ H1 H2 H3,
  (H1 \* H2) \* H3 = H1 \* (H2 \* H3).
Proof.
  intros H1 H2 H3. applys himpl_antisym; intros h.
  { intros (h'&h3&(h1&h2&M3&M4&D'&U')&M2&D&U). subst h'.
    ∃ h1 (h2 \+ h3). splits*. { applys* hstar_intro. } }
  { intros (h1&h'&M1&(h2&h3&M3&M4&D'&U')&D&U). subst h'.
    ∃ (h1 \+ h2) h3. splits*. { applys* hstar_intro. } }
Qed.
Lemma hstar_hempty_l : ∀ H,
  \[] \* H = H.
Proof.
  intros. applys himpl_antisym; intros h.
  { intros (h1&h2&M1&M2&D&U). hnf in M1. subst. rewrite* Fmap.union_empty_l. }
  { intros M. ∃ (@Fmap.empty loc val) h. splits*. { hnfs*. } }
Qed.
Lemma hstar_hexists : ∀ A (J:A→hprop) H,
  (hexists J) \* H = hexists (fun x ⇒ (J x) \* H).
Proof.
  intros. applys himpl_antisym; intros h.
  { intros (h1&h2&(x&M1)&M2&D&U). ∃* x h1 h2. }
  { intros (x&(h1&h2&M1&M2&D&U)). ∃ h1 h2. splits*. { ∃* x. } }
Qed.
Lemma hstar_hforall : ∀ H A (J:A→hprop),
  (hforall J) \* H ==> hforall (J \*+ H).
Proof.
  intros. intros h M. destruct M as (h1&h2&M1&M2&D&U). intros x. ∃* h1 h2.
Qed.
Lemma himpl_frame_l : ∀ H2 H1 H1',
  H1 ==> H1' →
  (H1 \* H2) ==> (H1' \* H2).
Proof. introv W (h1&h2&?). ∃* h1 h2. Qed.
Additional, symmetric results, useful for tactics
Lemma hstar_hempty_r : ∀ H,
  H \* \[] = H.
Proof.
  applys neutral_r_of_comm_neutral_l. applys* hstar_comm. applys* hstar_hempty_l.
Qed.
Lemma himpl_frame_r : ∀ H1 H2 H2',
  H2 ==> H2' →
  (H1 \* H2) ==> (H1 \* H2').
Proof.
  introv M. do 2 rewrite (@hstar_comm H1). applys* himpl_frame_l.
Qed.

Properties of hpure

Lemma hstar_hpure_l : ∀ P H h,
  (\[P] \* H) h = (P ∧ H h).
Proof.
  intros. apply prop_ext. unfold hpure.
  rewrite hstar_hexists. rewrite* hstar_hempty_l.
  iff (p&M) (p&M). { split*. } { ∃* p. }
Qed.
Lemma himpl_hstar_hpure_r : ∀ P H H',
  P →
  (H ==> H') →
  H ==> (\[P] \* H').
Proof. introv HP W. intros h K. rewrite* hstar_hpure_l. Qed.
Lemma himpl_hstar_hpure_l : ∀ P H H',
  (P → H ==> H') →
  (\[P] \* H) ==> H'.
Proof. introv W Hh. rewrite hstar_hpure_l in Hh. applys* W. Qed.

Properties of hexists

Lemma himpl_hexists_l : ∀ A H (J:A→hprop),
  (∀ x, J x ==> H) →
  (hexists J) ==> H.
Proof. introv W. intros h (x&Hh). applys* W. Qed.
Lemma himpl_hexists_r : ∀ A (x:A) H J,
  (H ==> J x) →
  H ==> (hexists J).
Proof. introv W. intros h. ∃ x. apply* W. Qed.
Lemma himpl_hexists : ∀ A (J1 J2:A→hprop),
  J1 ===> J2 →
  hexists J1 ==> hexists J2.
Proof.
  introv W. applys himpl_hexists_l. intros x. applys himpl_hexists_r W.
Qed.

Properties of hforall

Lemma himpl_hforall_r : ∀ A (J:A→hprop) H,
  (∀ x, H ==> J x) →
  H ==> (hforall J).
Proof. introv M. intros h Hh x. apply* M. Qed.
Lemma himpl_hforall_l : ∀ A x (J:A→hprop) H,
  (J x ==> H) →
  (hforall J) ==> H.
Proof. introv M. intros h Hh. apply* M. Qed.
Lemma himpl_hforall : ∀ A (J1 J2:A→hprop),
  J1 ===> J2 →
  hforall J1 ==> hforall J2.
Proof.
  introv W. applys himpl_hforall_r. intros x. applys himpl_hforall_l W.
Qed.

Properties of hsingle

Lemma hstar_hsingle_same_loc : ∀ p v1 v2,
  (p ~~> v1) \* (p ~~> v2) ==> \[False].
Proof.
  intros. unfold hsingle. intros h (h1&h2&E1&E2&D&E). false.
  subst. applys* Fmap.disjoint_single_single_same_inv.
Qed.

Basic Tactics for Simplifying Entailments

xsimpl performs immediate simplifications on entailment relations.
#[global] Hint Rewrite hstar_assoc hstar_hempty_l hstar_hempty_r : hstar.
Tactic Notation "xsimpl" :=
  try solve [ apply qimpl_refl ];
  try match goal with ⊢ _ ===> _ ⇒ intros ? end;
  autorewrite with hstar; repeat match goal with
  | ⊢ ?H \* _ ==> ?H \* _ ⇒ apply himpl_frame_r
  | ⊢ _ \* ?H ==> _ \* ?H ⇒ apply himpl_frame_l
  | ⊢ _ \* ?H ==> ?H \* _ ⇒ rewrite hstar_comm; apply himpl_frame_r
  | ⊢ ?H \* _ ==> _ \* ?H ⇒ rewrite hstar_comm; apply himpl_frame_l
  | ⊢ ?H ==> ?H ⇒ apply himpl_refl
  | ⊢ ?H ==> ?H' ⇒ is_evar H'; apply himpl_refl end.
Tactic Notation "xsimpl" "*" := xsimpl; auto_star.
xchange helps rewriting in entailments.
Lemma xchange_lemma : ∀ H1 H1',
  H1 ==> H1' → ∀ H H' H2,
  H ==> H1 \* H2 →
  H1' \* H2 ==> H' →
  H ==> H'.
Proof.
  introv M1 M2 M3. applys himpl_trans M2. applys himpl_trans M3.
  applys himpl_frame_l. applys M1.
Qed.
Tactic Notation "xchange" constr(M) :=
  forwards_nounfold_then M ltac:(fun K ⇒
    eapply xchange_lemma; [ eapply K | xsimpl | ]).

Separation Logic

Definition of Separation Logic triples

Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=
  ∀ s, H s → eval s t Q.

Key Properties of Omni-Big-Step Semantics

Lemma eval_conseq : ∀ s t Q1 Q2,
  eval s t Q1 →
  Q1 ===> Q2 →
  eval s t Q2.
Proof using.
  introv M W.
  asserts W': (∀ v h, Q1 v h → Q2 v h). { auto. } clear W.
  induction M; try solve [ constructors* ].
Qed.
Lemma eval_frame : ∀ h1 h2 t Q,
  eval h1 t Q →
  Fmap.disjoint h1 h2 →
  eval (Fmap.union h1 h2) t (Q \*+ (= h2)).
Proof using.
  introv M HD. gen h2. induction M; intros;
    try solve [ hint hstar_intro; constructors* ].
  { rename M into M1, H into M2, IHM into IH1, H0 into IH2.
    specializes IH1 HD. applys eval_let IH1. introv HK.
    lets (h1'&h2'&K1'&K2'&KD&KU): HK. subst. applys* IH2. }
  { rename H into M. applys eval_ref. intros p Hp.
    rewrite Fmap.indom_union_eq in Hp. rew_logic in Hp.
    destruct Hp as [Hp1 Hp2].
    rewrite* Fmap.update_union_not_r. applys hstar_intro.
    { applys* M. } { auto. } { applys* Fmap.disjoint_update_not_r. } }
  { applys eval_get. { rewrite* Fmap.indom_union_eq. }
    { rewrite* Fmap.read_union_l. applys* hstar_intro. } }
  { applys eval_set. { rewrite* Fmap.indom_union_eq. }
    { rewrite* Fmap.update_union_l. applys hstar_intro.
      { auto. } { auto. } { applys* Fmap.disjoint_update_l. } } }
  { applys eval_free. { rewrite* Fmap.indom_union_eq. }
    { rewrite* Fmap.remove_disjoint_union_l. applys hstar_intro.
      { auto. } { auto. } { applys* Fmap.disjoint_remove_l. } } }
Qed.

Structural Rules

Lemma triple_conseq : ∀ t H' Q' H Q,
  triple t H' Q' →
  H ==> H' →
  Q' ===> Q →
  triple t H Q.
Proof using. unfolds triple. introv M MH MQ HF. applys* eval_conseq. Qed.
Lemma triple_frame : ∀ t H Q H',
  triple t H Q →
  triple t (H \* H') (Q \*+ H').
Proof.
  introv M. intros h HF. lets (h1&h2&M1&M2&MD&MU): (rm HF).
  subst. specializes M M1. applys eval_conseq.
  { applys eval_frame M MD. } { xsimpl. intros h' →. applys M2. }
Qed.
Lemma triple_hexists : ∀ t (A:Type) (J:A→hprop) Q,
  (∀ (x:A), triple t (J x) Q) →
  triple t (hexists J) Q.
Proof using. introv M. intros h (x&Hh). applys M Hh. Qed.
Lemma triple_hpure : ∀ t (P:Prop) H Q,
  (P → triple t H Q) →
  triple t (\[P] \* H) Q.
Proof using.
  introv M. intros h (h1&h2&M1&M2&D&U). destruct M1 as (M1&HP).
  inverts HP. subst. rewrite Fmap.union_empty_l. applys¬M.
Qed.

Reasoning Rules for Terms

Lemma triple_val : ∀ v H Q,
  H ==> Q v →
  triple (trm_val v) H Q.
Proof using. introv M Hs. applys* eval_val. Qed.
Lemma triple_fix : ∀ f x t1 H Q,
  H ==> Q (val_fix f x t1) →
  triple (trm_fix f x t1) H Q.
Proof using. introv M Hs. applys* eval_fix. Qed.
Lemma triple_if : ∀ (b:bool) t1 t2 H Q,
  triple (if b then t1 else t2) H Q →
  triple (trm_if b t1 t2) H Q.
Proof using. introv M Hs. applys* eval_if. Qed.
Lemma triple_app_fix : ∀ v1 v2 f x t1 H Q,
  v1 = val_fix f x t1 →
  triple (subst x v2 (subst f v1 t1)) H Q →
  triple (trm_app v1 v2) H Q.
Proof using. introv E M Hs. applys* eval_app_fix. Qed.
Lemma triple_let : ∀ x t1 t2 Q1 H Q,
  triple t1 H Q1 →
  (∀ v1, triple (subst x v1 t2) (Q1 v1) Q) →
  triple (trm_let x t1 t2) H Q.
Proof using. introv M1 M2 Hs. applys* eval_let. Qed.

Specification of Primitive Operations

Lemma triple_add : ∀ n1 n2,
  triple (val_add n1 n2)
    \[]
    (fun r ⇒ \[r = val_int (n1 + n2)]).
Proof using.
  introv Hs. applys* eval_add. inverts Hs. ∃*. hnfs*.
Qed.
Lemma triple_div : ∀ n1 n2,
  n2 ≠ 0 →
  triple (val_div n1 n2)
    \[]
    (fun r ⇒ \[r = val_int (Z.quot n1 n2)]).
Proof using.
  introv Hn2 Hs. applys* eval_div. inverts Hs. ∃*. hnfs*.
Qed.
Lemma triple_rand : ∀ n,
  n > 0 →
  triple (val_rand n)
    \[]
    (fun r ⇒ \[∃ n1, r = val_int n1 ∧ 0 ≤ n1 < n]).
Proof using.
  introv Hn2 Hs. applys* eval_rand. inverts Hs.
  intros n1 Hn1. hnfs. ∃*. hnfs*.
Qed.
Lemma triple_ref : ∀ v,
  triple (val_ref v)
    \[]
    (fun r ⇒ \∃ p, \[r = val_loc p] \* p ~~> v).
Proof using.
  intros. intros s1 K. applys eval_ref. intros p D.
  inverts K. rewrite Fmap.update_empty. ∃ p.
  rewrite hstar_hpure_l. split*. hnfs*.
Qed.
Lemma triple_get : ∀ v p,
  triple (val_get p)
    (p ~~> v)
    (fun r ⇒ \[r = v] \* (p ~~> v)).
Proof using.
  intros. intros s K. inverts K. applys eval_get.
  { applys* Fmap.indom_single. }
  { rewrite hstar_hpure_l. split*. rewrite* Fmap.read_single. hnfs*. }
Qed.
Lemma triple_set : ∀ w p v,
  triple (val_set (val_loc p) v)
    (p ~~> w)
    (fun r ⇒ (p ~~> v)).
Proof using.
  intros. intros s1 K. inverts K. applys eval_set.
  { applys* Fmap.indom_single. }
  { rewrite Fmap.update_single. hnfs*. }
Qed.
Lemma triple_free : ∀ p v,
  triple (val_free (val_loc p))
    (p ~~> v)
    (fun r ⇒ \[]).
Proof using.
  intros. intros s1 K. inverts K. applys eval_free.
  { applys* Fmap.indom_single. }
  { rewrite* Fmap.remove_single. hnfs*. }
Qed.

Bonus: Example Proof

See chapter Rules for comments on this proof.
   let incr p =
      let n = !p in
      let m = n+1 in
      p := m
Definition of the function incr, using low-level syntax.
Open Scope string_scope.
Definition incr : val :=
  val_fix "f" "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")))).
Specification of the function incr.
Lemma triple_incr : ∀ (p:loc) (n:int),
  triple (trm_app incr p)
    (p ~~> n)
    (fun _ ⇒ p ~~> (n+1)).
Verification of incr, applying the reasoning rules by hand.
Proof using.
  intros. applys triple_app_fix. { reflexivity. } simpl.
  applys triple_let. { apply triple_get. }
  intros n'. simpl. apply triple_hpure. intros →.
  applys triple_let. { applys triple_conseq.
    { applys triple_frame. applys triple_add. }
    { xsimpl. }
    { xsimpl. } }
  intros m'. simpl. apply triple_hpure. intros →.
  { apply triple_set. }
Qed.
(* 2024-11-04 20:38 *)