From ce3a01ebfeb11ec1e25e90cccc55a1204fbef7b6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 20 Feb 2016 15:02:02 +0100
Subject: [PATCH] avoid wp_bindi

---
 barrier/barrier.v   | 14 ++++++++------
 heap_lang/lifting.v |  5 -----
 2 files changed, 8 insertions(+), 11 deletions(-)

diff --git a/barrier/barrier.v b/barrier/barrier.v
index f960c0cd0..fd34e8f9b 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -237,15 +237,17 @@ Section proof.
     heapN ⊥ N → (recv l P ★ (P -★ Φ '())) ⊑ || wait (LocV l) {{ Φ }}.
   Proof.
     rename P into R.
-    intros Hdisj. rewrite /wait. rewrite [(_ ★ _)%I](pvs_intro ⊤).
-    apply löb_strong_sep. rewrite pvs_frame_r. apply wp_strip_pvs.
+    intros Hdisj.
+    (* TODO we probably want a tactic or lemma that does the next 2 lines for us.
+       It should be general enough to also cover FindPred_spec. Probably this
+       should be the default behavior of wp_rec - since this is what we need every time
+       we prove a recursive function correct. *)
+    rewrite /wait. rewrite [(_ ★ _)%I](pvs_intro ⊤).
+    apply löb_strong_sep. rewrite pvs_frame_r. apply wp_strip_pvs. wp_rec.
     rewrite {1}/recv /barrier_ctx. rewrite !sep_exist_r.
     apply exist_elim=>γ. rewrite !sep_exist_r. apply exist_elim=>P.
     rewrite !sep_exist_r. apply exist_elim=>Q. rewrite !sep_exist_r.
-    apply exist_elim=>i. wp_rec.
-    (* TODO use automatic binding *)
-    rewrite -(wp_bindi (IfCtx _ _)) /=.
-    rewrite -(wp_bindi (BinOpLCtx _ _)) /=.
+    apply exist_elim=>i. wp_focus (! _)%L.
     (* I think some evars here are better than repeating *everything* *)
     eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
       eauto with I ndisj.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index b653903fe..5359b62ba 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -19,11 +19,6 @@ Lemma wp_bind {E e} K Φ :
   || e @ E {{ λ v, || fill K (of_val v) @ E {{ Φ }}}} ⊑ || fill K e @ E {{ Φ }}.
 Proof. apply weakestpre.wp_bind. Qed.
 
-Lemma wp_bindi {E e} Ki Φ :
-  || e @ E {{ λ v, || fill_item Ki (of_val v) @ E {{ Φ }}}}
-     ⊑ || fill_item Ki e @ E {{ Φ }}.
-Proof. apply weakestpre.wp_bind. Qed.
-
 (** Base axioms for core primitives of the language: Stateful reductions. *)
 Lemma wp_alloc_pst E σ e v Φ :
   to_val e = Some v →
-- 
GitLab