From 453d2b161d74c2f25e005d7ea5e927fc04ce829d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 20 Apr 2016 18:59:15 +0200
Subject: [PATCH] heap: start to use proof mode

---
 heap_lang/heap.v      | 39 ++++++++++++++++++---------------------
 heap_lang/proofmode.v |  3 ++-
 2 files changed, 20 insertions(+), 22 deletions(-)

diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 39b5f441e..b4eadc21f 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -2,6 +2,7 @@ From iris.heap_lang Require Export lifting.
 From iris.algebra Require Import upred_big_op frac dec_agree.
 From iris.program_logic Require Export invariants ghost_ownership.
 From iris.program_logic Require Import ownership auth.
+From iris.proofmode Require Import weakestpre.
 Import uPred.
 (* TODO: The entire construction could be generalized to arbitrary languages that have
    a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
@@ -140,29 +141,25 @@ Section heap.
 
   (** Weakest precondition *)
   Lemma wp_alloc N E e v P Φ :
-    to_val e = Some v →
-    P ⊢ heap_ctx N → nclose N ⊆ E →
-    P ⊢ (▷ ∀ l, l ↦ v -★ Φ (LitV (LitLoc l))) →
-    P ⊢ WP Alloc e @ E {{ Φ }}.
+    to_val e = Some v → nclose N ⊆ E →
+    (heap_ctx N ★ ▷ ∀ l, l ↦ v -★ Φ (LitV $ LitLoc l)) ⊢ WP Alloc e @ E {{ Φ }}.
   Proof.
-    rewrite /heap_ctx /heap_inv=> ??? HP.
-    trans (|={E}=> auth_own heap_name ∅ ★ P)%I.
-    { by rewrite -pvs_frame_r -(auth_empty _ E) left_id. }
-    apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
+    iIntros {??} "[#Hinv HΦ]". rewrite /heap_ctx.
+    iPvs (auth_empty heap_name) as "Hheap".
+    (* TODO: use an iTactic *)
+    apply (auth_fsa heap_inv (wp_fsa (Alloc e)))
       with N heap_name ∅; simpl; eauto with I.
-    rewrite -later_intro. apply sep_mono_r,forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc left_id; apply const_elim_sep_l=> ?.
-    rewrite -(wp_alloc_pst _ (of_heap h)) //.
-    apply sep_mono_r; rewrite HP; apply later_mono.
-    apply forall_mono=> l; apply wand_intro_l.
-    rewrite always_and_sep_l -assoc; apply const_elim_sep_l=> ?.
-    rewrite -(exist_intro (op {[ l := Frac 1 (DecAgree v) ]})).
-    repeat erewrite <-exist_intro by apply _; simpl.
-    rewrite -of_heap_insert left_id right_id.
-    rewrite /heap_mapsto. ecancel [_ -★ Φ _]%I.
-    rewrite -(insert_singleton_op h); last by apply of_heap_None.
-    rewrite const_equiv; last by apply (insert_valid h).
-    by rewrite left_id -later_intro.
+    iFrame "Hheap". iIntros {h}. rewrite [∅ ⋅ h]left_id.
+    iIntros "[% Hheap]". rewrite /heap_inv.
+    iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
+    iIntros {l} "[% Hheap]". iExists (op {[ l := Frac 1 (DecAgree v) ]}), _, _.
+    rewrite [{[ _ := _ ]} ⋅ ∅]right_id.
+    rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
+    iFrame "Hheap". iSplit.
+    { (* FIXME iTactic for introduction of constant assertions? *)
+      rewrite const_equiv; first done. split; first done.
+      by apply (insert_valid h). }
+    iIntros "Hheap". iApply "HΦ". rewrite /heap_mapsto. done.
   Qed.
 
   Lemma wp_load N E l q v P Φ :
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 05d5668bc..e0c6d31fc 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -25,7 +25,8 @@ Lemma tac_wp_alloc Δ Δ' N E j e v Φ :
     Δ'' ⊢ Φ (LitV (LitLoc l))) →
   Δ ⊢ WP Alloc e @ E {{ Φ }}.
 Proof.
-  intros ???? HΔ; eapply wp_alloc; eauto.
+  intros ???? HΔ. etrans; last apply: wp_alloc; eauto.
+  rewrite -always_and_sep_l. iSplit; first done.
   rewrite strip_later_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
   by rewrite right_id HΔ'.
-- 
GitLab