From 59ae6b91fd07ee80f703594086cbf44b1129b7cb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 Feb 2016 13:56:10 +0100
Subject: [PATCH] Remove a FIXME in barrier.lifting.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Remarks:
* eauto needs more fuel to automatically solve the side-conditions.
* ssreflect rewrite works if we do a set (φ ..) first. No idea why.
---
 barrier/lifting.v | 17 +++++------------
 1 file changed, 5 insertions(+), 12 deletions(-)

diff --git a/barrier/lifting.v b/barrier/lifting.v
index faf093142..4945c0e92 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -21,21 +21,14 @@ Lemma wp_alloc_pst E σ e v Q :
   (ownP σ ★ ▷ (∀ l, ■(σ !! l = None) ∧ ownP (<[l:=v]>σ) -★ Q (LocV l)))
        ⊑ wp E (Alloc e) Q.
 Proof.
-  intros.
-  (* FIXME RJ: ssreflect rewrite does not work. *)
-  rewrite <-(wp_lift_atomic_step (Alloc e)
-    (λ v' σ', ∃ l, v' = LocV l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None) σ)=> //;
-    last first.
-  { (* TODO RJ: Somehow automation used to kill all this...?? *)
-    intros. inv_step. eexists; split_ands; try done; [].
-    eexists; done. }
+  intros. set (φ v' σ' := ∃ l, v' = LocV l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
+  rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ;
+    last by intros; inv_step; eauto 10.
   apply sep_mono, later_mono; first done.
-  apply forall_intro=>e2; apply forall_intro=>σ2.
-  apply wand_intro_l.
+  apply forall_intro=>e2; apply forall_intro=>σ2; apply wand_intro_l.
   rewrite always_and_sep_l' -associative -always_and_sep_l'.
   apply const_elim_l=>-[l [-> [-> ?]]].
-  rewrite (forall_elim l) const_equiv //.
-  by rewrite left_id wand_elim_r.
+  by rewrite (forall_elim l) const_equiv // left_id wand_elim_r.
 Qed.
 
 Lemma wp_load_pst E σ l v Q :
-- 
GitLab