From 90075bbfd5b2631d4f5807bf9401a70c2d8524c2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 17 Feb 2016 09:48:55 +0100
Subject: [PATCH] barrier: Apply ndisj automation, and assume disjointness only
 where needed

This prevent the assumption from being dragged into lemmas that do not even need it
---
 algebra/upred.v   |  1 -
 barrier/barrier.v | 20 ++++++--------------
 2 files changed, 6 insertions(+), 15 deletions(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index fe1f10c1f..c2a8f4eac 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -973,7 +973,6 @@ Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
 End uPred_logic.
 
 (* Hint DB for the logic *)
-Create HintDb I.
 Hint Resolve const_intro.
 Hint Resolve or_elim or_intro_l' or_intro_r' : I.
 Hint Resolve and_intro and_elim_l' and_elim_r' : I.
diff --git a/barrier/barrier.v b/barrier/barrier.v
index bfe640071..da449d711 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -94,15 +94,9 @@ Import barrier_proto.
 (** Now we come to the Iris part of the proof. *)
 Section proof.
   Context {Σ : iFunctorG} (N : namespace).
-  (* TODO: Bundle HeapI and HeapG and have notation so that we can just write
-     "l ↦ '0". *)
   Context `{heapG Σ} (HeapN : namespace).
   Context `{stsG heap_lang Σ sts}.
   Context `{savedPropG heap_lang Σ}.
-  (* TODO We could alternatively construct the namespaces to be disjoint.
-     But that would take a lot of flexibility from the client, who probably
-     wants to also use the heap_ctx elsewhere. *)
-  Context (HeapN_disj : HeapN ⊥ N).
 
   Notation iProp := (iPropG heap_lang Σ).
 
@@ -136,20 +130,18 @@ Section proof.
   Abort.
 
   Lemma signal_spec l P (Q : val → iProp) :
-    (send l P ★ P ★ Q '()) ⊑ wp ⊤ (signal (LocV l)) Q.
+    HeapN ⊥ N → (send l P ★ P ★ Q '()) ⊑ wp ⊤ (signal (LocV l)) Q.
   Proof.
-    rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
+    intros Hdisj. rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
     apply exist_elim=>γ. wp_rec. (* FIXME wp_let *)
     (* I think some evars here are better than repeating *everything* *)
-    eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ);simpl; eauto with I.
-    { solve_elem_of+. (* FIXME eauto should do this *) }
+    eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
+      eauto with I ndisj.
     rewrite [(_ ★ sts_ownS _ _ _)%I]comm -!assoc /wp_fsa. apply sep_mono_r.
     apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
     apply const_elim_sep_l=>Hs. destruct p; last done.
     rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep.
-    eapply wp_store; eauto with I.
-    { (* FIXME can we make this more automatic? *)
-      apply ndisj_disjoint in HeapN_disj. solve_elem_of. }
+    eapply wp_store; eauto with I ndisj.
     rewrite -!assoc. apply sep_mono_r. etransitivity; last eapply later_mono.
     { (* Is this really the best way to strip the later? *)
       erewrite later_sep. apply sep_mono_r. apply later_intro. }
@@ -167,7 +159,7 @@ Section proof.
   Abort.
 
   Lemma wait_spec l P (Q : val → iProp) :
-    (recv l P ★ (P -★ Q '())) ⊑ wp ⊤ (wait (LocV l)) Q.
+    HeapN ⊥ N → (recv l P ★ (P -★ Q '())) ⊑ wp ⊤ (wait (LocV l)) Q.
   Proof.
   Abort.
 
-- 
GitLab