From 58d1d6c9cc4344297e37eb2aac262ae7d7a29d61 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Feb 2016 00:56:17 +0100
Subject: [PATCH] Use some wp tactics in heap example.

---
 heap_lang/tests.v | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 24374006d..fa4fed292 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -31,18 +31,17 @@ Section LiftingTests.
   Goal ∀ γh N, heap_ctx HeapI γh N ⊑ wp N e (λ v, v = '2).
   Proof.
     move=> γh N. rewrite /e.
-    rewrite -(wp_bindi (LetCtx _ _)). eapply wp_alloc; eauto; [].
+    wp_focus (ref '1)%L. eapply wp_alloc; eauto; [].
     rewrite -later_intro; apply forall_intro=>l; apply wand_intro_l.
-    rewrite -wp_let //= -later_intro.
-    rewrite -(wp_bindi (SeqCtx (Load (Loc _)))) /=. 
-    rewrite -(wp_bindi (StoreRCtx (LocV _))) /=.
-    rewrite -(wp_bindi (BinOpLCtx PlusOp _)) /=.
-    eapply wp_load; eauto with I; []. apply sep_mono; first done.
+    wp_rec.
+    wp_focus (! LocV l)%L.
+    eapply wp_load; eauto with I; []. apply sep_mono_r.
     rewrite -later_intro; apply wand_intro_l.
-    rewrite -wp_bin_op // -later_intro.
-    eapply wp_store; eauto with I; []. apply sep_mono; first done.
+    wp_bin_op.
+    wp_focus (_ <- _)%L.
+    eapply wp_store; eauto with I; []. apply sep_mono_r.
     rewrite -later_intro. apply wand_intro_l.
-    rewrite -wp_seq -wp_value' -later_intro.
+    wp_rec.
     eapply wp_load; eauto with I; []. apply sep_mono; first done.
     rewrite -later_intro. apply wand_intro_l.
     by apply const_intro.
-- 
GitLab