From demo Require Import simplified_iris.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file ltac2_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-core.plugins.ltac2_ltac1 is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file ltac2_ltac1_plugin.cmxs (using legacy method) ... done]

(** * deletetree from the Separation Logic CACM paper by O'Hearn *)

(** A tree will be a pointer to either None (represented InjL #()) or Some(l,r)
(represented InjR (l, r)), where l and r are themselves trees. *)

(** delete_tree is a version of the deletetree function from the paper, written
in an OCaml-like language rather than the C code in the paper. *)
Definition delete_tree: val :=
  (* the rec: here starts a recursive function *)
  rec: "delete_tree" "x" :=
    (* !"x" deferences the variable x (variables need to be quoted) *)
    match: !"x" with
      SOME "tree" =>
      (* if this tree has children, delete them first. Recall the tree is just a
      tuple of the left and right child tree pointers. *)
      (let: "left" := Fst "tree" in
       let: "right" := Snd "tree" in
       "delete_tree" "left";;
       "delete_tree" "right";;
      (* then free the root pointer *)
      Free "x")
    | NONE =>
      (* the way we've represented trees, even an empty tree is a pointer to a
      None, so free that, too *)
      Free "x"
    end.

Section proof.

Context `{!heapGS Σ}.
Implicit Types (t l r:loc).

(* You can ignore some magic that creates the recursive tree predicate. *)

Definition tree_pre (tree: loc -d> iPropO Σ): loc -d> iPropO Σ :=
  (λ t, t ↦ NONEV ∨
        (∃ l r, t ↦ SOMEV (#l, #r) ∗
                ▷ tree l ∗ ▷ tree r))%I.

Local Instance tree_pre_contractive : Contractive tree_pre.
Σ: gFunctors
heapGS0: heapGS Σ
Contractive tree_pre
Proof.
Σ: gFunctors
heapGS0: heapGS Σ
Contractive tree_pre solve_contractive. Qed.

Definition tree : loc → iProp Σ := fixpoint tree_pre.

(** You can take the following as a definition for [tree], in terms of a
recursive equation - the ⊣⊢ symbol means "equivalent". You can pretend ▷P is the
same as P; this is a technicality required to write recursive definitions. *)
Theorem tree_unfold t :
  tree t ⊣⊢
  t ↦ NONEV ∨ (∃ l r, t ↦ SOMEV (#l, #r) ∗ ▷ tree l ∗ ▷ tree r).
Σ: gFunctors
heapGS0: heapGS Σ
t: loc
tree t
⊣⊢ t ↦ NONEV
   ∨ ∃ l r, t ↦ SOMEV (#l, #r) ∗ ▷ tree l ∗ ▷ tree r
Proof.
Σ: gFunctors
heapGS0: heapGS Σ
t: loc
tree t
⊣⊢ t ↦ NONEV
   ∨ ∃ l r, t ↦ SOMEV (#l, #r) ∗ ▷ tree l ∗ ▷ tree r apply (fixpoint_unfold tree_pre). Qed.

Theorem wp_delete_tree t :
  tree t -∗
  WP delete_tree #t
  {{ λ _, emp }}.
Σ: gFunctors
heapGS0: heapGS Σ
t: loc
tree t -∗ WP delete_tree #t {{ _, emp }}
Proof.
Σ: gFunctors
heapGS0: heapGS Σ
t: loc
tree t -∗ WP delete_tree #t {{ _, emp }}
  iIntros "Ht".
Σ: gFunctors
heapGS0: heapGS Σ
t: loc
"Ht" : tree t
--------------------------------------∗
WP delete_tree #t {{ _, emp }}

  (* First we should understand how Hoare logic proofs are encoded in Iris. In
  Iris the goal is going to be [WP e {{ Q }}], which is a separation logic
  predicate, not a Coq assertion. For intuition, keep in mind that {{P}} e {{Q}}
  is the same thing as P ⊢ WP e {{ Q }}. Then, you can think of the spec being
  proven as one where the precondition is all of the premises (the hypotheses)
  and the program and postcondition are in the goal. *)

  (* this is how we start a recursive proof: *)
  iLöb as "IH" forall (t).
Σ: gFunctors
heapGS0: heapGS Σ
t: loc
"IH" : ▷ ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : tree t
--------------------------------------∗
WP delete_tree #t {{ _, emp }}
  (* What we get from iLöb is an assumption that delete_tree follows the
  specification. How is that possible? Couldn't we just use it right away and
  not have to any work? Indeed! That's why this assumption has the ▷ (pronounced
  "later") in front. ▷ P means we only get to know that P holds after one "step"
  within our function. This is enough to handle all the recursive calls but
  can't be used to just dismiss the whole proof (otherwise proofs would be easy
  but not very meaningful) *)

  (* We destruct the tree predicate into the two branches of the [∨], and carry
  out the proof separately in each case. *)
  iDestruct (tree_unfold with "Ht") as "[Ht|Ht]".
Σ: gFunctors
heapGS0: heapGS Σ
t: loc
"IH" : ▷ ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : t ↦ NONEV
--------------------------------------∗
WP delete_tree #t {{ _, emp }}
Σ: gFunctors
heapGS0: heapGS Σ
t: loc
"IH" : ▷ ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : ∃ l r, t ↦ SOMEV (#l, #r) ∗ ▷ tree l ∗ ▷ tree r
--------------------------------------∗
WP delete_tree #t {{ _, emp }}
  -
Σ: gFunctors
heapGS0: heapGS Σ
t: loc
"IH" : ▷ ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : t ↦ NONEV
--------------------------------------∗
WP delete_tree #t {{ _, emp }} (* The first case corresponds to an empty tree, where t ↦ None. In that case
    the code reduces down to just executing a Free on the root pointer. *)
    wp_rec.
Σ: gFunctors
heapGS0: heapGS Σ
t: loc
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : t ↦ NONEV
--------------------------------------∗
WP match: ! #t with
     InjL <> => Free #t
   | InjR "tree" =>
     let: "left" := Fst "tree" in
     let: "right" := Snd "tree" in
     delete_tree "left";; 
     delete_tree "right";; Free #t
   end
{{ _, emp }}
    (* I won't go through the motions of using the frame rule and
    load/store/free axioms; there's a tactic for that *)
    wp_load; wp_pures.
Σ: gFunctors
heapGS0: heapGS Σ
t: loc
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : t ↦ NONEV
--------------------------------------∗
WP Free #t {{ _, emp }}
    wp_free.
Σ: gFunctors
heapGS0: heapGS Σ
t: loc
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
|={⊤}=> emp
    auto.
  -
Σ: gFunctors
heapGS0: heapGS Σ
t: loc
"IH" : ▷ ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : ∃ l r, t ↦ SOMEV (#l, #r) ∗ ▷ tree l ∗ ▷ tree r
--------------------------------------∗
WP delete_tree #t {{ _, emp }} (* In the other case we need to further destruct [tree] to get out the left
    and right subtrees (both their root pointers and the corresponding [tree]
    predicates) *)
    iDestruct "Ht" as (l r) "(Ht & Hl & Hr)".
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
"IH" : ▷ ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : t ↦ SOMEV (#l, #r)
"Hl" : ▷ tree l
"Hr" : ▷ tree r
--------------------------------------∗
WP delete_tree #t {{ _, emp }}
    wp_rec.
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : t ↦ SOMEV (#l, #r)
"Hl" : tree l
"Hr" : tree r
--------------------------------------∗
WP match: ! #t with
     InjL <> => Free #t
   | InjR "tree" =>
     let: "left" := Fst "tree" in
     let: "right" := Snd "tree" in
     delete_tree "left";; 
     delete_tree "right";; Free #t
   end
{{ _, emp }}
    wp_load; wp_pures.
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : t ↦ SOMEV (#l, #r)
"Hl" : tree l
"Hr" : tree r
--------------------------------------∗
WP delete_tree #l;; delete_tree #r;; Free #t
{{ _, emp }}

    (* wp_bind is a tactic to apply the sequencing rule (it takes an argument to
    pick what should be sequenced, for example in e1;; e2;; e3 you can isolate
    (e1;;e2) if you want) *)
    wp_bind (delete_tree _).
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : t ↦ SOMEV (#l, #r)
"Hl" : tree l
"Hr" : tree r
--------------------------------------∗
WP delete_tree #l
{{ v, WP v;; delete_tree #r;; Free #t {{ _, emp }} }}

    (* The recursive calls make use of the inductive hypothesis "IH", which says
    any recursive calls to delete_tree can be assumed to satisfy this
    specification. *)
    iApply wp_frame.
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : t ↦ SOMEV (#l, #r)
"Hl" : tree l
"Hr" : tree r
--------------------------------------∗
WP delete_tree #l {{ v, ?Goal v }} ∗
∀ r0 : val,
  ?Goal r0 -∗
  WP r0;; delete_tree #r;; Free #t {{ _, emp }}
    iSplitL "Hl".
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Hl" : tree l
--------------------------------------∗
WP delete_tree #l {{ v, ?Goal v }}
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : t ↦ SOMEV (#l, #r)
"Hr" : tree r
--------------------------------------∗
∀ r0 : val,
  ?Goal r0 -∗
  WP r0;; delete_tree #r;; Free #t {{ _, emp }}
    {
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Hl" : tree l
--------------------------------------∗
WP delete_tree #l {{ v, ?Goal v }} iApply ("IH" with "Hl"). }
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : t ↦ SOMEV (#l, #r)
"Hr" : tree r
--------------------------------------∗
∀ r0 : val,
  (λ _ : language.val heap_lang, emp) r0 -∗
  WP r0;; delete_tree #r;; Free #t {{ _, emp }}
    (* I'm naming the postcondition from the [delete_tree] specification "Hl"
    just to emphasize where it came from (it's an [emp] and thus unimportant,
    the separation logic equivalent of having a hypothesis [True]) *)
    simpl; iIntros (?) "Hl"; wp_pures.
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
r0: val
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : t ↦ SOMEV (#l, #r)
"Hr" : tree r
"Hl" : emp
--------------------------------------∗
WP delete_tree #r;; Free #t {{ _, emp }}

    wp_bind (delete_tree _).
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
r0: val
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : t ↦ SOMEV (#l, #r)
"Hr" : tree r
"Hl" : emp
--------------------------------------∗
WP delete_tree #r {{ v, WP v;; Free #t {{ _, emp }} }}
    iApply wp_frame.
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
r0: val
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : t ↦ SOMEV (#l, #r)
"Hr" : tree r
"Hl" : emp
--------------------------------------∗
WP delete_tree #r {{ v, ?Goal v }} ∗
∀ r1 : val, ?Goal r1 -∗ WP r1;; Free #t {{ _, emp }}
    iSplitL "Hr".
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
r0: val
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Hr" : tree r
--------------------------------------∗
WP delete_tree #r {{ v, ?Goal v }}
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
r0: val
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : t ↦ SOMEV (#l, #r)
"Hl" : emp
--------------------------------------∗
∀ r1 : val, ?Goal r1 -∗ WP r1;; Free #t {{ _, emp }}
    {
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
r0: val
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Hr" : tree r
--------------------------------------∗
WP delete_tree #r {{ v, ?Goal v }} iApply ("IH" with "Hr"). }
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
r0: val
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : t ↦ SOMEV (#l, #r)
"Hl" : emp
--------------------------------------∗
∀ r : val,
  (λ _ : val, emp) r -∗ WP r;; Free #t {{ _, emp }}
    simpl; iIntros (?) "Hr"; wp_pures.
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
r0, r1: val
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Ht" : t ↦ SOMEV (#l, #r)
"Hl" : emp
"Hr" : emp
--------------------------------------∗
WP Free #t {{ _, emp }}
    wp_free.
Σ: gFunctors
heapGS0: heapGS Σ
t, l, r: loc
r0, r1: val
"IH" : ∀ t, tree t -∗ WP delete_tree #t {{ _, emp }}
--------------------------------------□
"Hl" : emp
"Hr" : emp
--------------------------------------∗
|={⊤}=> emp
    auto.
Qed.

End proof.