From 280d91b059f3372bf31f362eb051915c95598a2e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 1 Jul 2016 01:24:06 +0200
Subject: [PATCH] Clean up some ndisjoint stuff in the proofmode tactics.

---
 heap_lang/proofmode.v      | 10 +++++-----
 program_logic/namespaces.v |  2 ++
 proofmode/invariants.v     |  4 ++--
 proofmode/sts.v            |  2 +-
 4 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 8503a626f..c24b2fbd4 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -105,7 +105,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
       [let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_alloc:" e' "not a value"
       |iAssumption || fail "wp_alloc: cannot find heap_ctx"
-      |done || eauto with ndisj
+      |solve_ndisj
       |apply _
       |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
         eexists; split;
@@ -126,7 +126,7 @@ Tactic Notation "wp_load" :=
       |fail 1 "wp_load: cannot find 'Load' in" e];
     eapply tac_wp_load;
       [iAssumption || fail "wp_load: cannot find heap_ctx"
-      |done || eauto with ndisj
+      |solve_ndisj
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
@@ -145,7 +145,7 @@ Tactic Notation "wp_store" :=
       [let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_store:" e' "not a value"
       |iAssumption || fail "wp_store: cannot find heap_ctx"
-      |done || eauto with ndisj
+      |solve_ndisj
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
@@ -167,7 +167,7 @@ Tactic Notation "wp_cas_fail" :=
       |let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_cas_fail:" e' "not a value"
       |iAssumption || fail "wp_cas_fail: cannot find heap_ctx"
-      |done || eauto with ndisj
+      |solve_ndisj
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
@@ -189,7 +189,7 @@ Tactic Notation "wp_cas_suc" :=
       |let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_cas_suc:" e' "not a value"
       |iAssumption || fail "wp_cas_suc: cannot find heap_ctx"
-      |done || eauto with ndisj
+      |solve_ndisj
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index ea8b74ed5..a01052b78 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -67,3 +67,5 @@ Hint Resolve ndisj_subseteq_difference : ndisj.
 Hint Extern 0 (_ .@ _ ⊥ _ .@ _) => apply ndot_ne_disjoint; congruence : ndisj.
 Hint Resolve ndot_preserve_disjoint_l : ndisj.
 Hint Resolve ndot_preserve_disjoint_r : ndisj.
+
+Ltac solve_ndisj := eauto with ndisj.
diff --git a/proofmode/invariants.v b/proofmode/invariants.v
index 48277e7cf..bb080ac1b 100644
--- a/proofmode/invariants.v
+++ b/proofmode/invariants.v
@@ -39,7 +39,7 @@ Tactic Notation "iInvCore" constr(N) "as" constr(H) :=
     [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
      apply _ || fail "iInv: cannot viewshift in goal" P
     |try fast_done (* atomic *)
-    |done || eauto with ndisj (* [eauto with ndisj] is slow *)
+    |solve_ndisj
     |iAssumption || fail "iInv: invariant" N "not found"
     |env_cbv; reflexivity
     |simpl (* get rid of FSAs *)].
@@ -65,7 +65,7 @@ Tactic Notation "iInvCore>" constr(N) "as" constr(H) :=
     [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
      apply _ || fail "iInv: cannot viewshift in goal" P
     |try fast_done (* atomic *)
-    |done || eauto with ndisj (* [eauto with ndisj] is slow *)
+    |solve_ndisj
     |iAssumption || fail "iOpenInv: invariant" N "not found"
     |let P := match goal with |- TimelessP ?P => P end in
      apply _ || fail "iInv:" P "not timeless"
diff --git a/proofmode/sts.v b/proofmode/sts.v
index 4b535fb3c..c0c469b06 100644
--- a/proofmode/sts.v
+++ b/proofmode/sts.v
@@ -41,6 +41,6 @@ Tactic Notation "iSts" constr(H) "as"
     |try fast_done (* atomic *)
     |iAssumptionCore || fail "iSts:" H "not found"
     |iAssumption || fail "iSts: invariant not found"
-    |done || eauto with ndisj (* [eauto with ndisj] is slow *)
+    |solve_ndisj
     |intros s Hs; eexists; split; [env_cbv; reflexivity|simpl]].
 Tactic Notation "iSts" constr(H) "as" simple_intropattern(s) := iSts H as s ?.
-- 
GitLab