Week 12: Separation Logic

Author: Greg Morrisett, with modifications by CS-428 staff.
License: No redistribution allowed (usage by permission in CS-428).

Using Hoare logic we can derive statements like this, which capture the specification of the function that increments a variable:

{ x = n }
inc(x)
{ x = n + 1}

We'd like to be able to use such statements to construct proofs of statements that involve procedures like inc():

{ x = n ∧ y = m }
inc(x);
inc(y);
{ x = n + 1 ∧ y = m + 1 }

The problem is that we need an intermediate proposition that is stronger than what the specification for inc() gives us directly. One approach is to somehow say that things other than x aren't modified by the first increment.

There have been a number of attempts to extend the logic to support modular reasoning about heaps and procedures. Of these, separation logic is probably the most popular.

Separation logic has a similar structure to Hoare logic, but the meaning of {P} c {Q} is different. Semantically, ∀h1, ∀h2, if P(h1), then running c in heap (h1 ⨄ h2) yields a heap h3 = h4 ⨄ h2 where Q(h4). Note that by ⨄ here we mean disjoint union.

Specifications in separation logic generally have the following syntax:

emp            the heap is empty
x ↦ v          the heap contains a single mapping from x to v
P * Q          * is the _separating conjunction_ of separation logic.
               Holds on heap h = h1 ⨄ h2 where P(h1) and Q(h2).
P ∧ Q          Usual semantics
P -* Q         The "magic wand" implication. Idea: a heap satisfies it
               if it satisfies Q when extended with some disjoint heap that
               satisfies P. This is useful for weakest preconditions.

This is nice because the rules for assignment, consequence etc. still hold:

{x ↦ _ } x := v { x ↦ v}

just like in standard Hoare Logic.

Require Import Eqdep.
Require Import Lia.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
Require Import List.
Set Implicit Arguments.
Axiom proof_irrelevance : forall (P : Prop) (H1 H2 : P), H1 = H2.

In this lecture, we will develop a separation logic for reasoning about imperative Coq programs. Separation logic gives us a crucial principle for modularly reasoning about programs — the frame rule. Just in the Hoare logic lecture, we'll use a shallow-embedding for programs and properties.

Module FunctionalSepIMP.

  Definition ptr := nat.
  Definition ptr_eq := PeanoNat.Nat.eq_dec.
  Definition le_gt_dec := Arith.Compare_dec.le_gt_dec.

We choose a simple types for the values to store in the heap.

  Inductive value: Type :=
  | VNat : nat -> value
  | VPair: value -> value -> value.

Heaps

We will continue to use lists of pointers and values as the model for heaps. However, to support an easy definition of disjoint union, we will impose the additional constraint that the list is sorted in (strictly) increasing order. It's possible to capture this constraint by defining heaps as a sigma type, where we include a proof that the heap is sorted. That makes some things easier (e.g., arguing that disjoint union is commutative) but makes other things harder. For example, equality on sigmas would demand we need to compare proofs, and use proof-irrelevance. To avoid this we can put in well-formedness constraints in just the right places.

  Definition heap := list (ptr * value).

  Definition empty_heap : heap := nil.

Here is a predicate which says that each pointer in h is greater than x.

  Fixpoint list_greater (x : ptr) (h : heap) : Prop :=
    match h with
    | nil => True
    | (y, v) :: h' => x < y /\ list_greater x h'
    end.

A heap is well-formed if each pointer is less than the rest of the heap, and the rest of the heap is well-formed.

  Fixpoint wf (h : heap) : Prop :=
    match h with
    | nil => True
    | (x, v) :: h' => list_greater x h' /\ wf h'
    end.

  Fixpoint indom (x : ptr) (h : heap) : Prop :=
    match h with
    | nil => False
    | (y, _) :: h' => if ptr_eq x y then True else indom x h'
    end.

A pointer x is fresh for h when it's not in the domain of h.

  Definition fresh x (h : heap) : Prop := ~ indom x h.

Here are standard lookup and remove functions on heaps.

  Fixpoint lookup (x : ptr) (h : heap) : option value :=
    match h with
    | nil => None
    | (y, v) :: h' => if ptr_eq x y then Some v else lookup x h'
    end.

  Fixpoint remove (x : ptr) (h : heap) : heap :=
    match h with
    | nil => nil
    | (y, v) :: h' => if ptr_eq x y then h' else (y, v) :: (remove x h')
    end.

Two heaps are disjoint when each pointer in h1 is fresh for h2.

  Fixpoint disjoint (h1 h2 : heap) : Prop :=
    match h1 with
    | nil => True
    | (x, _) :: h1' => ~indom x h2 /\ disjoint h1' h2
    end.

To insert into a heap, we use insertion sort.

  Fixpoint insert (x : nat) (v : value) (h : heap) : heap :=
    match h with
    | nil => (x, v) :: nil
    | (y, w) :: h' =>
        if le_gt_dec x y then (x, v) :: (y, w) :: h'
        else (y, w) :: (insert x v h')
    end.

We can merge two ehaps using our insert function.

  Definition merge (h1 h2 : heap) : heap :=
    List.fold_right (fun p h => insert (fst p) (snd p) h) h2 h1.

Commands

As in earlier lectures, we model commands via shallow embedding and using a monad. That is, a command takes a heap and returns an optional heap and a result.

  Definition Cmd (t : Type) := heap -> option (heap * t).

  Definition ret t (x : t) : Cmd t := fun h => Some (h, x).

  Definition exit t : Cmd t := fun h => None.

  Definition bind t u (c : Cmd t) (f : t -> Cmd u) : Cmd u :=
    fun h1 => match c h1 with
            | None => None
            | Some (h2, v) => f v h2
            end.

  Declare Scope cmd_scope.

We introduce some notation similar to Haskell's "do" notation.

  Notation "x <- c ; f" := (bind c (fun x => f))
    (right associativity, at level 84) : cmd_scope.
  Notation "c ;; f" := (bind c (fun _ : unit => f))
    (right associativity, at level 84) : cmd_scope.
  Local Open Scope cmd_scope.

  Definition run (t : Type) (c : Cmd t) := c empty_heap.

The read operation returns a value. The other version expects to read a nat or fails.

  Definition read (p : ptr) : Cmd value :=
    fun h => match lookup p h with
          | None => None
          | Some u => Some (h, u)
          end.

  Definition read_nat (p:ptr) : Cmd nat :=
    v <- read p ;
  match v with
  | VNat n => ret n
  | _ => exit _
  end.

Likewise, we have the write operation.

  Definition write (p : ptr) (v : value) : Cmd unit :=
    fun h => match lookup p h with
           | None => None
           | Some _ => Some (insert p v (remove p h), tt)
           end.

To allocate a new pointer, we need to pick something fresh for the heap. So we choose the maximum value in the heap plus one.

  Definition max (p1 p2 : ptr) :=
    if le_gt_dec p1 p2 then p2 else p1.

  Definition max_heap (h : heap) :=
    List.fold_right (fun p n => max (fst p) n) 0 h.

  Definition new (v : value) : Cmd ptr :=
    fun h => let p := 1 + max_heap h in Some (insert p v h, p).

  Definition free (p : ptr) : Cmd unit :=
    fun h => match lookup p h with
           | None => None
           | Some _ => Some (remove p h, tt)
           end.

Heap Predicates (AKA "hprops")

An hprop is a predicate on heaps.

  Definition hprop := heap -> Prop.

emp holds only when the heap is empty. One way to think of emp is that as a pre-condition, it tells us that we don't have the right to access anything in the heap. emp plays the role of a unit for star which is defined below.

  Definition emp : hprop := fun h => h = nil.

top holds on any heap.

  Definition top : hprop := fun _ => True.

  Declare Scope sep_scope.

x --> d holds when the heap contains exactly one pointer x which points to d. So we can think of this predicate as permission to read or write x and if we read it, we'll get out the dynamic value d. However, we're not allowed to read or write any other location if this is our only pre-condition.

  Definition ptsto (x : ptr) (d : value) : hprop :=
    fun h => h = (x, d) :: nil.
  Infix "-->" := ptsto (at level 70) : sep_scope.
  Local Open Scope sep_scope.

P ** Q holds when the heap can be broken into disjoint heaps h1 and h2 such that h1 satisfies P and h2 satisfies Q. For example x --> v ** y --> v tells us that we have the right to access both x and y, but that x <> y.

  Definition star (P Q : hprop) : hprop :=
    fun h => exists h1 h2 : heap,
        wf h1 /\ wf h2 /\ P h1 /\ Q h2 /\
          h = merge h1 h2 /\ disjoint h1 h2.
  Infix "**" := star (right associativity, at level 80) : sep_scope.

When P is a pure predicate in the sense that it doesn't refer to a heap, then we can use pure P as a predicate on the heap. Note that we require that the heap that it corresponds to is empty.

  Definition pure (P : Prop) : hprop := fun h => emp h /\ P.

sing h is the singleton predciate on heaps -- i.e., it holds on h' only when h' is equal to h.

  Definition sing (h : heap) : hprop := fun h' => h = h'.

This definition lifts an existential quantifier up to a predicate on heaps.

  Definition hexists (T : Type) (f : T -> hprop) : hprop :=
    fun h => exists x : T, f x h.

So for instance, we can define x -->? as follows

  Local Open Scope sep_scope.
  Definition ptsto_some (x : ptr) := hexists (fun v => x --> v).
  Notation "x '-->?'" := (ptsto_some x) (at level 70) : sep_scope.

This notation will be useful for reasoning about when one separation predicate can be used in lieu of another -- i.e., a form of implication over heaps. Note that this is not the "magic-wand" of separation logic, but rather, a meta-level implication.

  Definition himp (P Q : hprop) : Prop := forall h, wf h -> P h -> Q h.
  Infix "==>" := himp (at level 90) : sep_scope.

Here is a standard simplification tactic.

  Ltac mysimpl := repeat (simpl;
    match goal with
    | [ p : (_ * _)%type |- _ ] => destruct p
    | [ H : _ /\ _ |- _ ] => destruct H
    | [ H : exists _, _ |- _ ] => destruct H
    | [ |- context[ptr_eq ?x ?y] ] =>
        destruct (ptr_eq x y); try subst; try congruence
    | [ H : context[ptr_eq ?x ?y] |- _ ] =>
        destruct (ptr_eq x y); try subst; try congruence
    | [ |- context[le_gt_dec ?x ?y] ] =>
        destruct (le_gt_dec x y); try lia
    | [ H : context[le_gt_dec ?x ?y] |- _ ] =>
        destruct (le_gt_dec x y); try lia
    | [ |- _ /\ _ ] => split
    | [ H : (_, _) = (_, _) |- _ ] =>
        injection H; clear H; intros; try subst
    | [ H : Some _ = Some _ |- _ ] =>
        injection H; clear H; intros; try subst
    | [ H : Some _ = None |- _ ] => congruence
    | [ H : None = Some _ |- _ ] => congruence
    | [ H : ?x <> ?x |- _ ] => congruence
    | [ H : ~ True |- _ ] => contradiction H; auto
    | [ H : False |- _ ] => contradiction H; auto
    | [ |- forall _, _ ] => intros
    | _ => auto
    end).

We need a ton of lemmas for reasoning about heaps. The keys ones are showing that various operations preserve well-formedness, or that merging well-formed heaps is commutative and associative, etc.

For example, removing a pointer keeps a heap well-formed.

  Lemma lg_remove x y h :
    list_greater x h -> list_greater x (remove y h).x, y: ptr
h: heap
list_greater x h -> list_greater x (remove y h)
  Proof.x, y: ptr
h: heap
list_greater x h -> list_greater x (remove y h)
    induction h; mysimpl.
  Qed.

  Lemma remove_wf x (h : heap) : wf h -> wf (remove x h).x: ptr
h: heap
wf h -> wf (remove x h)
  Proof.x: ptr
h: heap
wf h -> wf (remove x h)
    induction h; mysimpl.x, p: ptr
v: value
h: list (ptr * value)
IHh: wf h -> wf (remove x h)
n: x <> p
H: list_greater p h
H0: wf h
list_greater p (remove x h)
    apply lg_remove.x, p: ptr
v: value
h: list (ptr * value)
IHh: wf h -> wf (remove x h)
n: x <> p
H: list_greater p h
H0: wf h
list_greater p h assumption.
  Qed.

  Lemma disjoint_indom :
    forall h1 h2 p,
      disjoint h1 h2 -> indom p h1 -> ~indom p h2.forall (h1 h2 : heap) (p : ptr),
disjoint h1 h2 -> indom p h1 -> ~ indom p h2
  Proof.forall (h1 h2 : heap) (p : ptr),
disjoint h1 h2 -> indom p h1 -> ~ indom p h2
    induction h1; mysimpl.
  Qed.

  Lemma not_indom_cons:
    forall (h : heap) (p0 : ptr) (p : ptr) (d : value),
      ~indom p0 ((p, d) :: h) -> ~indom p0 h.forall (h : heap) (p0 p : ptr) (d : value),
~ indom p0 ((p, d) :: h) -> ~ indom p0 h
  Proof.forall (h : heap) (p0 p : ptr) (d : value),
~ indom p0 ((p, d) :: h) -> ~ indom p0 h
    mysimpl.
  Qed.

  Lemma disjoint_cons:
    forall h1 h2 p,
      disjoint h1 (p :: h2) -> disjoint h1 h2.forall (h1 : heap) (h2 : list (ptr * value))
  (p : ptr * value),
disjoint h1 (p :: h2) -> disjoint h1 h2
  Proof.forall (h1 : heap) (h2 : list (ptr * value))
  (p : ptr * value),
disjoint h1 (p :: h2) -> disjoint h1 h2
    induction h1; mysimpl.p: ptr
v: value
h1: list (ptr * value)
IHh1: forall (h2 : list (ptr * value))
  (p : ptr * value),
disjoint h1 (p :: h2) -> disjoint h1 h2
h2: list (ptr * value)
p0: ptr
v0: value
n: p <> p0
H: ~ indom p h2
H0: disjoint h1 ((p0, v0) :: h2)
disjoint h1 h2
    eapply IHh1; eassumption.
  Qed.

Disjointness is commutative.

  Lemma disjoint_comm : forall (h1 h2 : heap),
      disjoint h1 h2 -> disjoint h2 h1.forall h1 h2 : heap, disjoint h1 h2 -> disjoint h2 h1
  Proof.forall h1 h2 : heap, disjoint h1 h2 -> disjoint h2 h1
    induction h1; induction h2; mysimpl.p0: ptr
v0: value
h1: list (ptr * value)
IHh1: forall h2 : heap,
disjoint h1 h2 -> disjoint h2 h1
p: ptr
v: value
h2: list (ptr * value)
IHh2: disjoint ((p0, v0) :: h1) h2 ->
disjoint h2 ((p0, v0) :: h1)
n: p0 <> p
n0: p <> p0
H: ~ indom p0 h2
H0: disjoint h1 ((p, v) :: h2)
~ indom p h1
p0: ptr
v0: value
h1: list (ptr * value)
IHh1: forall h2 : heap,
disjoint h1 h2 -> disjoint h2 h1
p: ptr
v: value
h2: list (ptr * value)
IHh2: disjoint ((p0, v0) :: h1) h2 ->
disjoint h2 ((p0, v0) :: h1)
n: p0 <> p
n0: p <> p0
H: ~ indom p0 h2
H0: disjoint h1 ((p, v) :: h2)
disjoint h2 ((p0, v0) :: h1)
    -p0: ptr
v0: value
h1: list (ptr * value)
IHh1: forall h2 : heap,
disjoint h1 h2 -> disjoint h2 h1
p: ptr
v: value
h2: list (ptr * value)
IHh2: disjoint ((p0, v0) :: h1) h2 ->
disjoint h2 ((p0, v0) :: h1)
n: p0 <> p
n0: p <> p0
H: ~ indom p0 h2
H0: disjoint h1 ((p, v) :: h2)
~ indom p h1 eapply disjoint_indom; eauto.p0: ptr
v0: value
h1: list (ptr * value)
IHh1: forall h2 : heap,
disjoint h1 h2 -> disjoint h2 h1
p: ptr
v: value
h2: list (ptr * value)
IHh2: disjoint ((p0, v0) :: h1) h2 ->
disjoint h2 ((p0, v0) :: h1)
n: p0 <> p
n0: p <> p0
H: ~ indom p0 h2
H0: disjoint h1 ((p, v) :: h2)
indom p ((p, v) :: h2)
      mysimpl.
    -p0: ptr
v0: value
h1: list (ptr * value)
IHh1: forall h2 : heap,
disjoint h1 h2 -> disjoint h2 h1
p: ptr
v: value
h2: list (ptr * value)
IHh2: disjoint ((p0, v0) :: h1) h2 ->
disjoint h2 ((p0, v0) :: h1)
n: p0 <> p
n0: p <> p0
H: ~ indom p0 h2
H0: disjoint h1 ((p, v) :: h2)
disjoint h2 ((p0, v0) :: h1) apply IHh2.p0: ptr
v0: value
h1: list (ptr * value)
IHh1: forall h2 : heap,
disjoint h1 h2 -> disjoint h2 h1
p: ptr
v: value
h2: list (ptr * value)
IHh2: disjoint ((p0, v0) :: h1) h2 ->
disjoint h2 ((p0, v0) :: h1)
n: p0 <> p
n0: p <> p0
H: ~ indom p0 h2
H0: disjoint h1 ((p, v) :: h2)
disjoint ((p0, v0) :: h1) h2
      mysimpl.p0: ptr
v0: value
h1: list (ptr * value)
IHh1: forall h2 : heap,
disjoint h1 h2 -> disjoint h2 h1
p: ptr
v: value
h2: list (ptr * value)
IHh2: disjoint ((p0, v0) :: h1) h2 ->
disjoint h2 ((p0, v0) :: h1)
n: p0 <> p
n0: p <> p0
H: ~ indom p0 h2
H0: disjoint h1 ((p, v) :: h2)
disjoint h1 h2
      eapply disjoint_cons; eassumption.
  Qed.

  Lemma lg_trans x y :
    x < y -> forall h, list_greater y h -> list_greater x h.x, y: nat
x < y ->
forall h : heap, list_greater y h -> list_greater x h
  Proof.x, y: nat
x < y ->
forall h : heap, list_greater y h -> list_greater x h
    induction h; mysimpl.x, y: nat
H: x < y
p: ptr
v: value
h: list (ptr * value)
IHh: list_greater y h -> list_greater x h
H0: y < p
H1: list_greater y h
x < p lia.
  Qed.

Inserting a fresh pointer keeps a heap well-formed.

  Lemma insert_wf h :
    wf h -> forall x v, fresh x h -> wf (insert x v h).h: heap
wf h ->
forall (x : ptr) (v : value),
fresh x h -> wf (insert x v h)
  Proof.h: heap
wf h ->
forall (x : ptr) (v : value),
fresh x h -> wf (insert x v h)
    unfold fresh; induction h; mysimpl.p: ptr
v: value
h: list (ptr * value)
IHh: wf h -> forall (x : ptr) (v : value), ~ indom x h -> wf (insert x v h)
H: list_greater p h
H1: wf h
x: ptr
v0: value
n: x <> p
H0: ~ indom x h
l: x <= p
x < p
p: ptr
v: value
h: list (ptr * value)
IHh: wf h -> forall (x : ptr) (v : value), ~ indom x h -> wf (insert x v h)
H: list_greater p h
H1: wf h
x: ptr
v0: value
n: x <> p
H0: ~ indom x h
l: x <= p
list_greater x h
p: ptr
v: value
h: list (ptr * value)
IHh: wf h -> forall (x : ptr) (v : value), ~ indom x h -> wf (insert x v h)
H: list_greater p h
H1: wf h
x: ptr
v0: value
n: x <> p
H0: ~ indom x h
g: x > p
list_greater p (insert x v0 h)
    -p: ptr
v: value
h: list (ptr * value)
IHh: wf h -> forall (x : ptr) (v : value), ~ indom x h -> wf (insert x v h)
H: list_greater p h
H1: wf h
x: ptr
v0: value
n: x <> p
H0: ~ indom x h
l: x <= p
x < p lia.
    -p: ptr
v: value
h: list (ptr * value)
IHh: wf h -> forall (x : ptr) (v : value), ~ indom x h -> wf (insert x v h)
H: list_greater p h
H1: wf h
x: ptr
v0: value
n: x <> p
H0: ~ indom x h
l: x <= p
list_greater x h apply lg_trans with (y := p); [lia | assumption].
    -p: ptr
v: value
h: list (ptr * value)
IHh: wf h -> forall (x : ptr) (v : value), ~ indom x h -> wf (insert x v h)
H: list_greater p h
H1: wf h
x: ptr
v0: value
n: x <> p
H0: ~ indom x h
g: x > p
list_greater p (insert x v0 h) assert (wf (insert x v0 h)) by auto.p: ptr
v: value
h: list (ptr * value)
IHh: wf h -> forall (x : ptr) (v : value), ~ indom x h -> wf (insert x v h)
H: list_greater p h
H1: wf h
x: ptr
v0: value
n: x <> p
H0: ~ indom x h
g: x > p
H2: wf (insert x v0 h)
list_greater p (insert x v0 h)
      destruct h as [ | []]; simpl in *; mysimpl.p: ptr
v: value
p0: ptr
v1: value
h: list (ptr * value)
IHh: list_greater p0 h /\ wf h ->
forall (x : ptr) (v : value),
~ (if ptr_eq x p0 then True else indom x h) ->
wf
(if le_gt_dec x p0
then (x, v) :: (p0, v1) :: h
else (p0, v1) :: insert x v h)
H: p < p0
H4: list_greater p h
H1: list_greater p0 h
H3: wf h
x: ptr
v0: value
n: x <> p
n0: x <> p0
H0: ~ indom x h
g: x > p
g0: x > p0
H2: wf ((p0, v1) :: insert x v0 h)
list_greater p (insert x v0 h)
      eapply lg_trans with (y := p0); firstorder.
  Qed.

  Lemma lg_imp_not_indom p h : list_greater p h -> fresh p h.p: ptr
h: heap
list_greater p h -> fresh p h
  Proof.p: ptr
h: heap
list_greater p h -> fresh p h
    unfold fresh; induction h; mysimpl.p0: ptr
v: value
h: list (ptr * value)
IHh: list_greater p0 h -> ~ indom p0 h
H: p0 < p0
H0: list_greater p0 h
~ True lia.
  Qed.

  Lemma not_indom_insert x h :
    fresh x h -> forall y v,
        y <> x -> fresh x (insert y v h).x: ptr
h: heap
fresh x h ->
forall (y : ptr) (v : value),
y <> x -> fresh x (insert y v h)
  Proof.x: ptr
h: heap
fresh x h ->
forall (y : ptr) (v : value),
y <> x -> fresh x (insert y v h)
    unfold fresh; induction h; mysimpl.
  Qed.

  Lemma not_indom_merge h1 h2 p :
    fresh p h1 -> fresh p h2 -> fresh p (merge h1 h2).h1, h2: heap
p: ptr
fresh p h1 -> fresh p h2 -> fresh p (merge h1 h2)
  Proof.h1, h2: heap
p: ptr
fresh p h1 -> fresh p h2 -> fresh p (merge h1 h2)
    unfold fresh; induction h1; mysimpl.p0: ptr
v: value
h1: list (ptr * value)
h2: heap
p: ptr
IHh1: ~ indom p h1 ->
~ indom p h2 -> ~ indom p (merge h1 h2)
n: p <> p0
H: ~ indom p h1
H0: ~ indom p h2
~ indom p (insert p0 v (merge h1 h2))
    apply not_indom_insert; unfold fresh; auto.
  Qed.

Merging two well-formed, disjoint heaps results in a well-formed heap.

  Lemma merge_wf h1 h2 :
    wf h1 -> wf h2 -> disjoint h1 h2 -> wf (merge h1 h2).h1, h2: heap
wf h1 -> wf h2 -> disjoint h1 h2 -> wf (merge h1 h2)
  Proof.h1, h2: heap
wf h1 -> wf h2 -> disjoint h1 h2 -> wf (merge h1 h2)
    induction h1; mysimpl.p: ptr
v: value
h1: list (ptr * value)
h2: heap
IHh1: wf h1 ->
wf h2 -> disjoint h1 h2 -> wf (merge h1 h2)
H: list_greater p h1
H3: wf h1
H0: wf h2
H1: ~ indom p h2
H2: disjoint h1 h2
wf (insert p v (merge h1 h2))
    apply insert_wf; auto.p: ptr
v: value
h1: list (ptr * value)
h2: heap
IHh1: wf h1 ->
wf h2 -> disjoint h1 h2 -> wf (merge h1 h2)
H: list_greater p h1
H3: wf h1
H0: wf h2
H1: ~ indom p h2
H2: disjoint h1 h2
fresh p (merge h1 h2)
    apply not_indom_merge; auto.p: ptr
v: value
h1: list (ptr * value)
h2: heap
IHh1: wf h1 ->
wf h2 -> disjoint h1 h2 -> wf (merge h1 h2)
H: list_greater p h1
H3: wf h1
H0: wf h2
H1: ~ indom p h2
H2: disjoint h1 h2
fresh p h1
    apply lg_imp_not_indom; auto.
  Qed.

Insertion is commutative for distinct pointers.

  Lemma insert_comm h x1 v1 x2 v2 :
    x1 <> x2 ->
    insert x1 v1 (insert x2 v2 h) = insert x2 v2 (insert x1 v1 h).h: heap
x1: nat
v1: value
x2: nat
v2: value
x1 <> x2 ->
insert x1 v1 (insert x2 v2 h) =
insert x2 v2 (insert x1 v1 h)
  Proof.h: heap
x1: nat
v1: value
x2: nat
v2: value
x1 <> x2 ->
insert x1 v1 (insert x2 v2 h) =
insert x2 v2 (insert x1 v1 h)
    induction h; unfold ptr; mysimpl.p: ptr
v: value
h: list (ptr * value)
x1: nat
v1: value
x2: nat
v2: value
IHh: x1 <> x2 -> insert x1 v1 (insert x2 v2 h) = insert x2 v2 (insert x1 v1 h)
g: x2 > p
g0: x1 > p
g1: x2 > p
H: x1 <> x2
(p, v) :: insert x1 v1 (insert x2 v2 h) =
(p, v) :: insert x2 v2 (insert x1 v1 h)
    rewrite IHh; auto.
  Qed.

Merge is commutative when the heaps are well-formed and disjoint.

  Lemma merge_insert_comm : forall h1 h2 p d,
      wf h1 ->
      wf h2 ->
      disjoint h1 h2 ->
      ~indom p h1 ->
      insert p d (merge h1 h2) = merge (insert p d h1) h2.forall (h1 h2 : heap) (p : ptr) (d : value),
wf h1 ->
wf h2 ->
disjoint h1 h2 ->
~ indom p h1 ->
insert p d (merge h1 h2) = merge (insert p d h1) h2
  Proof.forall (h1 h2 : heap) (p : ptr) (d : value),
wf h1 ->
wf h2 ->
disjoint h1 h2 ->
~ indom p h1 ->
insert p d (merge h1 h2) = merge (insert p d h1) h2
    induction h1; mysimpl.p: ptr
v: value
h1: list (ptr * value)
IHh1: forall (h2 : heap) (p : ptr) (d : value),
wf h1 ->
wf h2 ->
disjoint h1 h2 ->
~ indom p h1 ->
insert p d (merge h1 h2) =
merge (insert p d h1) h2
h2: heap
p0: ptr
d: value
H: list_greater p h1
H4: wf h1
H0: wf h2
H1: ~ indom p h2
H3: disjoint h1 h2
n: p0 <> p
H2: ~ indom p0 h1
g: p0 > p
insert p0 d (insert p v (merge h1 h2)) =
insert p v (merge (insert p0 d h1) h2)
    rewrite insert_comm; auto.p: ptr
v: value
h1: list (ptr * value)
IHh1: forall (h2 : heap) (p : ptr) (d : value),
wf h1 ->
wf h2 ->
disjoint h1 h2 ->
~ indom p h1 ->
insert p d (merge h1 h2) =
merge (insert p d h1) h2
h2: heap
p0: ptr
d: value
H: list_greater p h1
H4: wf h1
H0: wf h2
H1: ~ indom p h2
H3: disjoint h1 h2
n: p0 <> p
H2: ~ indom p0 h1
g: p0 > p
insert p v (insert p0 d (merge h1 h2)) =
insert p v (merge (insert p0 d h1) h2)
    rewrite IHh1; auto.
  Qed.

  Lemma merge_comm h1 h2 :
    wf h1 ->
    wf h2 ->
    disjoint h1 h2 ->
    merge h1 h2 = merge h2 h1.h1, h2: heap
wf h1 ->
wf h2 -> disjoint h1 h2 -> merge h1 h2 = merge h2 h1
  Proof.h1, h2: heap
wf h1 ->
wf h2 -> disjoint h1 h2 -> merge h1 h2 = merge h2 h1
    induction h1; mysimpl.h2: heap
H: True
H0: wf h2
H1: True
h2 = merge h2 nil
p: ptr
v: value
h1: list (ptr * value)
h2: heap
IHh1: wf h1 ->
wf h2 ->
disjoint h1 h2 -> merge h1 h2 = merge h2 h1
H: list_greater p h1
H3: wf h1
H0: wf h2
H1: ~ indom p h2
H2: disjoint h1 h2
insert p v (merge h1 h2) = merge h2 ((p, v) :: h1)
    -h2: heap
H: True
H0: wf h2
H1: True
h2 = merge h2 nil induction h2; simpl in *; mysimpl.p: ptr
v: value
h2: list (ptr * value)
H: True
H0: list_greater p h2
H2: wf h2
H1: True
IHh2: wf h2 -> h2 = merge h2 nil
(p, v) :: h2 = insert p v (merge h2 nil)
      rewrite <- IHh2; auto.p: ptr
v: value
h2: list (ptr * value)
H: True
H0: list_greater p h2
H2: wf h2
H1: True
IHh2: wf h2 -> h2 = merge h2 nil
(p, v) :: h2 = insert p v h2
      destruct h2; simpl in *; mysimpl.
    -p: ptr
v: value
h1: list (ptr * value)
h2: heap
IHh1: wf h1 ->
wf h2 ->
disjoint h1 h2 -> merge h1 h2 = merge h2 h1
H: list_greater p h1
H3: wf h1
H0: wf h2
H1: ~ indom p h2
H2: disjoint h1 h2
insert p v (merge h1 h2) = merge h2 ((p, v) :: h1) rewrite IHh1; auto.p: ptr
v: value
h1: list (ptr * value)
h2: heap
IHh1: wf h1 ->
wf h2 ->
disjoint h1 h2 -> merge h1 h2 = merge h2 h1
H: list_greater p h1
H3: wf h1
H0: wf h2
H1: ~ indom p h2
H2: disjoint h1 h2
insert p v (merge h2 h1) = merge h2 ((p, v) :: h1) clear IHh1.p: ptr
v: value
h1: list (ptr * value)
h2: heap
H: list_greater p h1
H3: wf h1
H0: wf h2
H1: ~ indom p h2
H2: disjoint h1 h2
insert p v (merge h2 h1) = merge h2 ((p, v) :: h1)
      induction h2; mysimpl.p: ptr
v: value
h1: list (ptr * value)
H: list_greater p h1
H3: wf h1
H0: wf nil
H1: ~ indom p nil
H2: disjoint h1 nil
insert p v h1 = (p, v) :: h1
p: ptr
v: value
h1: list (ptr * value)
p0: ptr
v0: value
h2: list (ptr * value)
H: list_greater p h1
H3: wf h1
H0: wf ((p0, v0) :: h2)
H1: ~ indom p ((p0, v0) :: h2)
H2: disjoint h1 ((p0, v0) :: h2)
IHh2: wf h2 ->
~ indom p h2 ->
disjoint h1 h2 ->
insert p v (merge h2 h1) =
merge h2 ((p, v) :: h1)
insert p v (insert p0 v0 (merge h2 h1)) =
insert p0 v0 (merge h2 ((p, v) :: h1))
      +p: ptr
v: value
h1: list (ptr * value)
H: list_greater p h1
H3: wf h1
H0: wf nil
H1: ~ indom p nil
H2: disjoint h1 nil
insert p v h1 = (p, v) :: h1 destruct h1; simpl in *; mysimpl.
      +p: ptr
v: value
h1: list (ptr * value)
p0: ptr
v0: value
h2: list (ptr * value)
H: list_greater p h1
H3: wf h1
H0: wf ((p0, v0) :: h2)
H1: ~ indom p ((p0, v0) :: h2)
H2: disjoint h1 ((p0, v0) :: h2)
IHh2: wf h2 ->
~ indom p h2 ->
disjoint h1 h2 ->
insert p v (merge h2 h1) =
merge h2 ((p, v) :: h1)
insert p v (insert p0 v0 (merge h2 h1)) =
insert p0 v0 (merge h2 ((p, v) :: h1)) simpl in *; mysimpl.p: ptr
v: value
h1: list (ptr * value)
p0: ptr
v0: value
h2: list (ptr * value)
H: list_greater p h1
H3: wf h1
H0: list_greater p0 h2
H4: wf h2
n: p <> p0
H1: ~ indom p h2
H2: disjoint h1 ((p0, v0) :: h2)
IHh2: wf h2 ->
~ indom p h2 ->
disjoint h1 h2 ->
insert p v (merge h2 h1) =
merge h2 ((p, v) :: h1)
insert p v (insert p0 v0 (merge h2 h1)) =
insert p0 v0 (merge h2 ((p, v) :: h1))
        rewrite <- IHh2; auto.p: ptr
v: value
h1: list (ptr * value)
p0: ptr
v0: value
h2: list (ptr * value)
H: list_greater p h1
H3: wf h1
H0: list_greater p0 h2
H4: wf h2
n: p <> p0
H1: ~ indom p h2
H2: disjoint h1 ((p0, v0) :: h2)
IHh2: wf h2 ->
~ indom p h2 ->
disjoint h1 h2 ->
insert p v (merge h2 h1) =
merge h2 ((p, v) :: h1)
insert p v (insert p0 v0 (merge h2 h1)) =
insert p0 v0 (insert p v (merge h2 h1))
p: ptr
v: value
h1: list (ptr * value)
p0: ptr
v0: value
h2: list (ptr * value)
H: list_greater p h1
H3: wf h1
H0: list_greater p0 h2
H4: wf h2
n: p <> p0
H1: ~ indom p h2
H2: disjoint h1 ((p0, v0) :: h2)
IHh2: wf h2 ->
~ indom p h2 ->
disjoint h1 h2 ->
insert p v (merge h2 h1) =
merge h2 ((p, v) :: h1)
disjoint h1 h2
        *p: ptr
v: value
h1: list (ptr * value)
p0: ptr
v0: value
h2: list (ptr * value)
H: list_greater p h1
H3: wf h1
H0: list_greater p0 h2
H4: wf h2
n: p <> p0
H1: ~ indom p h2
H2: disjoint h1 ((p0, v0) :: h2)
IHh2: wf h2 ->
~ indom p h2 ->
disjoint h1 h2 ->
insert p v (merge h2 h1) =
merge h2 ((p, v) :: h1)
insert p v (insert p0 v0 (merge h2 h1)) =
insert p0 v0 (insert p v (merge h2 h1)) rewrite insert_comm; auto.
        *p: ptr
v: value
h1: list (ptr * value)
p0: ptr
v0: value
h2: list (ptr * value)
H: list_greater p h1
H3: wf h1
H0: list_greater p0 h2
H4: wf h2
n: p <> p0
H1: ~ indom p h2
H2: disjoint h1 ((p0, v0) :: h2)
IHh2: wf h2 ->
~ indom p h2 ->
disjoint h1 h2 ->
insert p v (merge h2 h1) =
merge h2 ((p, v) :: h1)
disjoint h1 h2 eapply disjoint_cons; eauto.
  Qed.

  Lemma disjoint_insert : forall h1 h2 p x,
      disjoint h1 h2 ->
      ~ indom p h2 ->
      disjoint (insert p x h1) h2.forall (h1 h2 : heap) (p : ptr) (x : value),
disjoint h1 h2 ->
~ indom p h2 -> disjoint (insert p x h1) h2
  Proof.forall (h1 h2 : heap) (p : ptr) (x : value),
disjoint h1 h2 ->
~ indom p h2 -> disjoint (insert p x h1) h2
    induction h1; mysimpl.
  Qed.

  Lemma disjoint_merge : forall h1 h2 h3,
      disjoint h1 h3 ->
      disjoint h2 h3 ->
      disjoint (merge h1 h2) h3.forall h1 h2 h3 : heap,
disjoint h1 h3 ->
disjoint h2 h3 -> disjoint (merge h1 h2) h3
  Proof.forall h1 h2 h3 : heap,
disjoint h1 h3 ->
disjoint h2 h3 -> disjoint (merge h1 h2) h3
    induction h1; mysimpl.p: ptr
v: value
h1: list (ptr * value)
IHh1: forall h2 h3 : heap,
disjoint h1 h3 ->
disjoint h2 h3 -> disjoint (merge h1 h2) h3
h2, h3: heap
H: ~ indom p h3
H1: disjoint h1 h3
H0: disjoint h2 h3
disjoint (insert p v (merge h1 h2)) h3
    apply disjoint_insert; auto.
  Qed.

Well-formed merges are associative.

  Lemma merge_assoc : forall h1 h2 h3,
      wf h1 ->
      wf h2 ->
      wf h3 ->
      disjoint h1 h2 ->
      disjoint h1 h3 ->
      disjoint h2 h3 ->
      merge h1 (merge h2 h3) = merge (merge h1 h2) h3.forall h1 h2 h3 : heap,
wf h1 ->
wf h2 ->
wf h3 ->
disjoint h1 h2 ->
disjoint h1 h3 ->
disjoint h2 h3 ->
merge h1 (merge h2 h3) = merge (merge h1 h2) h3
  Proof.forall h1 h2 h3 : heap,
wf h1 ->
wf h2 ->
wf h3 ->
disjoint h1 h2 ->
disjoint h1 h3 ->
disjoint h2 h3 ->
merge h1 (merge h2 h3) = merge (merge h1 h2) h3
    induction h1; mysimpl.p: ptr
v: value
h1: list (ptr * value)
IHh1: forall h2 h3 : heap,
wf h1 ->
wf h2 ->
wf h3 ->
disjoint h1 h2 ->
disjoint h1 h3 ->
disjoint h2 h3 ->
merge h1 (merge h2 h3) = merge (merge h1 h2) h3
h2, h3: heap
H: list_greater p h1
H7: wf h1
H0: wf h2
H1: wf h3
H2: ~ indom p h2
H6: disjoint h1 h2
H3: ~ indom p h3
H5: disjoint h1 h3
H4: disjoint h2 h3
insert p v (merge h1 (merge h2 h3)) =
merge (insert p v (merge h1 h2)) h3
    rewrite IHh1; auto.p: ptr
v: value
h1: list (ptr * value)
IHh1: forall h2 h3 : heap,
wf h1 ->
wf h2 ->
wf h3 ->
disjoint h1 h2 ->
disjoint h1 h3 ->
disjoint h2 h3 ->
merge h1 (merge h2 h3) = merge (merge h1 h2) h3
h2, h3: heap
H: list_greater p h1
H7: wf h1
H0: wf h2
H1: wf h3
H2: ~ indom p h2
H6: disjoint h1 h2
H3: ~ indom p h3
H5: disjoint h1 h3
H4: disjoint h2 h3
insert p v (merge (merge h1 h2) h3) =
merge (insert p v (merge h1 h2)) h3
    apply merge_insert_comm; auto.p: ptr
v: value
h1: list (ptr * value)
IHh1: forall h2 h3 : heap,
wf h1 ->
wf h2 ->
wf h3 ->
disjoint h1 h2 ->
disjoint h1 h3 ->
disjoint h2 h3 ->
merge h1 (merge h2 h3) = merge (merge h1 h2) h3
h2, h3: heap
H: list_greater p h1
H7: wf h1
H0: wf h2
H1: wf h3
H2: ~ indom p h2
H6: disjoint h1 h2
H3: ~ indom p h3
H5: disjoint h1 h3
H4: disjoint h2 h3
wf (merge h1 h2)
p: ptr
v: value
h1: list (ptr * value)
IHh1: forall h2 h3 : heap,
wf h1 ->
wf h2 ->
wf h3 ->
disjoint h1 h2 ->
disjoint h1 h3 ->
disjoint h2 h3 ->
merge h1 (merge h2 h3) = merge (merge h1 h2) h3
h2, h3: heap
H: list_greater p h1
H7: wf h1
H0: wf h2
H1: wf h3
H2: ~ indom p h2
H6: disjoint h1 h2
H3: ~ indom p h3
H5: disjoint h1 h3
H4: disjoint h2 h3
disjoint (merge h1 h2) h3
p: ptr
v: value
h1: list (ptr * value)
IHh1: forall h2 h3 : heap,
wf h1 ->
wf h2 ->
wf h3 ->
disjoint h1 h2 ->
disjoint h1 h3 ->
disjoint h2 h3 ->
merge h1 (merge h2 h3) = merge (merge h1 h2) h3
h2, h3: heap
H: list_greater p h1
H7: wf h1
H0: wf h2
H1: wf h3
H2: ~ indom p h2
H6: disjoint h1 h2
H3: ~ indom p h3
H5: disjoint h1 h3
H4: disjoint h2 h3
~ indom p (merge h1 h2)
    -p: ptr
v: value
h1: list (ptr * value)
IHh1: forall h2 h3 : heap,
wf h1 ->
wf h2 ->
wf h3 ->
disjoint h1 h2 ->
disjoint h1 h3 ->
disjoint h2 h3 ->
merge h1 (merge h2 h3) = merge (merge h1 h2) h3
h2, h3: heap
H: list_greater p h1
H7: wf h1
H0: wf h2
H1: wf h3
H2: ~ indom p h2
H6: disjoint h1 h2
H3: ~ indom p h3
H5: disjoint h1 h3
H4: disjoint h2 h3
wf (merge h1 h2) apply merge_wf; auto.
    -p: ptr
v: value
h1: list (ptr * value)
IHh1: forall h2 h3 : heap,
wf h1 ->
wf h2 ->
wf h3 ->
disjoint h1 h2 ->
disjoint h1 h3 ->
disjoint h2 h3 ->
merge h1 (merge h2 h3) = merge (merge h1 h2) h3
h2, h3: heap
H: list_greater p h1
H7: wf h1
H0: wf h2
H1: wf h3
H2: ~ indom p h2
H6: disjoint h1 h2
H3: ~ indom p h3
H5: disjoint h1 h3
H4: disjoint h2 h3
disjoint (merge h1 h2) h3 apply disjoint_merge; auto.
    -p: ptr
v: value
h1: list (ptr * value)
IHh1: forall h2 h3 : heap,
wf h1 ->
wf h2 ->
wf h3 ->
disjoint h1 h2 ->
disjoint h1 h3 ->
disjoint h2 h3 ->
merge h1 (merge h2 h3) = merge (merge h1 h2) h3
h2, h3: heap
H: list_greater p h1
H7: wf h1
H0: wf h2
H1: wf h3
H2: ~ indom p h2
H6: disjoint h1 h2
H3: ~ indom p h3
H5: disjoint h1 h3
H4: disjoint h2 h3
~ indom p (merge h1 h2) apply not_indom_merge; auto.p: ptr
v: value
h1: list (ptr * value)
IHh1: forall h2 h3 : heap,
wf h1 ->
wf h2 ->
wf h3 ->
disjoint h1 h2 ->
disjoint h1 h3 ->
disjoint h2 h3 ->
merge h1 (merge h2 h3) = merge (merge h1 h2) h3
h2, h3: heap
H: list_greater p h1
H7: wf h1
H0: wf h2
H1: wf h3
H2: ~ indom p h2
H6: disjoint h1 h2
H3: ~ indom p h3
H5: disjoint h1 h3
H4: disjoint h2 h3
fresh p h1
      apply lg_imp_not_indom; auto.
  Qed.

  Lemma indom_insert x h y v :
    x <> y -> fresh x (insert y v h) -> fresh x h.x: ptr
h: heap
y: ptr
v: value
x <> y -> fresh x (insert y v h) -> fresh x h
  Proof.x: ptr
h: heap
y: ptr
v: value
x <> y -> fresh x (insert y v h) -> fresh x h
    unfold fresh; induction h; simpl in *;
      intros; mysimpl; simpl in *; mysimpl.
  Qed.

If p is fresh for merge h1 h2, then it's also fresh for both h1 and h2.

  Lemma merge_not_indom h1 h2 p :
    fresh p (merge h1 h2) -> fresh p h1 /\ fresh p h2.h1, h2: heap
p: ptr
fresh p (merge h1 h2) -> fresh p h1 /\ fresh p h2
  Proof.h1, h2: heap
p: ptr
fresh p (merge h1 h2) -> fresh p h1 /\ fresh p h2
    unfold fresh; induction h1; simpl; auto.a: (ptr * value)%type
h1: list (ptr * value)
h2: heap
p: ptr
IHh1: ~ indom p (merge h1 h2) ->
~ indom p h1 /\ ~ indom p h2
~ indom p (insert (fst a) (snd a) (merge h1 h2)) ->
~
(let (y, _) := a in
 if ptr_eq p y then True else indom p h1) /\
~ indom p h2
    destruct a.p0: ptr
v: value
h1: list (ptr * value)
h2: heap
p: ptr
IHh1: ~ indom p (merge h1 h2) ->
~ indom p h1 /\ ~ indom p h2
~
indom p
  (insert (fst (p0, v)) (snd (p0, v)) (merge h1 h2)) ->
~ (if ptr_eq p p0 then True else indom p h1) /\
~ indom p h2
    intros; destruct (ptr_eq p0 p); subst.v: value
h1: list (ptr * value)
h2: heap
p: ptr
IHh1: ~ indom p (merge h1 h2) ->
~ indom p h1 /\ ~ indom p h2
H: ~
indom p
  (insert (fst (p, v)) (snd (p, v)) (merge h1 h2))
~ (if ptr_eq p p then True else indom p h1) /\
~ indom p h2
p0: ptr
v: value
h1: list (ptr * value)
h2: heap
p: ptr
IHh1: ~ indom p (merge h1 h2) ->
~ indom p h1 /\ ~ indom p h2
H: ~
indom p
  (insert (fst (p0, v)) (snd (p0, v))
     (merge h1 h2))
n: p0 <> p
~ (if ptr_eq p p0 then True else indom p h1) /\
~ indom p h2
    -v: value
h1: list (ptr * value)
h2: heap
p: ptr
IHh1: ~ indom p (merge h1 h2) ->
~ indom p h1 /\ ~ indom p h2
H: ~
indom p
  (insert (fst (p, v)) (snd (p, v)) (merge h1 h2))
~ (if ptr_eq p p then True else indom p h1) /\
~ indom p h2 simpl in *.v: value
h1: list (ptr * value)
h2: heap
p: ptr
IHh1: ~ indom p (merge h1 h2) ->
~ indom p h1 /\ ~ indom p h2
H: ~ indom p (insert p v (merge h1 h2))
~ (if ptr_eq p p then True else indom p h1) /\
~ indom p h2
      exfalso.v: value
h1: list (ptr * value)
h2: heap
p: ptr
IHh1: ~ indom p (merge h1 h2) ->
~ indom p h1 /\ ~ indom p h2
H: ~ indom p (insert p v (merge h1 h2))
False
      apply H.v: value
h1: list (ptr * value)
h2: heap
p: ptr
IHh1: ~ indom p (merge h1 h2) ->
~ indom p h1 /\ ~ indom p h2
H: ~ indom p (insert p v (merge h1 h2))
indom p (insert p v (merge h1 h2))
      generalize (merge h1 h2).v: value
h1: list (ptr * value)
h2: heap
p: ptr
IHh1: ~ indom p (merge h1 h2) ->
~ indom p h1 /\ ~ indom p h2
H: ~ indom p (insert p v (merge h1 h2))
forall h : heap, indom p (insert p v h)
      induction h; mysimpl.
    -p0: ptr
v: value
h1: list (ptr * value)
h2: heap
p: ptr
IHh1: ~ indom p (merge h1 h2) ->
~ indom p h1 /\ ~ indom p h2
H: ~
indom p
  (insert (fst (p0, v)) (snd (p0, v))
     (merge h1 h2))
n: p0 <> p
~ (if ptr_eq p p0 then True else indom p h1) /\
~ indom p h2 mysimpl; apply IHh1; eapply indom_insert; eauto.
  Qed.

  Lemma merge_disjoint h1 h2 h3 :
    disjoint h1 (merge h2 h3) -> disjoint h1 h2 /\ disjoint h1 h3.h1, h2, h3: heap
disjoint h1 (merge h2 h3) ->
disjoint h1 h2 /\ disjoint h1 h3
  Proof.h1, h2, h3: heap
disjoint h1 (merge h2 h3) ->
disjoint h1 h2 /\ disjoint h1 h3
    induction h1; mysimpl; firstorder;
      apply (merge_not_indom h2 h3); auto.
  Qed.

  Lemma max_heap_fresh : forall h n, n > max_heap h -> fresh n h.forall (h : heap) (n : nat),
n > max_heap h -> fresh n h
  Proof.forall (h : heap) (n : nat),
n > max_heap h -> fresh n h
    unfold fresh; induction h; mysimpl; unfold max in *; mysimpl.p: ptr
v: value
h: list (ptr * value)
IHh: forall n : nat, n > max_heap h -> ~ indom n h
n: nat
g: p > max_heap h
H: n > p
n0: n <> p
~ indom n h
    apply IHh.p: ptr
v: value
h: list (ptr * value)
IHh: forall n : nat, n > max_heap h -> ~ indom n h
n: nat
g: p > max_heap h
H: n > p
n0: n <> p
n > max_heap h lia.
  Qed.

  Lemma remove_not_indom : forall p h, wf h -> fresh p (remove p h).forall (p : ptr) (h : heap),
wf h -> fresh p (remove p h)
  Proof.forall (p : ptr) (h : heap),
wf h -> fresh p (remove p h)
    unfold fresh; induction h; mysimpl.p0: ptr
v: value
h: list (ptr * value)
IHh: wf h -> ~ indom p0 (remove p0 h)
H: list_greater p0 h
H0: wf h
~ indom p0 h
    apply lg_imp_not_indom; auto.
  Qed.

  Lemma lookup_insert : forall x v h,
      lookup x (insert x v h) = Some v.forall (x : ptr) (v : value) (h : heap),
lookup x (insert x v h) = Some v
  Proof.forall (x : ptr) (v : value) (h : heap),
lookup x (insert x v h) = Some v
    induction h; mysimpl.v: value
p: ptr
v0: value
h: list (ptr * value)
g: p > p
IHh: lookup p (insert p v h) = Some v
Some v0 = Some v lia.
  Qed.

  Lemma remove_insert : forall x v h, remove x (insert x v h) = h.forall (x : ptr) (v : value) (h : heap),
remove x (insert x v h) = h
  Proof.forall (x : ptr) (v : value) (h : heap),
remove x (insert x v h) = h
    induction h; mysimpl.v: value
p: ptr
v0: value
h: list (ptr * value)
g: p > p
IHh: remove p (insert p v h) = h
insert p v h = (p, v0) :: h lia.
  Qed.

Separation Reasoning

Reasoning directly in terms of heaps is painful. So we will define some rules for reasoning directly at the level of the separation logic. This list of lemmas is by no means complete...

  Lemma emp_star P :
    P ==> emp ** P.P: hprop
P ==> emp ** P
  Proof.P: hprop
P ==> emp ** P
    unfold himp, star, emp, disjoint; simpl; intros.P: hprop
h: heap
H: wf h
H0: P h
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  h1 = nil /\
  P h2 /\
  h = merge h1 h2 /\
  (fix disjoint (h0 h3 : heap) {struct h0} : Prop :=
     match h0 with
     | nil => True
     | (x, _) :: h1' =>
         ~ indom x h3 /\ disjoint h1' h3
     end) h1 h2
    exists empty_heap, h.P: hprop
h: heap
H: wf h
H0: P h
wf empty_heap /\
wf h /\
empty_heap = nil /\
P h /\
h = merge empty_heap h /\
(fix disjoint (h1 h2 : heap) {struct h1} : Prop :=
   match h1 with
   | nil => True
   | (x, _) :: h1' => ~ indom x h2 /\ disjoint h1' h2
   end) empty_heap h
    mysimpl.
  Qed.
  #[export] Hint Resolve emp_star : sep_db.

  Lemma star_comm P Q :
    P ** Q ==> Q ** P.P, Q: hprop
P ** Q ==> Q ** P
  Proof.P, Q: hprop
P ** Q ==> Q ** P
    unfold himp, star; mysimpl.P, Q: hprop
h: heap
H: wf h
x, x0: heap
H0: wf x
H1: wf x0
H2: P x
H3: Q x0
H4: h = merge x x0
H5: disjoint x x0
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  Q h1 /\ P h2 /\ h = merge h1 h2 /\ disjoint h1 h2
    exists x0, x.P, Q: hprop
h: heap
H: wf h
x, x0: heap
H0: wf x
H1: wf x0
H2: P x
H3: Q x0
H4: h = merge x x0
H5: disjoint x x0
wf x0 /\
wf x /\ Q x0 /\ P x /\ h = merge x0 x /\ disjoint x0 x
    simpl in *; mysimpl; subst; auto using merge_comm, disjoint_comm.
  Qed.

  Lemma star_emp P :
    P ==> P ** emp.P: hprop
P ==> P ** emp
  Proof.P: hprop
P ==> P ** emp
    unfold himp, star, emp; intros.P: hprop
h: heap
H: wf h
H0: P h
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  P h1 /\
  h2 = nil /\ h = merge h1 h2 /\ disjoint h1 h2
    apply star_comm; auto.P: hprop
h: heap
H: wf h
H0: P h
((fun h2 : heap => h2 = nil) ** P) h
    apply emp_star; auto.
  Qed.
  #[export] Hint Resolve star_emp : sep_db.

  Lemma star_assoc P Q R :
    P ** (Q ** R) ==> (P ** Q) ** R.P, Q, R: hprop
P ** Q ** R ==> (P ** Q) ** R
  Proof.P, Q, R: hprop
P ** Q ** R ==> (P ** Q) ** R
    unfold himp, star; mysimpl; subst.P, Q, R: hprop
x, x1, x2: heap
H: wf (merge x (merge x1 x2))
H0: wf x
H1: wf (merge x1 x2)
H2: P x
H3: wf x1
H6: wf x2
H7: Q x1
H8: R x2
H10: disjoint x1 x2
H5: disjoint x (merge x1 x2)
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  (exists h3 h4 : heap,
     wf h3 /\
     wf h4 /\
     P h3 /\
     Q h4 /\ h1 = merge h3 h4 /\ disjoint h3 h4) /\
  R h2 /\
  merge x (merge x1 x2) = merge h1 h2 /\
  disjoint h1 h2
    assert (disjoint x x1 /\ disjoint x x2) as [].P, Q, R: hprop
x, x1, x2: heap
H: wf (merge x (merge x1 x2))
H0: wf x
H1: wf (merge x1 x2)
H2: P x
H3: wf x1
H6: wf x2
H7: Q x1
H8: R x2
H10: disjoint x1 x2
H5: disjoint x (merge x1 x2)
disjoint x x1 /\ disjoint x x2
P, Q, R: hprop
x, x1, x2: heap
H: wf (merge x (merge x1 x2))
H0: wf x
H1: wf (merge x1 x2)
H2: P x
H3: wf x1
H6: wf x2
H7: Q x1
H8: R x2
H10: disjoint x1 x2
H5: disjoint x (merge x1 x2)
H4: disjoint x x1
H9: disjoint x x2
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  (exists h3 h4 : heap,
     wf h3 /\
     wf h4 /\
     P h3 /\
     Q h4 /\ h1 = merge h3 h4 /\ disjoint h3 h4) /\
  R h2 /\
  merge x (merge x1 x2) = merge h1 h2 /\
  disjoint h1 h2
    {P, Q, R: hprop
x, x1, x2: heap
H: wf (merge x (merge x1 x2))
H0: wf x
H1: wf (merge x1 x2)
H2: P x
H3: wf x1
H6: wf x2
H7: Q x1
H8: R x2
H10: disjoint x1 x2
H5: disjoint x (merge x1 x2)
disjoint x x1 /\ disjoint x x2 apply merge_disjoint.P, Q, R: hprop
x, x1, x2: heap
H: wf (merge x (merge x1 x2))
H0: wf x
H1: wf (merge x1 x2)
H2: P x
H3: wf x1
H6: wf x2
H7: Q x1
H8: R x2
H10: disjoint x1 x2
H5: disjoint x (merge x1 x2)
disjoint x (merge x1 x2) assumption. }P, Q, R: hprop
x, x1, x2: heap
H: wf (merge x (merge x1 x2))
H0: wf x
H1: wf (merge x1 x2)
H2: P x
H3: wf x1
H6: wf x2
H7: Q x1
H8: R x2
H10: disjoint x1 x2
H5: disjoint x (merge x1 x2)
H4: disjoint x x1
H9: disjoint x x2
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  (exists h3 h4 : heap,
     wf h3 /\
     wf h4 /\
     P h3 /\
     Q h4 /\ h1 = merge h3 h4 /\ disjoint h3 h4) /\
  R h2 /\
  merge x (merge x1 x2) = merge h1 h2 /\
  disjoint h1 h2
    exists (merge x x1), x2.P, Q, R: hprop
x, x1, x2: heap
H: wf (merge x (merge x1 x2))
H0: wf x
H1: wf (merge x1 x2)
H2: P x
H3: wf x1
H6: wf x2
H7: Q x1
H8: R x2
H10: disjoint x1 x2
H5: disjoint x (merge x1 x2)
H4: disjoint x x1
H9: disjoint x x2
wf (merge x x1) /\
wf x2 /\
(exists h1 h2 : heap,
   wf h1 /\
   wf h2 /\
   P h1 /\
   Q h2 /\ merge x x1 = merge h1 h2 /\ disjoint h1 h2) /\
R x2 /\
merge x (merge x1 x2) = merge (merge x x1) x2 /\
disjoint (merge x x1) x2
    mysimpl.P, Q, R: hprop
x, x1, x2: heap
H: wf (merge x (merge x1 x2))
H0: wf x
H1: wf (merge x1 x2)
H2: P x
H3: wf x1
H6: wf x2
H7: Q x1
H8: R x2
H10: disjoint x1 x2
H5: disjoint x (merge x1 x2)
H4: disjoint x x1
H9: disjoint x x2
wf (merge x x1)
P, Q, R: hprop
x, x1, x2: heap
H: wf (merge x (merge x1 x2))
H0: wf x
H1: wf (merge x1 x2)
H2: P x
H3: wf x1
H6: wf x2
H7: Q x1
H8: R x2
H10: disjoint x1 x2
H5: disjoint x (merge x1 x2)
H4: disjoint x x1
H9: disjoint x x2
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  P h1 /\
  Q h2 /\ merge x x1 = merge h1 h2 /\ disjoint h1 h2
P, Q, R: hprop
x, x1, x2: heap
H: wf (merge x (merge x1 x2))
H0: wf x
H1: wf (merge x1 x2)
H2: P x
H3: wf x1
H6: wf x2
H7: Q x1
H8: R x2
H10: disjoint x1 x2
H5: disjoint x (merge x1 x2)
H4: disjoint x x1
H9: disjoint x x2
merge x (merge x1 x2) = merge (merge x x1) x2
P, Q, R: hprop
x, x1, x2: heap
H: wf (merge x (merge x1 x2))
H0: wf x
H1: wf (merge x1 x2)
H2: P x
H3: wf x1
H6: wf x2
H7: Q x1
H8: R x2
H10: disjoint x1 x2
H5: disjoint x (merge x1 x2)
H4: disjoint x x1
H9: disjoint x x2
disjoint (merge x x1) x2
    -P, Q, R: hprop
x, x1, x2: heap
H: wf (merge x (merge x1 x2))
H0: wf x
H1: wf (merge x1 x2)
H2: P x
H3: wf x1
H6: wf x2
H7: Q x1
H8: R x2
H10: disjoint x1 x2
H5: disjoint x (merge x1 x2)
H4: disjoint x x1
H9: disjoint x x2
wf (merge x x1) apply merge_wf; auto.
    -P, Q, R: hprop
x, x1, x2: heap
H: wf (merge x (merge x1 x2))
H0: wf x
H1: wf (merge x1 x2)
H2: P x
H3: wf x1
H6: wf x2
H7: Q x1
H8: R x2
H10: disjoint x1 x2
H5: disjoint x (merge x1 x2)
H4: disjoint x x1
H9: disjoint x x2
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  P h1 /\
  Q h2 /\ merge x x1 = merge h1 h2 /\ disjoint h1 h2 exists x, x1.P, Q, R: hprop
x, x1, x2: heap
H: wf (merge x (merge x1 x2))
H0: wf x
H1: wf (merge x1 x2)
H2: P x
H3: wf x1
H6: wf x2
H7: Q x1
H8: R x2
H10: disjoint x1 x2
H5: disjoint x (merge x1 x2)
H4: disjoint x x1
H9: disjoint x x2
wf x /\
wf x1 /\
P x /\
Q x1 /\ merge x x1 = merge x x1 /\ disjoint x x1 mysimpl.
    -P, Q, R: hprop
x, x1, x2: heap
H: wf (merge x (merge x1 x2))
H0: wf x
H1: wf (merge x1 x2)
H2: P x
H3: wf x1
H6: wf x2
H7: Q x1
H8: R x2
H10: disjoint x1 x2
H5: disjoint x (merge x1 x2)
H4: disjoint x x1
H9: disjoint x x2
merge x (merge x1 x2) = merge (merge x x1) x2 apply merge_assoc; auto.
    -P, Q, R: hprop
x, x1, x2: heap
H: wf (merge x (merge x1 x2))
H0: wf x
H1: wf (merge x1 x2)
H2: P x
H3: wf x1
H6: wf x2
H7: Q x1
H8: R x2
H10: disjoint x1 x2
H5: disjoint x (merge x1 x2)
H4: disjoint x x1
H9: disjoint x x2
disjoint (merge x x1) x2 apply disjoint_merge; auto.
  Qed.

  Lemma pure_elim (P:hprop) (R:hprop) (Q:Prop) :
    Q -> R ==> P -> R ==> (pure Q) ** P.P, R: hprop
Q: Prop
Q -> R ==> P -> R ==> pure Q ** P
  Proof.P, R: hprop
Q: Prop
Q -> R ==> P -> R ==> pure Q ** P
    unfold himp, pure, star, emp, disjoint.P, R: hprop
Q: Prop
Q ->
(forall h : heap, wf h -> R h -> P h) ->
forall h : heap,
wf h ->
R h ->
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  (h1 = nil /\ Q) /\
  P h2 /\
  h = merge h1 h2 /\
  (fix disjoint (h0 h3 : heap) {struct h0} : Prop :=
     match h0 with
     | nil => True
     | (x, _) :: h1' =>
         ~ indom x h3 /\ disjoint h1' h3
     end) h1 h2 intros.P, R: hprop
Q: Prop
H: Q
H0: forall h : heap, wf h -> R h -> P h
h: heap
H1: wf h
H2: R h
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  (h1 = nil /\ Q) /\
  P h2 /\
  h = merge h1 h2 /\
  (fix disjoint (h0 h3 : heap) {struct h0} : Prop :=
     match h0 with
     | nil => True
     | (x, _) :: h1' =>
         ~ indom x h3 /\ disjoint h1' h3
     end) h1 h2
    exists empty_heap, h.P, R: hprop
Q: Prop
H: Q
H0: forall h : heap, wf h -> R h -> P h
h: heap
H1: wf h
H2: R h
wf empty_heap /\
wf h /\
(empty_heap = nil /\ Q) /\
P h /\
h = merge empty_heap h /\
(fix disjoint (h1 h2 : heap) {struct h1} : Prop :=
   match h1 with
   | nil => True
   | (x, _) :: h1' => ~ indom x h2 /\ disjoint h1' h2
   end) empty_heap h mysimpl.
  Qed.
  #[export] Hint Resolve pure_elim : sep_db.

  Lemma comm_conc P Q R :
    P ==> Q ** R -> P ==> R ** Q.P, Q, R: hprop
P ==> Q ** R -> P ==> R ** Q
  Proof.P, Q, R: hprop
P ==> Q ** R -> P ==> R ** Q
    intros.P, Q, R: hprop
H: P ==> Q ** R
P ==> R ** Q intros h Hwf HP.P, Q, R: hprop
H: P ==> Q ** R
h: heap
Hwf: wf h
HP: P h
(R ** Q) h
    apply star_comm; auto.
  Qed.

  Lemma himp_id : forall P, P ==> P.forall P : hprop, P ==> P
  Proof.forall P : hprop, P ==> P
    unfold himp.forall (P : hprop) (h : heap), wf h -> P h -> P h auto.
  Qed.
  #[export] Hint Resolve himp_id : sep_db.

  Lemma ptsto_ptsto_some : forall (x : ptr) (v : value),
      x --> v ==> x -->?.forall (x : ptr) (v : value), x --> v ==> x -->?
  Proof.forall (x : ptr) (v : value), x --> v ==> x -->?
    unfold himp, ptsto_some, hexists, ptsto.forall (x : ptr) (v : value) (h : heap),
wf h ->
h = (x, v) :: nil ->
exists x0 : value, h = (x, x0) :: nil
    eauto.
  Qed.
  #[export] Hint Resolve ptsto_ptsto_some : sep_db.

  Lemma hyp_comm : forall P Q R,
      P ** Q ==> R -> Q ** P ==> R.forall P Q R : hprop, P ** Q ==> R -> Q ** P ==> R
  Proof.forall P Q R : hprop, P ** Q ==> R -> Q ** P ==> R
    unfold himp; mysimpl.P, Q, R: hprop
H: forall h : heap, wf h -> (P ** Q) h -> R h
h: heap
H0: wf h
H1: (Q ** P) h
R h
    apply H; auto.P, Q, R: hprop
H: forall h : heap, wf h -> (P ** Q) h -> R h
h: heap
H0: wf h
H1: (Q ** P) h
(P ** Q) h
    apply star_comm; auto.
  Qed.

  Lemma hyp_pure : forall (P:Prop) Q R,
      (P -> Q ==> R) -> (pure P) ** Q ==> R.forall (P : Prop) (Q R : hprop),
(P -> Q ==> R) -> pure P ** Q ==> R
  Proof.forall (P : Prop) (Q R : hprop),
(P -> Q ==> R) -> pure P ** Q ==> R
    unfold himp, star, pure, emp; mysimpl; subst; simpl in *.P: Prop
Q, R: hprop
H: P -> forall h : heap, wf h -> Q h -> R h
x0: heap
H0: wf x0
H1: True
H2: wf x0
H7: P
H4: Q x0
H6: True
R x0
    apply H; auto.
  Qed.
  #[export] Hint Resolve hyp_pure : sep_db.

  Lemma ptsto_hexist : forall (p:ptr) (v:value),
    p --> v ==> hexists (fun v => p --> v).forall (p : ptr) (v : value),
p --> v ==> hexists (fun v0 : value => p --> v0)
  Proof.forall (p : ptr) (v : value),
p --> v ==> hexists (fun v0 : value => p --> v0)
    unfold himp, hexists, ptsto; mysimpl;
      subst; mysimpl.p: ptr
v: value
H: wf ((p, v) :: nil)
exists x : value, (p, v) :: nil = (p, x) :: nil
    eauto.
  Qed.
  #[export] Hint Resolve ptsto_hexist : sep_db.

  Lemma hyp_hexists : forall t (F:t->hprop) R,
    (forall x:t, F x ==> R) -> hexists F ==> R.forall (t : Type) (F : t -> hprop) (R : hprop),
(forall x : t, F x ==> R) -> hexists F ==> R
  Proof.forall (t : Type) (F : t -> hprop) (R : hprop),
(forall x : t, F x ==> R) -> hexists F ==> R
    unfold hexists.forall (t : Type) (F : t -> hprop) (R : hprop),
(forall x : t, F x ==> R) ->
(fun h : heap => exists x : t, F x h) ==> R
    intros.t: Type
F: t -> hprop
R: hprop
H: forall x : t, F x ==> R
(fun h : heap => exists x : t, F x h) ==> R intros h Hwf.t: Type
F: t -> hprop
R: hprop
H: forall x : t, F x ==> R
h: heap
Hwf: wf h
(exists x : t, F x h) -> R h
    mysimpl.t: Type
F: t -> hprop
R: hprop
H: forall x : t, F x ==> R
h: heap
Hwf: wf h
x: t
H0: F x h
R h
    firstorder.
  Qed.

  Definition himp_split P1 P2 Q1 Q2 :
    P1 ==> Q1 -> P2 ==> Q2 -> P1 ** P2 ==> Q1 ** Q2.P1, P2, Q1, Q2: hprop
P1 ==> Q1 -> P2 ==> Q2 -> P1 ** P2 ==> Q1 ** Q2
  Proof.P1, P2, Q1, Q2: hprop
P1 ==> Q1 -> P2 ==> Q2 -> P1 ** P2 ==> Q1 ** Q2
    unfold himp, star; intros; mysimpl.P1, P2, Q1, Q2: hprop
H: forall h : heap, wf h -> P1 h -> Q1 h
H0: forall h : heap, wf h -> P2 h -> Q2 h
h: heap
H1: wf h
x, x0: heap
H2: wf x
H3: wf x0
H4: P1 x
H5: P2 x0
H6: h = merge x x0
H7: disjoint x x0
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  Q1 h1 /\ Q2 h2 /\ h = merge h1 h2 /\ disjoint h1 h2
    exists x, x0.P1, P2, Q1, Q2: hprop
H: forall h : heap, wf h -> P1 h -> Q1 h
H0: forall h : heap, wf h -> P2 h -> Q2 h
h: heap
H1: wf h
x, x0: heap
H2: wf x
H3: wf x0
H4: P1 x
H5: P2 x0
H6: h = merge x x0
H7: disjoint x x0
wf x /\
wf x0 /\
Q1 x /\ Q2 x0 /\ h = merge x x0 /\ disjoint x x0 mysimpl.
  Qed.

This little tactic helps prove things are disjoint:

  Ltac disj :=
    repeat
      match goal with
      | [ H : disjoint ?x ?y |- disjoint ?y ?x ] =>
          apply disjoint_comm; auto
      | [ |- disjoint (merge _ _) _ ] => apply disjoint_merge
      | [ |- disjoint _ (merge _ _) ] => apply disjoint_comm
      | [ H : disjoint (merge _ _) _ |- _ ] =>
          generalize (merge_disjoint _ _ _ (disjoint_comm _ _ H));
          clear H; mysimpl
      | [ H : disjoint _ (merge _ _) |- _ ] =>
          generalize (merge_disjoint _ _ _ H); clear H; mysimpl
      | [ |- wf (merge _ _) ] => apply merge_wf; mysimpl
      | [ |- _ ] => assumption
      end.

  Lemma star_assoc_l P Q R : (P ** Q) ** R ==> P ** Q ** R.P, Q, R: hprop
(P ** Q) ** R ==> P ** Q ** R
  Proof.P, Q, R: hprop
(P ** Q) ** R ==> P ** Q ** R
    unfold himp, star.P, Q, R: hprop
forall h : heap,
wf h ->
(exists h1 h2 : heap,
   wf h1 /\
   wf h2 /\
   (exists h3 h4 : heap,
      wf h3 /\
      wf h4 /\
      P h3 /\
      Q h4 /\ h1 = merge h3 h4 /\ disjoint h3 h4) /\
   R h2 /\ h = merge h1 h2 /\ disjoint h1 h2) ->
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  P h1 /\
  (exists h3 h4 : heap,
     wf h3 /\
     wf h4 /\
     Q h3 /\
     R h4 /\ h2 = merge h3 h4 /\ disjoint h3 h4) /\
  h = merge h1 h2 /\ disjoint h1 h2
    mysimpl; disj.P, Q, R: hprop
h: heap
H: wf h
x, x0: heap
H0: wf x
H1: wf x0
x1, x2: heap
H2: wf x1
H6: wf x2
H7: P x1
H8: Q x2
H9: x = merge x1 x2
H10: disjoint x1 x2
H3: R x0
H4: h = merge x x0
H5: disjoint x x0
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  P h1 /\
  (exists h3 h4 : heap,
     wf h3 /\
     wf h4 /\
     Q h3 /\
     R h4 /\ h2 = merge h3 h4 /\ disjoint h3 h4) /\
  h = merge h1 h2 /\ disjoint h1 h2 subst.P, Q, R: hprop
x0, x1, x2: heap
H: wf (merge (merge x1 x2) x0)
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: Q x2
H10: disjoint x1 x2
H3: R x0
H5: disjoint (merge x1 x2) x0
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  P h1 /\
  (exists h3 h4 : heap,
     wf h3 /\
     wf h4 /\
     Q h3 /\
     R h4 /\ h2 = merge h3 h4 /\ disjoint h3 h4) /\
  merge (merge x1 x2) x0 = merge h1 h2 /\
  disjoint h1 h2
    exists x1, (merge x2 x0).P, Q, R: hprop
x0, x1, x2: heap
H: wf (merge (merge x1 x2) x0)
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: Q x2
H10: disjoint x1 x2
H3: R x0
H5: disjoint (merge x1 x2) x0
wf x1 /\
wf (merge x2 x0) /\
P x1 /\
(exists h1 h2 : heap,
   wf h1 /\
   wf h2 /\
   Q h1 /\
   R h2 /\ merge x2 x0 = merge h1 h2 /\ disjoint h1 h2) /\
merge (merge x1 x2) x0 = merge x1 (merge x2 x0) /\
disjoint x1 (merge x2 x0)
    mysimpl; disj.P, Q, R: hprop
x0, x1, x2: heap
H: wf (merge (merge x1 x2) x0)
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: Q x2
H10: disjoint x1 x2
H3: R x0
H4: disjoint x0 x1
H5: disjoint x0 x2
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  Q h1 /\
  R h2 /\ merge x2 x0 = merge h1 h2 /\ disjoint h1 h2
P, Q, R: hprop
x0, x1, x2: heap
H: wf (merge (merge x1 x2) x0)
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: Q x2
H10: disjoint x1 x2
H3: R x0
H4: disjoint x0 x1
H5: disjoint x0 x2
merge (merge x1 x2) x0 = merge x1 (merge x2 x0)
    -P, Q, R: hprop
x0, x1, x2: heap
H: wf (merge (merge x1 x2) x0)
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: Q x2
H10: disjoint x1 x2
H3: R x0
H4: disjoint x0 x1
H5: disjoint x0 x2
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  Q h1 /\
  R h2 /\ merge x2 x0 = merge h1 h2 /\ disjoint h1 h2 exists x2, x0.P, Q, R: hprop
x0, x1, x2: heap
H: wf (merge (merge x1 x2) x0)
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: Q x2
H10: disjoint x1 x2
H3: R x0
H4: disjoint x0 x1
H5: disjoint x0 x2
wf x2 /\
wf x0 /\
Q x2 /\
R x0 /\ merge x2 x0 = merge x2 x0 /\ disjoint x2 x0 mysimpl; disj.
    -P, Q, R: hprop
x0, x1, x2: heap
H: wf (merge (merge x1 x2) x0)
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: Q x2
H10: disjoint x1 x2
H3: R x0
H4: disjoint x0 x1
H5: disjoint x0 x2
merge (merge x1 x2) x0 = merge x1 (merge x2 x0) rewrite merge_assoc; auto; disj.
  Qed.

This lemma will help me simplify some reasoning involving existentials.

  Lemma existPull (A : Type) (F : A -> Prop) (Y Z : Prop) :
    (exists x : A, F x) -> (Y -> Z) ->
    ((exists x : A, F x) -> Y) -> Z.A: Type
F: A -> Prop
Y, Z: Prop
(exists x : A, F x) ->
(Y -> Z) -> ((exists x : A, F x) -> Y) -> Z
  Proof.A: Type
F: A -> Prop
Y, Z: Prop
(exists x : A, F x) ->
(Y -> Z) -> ((exists x : A, F x) -> Y) -> Z
    firstorder.
  Qed.

  Lemma hyp_assoc_r P1 P2 P3 Q :
    P1 ** P2 ** P3 ==> Q -> (P1 ** P2) ** P3 ==> Q.P1, P2, P3, Q: hprop
P1 ** P2 ** P3 ==> Q -> (P1 ** P2) ** P3 ==> Q
  Proof.P1, P2, P3, Q: hprop
P1 ** P2 ** P3 ==> Q -> (P1 ** P2) ** P3 ==> Q
    unfold himp; intros.P1, P2, P3, Q: hprop
H: forall h : heap, wf h -> (P1 ** P2 ** P3) h -> Q h
h: heap
H0: wf h
H1: ((P1 ** P2) ** P3) h
Q h
    apply H; auto with sep_db.P1, P2, P3, Q: hprop
H: forall h : heap, wf h -> (P1 ** P2 ** P3) h -> Q h
h: heap
H0: wf h
H1: ((P1 ** P2) ** P3) h
(P1 ** P2 ** P3) h
    apply star_assoc_l; auto.
  Qed.
  #[export] Hint Resolve hyp_assoc_r : sep_db.

  Lemma conc_emp P Q : P ==> Q -> P ==> Q ** emp.P, Q: hprop
P ==> Q -> P ==> Q ** emp
  Proof.P, Q: hprop
P ==> Q -> P ==> Q ** emp
    unfold himp, emp, star.P, Q: hprop
(forall h : heap, wf h -> P h -> Q h) ->
forall h : heap,
wf h ->
P h ->
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  Q h1 /\
  h2 = nil /\ h = merge h1 h2 /\ disjoint h1 h2
    intros.P, Q: hprop
H: forall h : heap, wf h -> P h -> Q h
h: heap
H0: wf h
H1: P h
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  Q h1 /\
  h2 = nil /\ h = merge h1 h2 /\ disjoint h1 h2
    apply star_comm; auto.P, Q: hprop
H: forall h : heap, wf h -> P h -> Q h
h: heap
H0: wf h
H1: P h
((fun h2 : heap => h2 = nil) ** Q) h
    unfold star.P, Q: hprop
H: forall h : heap, wf h -> P h -> Q h
h: heap
H0: wf h
H1: P h
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  h1 = nil /\
  Q h2 /\ h = merge h1 h2 /\ disjoint h1 h2
    exists nil, h.P, Q: hprop
H: forall h : heap, wf h -> P h -> Q h
h: heap
H0: wf h
H1: P h
wf nil /\
wf h /\
nil = nil /\ Q h /\ h = merge nil h /\ disjoint nil h
    mysimpl.
  Qed.
  #[export] Hint Resolve conc_emp : sep_db.

  Lemma hyp_emp P Q : P ==> Q -> emp ** P ==> Q.P, Q: hprop
P ==> Q -> emp ** P ==> Q
  Proof.P, Q: hprop
P ==> Q -> emp ** P ==> Q
    unfold himp, emp, star.P, Q: hprop
(forall h : heap, wf h -> P h -> Q h) ->
forall h : heap,
wf h ->
(exists h1 h2 : heap,
   wf h1 /\
   wf h2 /\
   h1 = nil /\
   P h2 /\ h = merge h1 h2 /\ disjoint h1 h2) -> Q h
    mysimpl; subst; simpl in *; auto.
  Qed.
  #[export] Hint Resolve hyp_emp : sep_db.

  Lemma assoc_concl P Q1 Q2 Q3 :
    P ==> Q1 ** Q2 ** Q3 -> P ==> (Q1 ** Q2) ** Q3.P, Q1, Q2, Q3: hprop
P ==> Q1 ** Q2 ** Q3 -> P ==> (Q1 ** Q2) ** Q3
  Proof.P, Q1, Q2, Q3: hprop
P ==> Q1 ** Q2 ** Q3 -> P ==> (Q1 ** Q2) ** Q3
    unfold himp; intros.P, Q1, Q2, Q3: hprop
H: forall h : heap, wf h -> P h -> (Q1 ** Q2 ** Q3) h
h: heap
H0: wf h
H1: P h
((Q1 ** Q2) ** Q3) h
    apply star_assoc; auto.
  Qed.

  Lemma himp_mp Q P R : Q ==> R -> P ==> Q -> P ==> R.Q, P, R: hprop
Q ==> R -> P ==> Q -> P ==> R
  Proof.Q, P, R: hprop
Q ==> R -> P ==> Q -> P ==> R
    unfold himp; mysimpl.
  Qed.

Separation Logic

In separation logic, a total correctness assertion:

{{ P }} c {{ Q }}

holds iff (1) we start with a heap h that can be broken into two parts, one that satisfies P and another satisfying sing h2 for some h2, (2) we run the command c on heap h and get out Some heap h' and value v, and (3) the output heap h' satisfies Q v ** sing h2. That is, the output heap can be broken into two disjoint heaps, one satisfying Q v, and one satisfying sing h2.

This effectively forces the command to be parametric in some part of the heap (h2) and leave it alone. In turn, this means that if we have proven a separate property about h2, this property will be preserved when we run c.

  Definition sep_tc_triple
             (t : Type) (P : hprop) (c : Cmd t) (Q : t -> hprop) :=
    forall h h2, (P ** sing h2) h ->
      match c h with
      | None => False
      | Some (h', v) => (Q v ** sing h2) h'
      end.
  Notation "{{ P }} c {{ Q }}" :=
    (sep_tc_triple P c Q) (at level 90) : cmd_scope.

Lots of definitions to be unwound...

  Ltac unf := unfold sep_tc_triple, star, hexists, pure, emp, sing.

This says that ret v can be run in a heap satisfying emp and returns a heap satisfying emp and the return value is equal to v. But remember that this really means that ret can be run in any heap h that can be broken into a portion satisfying emp (i.e., the empty heap and some other heap (which must be h!) and that the other portion will be preserved. In short, the specification captures the fact that ret will not change the heap.

  Lemma ret_tc (t : Type) (v : t) :
    {{ emp }} ret v {{ fun x => pure (x = v) }}.t: Type
v: t
{{emp}} ret v {{fun x : t => pure (x = v)}}
  Proof.t: Type
v: t
{{emp}} ret v {{fun x : t => pure (x = v)}}
    unf; mysimpl; subst.t: Type
v: t
x0: heap
H: wf nil
H0: wf x0
H4: disjoint nil x0
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  (h1 = nil /\ v = v) /\
  x0 = h2 /\
  merge nil x0 = merge h1 h2 /\ disjoint h1 h2 exists empty_heap, x0.t: Type
v: t
x0: heap
H: wf nil
H0: wf x0
H4: disjoint nil x0
wf empty_heap /\
wf x0 /\
(empty_heap = nil /\ v = v) /\
x0 = x0 /\
merge nil x0 = merge empty_heap x0 /\
disjoint empty_heap x0 mysimpl.
  Qed.

new v consumes an empty heap, and produces a pointer x and a heap satisfying x --> v. Because of the definition of the separation-total-correctness triple, x must be fresh for the whole heap.

  Lemma new_tc (v : value) :
    {{ emp }} new v {{ fun (x : ptr) => x --> v }}.v: value
{{emp}} new v {{fun x : ptr => x --> v}}
  Proof.v: value
{{emp}} new v {{fun x : ptr => x --> v}}
    unfold new, ptsto; unf; mysimpl; subst.v: value
x0: heap
H: wf nil
H0: wf x0
H4: disjoint nil x0
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  h1 = (S (max_heap (merge nil x0)), v) :: nil /\
  x0 = h2 /\
  insert (S (max_heap (merge nil x0))) v
    (merge nil x0) = merge h1 h2 /\ disjoint h1 h2
    exists ((S (max_heap x0), v) :: nil), x0.v: value
x0: heap
H: wf nil
H0: wf x0
H4: disjoint nil x0
wf ((S (max_heap x0), v) :: nil) /\
wf x0 /\
(S (max_heap x0), v) :: nil =
(S (max_heap (merge nil x0)), v) :: nil /\
x0 = x0 /\
insert (S (max_heap (merge nil x0))) v (merge nil x0) =
merge ((S (max_heap x0), v) :: nil) x0 /\
disjoint ((S (max_heap x0), v) :: nil) x0
    mysimpl.v: value
x0: heap
H: wf nil
H0: wf x0
H4: disjoint nil x0
~ indom (S (max_heap x0)) x0
    apply max_heap_fresh.v: value
x0: heap
H: wf nil
H0: wf x0
H4: disjoint nil x0
S (max_heap x0) > max_heap x0 lia.
  Qed.

free x is nicely dual to new.

  Lemma free_tc (p : ptr) :
    {{ p-->? }} free p {{ fun _ => emp }}.p: ptr
{{p -->?}} free p {{fun _ : unit => emp}}
  Proof.p: ptr
{{p -->?}} free p {{fun _ : unit => emp}}
    unf; unfold ptsto_some, hexists, ptsto, free;
      mysimpl; subst; mysimpl.p: ptr
x0: heap
x1: value
H: wf ((p, x1) :: nil)
H0: wf x0
H4: disjoint ((p, x1) :: nil) x0
match
  match lookup p (insert p x1 x0) with
  | Some _ => Some (remove p (insert p x1 x0), tt)
  | None => None
  end
with
| Some (h', _) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      h1 = nil /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
    rewrite lookup_insert.p: ptr
x0: heap
x1: value
H: wf ((p, x1) :: nil)
H0: wf x0
H4: disjoint ((p, x1) :: nil) x0
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  h1 = nil /\
  x0 = h2 /\
  remove p (insert p x1 x0) = merge h1 h2 /\
  disjoint h1 h2
    exists nil, x0.p: ptr
x0: heap
x1: value
H: wf ((p, x1) :: nil)
H0: wf x0
H4: disjoint ((p, x1) :: nil) x0
wf nil /\
wf x0 /\
nil = nil /\
x0 = x0 /\
remove p (insert p x1 x0) = merge nil x0 /\
disjoint nil x0 mysimpl.p: ptr
x0: heap
x1: value
H: wf ((p, x1) :: nil)
H0: wf x0
H4: disjoint ((p, x1) :: nil) x0
remove p (insert p x1 x0) = x0
    apply remove_insert.
  Qed.

write p v requires a heap where p points to some value, and ensures p points to v afterwards.

  Lemma write_tc (p:ptr) (v:value) :
    {{ p -->? }} write p v {{ fun _ => p --> v }}.p: ptr
v: value
{{p -->?}} write p v {{fun _ : unit => p --> v}}
  Proof.p: ptr
v: value
{{p -->?}} write p v {{fun _ : unit => p --> v}}
    unfold ptsto_some, hexists, ptsto,
      write; unf.p: ptr
v: value
forall h h2 : heap,
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   (exists x : value, h1 = (p, x) :: nil) /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match
  match lookup p h with
  | Some _ => Some (insert p v (remove p h), tt)
  | None => None
  end
with
| Some (h', _) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      h1 = (p, v) :: nil /\
      h2 = h3 /\ h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
    mysimpl; subst; mysimpl; simpl in *.p: ptr
v: value
x0: heap
x1: value
H: True /\ True
H0: wf x0
H4: ~ indom p x0 /\ True
match
  match lookup p (insert p x1 x0) with
  | Some _ =>
      Some
        (insert p v (remove p (insert p x1 x0)), tt)
  | None => None
  end
with
| Some (h', _) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      h1 = (p, v) :: nil /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
    rewrite lookup_insert.p: ptr
v: value
x0: heap
x1: value
H: True /\ True
H0: wf x0
H4: ~ indom p x0 /\ True
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  h1 = (p, v) :: nil /\
  x0 = h2 /\
  insert p v (remove p (insert p x1 x0)) = merge h1 h2 /\
  disjoint h1 h2
    exists ((p, v) :: nil), x0.p: ptr
v: value
x0: heap
x1: value
H: True /\ True
H0: wf x0
H4: ~ indom p x0 /\ True
wf ((p, v) :: nil) /\
wf x0 /\
(p, v) :: nil = (p, v) :: nil /\
x0 = x0 /\
insert p v (remove p (insert p x1 x0)) =
merge ((p, v) :: nil) x0 /\
disjoint ((p, v) :: nil) x0
    mysimpl.p: ptr
v: value
x0: heap
x1: value
H, H3: True
H0: wf x0
H1: ~ indom p x0
H2: True
insert p v (remove p (insert p x1 x0)) = insert p v x0
    rewrite remove_insert; auto.
  Qed.

read p requires a heap where p points to some value v, and ensures p points to v afterwards, and the result is equal to v.

  Lemma read_tc (p:ptr) (v:value) :
    {{ p --> v }}
    read p
    {{ fun x => p --> x ** pure (x = v) }}.p: ptr
v: value
{{p --> v}} read p
{{fun x : value => p --> x ** pure (x = v)}}
  Proof.p: ptr
v: value
{{p --> v}} read p
{{fun x : value => p --> x ** pure (x = v)}}
    unf; unfold ptsto, read, read, bind;
      mysimpl; subst; mysimpl; simpl in *; mysimpl.p: ptr
v: value
x0: heap
H, H3: True
H0: wf x0
H1: ~ indom p x0
H2: True
match
  match lookup p (insert p v x0) with
  | Some u => Some (insert p v x0, u)
  | None => None
  end
with
| Some (h', v0) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      (exists h3 h4 : heap,
         wf h3 /\
         wf h4 /\
         h3 = (p, v0) :: nil /\
         (h4 = nil /\ v0 = v) /\
         h1 = merge h3 h4 /\ disjoint h3 h4) /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
    rewrite lookup_insert.p: ptr
v: value
x0: heap
H, H3: True
H0: wf x0
H1: ~ indom p x0
H2: True
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  (exists h3 h4 : heap,
     wf h3 /\
     wf h4 /\
     h3 = (p, v) :: nil /\
     (h4 = nil /\ v = v) /\
     h1 = merge h3 h4 /\ disjoint h3 h4) /\
  x0 = h2 /\
  insert p v x0 = merge h1 h2 /\ disjoint h1 h2
    unfold eq_rec_r; simpl.p: ptr
v: value
x0: heap
H, H3: True
H0: wf x0
H1: ~ indom p x0
H2: True
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  (exists h3 h4 : heap,
     wf h3 /\
     wf h4 /\
     h3 = (p, v) :: nil /\
     (h4 = nil /\ v = v) /\
     h1 = merge h3 h4 /\ disjoint h3 h4) /\
  x0 = h2 /\
  insert p v x0 = merge h1 h2 /\ disjoint h1 h2
    exists ((p,v) :: nil), x0.p: ptr
v: value
x0: heap
H, H3: True
H0: wf x0
H1: ~ indom p x0
H2: True
wf ((p, v) :: nil) /\
wf x0 /\
(exists h1 h2 : heap,
   wf h1 /\
   wf h2 /\
   h1 = (p, v) :: nil /\
   (h2 = nil /\ v = v) /\
   (p, v) :: nil = merge h1 h2 /\ disjoint h1 h2) /\
x0 = x0 /\
insert p v x0 = merge ((p, v) :: nil) x0 /\
disjoint ((p, v) :: nil) x0 mysimpl.p: ptr
v: value
x0: heap
H, H3: True
H0: wf x0
H1: ~ indom p x0
H2: True
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  h1 = (p, v) :: nil /\
  (h2 = nil /\ v = v) /\
  (p, v) :: nil = merge h1 h2 /\ disjoint h1 h2
    exists ((p, v) :: nil), nil.p: ptr
v: value
x0: heap
H, H3: True
H0: wf x0
H1: ~ indom p x0
H2: True
wf ((p, v) :: nil) /\
wf nil /\
(p, v) :: nil = (p, v) :: nil /\
(nil = nil /\ v = v) /\
(p, v) :: nil = merge ((p, v) :: nil) nil /\
disjoint ((p, v) :: nil) nil mysimpl.
  Qed.

  Lemma read_nat_tc (p:ptr) (n:nat) :
    {{ p --> VNat n }}
    read_nat p
    {{ fun x => p --> VNat x ** pure (x = n) }}.p: ptr
n: nat
{{p --> VNat n}} read_nat p
{{fun x : nat => p --> VNat x ** pure (x = n)}}
  Proof.p: ptr
n: nat
{{p --> VNat n}} read_nat p
{{fun x : nat => p --> VNat x ** pure (x = n)}}
    unf; unfold ptsto, read_nat, read, bind;
      mysimpl; subst; mysimpl; simpl in *; mysimpl.p: ptr
n: nat
x0: heap
H, H3: True
H0: wf x0
H1: ~ indom p x0
H2: True
match
  match
    match lookup p (insert p (VNat n) x0) with
    | Some u => Some (insert p (VNat n) x0, u)
    | None => None
    end
  with
  | Some (h2, v) =>
      match v with
      | VNat n => ret n
      | VPair _ _ => exit nat
      end h2
  | None => None
  end
with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      (exists h3 h4 : heap,
         wf h3 /\
         wf h4 /\
         h3 = (p, VNat v) :: nil /\
         (h4 = nil /\ v = n) /\
         h1 = merge h3 h4 /\ disjoint h3 h4) /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
    rewrite lookup_insert.p: ptr
n: nat
x0: heap
H, H3: True
H0: wf x0
H1: ~ indom p x0
H2: True
match ret n (insert p (VNat n) x0) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      (exists h3 h4 : heap,
         wf h3 /\
         wf h4 /\
         h3 = (p, VNat v) :: nil /\
         (h4 = nil /\ v = n) /\
         h1 = merge h3 h4 /\ disjoint h3 h4) /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
    unfold eq_rec_r; simpl.p: ptr
n: nat
x0: heap
H, H3: True
H0: wf x0
H1: ~ indom p x0
H2: True
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  (exists h3 h4 : heap,
     wf h3 /\
     wf h4 /\
     h3 = (p, VNat n) :: nil /\
     (h4 = nil /\ n = n) /\
     h1 = merge h3 h4 /\ disjoint h3 h4) /\
  x0 = h2 /\
  insert p (VNat n) x0 = merge h1 h2 /\ disjoint h1 h2
    exists ((p,VNat n) :: nil), x0.p: ptr
n: nat
x0: heap
H, H3: True
H0: wf x0
H1: ~ indom p x0
H2: True
wf ((p, VNat n) :: nil) /\
wf x0 /\
(exists h1 h2 : heap,
   wf h1 /\
   wf h2 /\
   h1 = (p, VNat n) :: nil /\
   (h2 = nil /\ n = n) /\
   (p, VNat n) :: nil = merge h1 h2 /\ disjoint h1 h2) /\
x0 = x0 /\
insert p (VNat n) x0 = merge ((p, VNat n) :: nil) x0 /\
disjoint ((p, VNat n) :: nil) x0 mysimpl.p: ptr
n: nat
x0: heap
H, H3: True
H0: wf x0
H1: ~ indom p x0
H2: True
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  h1 = (p, VNat n) :: nil /\
  (h2 = nil /\ n = n) /\
  (p, VNat n) :: nil = merge h1 h2 /\ disjoint h1 h2
    exists ((p,VNat n) :: nil), nil.p: ptr
n: nat
x0: heap
H, H3: True
H0: wf x0
H1: ~ indom p x0
H2: True
wf ((p, VNat n) :: nil) /\
wf nil /\
(p, VNat n) :: nil = (p, VNat n) :: nil /\
(nil = nil /\ n = n) /\
(p, VNat n) :: nil = merge ((p, VNat n) :: nil) nil /\
disjoint ((p, VNat n) :: nil) nil mysimpl.
  Qed.

This is one possible proof rule for bind. Basically, we require that the post-condition of the first command implies the pre-condition of the second command.

  Lemma bind_tc
        (T1 T2 : Type) P1 Q1 P2 Q2
        (c : Cmd T1) (f : T1 -> Cmd T2) :
    {{ P1 }} c {{ Q1 }} ->
    (forall x, {{ P2 x }} (f x) {{ Q2 }}) ->
    (forall x, Q1 x ==> P2 x) ->
    {{ P1 }} bind c f {{ Q2 }}.T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
{{P1}} c {{Q1}} ->
(forall x : T1, {{P2 x}} f x {{Q2}}) ->
(forall x : T1, Q1 x ==> P2 x) ->
{{P1}} x <- c; f x {{Q2}}
  Proof.T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
{{P1}} c {{Q1}} ->
(forall x : T1, {{P2 x}} f x {{Q2}}) ->
(forall x : T1, Q1 x ==> P2 x) ->
{{P1}} x <- c; f x {{Q2}}
    unfold bind; unf; mysimpl; subst.T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H: forall h h2 : heap,
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P1 h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match c h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q1 v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
H0: forall (x : T1) (h h2 : heap),
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P2 x h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match f x h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q2 v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
H1: forall x : T1, Q1 x ==> P2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P1 x
H7: disjoint x x0
match
  match c (merge x x0) with
  | Some (h2, v) => f v h2
  | None => None
  end
with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
    generalize (H (merge x x0) x0).T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H: forall h h2 : heap,
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P1 h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match c h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q1 v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
H0: forall (x : T1) (h h2 : heap),
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P2 x h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match f x h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q2 v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
H1: forall x : T1, Q1 x ==> P2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P1 x
H7: disjoint x x0
((exists h1 h2 : heap,
    wf h1 /\
    wf h2 /\
    P1 h1 /\
    x0 = h2 /\
    merge x x0 = merge h1 h2 /\ disjoint h1 h2) ->
 match c (merge x x0) with
 | Some (h', v) =>
     exists h1 h2 : heap,
       wf h1 /\
       wf h2 /\
       Q1 v h1 /\
       x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
 | None => False
 end) ->
match
  match c (merge x x0) with
  | Some (h2, v) => f v h2
  | None => None
  end
with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end clear H.T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H0: forall (x : T1) (h h2 : heap),
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P2 x h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match f x h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q2 v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
H1: forall x : T1, Q1 x ==> P2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P1 x
H7: disjoint x x0
((exists h1 h2 : heap,
    wf h1 /\
    wf h2 /\
    P1 h1 /\
    x0 = h2 /\
    merge x x0 = merge h1 h2 /\ disjoint h1 h2) ->
 match c (merge x x0) with
 | Some (h', v) =>
     exists h1 h2 : heap,
       wf h1 /\
       wf h2 /\
       Q1 v h1 /\
       x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
 | None => False
 end) ->
match
  match c (merge x x0) with
  | Some (h2, v) => f v h2
  | None => None
  end
with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
    apply existPull.T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H0: forall (x : T1) (h h2 : heap),
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P2 x h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match f x h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q2 v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
H1: forall x : T1, Q1 x ==> P2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P1 x
H7: disjoint x x0
exists x1 h2 : heap,
  wf x1 /\
  wf h2 /\
  P1 x1 /\
  x0 = h2 /\
  merge x x0 = merge x1 h2 /\ disjoint x1 h2
T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H0: forall (x : T1) (h h2 : heap),
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P2 x h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match f x h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q2 v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
H1: forall x : T1, Q1 x ==> P2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P1 x
H7: disjoint x x0
match c (merge x x0) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q1 v h1 /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end ->
match
  match c (merge x x0) with
  | Some (h2, v) => f v h2
  | None => None
  end
with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
    -T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H0: forall (x : T1) (h h2 : heap),
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P2 x h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match f x h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q2 v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
H1: forall x : T1, Q1 x ==> P2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P1 x
H7: disjoint x x0
exists x1 h2 : heap,
  wf x1 /\
  wf h2 /\
  P1 x1 /\
  x0 = h2 /\
  merge x x0 = merge x1 h2 /\ disjoint x1 h2 exists x, x0.T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H0: forall (x : T1) (h h2 : heap),
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P2 x h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match f x h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q2 v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
H1: forall x : T1, Q1 x ==> P2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P1 x
H7: disjoint x x0
wf x /\
wf x0 /\
P1 x /\
x0 = x0 /\ merge x x0 = merge x x0 /\ disjoint x x0 mysimpl.
    -T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H0: forall (x : T1) (h h2 : heap),
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P2 x h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match f x h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q2 v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
H1: forall x : T1, Q1 x ==> P2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P1 x
H7: disjoint x x0
match c (merge x x0) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q1 v h1 /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end ->
match
  match c (merge x x0) with
  | Some (h2, v) => f v h2
  | None => None
  end
with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end destruct (c (merge x x0)); mysimpl.T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H0: forall (x : T1) (h h2 : heap),
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P2 x h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match f x h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q2 v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
H1: forall x : T1, Q1 x ==> P2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P1 x
H7: disjoint x x0
h: heap
t: T1
x1, x2: heap
H: wf x1
H5: wf x2
H6: Q1 t x1
H8: x0 = x2
H9: h = merge x1 x2
H10: disjoint x1 x2
match f t h with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
      subst.T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H0: forall (x : T1) (h h2 : heap),
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P2 x h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match f x h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q2 v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
H1: forall x : T1, Q1 x ==> P2 x
x: heap
H2: wf x
x2: heap
H3: wf x2
H4: P1 x
H7: disjoint x x2
t: T1
x1: heap
H: wf x1
H5: wf x2
H6: Q1 t x1
H10: disjoint x1 x2
match f t (merge x1 x2) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x2 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
      generalize (H0 t (merge x1 x2) x2).T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H0: forall (x : T1) (h h2 : heap),
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P2 x h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match f x h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q2 v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
H1: forall x : T1, Q1 x ==> P2 x
x: heap
H2: wf x
x2: heap
H3: wf x2
H4: P1 x
H7: disjoint x x2
t: T1
x1: heap
H: wf x1
H5: wf x2
H6: Q1 t x1
H10: disjoint x1 x2
((exists h1 h2 : heap,
    wf h1 /\
    wf h2 /\
    P2 t h1 /\
    x2 = h2 /\
    merge x1 x2 = merge h1 h2 /\ disjoint h1 h2) ->
 match f t (merge x1 x2) with
 | Some (h', v) =>
     exists h1 h2 : heap,
       wf h1 /\
       wf h2 /\
       Q2 v h1 /\
       x2 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
 | None => False
 end) ->
match f t (merge x1 x2) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x2 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end clear H0.T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H1: forall x : T1, Q1 x ==> P2 x
x: heap
H2: wf x
x2: heap
H3: wf x2
H4: P1 x
H7: disjoint x x2
t: T1
x1: heap
H: wf x1
H5: wf x2
H6: Q1 t x1
H10: disjoint x1 x2
((exists h1 h2 : heap,
    wf h1 /\
    wf h2 /\
    P2 t h1 /\
    x2 = h2 /\
    merge x1 x2 = merge h1 h2 /\ disjoint h1 h2) ->
 match f t (merge x1 x2) with
 | Some (h', v) =>
     exists h1 h2 : heap,
       wf h1 /\
       wf h2 /\
       Q2 v h1 /\
       x2 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
 | None => False
 end) ->
match f t (merge x1 x2) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x2 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
      apply existPull.T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H1: forall x : T1, Q1 x ==> P2 x
x: heap
H2: wf x
x2: heap
H3: wf x2
H4: P1 x
H7: disjoint x x2
t: T1
x1: heap
H: wf x1
H5: wf x2
H6: Q1 t x1
H10: disjoint x1 x2
exists x h2 : heap,
  wf x /\
  wf h2 /\
  P2 t x /\
  x2 = h2 /\ merge x1 x2 = merge x h2 /\ disjoint x h2
T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H1: forall x : T1, Q1 x ==> P2 x
x: heap
H2: wf x
x2: heap
H3: wf x2
H4: P1 x
H7: disjoint x x2
t: T1
x1: heap
H: wf x1
H5: wf x2
H6: Q1 t x1
H10: disjoint x1 x2
match f t (merge x1 x2) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x2 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end ->
match f t (merge x1 x2) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x2 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
      +T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H1: forall x : T1, Q1 x ==> P2 x
x: heap
H2: wf x
x2: heap
H3: wf x2
H4: P1 x
H7: disjoint x x2
t: T1
x1: heap
H: wf x1
H5: wf x2
H6: Q1 t x1
H10: disjoint x1 x2
exists x h2 : heap,
  wf x /\
  wf h2 /\
  P2 t x /\
  x2 = h2 /\ merge x1 x2 = merge x h2 /\ disjoint x h2 exists x1, x2.T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H1: forall x : T1, Q1 x ==> P2 x
x: heap
H2: wf x
x2: heap
H3: wf x2
H4: P1 x
H7: disjoint x x2
t: T1
x1: heap
H: wf x1
H5: wf x2
H6: Q1 t x1
H10: disjoint x1 x2
wf x1 /\
wf x2 /\
P2 t x1 /\
x2 = x2 /\ merge x1 x2 = merge x1 x2 /\ disjoint x1 x2 mysimpl.T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H1: forall x : T1, Q1 x ==> P2 x
x: heap
H2: wf x
x2: heap
H3: wf x2
H4: P1 x
H7: disjoint x x2
t: T1
x1: heap
H: wf x1
H5: wf x2
H6: Q1 t x1
H10: disjoint x1 x2
P2 t x1
        eapply H1; eauto.
      +T1, T2: Type
P1: hprop
Q1, P2: T1 -> hprop
Q2: T2 -> hprop
c: Cmd T1
f: T1 -> Cmd T2
H1: forall x : T1, Q1 x ==> P2 x
x: heap
H2: wf x
x2: heap
H3: wf x2
H4: P1 x
H7: disjoint x x2
t: T1
x1: heap
H: wf x1
H5: wf x2
H6: Q1 t x1
H10: disjoint x1 x2
match f t (merge x1 x2) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x2 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end ->
match f t (merge x1 x2) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x2 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end auto.
  Qed.
  Arguments bind_tc {T1 T2 P1 Q1 P2 Q2 c f}.

And we also have a rule of consequence which allows us to strengthen the pre-condition and weaken the post-condition. Note however, that this will not allow us to "forget" any locations in our footprint.

  Lemma consequence_tc (T : Type) P1 Q1 P2 Q2 (c : Cmd T) :
    {{ P1 }} c {{ Q1 }} ->
    P2 ==> P1 ->
    (forall x, Q1 x ==> Q2 x) ->
    {{ P2 }} c {{ Q2 }}.T: Type
P1: hprop
Q1: T -> hprop
P2: hprop
Q2: T -> hprop
c: Cmd T
{{P1}} c {{Q1}} ->
P2 ==> P1 ->
(forall x : T, Q1 x ==> Q2 x) -> {{P2}} c {{Q2}}
  Proof.T: Type
P1: hprop
Q1: T -> hprop
P2: hprop
Q2: T -> hprop
c: Cmd T
{{P1}} c {{Q1}} ->
P2 ==> P1 ->
(forall x : T, Q1 x ==> Q2 x) -> {{P2}} c {{Q2}}
    unf; mysimpl; subst; mysimpl.T: Type
P1: hprop
Q1: T -> hprop
P2: hprop
Q2: T -> hprop
c: Cmd T
H: forall h h2 : heap,
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P1 h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match c h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q1 v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
H0: P2 ==> P1
H1: forall x : T, Q1 x ==> Q2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P2 x
H7: disjoint x x0
match c (merge x x0) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
    generalize (H (merge x x0) x0).T: Type
P1: hprop
Q1: T -> hprop
P2: hprop
Q2: T -> hprop
c: Cmd T
H: forall h h2 : heap,
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P1 h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match c h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q1 v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
H0: P2 ==> P1
H1: forall x : T, Q1 x ==> Q2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P2 x
H7: disjoint x x0
((exists h1 h2 : heap,
    wf h1 /\
    wf h2 /\
    P1 h1 /\
    x0 = h2 /\
    merge x x0 = merge h1 h2 /\ disjoint h1 h2) ->
 match c (merge x x0) with
 | Some (h', v) =>
     exists h1 h2 : heap,
       wf h1 /\
       wf h2 /\
       Q1 v h1 /\
       x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
 | None => False
 end) ->
match c (merge x x0) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end clear H.T: Type
P1: hprop
Q1: T -> hprop
P2: hprop
Q2: T -> hprop
c: Cmd T
H0: P2 ==> P1
H1: forall x : T, Q1 x ==> Q2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P2 x
H7: disjoint x x0
((exists h1 h2 : heap,
    wf h1 /\
    wf h2 /\
    P1 h1 /\
    x0 = h2 /\
    merge x x0 = merge h1 h2 /\ disjoint h1 h2) ->
 match c (merge x x0) with
 | Some (h', v) =>
     exists h1 h2 : heap,
       wf h1 /\
       wf h2 /\
       Q1 v h1 /\
       x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
 | None => False
 end) ->
match c (merge x x0) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
    apply existPull.T: Type
P1: hprop
Q1: T -> hprop
P2: hprop
Q2: T -> hprop
c: Cmd T
H0: P2 ==> P1
H1: forall x : T, Q1 x ==> Q2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P2 x
H7: disjoint x x0
exists x1 h2 : heap,
  wf x1 /\
  wf h2 /\
  P1 x1 /\
  x0 = h2 /\
  merge x x0 = merge x1 h2 /\ disjoint x1 h2
T: Type
P1: hprop
Q1: T -> hprop
P2: hprop
Q2: T -> hprop
c: Cmd T
H0: P2 ==> P1
H1: forall x : T, Q1 x ==> Q2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P2 x
H7: disjoint x x0
match c (merge x x0) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q1 v h1 /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end ->
match c (merge x x0) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
    -T: Type
P1: hprop
Q1: T -> hprop
P2: hprop
Q2: T -> hprop
c: Cmd T
H0: P2 ==> P1
H1: forall x : T, Q1 x ==> Q2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P2 x
H7: disjoint x x0
exists x1 h2 : heap,
  wf x1 /\
  wf h2 /\
  P1 x1 /\
  x0 = h2 /\
  merge x x0 = merge x1 h2 /\ disjoint x1 h2 exists x, x0.T: Type
P1: hprop
Q1: T -> hprop
P2: hprop
Q2: T -> hprop
c: Cmd T
H0: P2 ==> P1
H1: forall x : T, Q1 x ==> Q2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P2 x
H7: disjoint x x0
wf x /\
wf x0 /\
P1 x /\
x0 = x0 /\ merge x x0 = merge x x0 /\ disjoint x x0 mysimpl.
    -T: Type
P1: hprop
Q1: T -> hprop
P2: hprop
Q2: T -> hprop
c: Cmd T
H0: P2 ==> P1
H1: forall x : T, Q1 x ==> Q2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P2 x
H7: disjoint x x0
match c (merge x x0) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q1 v h1 /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end ->
match c (merge x x0) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q2 v h1 /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end destruct (c (merge x x0)); mysimpl.T: Type
P1: hprop
Q1: T -> hprop
P2: hprop
Q2: T -> hprop
c: Cmd T
H0: P2 ==> P1
H1: forall x : T, Q1 x ==> Q2 x
x, x0: heap
H2: wf x
H3: wf x0
H4: P2 x
H7: disjoint x x0
h: heap
t: T
x1, x2: heap
H: wf x1
H5: wf x2
H6: Q1 t x1
H8: x0 = x2
H9: h = merge x1 x2
H10: disjoint x1 x2
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  Q2 t h1 /\
  x0 = h2 /\ h = merge h1 h2 /\ disjoint h1 h2
      subst.T: Type
P1: hprop
Q1: T -> hprop
P2: hprop
Q2: T -> hprop
c: Cmd T
H0: P2 ==> P1
H1: forall x : T, Q1 x ==> Q2 x
x: heap
H2: wf x
x2: heap
H3: wf x2
H4: P2 x
H7: disjoint x x2
t: T
x1: heap
H: wf x1
H5: wf x2
H6: Q1 t x1
H10: disjoint x1 x2
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  Q2 t h1 /\
  x2 = h2 /\
  merge x1 x2 = merge h1 h2 /\ disjoint h1 h2
      exists x1, x2.T: Type
P1: hprop
Q1: T -> hprop
P2: hprop
Q2: T -> hprop
c: Cmd T
H0: P2 ==> P1
H1: forall x : T, Q1 x ==> Q2 x
x: heap
H2: wf x
x2: heap
H3: wf x2
H4: P2 x
H7: disjoint x x2
t: T
x1: heap
H: wf x1
H5: wf x2
H6: Q1 t x1
H10: disjoint x1 x2
wf x1 /\
wf x2 /\
Q2 t x1 /\
x2 = x2 /\ merge x1 x2 = merge x1 x2 /\ disjoint x1 x2
      firstorder.
  Qed.
  Arguments consequence_tc {T} _ _ {P2 Q2 c}.

This is a specialization of consequence that is a little more useful.

  Lemma strengthen_tc (T : Type) P1 P2 Q1 (c : Cmd T):
    {{P1}} c {{Q1}} ->
    P2 ==> P1 ->
    {{P2}} c {{Q1}}.T: Type
P1, P2: hprop
Q1: T -> hprop
c: Cmd T
{{P1}} c {{Q1}} -> P2 ==> P1 -> {{P2}} c {{Q1}}
  Proof.T: Type
P1, P2: hprop
Q1: T -> hprop
c: Cmd T
{{P1}} c {{Q1}} -> P2 ==> P1 -> {{P2}} c {{Q1}}
    intros.T: Type
P1, P2: hprop
Q1: T -> hprop
c: Cmd T
H: {{P1}} c {{Q1}}
H0: P2 ==> P1
{{P2}} c {{Q1}} eapply consequence_tc; eauto with sep_db.
  Qed.
  Arguments strengthen_tc {T} _ {P2 Q1 c}.

This is a specialization of consequence that is a little more useful.

  Lemma weaken_tc (T : Type) P1 Q1 Q2 (c : Cmd T):
    {{P1}} c {{Q1}} ->
    (forall x, Q1 x ==> Q2 x) ->
    {{P1}} c {{Q2}}.T: Type
P1: hprop
Q1, Q2: T -> hprop
c: Cmd T
{{P1}} c {{Q1}} ->
(forall x : T, Q1 x ==> Q2 x) -> {{P1}} c {{Q2}}
  Proof.T: Type
P1: hprop
Q1, Q2: T -> hprop
c: Cmd T
{{P1}} c {{Q1}} ->
(forall x : T, Q1 x ==> Q2 x) -> {{P1}} c {{Q2}}
    intros.T: Type
P1: hprop
Q1, Q2: T -> hprop
c: Cmd T
H: {{P1}} c {{Q1}}
H0: forall x : T, Q1 x ==> Q2 x
{{P1}} c {{Q2}} eapply consequence_tc; eauto with sep_db.
  Qed.

Finally, this is the most important rule and the one we lacked with Hoare logic: If {{ P }} c {{ Q }}, then also {{ P ** R }} c {{ Q ** R }}. That is, properties such as R which are disjoint from the footprint are preserved when we run the command.

  Lemma frame_tc (T : Type) (c : Cmd T) P Q R :
    {{ P }} c {{ Q }} ->
    {{ P ** R }} c {{ fun x => (Q x) ** R }}.T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
{{P}} c {{Q}} ->
{{P ** R}} c {{fun x : T => Q x ** R}}
  Proof.T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
{{P}} c {{Q}} ->
{{P ** R}} c {{fun x : T => Q x ** R}}
    unf; mysimpl; subst; mysimpl.T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
H: forall h h2 : heap,
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match c h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
x0, x1, x2: heap
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: R x2
H10: disjoint x1 x2
H5: disjoint (merge x1 x2) x0
match c (merge (merge x1 x2) x0) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      (exists h3 h4 : heap,
         wf h3 /\
         wf h4 /\
         Q v h3 /\
         R h4 /\ h1 = merge h3 h4 /\ disjoint h3 h4) /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
    rewrite <- merge_assoc; auto; disj.T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
H: forall h h2 : heap,
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match c h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
x0, x1, x2: heap
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: R x2
H10: disjoint x1 x2
H3: disjoint x0 x1
H4: disjoint x0 x2
match c (merge x1 (merge x2 x0)) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      (exists h3 h4 : heap,
         wf h3 /\
         wf h4 /\
         Q v h3 /\
         R h4 /\ h1 = merge h3 h4 /\ disjoint h3 h4) /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
    generalize (H (merge x1 (merge x2 x0)) (merge x2 x0)).T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
H: forall h h2 : heap,
(exists h1 h3 : heap,
   wf h1 /\
   wf h3 /\
   P h1 /\
   h2 = h3 /\ h = merge h1 h3 /\ disjoint h1 h3) ->
match c h with
| Some (h', v) =>
    exists h1 h3 : heap,
      wf h1 /\
      wf h3 /\
      Q v h1 /\
      h2 = h3 /\
      h' = merge h1 h3 /\ disjoint h1 h3
| None => False
end
x0, x1, x2: heap
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: R x2
H10: disjoint x1 x2
H3: disjoint x0 x1
H4: disjoint x0 x2
((exists h1 h2 : heap,
    wf h1 /\
    wf h2 /\
    P h1 /\
    merge x2 x0 = h2 /\
    merge x1 (merge x2 x0) = merge h1 h2 /\
    disjoint h1 h2) ->
 match c (merge x1 (merge x2 x0)) with
 | Some (h', v) =>
     exists h1 h2 : heap,
       wf h1 /\
       wf h2 /\
       Q v h1 /\
       merge x2 x0 = h2 /\
       h' = merge h1 h2 /\ disjoint h1 h2
 | None => False
 end) ->
match c (merge x1 (merge x2 x0)) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      (exists h3 h4 : heap,
         wf h3 /\
         wf h4 /\
         Q v h3 /\
         R h4 /\ h1 = merge h3 h4 /\ disjoint h3 h4) /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
    clear H.T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
x0, x1, x2: heap
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: R x2
H10: disjoint x1 x2
H3: disjoint x0 x1
H4: disjoint x0 x2
((exists h1 h2 : heap,
    wf h1 /\
    wf h2 /\
    P h1 /\
    merge x2 x0 = h2 /\
    merge x1 (merge x2 x0) = merge h1 h2 /\
    disjoint h1 h2) ->
 match c (merge x1 (merge x2 x0)) with
 | Some (h', v) =>
     exists h1 h2 : heap,
       wf h1 /\
       wf h2 /\
       Q v h1 /\
       merge x2 x0 = h2 /\
       h' = merge h1 h2 /\ disjoint h1 h2
 | None => False
 end) ->
match c (merge x1 (merge x2 x0)) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      (exists h3 h4 : heap,
         wf h3 /\
         wf h4 /\
         Q v h3 /\
         R h4 /\ h1 = merge h3 h4 /\ disjoint h3 h4) /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
    apply existPull.T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
x0, x1, x2: heap
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: R x2
H10: disjoint x1 x2
H3: disjoint x0 x1
H4: disjoint x0 x2
exists x h2 : heap,
  wf x /\
  wf h2 /\
  P x /\
  merge x2 x0 = h2 /\
  merge x1 (merge x2 x0) = merge x h2 /\ disjoint x h2
T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
x0, x1, x2: heap
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: R x2
H10: disjoint x1 x2
H3: disjoint x0 x1
H4: disjoint x0 x2
match c (merge x1 (merge x2 x0)) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q v h1 /\
      merge x2 x0 = h2 /\
      h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end ->
match c (merge x1 (merge x2 x0)) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      (exists h3 h4 : heap,
         wf h3 /\
         wf h4 /\
         Q v h3 /\
         R h4 /\ h1 = merge h3 h4 /\ disjoint h3 h4) /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end
    -T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
x0, x1, x2: heap
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: R x2
H10: disjoint x1 x2
H3: disjoint x0 x1
H4: disjoint x0 x2
exists x h2 : heap,
  wf x /\
  wf h2 /\
  P x /\
  merge x2 x0 = h2 /\
  merge x1 (merge x2 x0) = merge x h2 /\ disjoint x h2 exists x1, (merge x2 x0).T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
x0, x1, x2: heap
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: R x2
H10: disjoint x1 x2
H3: disjoint x0 x1
H4: disjoint x0 x2
wf x1 /\
wf (merge x2 x0) /\
P x1 /\
merge x2 x0 = merge x2 x0 /\
merge x1 (merge x2 x0) = merge x1 (merge x2 x0) /\
disjoint x1 (merge x2 x0)
      mysimpl; disj.
    -T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
x0, x1, x2: heap
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: R x2
H10: disjoint x1 x2
H3: disjoint x0 x1
H4: disjoint x0 x2
match c (merge x1 (merge x2 x0)) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      Q v h1 /\
      merge x2 x0 = h2 /\
      h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end ->
match c (merge x1 (merge x2 x0)) with
| Some (h', v) =>
    exists h1 h2 : heap,
      wf h1 /\
      wf h2 /\
      (exists h3 h4 : heap,
         wf h3 /\
         wf h4 /\
         Q v h3 /\
         R h4 /\ h1 = merge h3 h4 /\ disjoint h3 h4) /\
      x0 = h2 /\ h' = merge h1 h2 /\ disjoint h1 h2
| None => False
end destruct (c (merge x1 (merge x2 x0))); mysimpl; subst.T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
x0, x1, x2: heap
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: R x2
H10: disjoint x1 x2
H3: disjoint x0 x1
H4: disjoint x0 x2
t: T
x: heap
H: wf x
H5: wf (merge x2 x0)
H9: Q t x
H13: disjoint x (merge x2 x0)
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  (exists h3 h4 : heap,
     wf h3 /\
     wf h4 /\
     Q t h3 /\
     R h4 /\ h1 = merge h3 h4 /\ disjoint h3 h4) /\
  x0 = h2 /\
  merge x (merge x2 x0) = merge h1 h2 /\
  disjoint h1 h2
      exists (merge x x2), x0.T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
x0, x1, x2: heap
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: R x2
H10: disjoint x1 x2
H3: disjoint x0 x1
H4: disjoint x0 x2
t: T
x: heap
H: wf x
H5: wf (merge x2 x0)
H9: Q t x
H13: disjoint x (merge x2 x0)
wf (merge x x2) /\
wf x0 /\
(exists h1 h2 : heap,
   wf h1 /\
   wf h2 /\
   Q t h1 /\
   R h2 /\ merge x x2 = merge h1 h2 /\ disjoint h1 h2) /\
x0 = x0 /\
merge x (merge x2 x0) = merge (merge x x2) x0 /\
disjoint (merge x x2) x0 mysimpl; disj.T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
x0, x1, x2: heap
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: R x2
H10: disjoint x1 x2
H3: disjoint x0 x1
H4: disjoint x0 x2
t: T
x: heap
H: wf x
H5: wf (merge x2 x0)
H9: Q t x
H11: disjoint x x2
H12: disjoint x x0
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  Q t h1 /\
  R h2 /\ merge x x2 = merge h1 h2 /\ disjoint h1 h2
T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
x0, x1, x2: heap
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: R x2
H10: disjoint x1 x2
H3: disjoint x0 x1
H4: disjoint x0 x2
t: T
x: heap
H: wf x
H5: wf (merge x2 x0)
H9: Q t x
H11: disjoint x x2
H12: disjoint x x0
merge x (merge x2 x0) = merge (merge x x2) x0
      +T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
x0, x1, x2: heap
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: R x2
H10: disjoint x1 x2
H3: disjoint x0 x1
H4: disjoint x0 x2
t: T
x: heap
H: wf x
H5: wf (merge x2 x0)
H9: Q t x
H11: disjoint x x2
H12: disjoint x x0
exists h1 h2 : heap,
  wf h1 /\
  wf h2 /\
  Q t h1 /\
  R h2 /\ merge x x2 = merge h1 h2 /\ disjoint h1 h2 exists x, x2.T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
x0, x1, x2: heap
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: R x2
H10: disjoint x1 x2
H3: disjoint x0 x1
H4: disjoint x0 x2
t: T
x: heap
H: wf x
H5: wf (merge x2 x0)
H9: Q t x
H11: disjoint x x2
H12: disjoint x x0
wf x /\
wf x2 /\
Q t x /\
R x2 /\ merge x x2 = merge x x2 /\ disjoint x x2 mysimpl; disj.
      +T: Type
c: Cmd T
P: hprop
Q: T -> hprop
R: hprop
x0, x1, x2: heap
H0: wf (merge x1 x2)
H1: wf x0
H2: wf x1
H6: wf x2
H7: P x1
H8: R x2
H10: disjoint x1 x2
H3: disjoint x0 x1
H4: disjoint x0 x2
t: T
x: heap
H: wf x
H5: wf (merge x2 x0)
H9: Q t x
H11: disjoint x x2
H12: disjoint x x0
merge x (merge x2 x0) = merge (merge x x2) x0 rewrite merge_assoc; disj; auto.
  Qed.
  Arguments frame_tc {T c P Q}.

  Ltac sep := repeat
    (simpl in *; (try subst);
     match goal with
     | [ |- forall _, _ ] =>
         intros
     | [ |- _ ** ?Q ==> _ ** ?Q ] =>
         eapply himp_split
     | [ |- ?P ** _ ==> ?P ** _ ] =>
         eapply himp_split
     | [ |- ?P ** _ ==> _ ** ?P ] =>
         eapply hyp_comm
     | [ |- hexists _ ==> _ ] =>
         eapply hyp_hexists
     | [ |- _ ** pure _ ==> _ ] =>
         eapply hyp_comm; eapply hyp_pure
     | [ |- (_ ** _) ** _ ==> _ ] =>
         eapply hyp_assoc_r
     | [ |- _ ==> (_ ** _) ** _ ] =>
         eapply assoc_concl
     | _ =>
         eauto with sep_db
      end).

Examples

Following are a few examples that illustrate the use of Separation Logic.

  Definition inc(p:ptr) :=
    v <- read_nat p;
    write p (VNat (1 + v)).

The next definition says that if we start in a state where p holds n, then after running inc, we do not fail and get into a state where p holds 1+n. Notice that it's rather delicate to hang on to the fact that the value read out is equal to n. If we used binary post-conditions (a relation on both the input heap and output heap), this wouldn't be necessary.

  Definition inc_tc (p : ptr) (n : nat) :
    {{ p --> VNat n }} inc p {{ fun _ => p --> VNat (1 + n) }}.p: ptr
n: nat
{{p --> VNat n}} inc p
{{fun _ : unit => p --> VNat (1 + n)}}
  Proof.p: ptr
n: nat
{{p --> VNat n}} inc p
{{fun _ : unit => p --> VNat (1 + n)}}
    unfold inc; sep.p: ptr
n: nat
{{p --> VNat n}} v <- read_nat p; write p (VNat (S v))
{{fun _ : unit => p --> VNat (S n)}}
    eapply bind_tc; sep.p: ptr
n: nat
{{p --> VNat n}} read_nat p {{?Q1}}
p: ptr
n, x: nat
{{?Q1 x}} write p (VNat (S x))
{{fun _ : unit => p --> VNat (S n)}}
    -p: ptr
n: nat
{{p --> VNat n}} read_nat p {{?Q1}} apply (@read_nat_tc); sep.
    -p: ptr
n, x: nat
{{(fun x : nat => p --> VNat x ** pure (x = n)) x}} 
write p (VNat (S x))
{{fun _ : unit => p --> VNat (S n)}} simpl.p: ptr
n, x: nat
{{p --> VNat x ** pure (x = n)}} write p (VNat (S x))
{{fun _ : unit => p --> VNat (S n)}}
      eapply consequence_tc.p: ptr
n, x: nat
{{?P1}} write p (VNat (S x)) {{?Q1}}
p: ptr
n, x: nat
p --> VNat x ** pure (x = n) ==> ?P1
p: ptr
n, x: nat
forall x0 : unit, ?Q1 x0 ==> p --> VNat (S n)
      +p: ptr
n, x: nat
{{?P1}} write p (VNat (S x)) {{?Q1}} eapply (frame_tc (pure (x = n))).p: ptr
n, x: nat
{{?P}} write p (VNat (S x)) {{?Q}}
        eapply write_tc.
      +p: ptr
n, x: nat
p --> VNat x ** pure (x = n) ==>
p -->? ** pure (x = n) sep.
      +p: ptr
n, x: nat
forall x0 : unit,
(fun x1 : unit =>
 (fun _ : unit => p --> VNat (S x)) x1 ** pure (x = n))
  x0 ==> p --> VNat (S n) sep.
  Qed.

The great part is that now if we have a property on some disjoint part of the state, say p2 --> n2, then after calling inc, we are guaranteed that property is preserved via the frame rule.

  Definition inc_two (p1 p2 : ptr) (n1 : nat) (v2: value) :
    {{ p1 --> VNat n1 ** p2 --> v2 }}
    inc p1
    {{ fun _ => p1 --> VNat (1 + n1) ** p2 --> v2 }}.p1, p2: ptr
n1: nat
v2: value
{{p1 --> VNat n1 ** p2 --> v2}} inc p1
{{fun _ : unit => p1 --> VNat (1 + n1) ** p2 --> v2}}
  Proof.p1, p2: ptr
n1: nat
v2: value
{{p1 --> VNat n1 ** p2 --> v2}} inc p1
{{fun _ : unit => p1 --> VNat (1 + n1) ** p2 --> v2}}
    apply (frame_tc (p2 --> v2)).p1, p2: ptr
n1: nat
v2: value
{{p1 --> VNat n1}} inc p1
{{fun _ : unit => p1 --> VNat (1 + n1)}}
    apply inc_tc.
  Qed.

Here is a function to swap the contents of two pointers.

  Definition swap (p1 p2 : ptr) :=
    v1 <- read p1;
    v2 <- read p2;
    write p2 v1;;
    write p1 v2.

Alas, reasoning isn't quite as simple as we might hope. We have to not only put in the right uses of the frame and consequence rules, but we must also so a lot of commuting and re-associating to discharge the verification conditions. For Ynot, Adam Chlipala wrote an Ltac tactic that mostly took care of this sort of simple reasoning for us. And Gonthier et al. have done some nice work showing how to use type-classes or canonical-structures to automate a lot of this sort of thing. Below, we'll see you an alternative technique based on reflection.

   Lemma swap_tc (p1 p2 : ptr) (v1 v2 : value) :
    {{ p1 --> v1 ** p2 --> v2 }}
    swap p1 p2
    {{ fun _ => p1 --> v2 ** p2 --> v1 }}.p1, p2: ptr
v1, v2: value
{{p1 --> v1 ** p2 --> v2}} swap p1 p2
{{fun _ : unit => p1 --> v2 ** p2 --> v1}}
  Proof.p1, p2: ptr
v1, v2: value
{{p1 --> v1 ** p2 --> v2}} swap p1 p2
{{fun _ : unit => p1 --> v2 ** p2 --> v1}}
    unfold swap; sep.p1, p2: ptr
v1, v2: value
{{p1 --> v1 ** p2 --> v2}} v1 <- read p1;
                           v2 <- read p2;
                           write p2 v1;; write p1 v2
{{fun _ : unit => p1 --> v2 ** p2 --> v1}}
    eapply bind_tc; sep.p1, p2: ptr
v1, v2: value
{{p1 --> v1 ** p2 --> v2}} read p1 {{?Q1}}
p1, p2: ptr
v1, v2, x: value
{{?Q1 x}} v2 <- read p2; write p2 x;; write p1 v2
{{fun _ : unit => p1 --> v2 ** p2 --> v1}}
    -p1, p2: ptr
v1, v2: value
{{p1 --> v1 ** p2 --> v2}} read p1 {{?Q1}} eapply (frame_tc (p2 --> v2)).p1, p2: ptr
v1, v2: value
{{p1 --> v1}} read p1 {{?Q}}
      eapply read_tc.
    -p1, p2: ptr
v1, v2, x: value
{{(fun x : value =>
   (fun x0 : value => p1 --> x0 ** pure (x0 = v1)) x **
   p2 --> v2) x}} v2 <- read p2;
                  write p2 x;; write p1 v2
{{fun _ : unit => p1 --> v2 ** p2 --> v1}} sep.p1, p2: ptr
v1, v2, x: value
{{(p1 --> x ** pure (x = v1)) ** p2 --> v2}} v2 <-
                                             read p2;
                                             write p2
                                               x;;
                                             write p1
                                               v2
{{fun _ : unit => p1 --> v2 ** p2 --> v1}}
      eapply (consequence_tc
                ((p2 --> v2 ** p1 --> x) ** pure (x = v1))).p1, p2: ptr
v1, v2, x: value
{{(p2 --> v2 ** p1 --> x) ** pure (x = v1)}} v2 <-
                                             read p2;
                                             write p2
                                               x;;
                                             write p1
                                               v2
{{?Q1}}
p1, p2: ptr
v1, v2, x: value
(p1 --> x ** pure (x = v1)) ** p2 --> v2 ==>
(p2 --> v2 ** p1 --> x) ** pure (x = v1)
p1, p2: ptr
v1, v2, x: value
forall x0 : unit, ?Q1 x0 ==> p1 --> v2 ** p2 --> v1
      +p1, p2: ptr
v1, v2, x: value
{{(p2 --> v2 ** p1 --> x) ** pure (x = v1)}} v2 <-
                                             read p2;
                                             write p2
                                               x;;
                                             write p1
                                               v2
{{?Q1}} eapply (frame_tc (pure (x = v1))).p1, p2: ptr
v1, v2, x: value
{{p2 --> v2 ** p1 --> x}} v2 <- read p2;
                          write p2 x;; write p1 v2
{{?Q}}
        eapply bind_tc; sep.p1, p2: ptr
v1, v2, x: value
{{p2 --> v2 ** p1 --> x}} read p2 {{?Q1}}
p1, p2: ptr
v1, v2, x, x0: value
{{?Q1 x0}} write p2 x;; write p1 x0 {{?Q}}
        *p1, p2: ptr
v1, v2, x: value
{{p2 --> v2 ** p1 --> x}} read p2 {{?Q1}} eapply (frame_tc (p1 --> x)).p1, p2: ptr
v1, v2, x: value
{{p2 --> v2}} read p2 {{?Q0}}
          eapply read_tc; sep.
        *p1, p2: ptr
v1, v2, x, x0: value
{{(fun x0 : value =>
   (fun x : value => p2 --> x ** pure (x = v2)) x0 **
   p1 --> x) x0}} write p2 x;; write p1 x0 {{?Q}} simpl.p1, p2: ptr
v1, v2, x, x0: value
{{(p2 --> x0 ** pure (x0 = v2)) ** p1 --> x}} write p2
                                                x;;
                                              write p1
                                                x0
{{?Q}}
          eapply (consequence_tc
                    ((p2 -->? ** p1 --> x) ** pure (x0 = v2))).p1, p2: ptr
v1, v2, x, x0: value
{{(p2 -->? ** p1 --> x) ** pure (x0 = v2)}} write p2 x;;
                                            write p1
                                              x0
{{?Q1}}
p1, p2: ptr
v1, v2, x, x0: value
(p2 --> x0 ** pure (x0 = v2)) ** p1 --> x ==>
(p2 -->? ** p1 --> x) ** pure (x0 = v2)
p1, p2: ptr
v1, v2, x, x0: value
forall x1 : unit, ?Q1 x1 ==> ?Q x1
          --p1, p2: ptr
v1, v2, x, x0: value
{{(p2 -->? ** p1 --> x) ** pure (x0 = v2)}} write p2 x;;
                                            write p1
                                              x0
{{?Q1}} eapply (frame_tc (pure (x0 = v2))).p1, p2: ptr
v1, v2, x, x0: value
{{p2 -->? ** p1 --> x}} write p2 x;; write p1 x0
{{?Q0}}
             eapply bind_tc; sep.p1, p2: ptr
v1, v2, x, x0: value
{{p2 -->? ** p1 --> x}} write p2 x {{?Q1}}
p1, p2: ptr
v1, v2, x, x0: value
x1: unit
{{?Q1 x1}} write p1 x0 {{?Q0}}
             ++p1, p2: ptr
v1, v2, x, x0: value
{{p2 -->? ** p1 --> x}} write p2 x {{?Q1}} eapply (frame_tc (p1 --> x)).p1, p2: ptr
v1, v2, x, x0: value
{{p2 -->?}} write p2 x {{?Q1}}
                eapply write_tc; sep.
             ++p1, p2: ptr
v1, v2, x, x0: value
x1: unit
{{(fun x0 : unit =>
   (fun _ : unit => p2 --> x) x0 ** p1 --> x) x1}} 
write p1 x0 {{?Q0}} sep.p1, p2: ptr
v1, v2, x, x0: value
x1: unit
{{p2 --> x ** p1 --> x}} write p1 x0 {{?Q0}}
                eapply (consequence_tc (p1 -->? ** p2 --> x)).p1, p2: ptr
v1, v2, x, x0: value
x1: unit
{{p1 -->? ** p2 --> x}} write p1 x0 {{?Q1}}
p1, p2: ptr
v1, v2, x, x0: value
x1: unit
p2 --> x ** p1 --> x ==> p1 -->? ** p2 --> x
p1, p2: ptr
v1, v2, x, x0: value
x1: unit
forall x2 : unit, ?Q1 x2 ==> ?Q0 x2
                **p1, p2: ptr
v1, v2, x, x0: value
x1: unit
{{p1 -->? ** p2 --> x}} write p1 x0 {{?Q1}} eapply (frame_tc (p2 --> x)).p1, p2: ptr
v1, v2, x, x0: value
x1: unit
{{p1 -->?}} write p1 x0 {{?Q1}}
                   eapply write_tc; sep.
                **p1, p2: ptr
v1, v2, x, x0: value
x1: unit
p2 --> x ** p1 --> x ==> p1 -->? ** p2 --> x apply hyp_comm.p1, p2: ptr
v1, v2, x, x0: value
x1: unit
p1 --> x ** p2 --> x ==> p1 -->? ** p2 --> x
                   sep.
                **p1, p2: ptr
v1, v2, x, x0: value
x1: unit
forall x1 : unit,
(fun x2 : unit =>
 (fun _ : unit => p1 --> x0) x2 ** p2 --> x) x1 ==>
?Q0 x1 sep.p1, p2: ptr
v1, v2, x, x0: value
x1, x2: unit
p1 --> x0 ** p2 --> x ==> ?Q0 x2
                   eapply himp_id.
          --p1, p2: ptr
v1, v2, x, x0: value
(p2 --> x0 ** pure (x0 = v2)) ** p1 --> x ==>
(p2 -->? ** p1 --> x) ** pure (x0 = v2) sep.p1, p2: ptr
v1, v2, x, x0: value
p2 --> x0 ** pure (x0 = v2) ** p1 --> x ==>
p2 -->? ** p1 --> x ** pure (x0 = v2)
             eapply himp_split; sep.
          --p1, p2: ptr
v1, v2, x, x0: value
forall x1 : unit,
(fun x2 : unit =>
 (fun _ : unit => p1 --> x0 ** p2 --> x) x2 **
 pure (x0 = v2)) x1 ==> ?Q x1 sep.p1, p2: ptr
v1, v2, x: value
x1: unit
p1 --> v2 ** p2 --> x ==> ?Q x1
             eapply himp_id.
      +p1, p2: ptr
v1, v2, x: value
(p1 --> x ** pure (x = v1)) ** p2 --> v2 ==>
(p2 --> v2 ** p1 --> x) ** pure (x = v1) eapply hyp_comm.p1, p2: ptr
v1, v2, x: value
p2 --> v2 ** p1 --> x ** pure (x = v1) ==>
(p2 --> v2 ** p1 --> x) ** pure (x = v1)
        sep.
      +p1, p2: ptr
v1, v2, x: value
forall x0 : unit,
(fun x1 : unit =>
 (fun _ : unit => p1 --> v2 ** p2 --> x) x1 **
 pure (x = v1)) x0 ==> p1 --> v2 ** p2 --> v1 sep.
  Qed.

Reflection and a Simple, Correct Semi-Decision Procedure

Our goal will be to build a Coq function that can simplify a separation implication P ==> Q and prove that function correct. One simple strategy is to flatten out all of the stars and cross off all of the simple predicates that appear in both P and Q.

But of course, we can't just crawl over an hprop because in general, these are functions! So our trick is to write down some syntax that represents a particular predicate, and then give an interpretation that maps that syntax back to our real predicate. Then we can compute with the syntax.

The Quote library should help us with this, but alas, it's not as clever as we might hope it would be...

  Definition hprop_name := nat.
  Definition hprop_map := list (hprop_name * hprop).
  Definition hprop_name_eq := PeanoNat.Nat.eq_dec.

We begin by giving a basic syntax for predicates. Atom will be used to represent things like abstract predicates (e.g., a variable P) or a points-to-predicate etc. We'll use an environment to map hprop_names to the real hprop.

  Inductive Hprop : Set :=
  | Emp : Hprop
  | Atom : hprop_name -> Hprop
  | Star : Hprop -> Hprop -> Hprop.

  Infix "#" := Star (right associativity, at level 80) : sep_scope.

  Fixpoint lookup_hprop (n : hprop_name) (hp : hprop_map) :=
    match hp with
    | nil => (pure False)
    | (m, P) :: rest =>
        if hprop_name_eq n m then P else lookup_hprop n rest
    end.

  Section HINTERP.

We'll assume we have an hprop_map lying around.

    Variable hmap : hprop_map.

Now we given an interpretation to the syntax for predicates:

    Fixpoint hinterp (hp : Hprop) : hprop :=
      match hp with
      | Emp => emp
      | Atom n => lookup_hprop n hmap
      | Star h1 h2 => star (hinterp h1) (hinterp h2)
      end.

We can flatten a predicate into a list of hprop_names.

    Fixpoint flatten (hp : Hprop) : list hprop_name :=
      match hp with
      | Emp => nil
      | Atom n => n :: nil
      | Star h1 h2 => (flatten h1) ++ (flatten h2)
      end.

This function removes exactly one copy of the hprop_name n from the input list, returning None if we fail to find a copy of n.

    Fixpoint remove_one (n : hprop_name) (hps : list hprop_name)
      : option (list hprop_name) :=
      match hps with
      | nil => None
      | m :: rest =>
          if hprop_name_eq n m then Some rest else
            match remove_one n rest with
            | None => None
            | Some hps' => Some (m :: hps')
            end
      end.

This is the heart of our simplification algorithm. Here, we are running through the list of names hp1, trying to cross off each one that occurs in hp2. If the current name doesn't occur, we add it to the end of hp0 so that we can keep track of it. That is, our invariant at each step should be that hp0 ** hp1 ==> hp2 once we map the lists back to hprops.

    Fixpoint simplify (hp0 hp1 hp2 : list hprop_name) :=
      match hp1 with
      | nil => (hp0, hp2)
      | n :: hp1' =>
          match remove_one n hp2 with
          | Some hp2' => simplify hp0 hp1' hp2'
          | None => simplify (hp0 ++ n :: nil) hp1' hp2
          end
      end.

Convert a list of names back into an Hprop.

    Definition collapse :=
      List.fold_right (fun n p => Star (Atom n) p) Emp.

Convert a list of names into an hprop.

    Definition interp_list :=
      List.fold_right (fun n p => (lookup_hprop n hmap) ** p) emp.

Our cross-off algorithm takes two Hprops, flattens them into lists of names, simplifies the two lists by crossing off common names, and then returns the two Hprop's we get by collapsing the resulting simplified lists.

    Definition cross_off (hp1 hp2 : Hprop) : Hprop * Hprop :=
      let (hp1', hp2') :=
        simplify nil (flatten hp1) (flatten hp2) in
      (collapse hp1', collapse hp2').

    Lemma collapse_interp hp :
      hinterp (collapse hp) = interp_list hp.hmap: hprop_map
hp: list hprop_name
hinterp (collapse hp) = interp_list hp
    Proof.hmap: hprop_map
hp: list hprop_name
hinterp (collapse hp) = interp_list hp
      induction hp; mysimpl.hmap: hprop_map
a: hprop_name
hp: list hprop_name
IHhp: hinterp (collapse hp) = interp_list hp
(lookup_hprop a hmap ** hinterp (collapse hp)) =
(lookup_hprop a hmap ** interp_list hp)
      rewrite IHhp.hmap: hprop_map
a: hprop_name
hp: list hprop_name
IHhp: hinterp (collapse hp) = interp_list hp
(lookup_hprop a hmap ** interp_list hp) =
(lookup_hprop a hmap ** interp_list hp)
      auto.
    Qed.

The following are various lemmas needed to reason about the interpretation of the syntax.

    Lemma interp_list_app hp1 hp2 :
      interp_list (hp1 ++ hp2) ==>
        ((interp_list hp1) ** (interp_list hp2)).hmap: hprop_map
hp1, hp2: list hprop_name
interp_list (hp1 ++ hp2) ==>
interp_list hp1 ** interp_list hp2
    Proof.hmap: hprop_map
hp1, hp2: list hprop_name
interp_list (hp1 ++ hp2) ==>
interp_list hp1 ** interp_list hp2
      induction hp1; simpl; intros.hmap: hprop_map
hp2: list hprop_name
interp_list hp2 ==> emp ** interp_list hp2
hmap: hprop_map
a: hprop_name
hp1, hp2: list hprop_name
IHhp1: interp_list (hp1 ++ hp2) ==>
interp_list hp1 ** interp_list hp2
lookup_hprop a hmap ** interp_list (hp1 ++ hp2) ==>
(lookup_hprop a hmap ** interp_list hp1) **
interp_list hp2
      -hmap: hprop_map
hp2: list hprop_name
interp_list hp2 ==> emp ** interp_list hp2 apply comm_conc.hmap: hprop_map
hp2: list hprop_name
interp_list hp2 ==> interp_list hp2 ** emp
        apply conc_emp.hmap: hprop_map
hp2: list hprop_name
interp_list hp2 ==> interp_list hp2
        auto with sep_db.
      -hmap: hprop_map
a: hprop_name
hp1, hp2: list hprop_name
IHhp1: interp_list (hp1 ++ hp2) ==>
interp_list hp1 ** interp_list hp2
lookup_hprop a hmap ** interp_list (hp1 ++ hp2) ==>
(lookup_hprop a hmap ** interp_list hp1) **
interp_list hp2 sep.
    Qed.

    Lemma app_interp_list hp1 hp2 :
      ((interp_list hp1) ** (interp_list hp2)) ==>
        interp_list (hp1 ++ hp2).hmap: hprop_map
hp1, hp2: list hprop_name
interp_list hp1 ** interp_list hp2 ==>
interp_list (hp1 ++ hp2)
    Proof.hmap: hprop_map
hp1, hp2: list hprop_name
interp_list hp1 ** interp_list hp2 ==>
interp_list (hp1 ++ hp2)
      induction hp1; simpl; intros.hmap: hprop_map
hp2: list hprop_name
emp ** interp_list hp2 ==> interp_list hp2
hmap: hprop_map
a: hprop_name
hp1, hp2: list hprop_name
IHhp1: interp_list hp1 ** interp_list hp2 ==>
interp_list (hp1 ++ hp2)
(lookup_hprop a hmap ** interp_list hp1) **
interp_list hp2 ==>
lookup_hprop a hmap ** interp_list (hp1 ++ hp2)
      -hmap: hprop_map
hp2: list hprop_name
emp ** interp_list hp2 ==> interp_list hp2 apply hyp_emp.hmap: hprop_map
hp2: list hprop_name
interp_list hp2 ==> interp_list hp2 sep.
      -hmap: hprop_map
a: hprop_name
hp1, hp2: list hprop_name
IHhp1: interp_list hp1 ** interp_list hp2 ==>
interp_list (hp1 ++ hp2)
(lookup_hprop a hmap ** interp_list hp1) **
interp_list hp2 ==>
lookup_hprop a hmap ** interp_list (hp1 ++ hp2) sep.
    Qed.

    Lemma hinterp_flatten hp :
      hinterp hp ==> interp_list (flatten hp).hmap: hprop_map
hp: Hprop
hinterp hp ==> interp_list (flatten hp)
    Proof.hmap: hprop_map
hp: Hprop
hinterp hp ==> interp_list (flatten hp)
      induction hp; simpl.hmap: hprop_map
emp ==> emp
hmap: hprop_map
h: hprop_name
lookup_hprop h hmap ==> lookup_hprop h hmap ** emp
hmap: hprop_map
hp1, hp2: Hprop
IHhp1: hinterp hp1 ==> interp_list (flatten hp1)
IHhp2: hinterp hp2 ==> interp_list (flatten hp2)
hinterp hp1 ** hinterp hp2 ==>
interp_list (flatten hp1 ++ flatten hp2)
      -hmap: hprop_map
emp ==> emp sep.
      -hmap: hprop_map
h: hprop_name
lookup_hprop h hmap ==> lookup_hprop h hmap ** emp apply conc_emp.hmap: hprop_map
h: hprop_name
lookup_hprop h hmap ==> lookup_hprop h hmap sep.
      -hmap: hprop_map
hp1, hp2: Hprop
IHhp1: hinterp hp1 ==> interp_list (flatten hp1)
IHhp2: hinterp hp2 ==> interp_list (flatten hp2)
hinterp hp1 ** hinterp hp2 ==>
interp_list (flatten hp1 ++ flatten hp2) eapply himp_mp.hmap: hprop_map
hp1, hp2: Hprop
IHhp1: hinterp hp1 ==> interp_list (flatten hp1)
IHhp2: hinterp hp2 ==> interp_list (flatten hp2)
?Q ==> interp_list (flatten hp1 ++ flatten hp2)
hmap: hprop_map
hp1, hp2: Hprop
IHhp1: hinterp hp1 ==> interp_list (flatten hp1)
IHhp2: hinterp hp2 ==> interp_list (flatten hp2)
hinterp hp1 ** hinterp hp2 ==> ?Q
        +hmap: hprop_map
hp1, hp2: Hprop
IHhp1: hinterp hp1 ==> interp_list (flatten hp1)
IHhp2: hinterp hp2 ==> interp_list (flatten hp2)
?Q ==> interp_list (flatten hp1 ++ flatten hp2) eapply app_interp_list.
        +hmap: hprop_map
hp1, hp2: Hprop
IHhp1: hinterp hp1 ==> interp_list (flatten hp1)
IHhp2: hinterp hp2 ==> interp_list (flatten hp2)
hinterp hp1 ** hinterp hp2 ==>
interp_list (flatten hp1) ** interp_list (flatten hp2) eapply himp_split; eauto.
    Qed.

    Lemma remove_one_splits n hp:
      match remove_one n hp with
      | Some hp' => exists hp1, exists hp2,
            hp = hp1 ++ n :: hp2 /\ hp' = hp1 ++ hp2
      | None => True
      end.hmap: hprop_map
n: hprop_name
hp: list hprop_name
match remove_one n hp with
| Some hp' =>
    exists hp1 hp2 : list hprop_name,
      hp = hp1 ++ n :: hp2 /\ hp' = hp1 ++ hp2
| None => True
end
    Proof.hmap: hprop_map
n: hprop_name
hp: list hprop_name
match remove_one n hp with
| Some hp' =>
    exists hp1 hp2 : list hprop_name,
      hp = hp1 ++ n :: hp2 /\ hp' = hp1 ++ hp2
| None => True
end
      induction hp; mysimpl.hmap: hprop_map
n, a: hprop_name
hp: list hprop_name
IHhp: match remove_one n hp with
| Some hp' =>
    exists hp1 hp2 : list hprop_name,
      hp = hp1 ++ n :: hp2 /\ hp' = hp1 ++ hp2
| None => True
end
match
  (if hprop_name_eq n a
   then Some hp
   else
    match remove_one n hp with
    | Some hps' => Some (a :: hps')
    | None => None
    end)
with
| Some hp' =>
    exists hp1 hp2 : list hprop_name,
      a :: hp = hp1 ++ n :: hp2 /\ hp' = hp1 ++ hp2
| None => True
end
      destruct hprop_name_eq.hmap: hprop_map
n, a: hprop_name
hp: list hprop_name
IHhp: match remove_one n hp with
| Some hp' =>
    exists hp1 hp2 : list hprop_name,
      hp = hp1 ++ n :: hp2 /\ hp' = hp1 ++ hp2
| None => True
end
e: n = a
exists hp1 hp2 : list hprop_name,
  a :: hp = hp1 ++ n :: hp2 /\ hp = hp1 ++ hp2
hmap: hprop_map
n, a: hprop_name
hp: list hprop_name
IHhp: match remove_one n hp with
| Some hp' =>
    exists hp1 hp2 : list hprop_name,
      hp = hp1 ++ n :: hp2 /\ hp' = hp1 ++ hp2
| None => True
end
n0: n <> a
match
  match remove_one n hp with
  | Some hps' => Some (a :: hps')
  | None => None
  end
with
| Some hp' =>
    exists hp1 hp2 : list hprop_name,
      a :: hp = hp1 ++ n :: hp2 /\ hp' = hp1 ++ hp2
| None => True
end
      -hmap: hprop_map
n, a: hprop_name
hp: list hprop_name
IHhp: match remove_one n hp with
| Some hp' =>
    exists hp1 hp2 : list hprop_name,
      hp = hp1 ++ n :: hp2 /\ hp' = hp1 ++ hp2
| None => True
end
e: n = a
exists hp1 hp2 : list hprop_name,
  a :: hp = hp1 ++ n :: hp2 /\ hp = hp1 ++ hp2 subst.hmap: hprop_map
a: hprop_name
hp: list hprop_name
IHhp: match remove_one a hp with
| Some hp' =>
    exists hp1 hp2 : list hprop_name,
      hp = hp1 ++ a :: hp2 /\ hp' = hp1 ++ hp2
| None => True
end
exists hp1 hp2 : list hprop_name,
  a :: hp = hp1 ++ a :: hp2 /\ hp = hp1 ++ hp2
        exists nil, hp.hmap: hprop_map
a: hprop_name
hp: list hprop_name
IHhp: match remove_one a hp with
| Some hp' =>
    exists hp1 hp2 : list hprop_name,
      hp = hp1 ++ a :: hp2 /\ hp' = hp1 ++ hp2
| None => True
end
a :: hp = nil ++ a :: hp /\ hp = nil ++ hp
        mysimpl.
      -hmap: hprop_map
n, a: hprop_name
hp: list hprop_name
IHhp: match remove_one n hp with
| Some hp' =>
    exists hp1 hp2 : list hprop_name,
      hp = hp1 ++ n :: hp2 /\ hp' = hp1 ++ hp2
| None => True
end
n0: n <> a
match
  match remove_one n hp with
  | Some hps' => Some (a :: hps')
  | None => None
  end
with
| Some hp' =>
    exists hp1 hp2 : list hprop_name,
      a :: hp = hp1 ++ n :: hp2 /\ hp' = hp1 ++ hp2
| None => True
end destruct remove_one; mysimpl.hmap: hprop_map
n, a: hprop_name
hp, l, x, x0: list hprop_name
H: hp = x ++ n :: x0
H0: l = x ++ x0
n0: n <> a
exists hp1 hp2 : list hprop_name,
  a :: hp = hp1 ++ n :: hp2 /\ a :: l = hp1 ++ hp2
        subst.hmap: hprop_map
n, a: hprop_name
x, x0: list hprop_name
n0: n <> a
exists hp1 hp2 : list hprop_name,
  a :: x ++ n :: x0 = hp1 ++ n :: hp2 /\
  a :: x ++ x0 = hp1 ++ hp2
        exists (a :: x), x0.hmap: hprop_map
n, a: hprop_name
x, x0: list hprop_name
n0: n <> a
a :: x ++ n :: x0 = (a :: x) ++ n :: x0 /\
a :: x ++ x0 = (a :: x) ++ x0
        mysimpl.
    Qed.

    Lemma interp_list_comm x1 x2 :
      interp_list (x1 ++ x2) ==> interp_list (x2 ++ x1).hmap: hprop_map
x1, x2: list hprop_name
interp_list (x1 ++ x2) ==> interp_list (x2 ++ x1)
    Proof.hmap: hprop_map
x1, x2: list hprop_name
interp_list (x1 ++ x2) ==> interp_list (x2 ++ x1)
      induction x1; simpl; intros.hmap: hprop_map
x2: list hprop_name
interp_list x2 ==> interp_list (x2 ++ nil)
hmap: hprop_map
a: hprop_name
x1, x2: list hprop_name
IHx1: interp_list (x1 ++ x2) ==>
interp_list (x2 ++ x1)
lookup_hprop a hmap ** interp_list (x1 ++ x2) ==>
interp_list (x2 ++ a :: x1)
      -hmap: hprop_map
x2: list hprop_name
interp_list x2 ==> interp_list (x2 ++ nil) rewrite app_nil_r.hmap: hprop_map
x2: list hprop_name
interp_list x2 ==> interp_list x2 sep.
      -hmap: hprop_map
a: hprop_name
x1, x2: list hprop_name
IHx1: interp_list (x1 ++ x2) ==>
interp_list (x2 ++ x1)
lookup_hprop a hmap ** interp_list (x1 ++ x2) ==>
interp_list (x2 ++ a :: x1) eapply himp_mp.hmap: hprop_map
a: hprop_name
x1, x2: list hprop_name
IHx1: interp_list (x1 ++ x2) ==>
interp_list (x2 ++ x1)
?Q ==> interp_list (x2 ++ a :: x1)
hmap: hprop_map
a: hprop_name
x1, x2: list hprop_name
IHx1: interp_list (x1 ++ x2) ==>
interp_list (x2 ++ x1)
lookup_hprop a hmap ** interp_list (x1 ++ x2) ==> ?Q
        +hmap: hprop_map
a: hprop_name
x1, x2: list hprop_name
IHx1: interp_list (x1 ++ x2) ==>
interp_list (x2 ++ x1)
?Q ==> interp_list (x2 ++ a :: x1) eapply app_interp_list.
        +hmap: hprop_map
a: hprop_name
x1, x2: list hprop_name
IHx1: interp_list (x1 ++ x2) ==>
interp_list (x2 ++ x1)
lookup_hprop a hmap ** interp_list (x1 ++ x2) ==>
interp_list x2 ** interp_list (a :: x1) eapply comm_conc.hmap: hprop_map
a: hprop_name
x1, x2: list hprop_name
IHx1: interp_list (x1 ++ x2) ==>
interp_list (x2 ++ x1)
lookup_hprop a hmap ** interp_list (x1 ++ x2) ==>
interp_list (a :: x1) ** interp_list x2
          simpl.hmap: hprop_map
a: hprop_name
x1, x2: list hprop_name
IHx1: interp_list (x1 ++ x2) ==>
interp_list (x2 ++ x1)
lookup_hprop a hmap ** interp_list (x1 ++ x2) ==>
(lookup_hprop a hmap ** interp_list x1) **
interp_list x2 sep.hmap: hprop_map
a: hprop_name
x1, x2: list hprop_name
IHx1: interp_list (x1 ++ x2) ==>
interp_list (x2 ++ x1)
interp_list (x1 ++ x2) ==>
interp_list x1 ** interp_list x2
          apply interp_list_app.
    Qed.

    Lemma himp_remove_one n hp1 hp2 :
      match remove_one n hp1, remove_one n hp2 with
      | Some hp1', Some hp2' =>
          (interp_list hp1' ==> interp_list hp2') ->
          interp_list hp1 ==> interp_list hp2
      | _, _ => True
      end.hmap: hprop_map
n: hprop_name
hp1, hp2: list hprop_name
match remove_one n hp1 with
| Some hp1' =>
    match remove_one n hp2 with
    | Some hp2' =>
        interp_list hp1' ==> interp_list hp2' ->
        interp_list hp1 ==> interp_list hp2
    | None => True
    end
| None => True
end
    Proof.hmap: hprop_map
n: hprop_name
hp1, hp2: list hprop_name
match remove_one n hp1 with
| Some hp1' =>
    match remove_one n hp2 with
    | Some hp2' =>
        interp_list hp1' ==> interp_list hp2' ->
        interp_list hp1 ==> interp_list hp2
    | None => True
    end
| None => True
end
      intros.hmap: hprop_map
n: hprop_name
hp1, hp2: list hprop_name
match remove_one n hp1 with
| Some hp1' =>
    match remove_one n hp2 with
    | Some hp2' =>
        interp_list hp1' ==> interp_list hp2' ->
        interp_list hp1 ==> interp_list hp2
    | None => True
    end
| None => True
end
      generalize (remove_one_splits n hp1).hmap: hprop_map
n: hprop_name
hp1, hp2: list hprop_name
match remove_one n hp1 with
| Some hp' =>
    exists hp2 hp3 : list hprop_name,
      hp1 = hp2 ++ n :: hp3 /\ hp' = hp2 ++ hp3
| None => True
end ->
match remove_one n hp1 with
| Some hp1' =>
    match remove_one n hp2 with
    | Some hp2' =>
        interp_list hp1' ==> interp_list hp2' ->
        interp_list hp1 ==> interp_list hp2
    | None => True
    end
| None => True
end
      generalize (remove_one_splits n hp2).hmap: hprop_map
n: hprop_name
hp1, hp2: list hprop_name
match remove_one n hp2 with
| Some hp' =>
    exists hp1 hp3 : list hprop_name,
      hp2 = hp1 ++ n :: hp3 /\ hp' = hp1 ++ hp3
| None => True
end ->
match remove_one n hp1 with
| Some hp' =>
    exists hp2 hp3 : list hprop_name,
      hp1 = hp2 ++ n :: hp3 /\ hp' = hp2 ++ hp3
| None => True
end ->
match remove_one n hp1 with
| Some hp1' =>
    match remove_one n hp2 with
    | Some hp2' =>
        interp_list hp1' ==> interp_list hp2' ->
        interp_list hp1 ==> interp_list hp2
    | None => True
    end
| None => True
end
      destruct (remove_one n hp1); auto.hmap: hprop_map
n: hprop_name
hp1, hp2, l: list hprop_name
match remove_one n hp2 with
| Some hp' =>
    exists hp1 hp3 : list hprop_name,
      hp2 = hp1 ++ n :: hp3 /\ hp' = hp1 ++ hp3
| None => True
end ->
(exists hp2 hp3 : list hprop_name,
   hp1 = hp2 ++ n :: hp3 /\ l = hp2 ++ hp3) ->
match remove_one n hp2 with
| Some hp2' =>
    interp_list l ==> interp_list hp2' ->
    interp_list hp1 ==> interp_list hp2
| None => True
end
      destruct (remove_one n hp2); auto.hmap: hprop_map
n: hprop_name
hp1, hp2, l, l0: list hprop_name
(exists hp1 hp3 : list hprop_name,
   hp2 = hp1 ++ n :: hp3 /\ l0 = hp1 ++ hp3) ->
(exists hp2 hp3 : list hprop_name,
   hp1 = hp2 ++ n :: hp3 /\ l = hp2 ++ hp3) ->
interp_list l ==> interp_list l0 ->
interp_list hp1 ==> interp_list hp2
      mysimpl.hmap: hprop_map
n: hprop_name
hp1, hp2, l, l0, x1, x2: list hprop_name
H: hp2 = x1 ++ n :: x2
H3: l0 = x1 ++ x2
x, x0: list hprop_name
H0: hp1 = x ++ n :: x0
H2: l = x ++ x0
H1: interp_list l ==> interp_list l0
interp_list hp1 ==> interp_list hp2 subst.hmap: hprop_map
n: hprop_name
x1, x2, x, x0: list hprop_name
H1: interp_list (x ++ x0) ==> interp_list (x1 ++ x2)
interp_list (x ++ n :: x0) ==>
interp_list (x1 ++ n :: x2)
      eapply himp_mp.hmap: hprop_map
n: hprop_name
x1, x2, x, x0: list hprop_name
H1: interp_list (x ++ x0) ==> interp_list (x1 ++ x2)
?Q ==> interp_list (x1 ++ n :: x2)
hmap: hprop_map
n: hprop_name
x1, x2, x, x0: list hprop_name
H1: interp_list (x ++ x0) ==> interp_list (x1 ++ x2)
interp_list (x ++ n :: x0) ==> ?Q
      -hmap: hprop_map
n: hprop_name
x1, x2, x, x0: list hprop_name
H1: interp_list (x ++ x0) ==> interp_list (x1 ++ x2)
?Q ==> interp_list (x1 ++ n :: x2) eapply interp_list_comm.
      -hmap: hprop_map
n: hprop_name
x1, x2, x, x0: list hprop_name
H1: interp_list (x ++ x0) ==> interp_list (x1 ++ x2)
interp_list (x ++ n :: x0) ==>
interp_list ((n :: x2) ++ x1) sep.hmap: hprop_map
n: hprop_name
x1, x2, x, x0: list hprop_name
H1: interp_list (x ++ x0) ==> interp_list (x1 ++ x2)
interp_list (x ++ n :: x0) ==>
lookup_hprop n hmap ** interp_list (x2 ++ x1)
        eapply (@himp_mp (interp_list ((n :: x0) ++ x)));
          try apply interp_list_comm.hmap: hprop_map
n: hprop_name
x1, x2, x, x0: list hprop_name
H1: interp_list (x ++ x0) ==> interp_list (x1 ++ x2)
interp_list ((n :: x0) ++ x) ==>
lookup_hprop n hmap ** interp_list (x2 ++ x1)
        sep.hmap: hprop_map
n: hprop_name
x1, x2, x, x0: list hprop_name
H1: interp_list (x ++ x0) ==> interp_list (x1 ++ x2)
interp_list (x0 ++ x) ==> interp_list (x2 ++ x1)
        eapply himp_mp.hmap: hprop_map
n: hprop_name
x1, x2, x, x0: list hprop_name
H1: interp_list (x ++ x0) ==> interp_list (x1 ++ x2)
?Q ==> interp_list (x2 ++ x1)
hmap: hprop_map
n: hprop_name
x1, x2, x, x0: list hprop_name
H1: interp_list (x ++ x0) ==> interp_list (x1 ++ x2)
interp_list (x0 ++ x) ==> ?Q
        apply interp_list_comm.hmap: hprop_map
n: hprop_name
x1, x2, x, x0: list hprop_name
H1: interp_list (x ++ x0) ==> interp_list (x1 ++ x2)
interp_list (x0 ++ x) ==> interp_list (x1 ++ x2)
        eapply (@himp_mp (interp_list (x ++ x0))).hmap: hprop_map
n: hprop_name
x1, x2, x, x0: list hprop_name
H1: interp_list (x ++ x0) ==> interp_list (x1 ++ x2)
interp_list (x ++ x0) ==> interp_list (x1 ++ x2)
hmap: hprop_map
n: hprop_name
x1, x2, x, x0: list hprop_name
H1: interp_list (x ++ x0) ==> interp_list (x1 ++ x2)
interp_list (x0 ++ x) ==> interp_list (x ++ x0)
        +hmap: hprop_map
n: hprop_name
x1, x2, x, x0: list hprop_name
H1: interp_list (x ++ x0) ==> interp_list (x1 ++ x2)
interp_list (x ++ x0) ==> interp_list (x1 ++ x2) auto.
        +hmap: hprop_map
n: hprop_name
x1, x2, x, x0: list hprop_name
H1: interp_list (x ++ x0) ==> interp_list (x1 ++ x2)
interp_list (x0 ++ x) ==> interp_list (x ++ x0) apply interp_list_comm.
    Qed.

    Lemma himp_simp n hp1 hp2 :
      match remove_one n hp2 with
      | Some hp2' =>
          (interp_list hp1 ==> interp_list hp2') ->
          (interp_list (n :: hp1) ==> interp_list hp2)
      | None => True
      end.hmap: hprop_map
n: hprop_name
hp1, hp2: list hprop_name
match remove_one n hp2 with
| Some hp2' =>
    interp_list hp1 ==> interp_list hp2' ->
    interp_list (n :: hp1) ==> interp_list hp2
| None => True
end
    Proof.hmap: hprop_map
n: hprop_name
hp1, hp2: list hprop_name
match remove_one n hp2 with
| Some hp2' =>
    interp_list hp1 ==> interp_list hp2' ->
    interp_list (n :: hp1) ==> interp_list hp2
| None => True
end
      intros.hmap: hprop_map
n: hprop_name
hp1, hp2: list hprop_name
match remove_one n hp2 with
| Some hp2' =>
    interp_list hp1 ==> interp_list hp2' ->
    interp_list (n :: hp1) ==> interp_list hp2
| None => True
end
      pose proof (himp_remove_one n (n :: hp1) hp2).hmap: hprop_map
n: hprop_name
hp1, hp2: list hprop_name
H: match remove_one n (n :: hp1) with
| Some hp1' =>
    match remove_one n hp2 with
    | Some hp2' =>
        interp_list hp1' ==> interp_list hp2' ->
        interp_list (n :: hp1) ==> interp_list hp2
    | None => True
    end
| None => True
end
match remove_one n hp2 with
| Some hp2' =>
    interp_list hp1 ==> interp_list hp2' ->
    interp_list (n :: hp1) ==> interp_list hp2
| None => True
end
      simpl in *.hmap: hprop_map
n: hprop_name
hp1, hp2: list hprop_name
H: match
  (if hprop_name_eq n n
   then Some hp1
   else
    match remove_one n hp1 with
    | Some hps' => Some (n :: hps')
    | None => None
    end)
with
| Some hp1' =>
    match remove_one n hp2 with
    | Some hp2' =>
        interp_list hp1' ==> interp_list hp2' ->
        lookup_hprop n hmap ** interp_list hp1 ==>
        interp_list hp2
    | None => True
    end
| None => True
end
match remove_one n hp2 with
| Some hp2' =>
    interp_list hp1 ==> interp_list hp2' ->
    lookup_hprop n hmap ** interp_list hp1 ==>
    interp_list hp2
| None => True
end
      destruct hprop_name_eq; mysimpl.
    Qed.

This is the key invariant for our simplify routine.

    Lemma simplify_corr :
      forall hp1 hp0 hp2,
        interp_list (fst (simplify hp0 hp1 hp2)) ==>
        interp_list (snd (simplify hp0 hp1 hp2)) ->
        interp_list (hp0 ++ hp1) ==> interp_list hp2.hmap: hprop_map
forall hp1 hp0 hp2 : list hprop_name,
interp_list (fst (simplify hp0 hp1 hp2)) ==>
interp_list (snd (simplify hp0 hp1 hp2)) ->
interp_list (hp0 ++ hp1) ==> interp_list hp2
    Proof.hmap: hprop_map
forall hp1 hp0 hp2 : list hprop_name,
interp_list (fst (simplify hp0 hp1 hp2)) ==>
interp_list (snd (simplify hp0 hp1 hp2)) ->
interp_list (hp0 ++ hp1) ==> interp_list hp2
      induction hp1; simpl; intros.hmap: hprop_map
hp0, hp2: list hprop_name
H: interp_list hp0 ==> interp_list hp2
interp_list (hp0 ++ nil) ==> interp_list hp2
hmap: hprop_map
a: hprop_name
hp1: list hprop_name
IHhp1: forall hp0 hp2 : list hprop_name,
interp_list (fst (simplify hp0 hp1 hp2)) ==>
interp_list (snd (simplify hp0 hp1 hp2)) ->
interp_list (hp0 ++ hp1) ==> interp_list hp2
hp0, hp2: list hprop_name
H: interp_list
  (fst
     match remove_one a hp2 with
     | Some hp2' => simplify hp0 hp1 hp2'
     | None => simplify (hp0 ++ a :: nil) hp1 hp2
     end) ==>
interp_list
  (snd
     match remove_one a hp2 with
     | Some hp2' => simplify hp0 hp1 hp2'
     | None => simplify (hp0 ++ a :: nil) hp1 hp2
     end)
interp_list (hp0 ++ a :: hp1) ==> interp_list hp2
      -hmap: hprop_map
hp0, hp2: list hprop_name
H: interp_list hp0 ==> interp_list hp2
interp_list (hp0 ++ nil) ==> interp_list hp2 rewrite app_nil_r.hmap: hprop_map
hp0, hp2: list hprop_name
H: interp_list hp0 ==> interp_list hp2
interp_list hp0 ==> interp_list hp2 auto.
      -hmap: hprop_map
a: hprop_name
hp1: list hprop_name
IHhp1: forall hp0 hp2 : list hprop_name,
interp_list (fst (simplify hp0 hp1 hp2)) ==>
interp_list (snd (simplify hp0 hp1 hp2)) ->
interp_list (hp0 ++ hp1) ==> interp_list hp2
hp0, hp2: list hprop_name
H: interp_list
  (fst
     match remove_one a hp2 with
     | Some hp2' => simplify hp0 hp1 hp2'
     | None => simplify (hp0 ++ a :: nil) hp1 hp2
     end) ==>
interp_list
  (snd
     match remove_one a hp2 with
     | Some hp2' => simplify hp0 hp1 hp2'
     | None => simplify (hp0 ++ a :: nil) hp1 hp2
     end)
interp_list (hp0 ++ a :: hp1) ==> interp_list hp2 pose proof (himp_simp a (hp0 ++ hp1) hp2).hmap: hprop_map
a: hprop_name
hp1: list hprop_name
IHhp1: forall hp0 hp2 : list hprop_name,
interp_list (fst (simplify hp0 hp1 hp2)) ==>
interp_list (snd (simplify hp0 hp1 hp2)) ->
interp_list (hp0 ++ hp1) ==> interp_list hp2
hp0, hp2: list hprop_name
H: interp_list
  (fst
     match remove_one a hp2 with
     | Some hp2' => simplify hp0 hp1 hp2'
     | None => simplify (hp0 ++ a :: nil) hp1 hp2
     end) ==>
interp_list
  (snd
     match remove_one a hp2 with
     | Some hp2' => simplify hp0 hp1 hp2'
     | None => simplify (hp0 ++ a :: nil) hp1 hp2
     end)
H0: match remove_one a hp2 with
| Some hp2' =>
    interp_list (hp0 ++ hp1) ==> interp_list hp2' ->
    interp_list (a :: hp0 ++ hp1) ==>
    interp_list hp2
| None => True
end
interp_list (hp0 ++ a :: hp1) ==> interp_list hp2
        destruct remove_one.hmap: hprop_map
a: hprop_name
hp1: list hprop_name
IHhp1: forall hp0 hp2 : list hprop_name,
interp_list (fst (simplify hp0 hp1 hp2)) ==>
interp_list (snd (simplify hp0 hp1 hp2)) ->
interp_list (hp0 ++ hp1) ==> interp_list hp2
hp0, hp2, l: list hprop_name
H: interp_list (fst (simplify hp0 hp1 l)) ==>
interp_list (snd (simplify hp0 hp1 l))
H0: interp_list (hp0 ++ hp1) ==> interp_list l ->
interp_list (a :: hp0 ++ hp1) ==> interp_list hp2
interp_list (hp0 ++ a :: hp1) ==> interp_list hp2
hmap: hprop_map
a: hprop_name
hp1: list hprop_name
IHhp1: forall hp0 hp2 : list hprop_name,
interp_list (fst (simplify hp0 hp1 hp2)) ==>
interp_list (snd (simplify hp0 hp1 hp2)) ->
interp_list (hp0 ++ hp1) ==> interp_list hp2
hp0, hp2: list hprop_name
H: interp_list
  (fst (simplify (hp0 ++ a :: nil) hp1 hp2)) ==>
interp_list
  (snd (simplify (hp0 ++ a :: nil) hp1 hp2))
H0: True
interp_list (hp0 ++ a :: hp1) ==> interp_list hp2
        +hmap: hprop_map
a: hprop_name
hp1: list hprop_name
IHhp1: forall hp0 hp2 : list hprop_name,
interp_list (fst (simplify hp0 hp1 hp2)) ==>
interp_list (snd (simplify hp0 hp1 hp2)) ->
interp_list (hp0 ++ hp1) ==> interp_list hp2
hp0, hp2, l: list hprop_name
H: interp_list (fst (simplify hp0 hp1 l)) ==>
interp_list (snd (simplify hp0 hp1 l))
H0: interp_list (hp0 ++ hp1) ==> interp_list l ->
interp_list (a :: hp0 ++ hp1) ==> interp_list hp2
interp_list (hp0 ++ a :: hp1) ==> interp_list hp2 eapply himp_mp.hmap: hprop_map
a: hprop_name
hp1: list hprop_name
IHhp1: forall hp0 hp2 : list hprop_name,
interp_list (fst (simplify hp0 hp1 hp2)) ==>
interp_list (snd (simplify hp0 hp1 hp2)) ->
interp_list (hp0 ++ hp1) ==> interp_list hp2
hp0, hp2, l: list hprop_name
H: interp_list (fst (simplify hp0 hp1 l)) ==>
interp_list (snd (simplify hp0 hp1 l))
H0: interp_list (hp0 ++ hp1) ==> interp_list l ->
interp_list (a :: hp0 ++ hp1) ==> interp_list hp2
?Q ==> interp_list hp2
hmap: hprop_map
a: hprop_name
hp1: list hprop_name
IHhp1: forall hp0 hp2 : list hprop_name,
interp_list (fst (simplify hp0 hp1 hp2)) ==>
interp_list (snd (simplify hp0 hp1 hp2)) ->
interp_list (hp0 ++ hp1) ==> interp_list hp2
hp0, hp2, l: list hprop_name
H: interp_list (fst (simplify hp0 hp1 l)) ==>
interp_list (snd (simplify hp0 hp1 l))
H0: interp_list (hp0 ++ hp1) ==> interp_list l ->
interp_list (a :: hp0 ++ hp1) ==> interp_list hp2
interp_list (hp0 ++ a :: hp1) ==> ?Q
          *hmap: hprop_map
a: hprop_name
hp1: list hprop_name
IHhp1: forall hp0 hp2 : list hprop_name,
interp_list (fst (simplify hp0 hp1 hp2)) ==>
interp_list (snd (simplify hp0 hp1 hp2)) ->
interp_list (hp0 ++ hp1) ==> interp_list hp2
hp0, hp2, l: list hprop_name
H: interp_list (fst (simplify hp0 hp1 l)) ==>
interp_list (snd (simplify hp0 hp1 l))
H0: interp_list (hp0 ++ hp1) ==> interp_list l ->
interp_list (a :: hp0 ++ hp1) ==> interp_list hp2
?Q ==> interp_list hp2 eapply H0.hmap: hprop_map
a: hprop_name
hp1: list hprop_name
IHhp1: forall hp0 hp2 : list hprop_name,
interp_list (fst (simplify hp0 hp1 hp2)) ==>
interp_list (snd (simplify hp0 hp1 hp2)) ->
interp_list (hp0 ++ hp1) ==> interp_list hp2
hp0, hp2, l: list hprop_name
H: interp_list (fst (simplify hp0 hp1 l)) ==>
interp_list (snd (simplify hp0 hp1 l))
H0: interp_list (hp0 ++ hp1) ==> interp_list l ->
interp_list (a :: hp0 ++ hp1) ==> interp_list hp2
interp_list (hp0 ++ hp1) ==> interp_list l
            eapply IHhp1.hmap: hprop_map
a: hprop_name
hp1: list hprop_name
IHhp1: forall hp0 hp2 : list hprop_name,
interp_list (fst (simplify hp0 hp1 hp2)) ==>
interp_list (snd (simplify hp0 hp1 hp2)) ->
interp_list (hp0 ++ hp1) ==> interp_list hp2
hp0, hp2, l: list hprop_name
H: interp_list (fst (simplify hp0 hp1 l)) ==>
interp_list (snd (simplify hp0 hp1 l))
H0: interp_list (hp0 ++ hp1) ==> interp_list l ->
interp_list (a :: hp0 ++ hp1) ==> interp_list hp2
interp_list (fst (simplify hp0 hp1 l)) ==>
interp_list (snd (simplify hp0 hp1 l))
            eauto with sep_db.
          *hmap: hprop_map
a: hprop_name
hp1: list hprop_name
IHhp1: forall hp0 hp2 : list hprop_name,
interp_list (fst (simplify hp0 hp1 hp2)) ==>
interp_list (snd (simplify hp0 hp1 hp2)) ->
interp_list (hp0 ++ hp1) ==> interp_list hp2
hp0, hp2, l: list hprop_name
H: interp_list (fst (simplify hp0 hp1 l)) ==>
interp_list (snd (simplify hp0 hp1 l))
H0: interp_list (hp0 ++ hp1) ==> interp_list l ->
interp_list (a :: hp0 ++ hp1) ==> interp_list hp2
interp_list (hp0 ++ a :: hp1) ==>
interp_list (a :: hp0 ++ hp1) eapply (@himp_mp (interp_list ((a::hp1) ++ hp0)));
              sep;
              apply interp_list_comm.
        +hmap: hprop_map
a: hprop_name
hp1: list hprop_name
IHhp1: forall hp0 hp2 : list hprop_name,
interp_list (fst (simplify hp0 hp1 hp2)) ==>
interp_list (snd (simplify hp0 hp1 hp2)) ->
interp_list (hp0 ++ hp1) ==> interp_list hp2
hp0, hp2: list hprop_name
H: interp_list
  (fst (simplify (hp0 ++ a :: nil) hp1 hp2)) ==>
interp_list
  (snd (simplify (hp0 ++ a :: nil) hp1 hp2))
H0: True
interp_list (hp0 ++ a :: hp1) ==> interp_list hp2 generalize (IHhp1 (hp0 ++ (a :: nil)) hp2);
          rewrite <- app_assoc; simpl; auto.
    Qed.

    Lemma flatten_hinterp hp :
      interp_list (flatten hp) ==> hinterp hp.hmap: hprop_map
hp: Hprop
interp_list (flatten hp) ==> hinterp hp
    Proof.hmap: hprop_map
hp: Hprop
interp_list (flatten hp) ==> hinterp hp
      induction hp; mysimpl.hmap: hprop_map
emp ==> emp
hmap: hprop_map
h: hprop_name
lookup_hprop h hmap ** emp ==> lookup_hprop h hmap
hmap: hprop_map
hp1, hp2: Hprop
IHhp1: interp_list (flatten hp1) ==> hinterp hp1
IHhp2: interp_list (flatten hp2) ==> hinterp hp2
interp_list (flatten hp1 ++ flatten hp2) ==>
hinterp hp1 ** hinterp hp2
      -hmap: hprop_map
emp ==> emp sep.
      -hmap: hprop_map
h: hprop_name
lookup_hprop h hmap ** emp ==> lookup_hprop h hmap apply hyp_comm.hmap: hprop_map
h: hprop_name
emp ** lookup_hprop h hmap ==> lookup_hprop h hmap
        apply hyp_emp.hmap: hprop_map
h: hprop_name
lookup_hprop h hmap ==> lookup_hprop h hmap
        sep.
      -hmap: hprop_map
hp1, hp2: Hprop
IHhp1: interp_list (flatten hp1) ==> hinterp hp1
IHhp2: interp_list (flatten hp2) ==> hinterp hp2
interp_list (flatten hp1 ++ flatten hp2) ==>
hinterp hp1 ** hinterp hp2 eapply (@himp_mp (interp_list (flatten hp1) **
                          interp_list (flatten hp2))).hmap: hprop_map
hp1, hp2: Hprop
IHhp1: interp_list (flatten hp1) ==> hinterp hp1
IHhp2: interp_list (flatten hp2) ==> hinterp hp2
interp_list (flatten hp1) ** interp_list (flatten hp2) ==>
hinterp hp1 ** hinterp hp2
hmap: hprop_map
hp1, hp2: Hprop
IHhp1: interp_list (flatten hp1) ==> hinterp hp1
IHhp2: interp_list (flatten hp2) ==> hinterp hp2
interp_list (flatten hp1 ++ flatten hp2) ==>
interp_list (flatten hp1) ** interp_list (flatten hp2)
        eapply himp_split; auto.hmap: hprop_map
hp1, hp2: Hprop
IHhp1: interp_list (flatten hp1) ==> hinterp hp1
IHhp2: interp_list (flatten hp2) ==> hinterp hp2
interp_list (flatten hp1 ++ flatten hp2) ==>
interp_list (flatten hp1) ** interp_list (flatten hp2)
        apply interp_list_app.
    Qed.

This is the proof that the cross_off algorithm is correct. That is, if we can prove that the resulting implication holds after crossing off, then the original implication holds.

    Lemma cross_off_corr :
      forall hp1 hp2,
        let (hp1',hp2') := cross_off hp1 hp2 in
        (hinterp hp1') ==> (hinterp hp2') ->
        (hinterp hp1) ==> (hinterp hp2).hmap: hprop_map
forall hp1 hp2 : Hprop,
let (hp1', hp2') := cross_off hp1 hp2 in
hinterp hp1' ==> hinterp hp2' ->
hinterp hp1 ==> hinterp hp2
    Proof.hmap: hprop_map
forall hp1 hp2 : Hprop,
let (hp1', hp2') := cross_off hp1 hp2 in
hinterp hp1' ==> hinterp hp2' ->
hinterp hp1 ==> hinterp hp2
      intros.hmap: hprop_map
hp1, hp2: Hprop
let (hp1', hp2') := cross_off hp1 hp2 in
hinterp hp1' ==> hinterp hp2' ->
hinterp hp1 ==> hinterp hp2
      remember (cross_off hp1 hp2) as e.hmap: hprop_map
hp1, hp2: Hprop
e: (Hprop * Hprop)%type
Heqe: e = cross_off hp1 hp2
let (hp1', hp2') := e in
hinterp hp1' ==> hinterp hp2' ->
hinterp hp1 ==> hinterp hp2
      unfold cross_off in Heqe.hmap: hprop_map
hp1, hp2: Hprop
e: (Hprop * Hprop)%type
Heqe: e =
(let (hp1', hp2') :=
   simplify nil (flatten hp1) (flatten hp2) in
 (collapse hp1', collapse hp2'))
let (hp1', hp2') := e in
hinterp hp1' ==> hinterp hp2' ->
hinterp hp1 ==> hinterp hp2
      destruct e.hmap: hprop_map
hp1, hp2, h, h0: Hprop
Heqe: (h, h0) =
(let (hp1', hp2') :=
   simplify nil (flatten hp1) (flatten hp2) in
 (collapse hp1', collapse hp2'))
hinterp h ==> hinterp h0 ->
hinterp hp1 ==> hinterp hp2
      intros.hmap: hprop_map
hp1, hp2, h, h0: Hprop
Heqe: (h, h0) =
(let (hp1', hp2') :=
   simplify nil (flatten hp1) (flatten hp2) in
 (collapse hp1', collapse hp2'))
H: hinterp h ==> hinterp h0
hinterp hp1 ==> hinterp hp2
      eapply (@himp_mp (interp_list (flatten hp1)));
        [ | apply hinterp_flatten ].hmap: hprop_map
hp1, hp2, h, h0: Hprop
Heqe: (h, h0) =
(let (hp1', hp2') :=
   simplify nil (flatten hp1) (flatten hp2) in
 (collapse hp1', collapse hp2'))
H: hinterp h ==> hinterp h0
interp_list (flatten hp1) ==> hinterp hp2
      generalize (simplify_corr (flatten hp1) nil (flatten hp2)).hmap: hprop_map
hp1, hp2, h, h0: Hprop
Heqe: (h, h0) =
(let (hp1', hp2') :=
   simplify nil (flatten hp1) (flatten hp2) in
 (collapse hp1', collapse hp2'))
H: hinterp h ==> hinterp h0
(interp_list
   (fst (simplify nil (flatten hp1) (flatten hp2))) ==>
 interp_list
   (snd (simplify nil (flatten hp1) (flatten hp2))) ->
 interp_list (nil ++ flatten hp1) ==>
 interp_list (flatten hp2)) ->
interp_list (flatten hp1) ==> hinterp hp2
      intros.hmap: hprop_map
hp1, hp2, h, h0: Hprop
Heqe: (h, h0) =
(let (hp1', hp2') :=
   simplify nil (flatten hp1) (flatten hp2) in
 (collapse hp1', collapse hp2'))
H: hinterp h ==> hinterp h0
H0: interp_list
  (fst (simplify nil (flatten hp1) (flatten hp2))) ==>
interp_list
  (snd (simplify nil (flatten hp1) (flatten hp2))) ->
interp_list (nil ++ flatten hp1) ==>
interp_list (flatten hp2)
interp_list (flatten hp1) ==> hinterp hp2
      eapply himp_mp.hmap: hprop_map
hp1, hp2, h, h0: Hprop
Heqe: (h, h0) =
(let (hp1', hp2') :=
   simplify nil (flatten hp1) (flatten hp2) in
 (collapse hp1', collapse hp2'))
H: hinterp h ==> hinterp h0
H0: interp_list
  (fst (simplify nil (flatten hp1) (flatten hp2))) ==>
interp_list
  (snd (simplify nil (flatten hp1) (flatten hp2))) ->
interp_list (nil ++ flatten hp1) ==>
interp_list (flatten hp2)
?Q ==> hinterp hp2
hmap: hprop_map
hp1, hp2, h, h0: Hprop
Heqe: (h, h0) =
(let (hp1', hp2') :=
   simplify nil (flatten hp1) (flatten hp2) in
 (collapse hp1', collapse hp2'))
H: hinterp h ==> hinterp h0
H0: interp_list
  (fst (simplify nil (flatten hp1) (flatten hp2))) ==>
interp_list
  (snd (simplify nil (flatten hp1) (flatten hp2))) ->
interp_list (nil ++ flatten hp1) ==>
interp_list (flatten hp2)
interp_list (flatten hp1) ==> ?Q
      +hmap: hprop_map
hp1, hp2, h, h0: Hprop
Heqe: (h, h0) =
(let (hp1', hp2') :=
   simplify nil (flatten hp1) (flatten hp2) in
 (collapse hp1', collapse hp2'))
H: hinterp h ==> hinterp h0
H0: interp_list
  (fst (simplify nil (flatten hp1) (flatten hp2))) ==>
interp_list
  (snd (simplify nil (flatten hp1) (flatten hp2))) ->
interp_list (nil ++ flatten hp1) ==>
interp_list (flatten hp2)
?Q ==> hinterp hp2 eapply flatten_hinterp.
      +hmap: hprop_map
hp1, hp2, h, h0: Hprop
Heqe: (h, h0) =
(let (hp1', hp2') :=
   simplify nil (flatten hp1) (flatten hp2) in
 (collapse hp1', collapse hp2'))
H: hinterp h ==> hinterp h0
H0: interp_list
  (fst (simplify nil (flatten hp1) (flatten hp2))) ==>
interp_list
  (snd (simplify nil (flatten hp1) (flatten hp2))) ->
interp_list (nil ++ flatten hp1) ==>
interp_list (flatten hp2)
interp_list (flatten hp1) ==>
interp_list (flatten hp2) simpl in H0.hmap: hprop_map
hp1, hp2, h, h0: Hprop
Heqe: (h, h0) =
(let (hp1', hp2') :=
   simplify nil (flatten hp1) (flatten hp2) in
 (collapse hp1', collapse hp2'))
H: hinterp h ==> hinterp h0
H0: interp_list
  (fst (simplify nil (flatten hp1) (flatten hp2))) ==>
interp_list
  (snd (simplify nil (flatten hp1) (flatten hp2))) ->
interp_list (flatten hp1) ==>
interp_list (flatten hp2)
interp_list (flatten hp1) ==>
interp_list (flatten hp2)
        apply H0.hmap: hprop_map
hp1, hp2, h, h0: Hprop
Heqe: (h, h0) =
(let (hp1', hp2') :=
   simplify nil (flatten hp1) (flatten hp2) in
 (collapse hp1', collapse hp2'))
H: hinterp h ==> hinterp h0
H0: interp_list
  (fst (simplify nil (flatten hp1) (flatten hp2))) ==>
interp_list
  (snd (simplify nil (flatten hp1) (flatten hp2))) ->
interp_list (flatten hp1) ==>
interp_list (flatten hp2)
interp_list
  (fst (simplify nil (flatten hp1) (flatten hp2))) ==>
interp_list
  (snd (simplify nil (flatten hp1) (flatten hp2)))
        destruct simplify.hmap: hprop_map
hp1, hp2, h, h0: Hprop
l, l0: list hprop_name
Heqe: (h, h0) = (collapse l, collapse l0)
H: hinterp h ==> hinterp h0
H0: interp_list (fst (l, l0)) ==>
interp_list (snd (l, l0)) ->
interp_list (flatten hp1) ==>
interp_list (flatten hp2)
interp_list (fst (l, l0)) ==>
interp_list (snd (l, l0)) simpl in *.hmap: hprop_map
hp1, hp2, h, h0: Hprop
l, l0: list hprop_name
Heqe: (h, h0) = (collapse l, collapse l0)
H: hinterp h ==> hinterp h0
H0: interp_list l ==> interp_list l0 ->
interp_list (flatten hp1) ==>
interp_list (flatten hp2)
interp_list l ==> interp_list l0
        do 2 rewrite <- collapse_interp.hmap: hprop_map
hp1, hp2, h, h0: Hprop
l, l0: list hprop_name
Heqe: (h, h0) = (collapse l, collapse l0)
H: hinterp h ==> hinterp h0
H0: interp_list l ==> interp_list l0 ->
interp_list (flatten hp1) ==>
interp_list (flatten hp2)
hinterp (collapse l) ==> hinterp (collapse l0)
        mysimpl.
    Qed.
  End HINTERP.

Here is an example using the reflection. We have a large implication to prove that demands many re-associations, commutations, etc. So we first build an hmap from numbers to hprops, then we build syntax that parallels the predicates, being sure to use the right atoms according to the hmap, and finally we invoke the cross_off_corr lemma to get a much simplified routine. In this case, the simplification gets everything down to emp ==> emp.

  Lemma crazy P Q R S T :
    Q ** (P ** R) ** (S ** T) ==> T ** (S ** P) ** Q ** R.P, Q, R, S, T: hprop
Q ** (P ** R) ** S ** T ==> T ** (S ** P) ** Q ** R
  Proof.P, Q, R, S, T: hprop
Q ** (P ** R) ** S ** T ==> T ** (S ** P) ** Q ** R
    intros.P, Q, R, S, T: hprop
Q ** (P ** R) ** S ** T ==> T ** (S ** P) ** Q ** R
    generalize (
        let hmap := (0, P) :: (1, Q) :: (2, R)
                          :: (3, S) :: (4, T) :: nil in
      let H1 := Atom 1 # (Atom 0 # Atom 2) # (Atom 3 # Atom 4) in
      let H2 := Atom 4 # (Atom 3 # Atom 0) # Atom 1 # Atom 2 in
        cross_off_corr hmap H1 H2
    ).P, Q, R, S, T: hprop
(let (hp1', hp2') :=
   cross_off
     (Atom 1 # (Atom 0 # Atom 2) # Atom 3 # Atom 4)
     (Atom 4 # (Atom 3 # Atom 0) # Atom 1 # Atom 2) in
 hinterp
   ((0, P)
    :: (1, Q) :: (2, R) :: (3, S) :: (4, T) :: nil)
   hp1' ==>
 hinterp
   ((0, P)
    :: (1, Q) :: (2, R) :: (3, S) :: (4, T) :: nil)
   hp2' ->
 hinterp
   ((0, P)
    :: (1, Q) :: (2, R) :: (3, S) :: (4, T) :: nil)
   (Atom 1 # (Atom 0 # Atom 2) # Atom 3 # Atom 4) ==>
 hinterp
   ((0, P)
    :: (1, Q) :: (2, R) :: (3, S) :: (4, T) :: nil)
   (Atom 4 # (Atom 3 # Atom 0) # Atom 1 # Atom 2)) ->
Q ** (P ** R) ** S ** T ==> T ** (S ** P) ** Q ** R
    simpl.P, Q, R, S, T: hprop
(emp ==> emp ->
 Q ** (P ** R) ** S ** T ==> T ** (S ** P) ** Q ** R) ->
Q ** (P ** R) ** S ** T ==> T ** (S ** P) ** Q ** R
    sep.
  Qed.

  Ltac lookup_name term map :=
    match map with
    | (?n, ?P) :: ?rest =>
        match term with
        | P => constr:(Some (Atom n))
        | _ => lookup_name term rest
        end
    | _ => constr:(@None Hprop)
    end.

  Ltac reflect term map :=
    match term with
    | star ?P ?Q =>
        match reflect P map with
        | (?t1, ?map1) =>
            match reflect Q map1 with
            | (?t2, ?map2) => constr:((Star t1 t2, map2))
            end
        end
    | emp => constr:((Emp, map))
    | _ =>
        match lookup_name term map with
        | Some ?t =>
            constr:((t, map))
        | None =>
            let n := constr:(S (List.length map)) in
            constr:((Atom n, ((n, term) :: map)))
        end
    end.

  Ltac cross :=
    match goal with
    | [ |- ?A ==> ?B ] =>
        let map := constr:(@nil (hprop_name * hprop)) in
        match reflect A map with
        | (?t1, ?map1) =>
            match reflect B map1 with
            | (?t2, ?map2) =>
                apply (cross_off_corr map2 t1 t2); simpl
            end
        end
    end.

  Lemma crazy2 P Q R S T:
    Q ** (P ** R) ** (S ** T) ==>
      T ** (S ** P) ** Q ** R.P, Q, R, S, T: hprop
Q ** (P ** R) ** S ** T ==> T ** (S ** P) ** Q ** R
  Proof.P, Q, R, S, T: hprop
Q ** (P ** R) ** S ** T ==> T ** (S ** P) ** Q ** R
    cross.P, Q, R, S, T: hprop
emp ==> emp
    sep.
  Defined.
  Eval compute in crazy2.= fun P Q R S0 T : list (nat * value) -> Prop =>
  cross_off_corr
    ((5, T)
     :: (4, S0)
        :: (3, R) :: (2, P) :: (1, Q) :: nil)
    (Atom 1 # (Atom 2 # Atom 3) # Atom 4 # Atom 5)
    (Atom 5 # (Atom 4 # Atom 2) # Atom 1 # Atom 3)
    (himp_id
       (fun h : list (nat * value) => h = nil))
: forall P Q R S T : hprop,
  Q ** (P ** R) ** S ** T ==>
  T ** (S ** P) ** Q ** R

  Lemma crazy3 (p q r s:ptr) :
    ((p --> VNat 0 ** q --> VNat 1)
       ** (r --> VNat 2 ** emp)
       ** (s --> VNat 3))
      ==>
      (s --> VNat 3
         ** q --> VNat 1
         ** p --> VNat 0
         ** r --> VNat 2).p, q, r, s: ptr
(p --> VNat 0 ** q --> VNat 1) **
(r --> VNat 2 ** emp) ** s --> VNat 3 ==>
s --> VNat 3 **
q --> VNat 1 ** p --> VNat 0 ** r --> VNat 2
  Proof.p, q, r, s: ptr
(p --> VNat 0 ** q --> VNat 1) **
(r --> VNat 2 ** emp) ** s --> VNat 3 ==>
s --> VNat 3 **
q --> VNat 1 ** p --> VNat 0 ** r --> VNat 2
    cross.p, q, r, s: ptr
emp ==> emp
    sep.
  Defined.

End FunctionalSepIMP.