From 1fcbf67911676ad2fb1b4a3a2fa7e4de28321060 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 3 Dec 2019 12:25:31 +0100
Subject: [PATCH] Strengthen `tac_specialize_assert` to put the result in the
 intuitionistic context.

The result of `iSpecialize ("H" with "[H1 .. Hn]")` was always put in the
spatial context. This commit strenghtens this tactic by putting the result
in the intuitionistic context if the following conditions hold:

1. The hypothesis `H` is persistent.
2. All the hypotheses `H1 .. Hn` are intuitionistic (or similarly, in case
   `[-H1 .. Hn]` is used, if all remaining hypotheses are intuitionistic).
3. If the pattern `[> ..]` for adding a modality is not used.
---
 theories/proofmode/coq_tactics.v  | 21 ++++++++++++++-------
 theories/proofmode/ltac_tactics.v |  8 +++-----
 2 files changed, 17 insertions(+), 12 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 757a3b6c6..5720969d2 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -286,13 +286,14 @@ Proof.
   - by rewrite HR assoc !wand_elim_r.
 Qed.
 
-Lemma tac_specialize_assert Δ j q neg js R P1 P2 P1' Q :
+Lemma tac_specialize_assert Δ j (q am neg : bool) js R P1 P2 P1' Q :
   envs_lookup j Δ = Some (q, R) →
-  IntoWand q false R P1 P2 → AddModal P1' P1 Q →
+  IntoWand q false R P1 P2 →
+  (if am then AddModal P1' P1 Q else TCEq P1' P1) →
   match
     ''(Δ1,Δ2) ← envs_split (if neg is true then Right else Left)
-    js (envs_delete true j q Δ);
-    Δ2' ← envs_app false (Esnoc Enil j P2) Δ2;
+                           js (envs_delete true j q Δ);
+    Δ2' ← envs_app (negb am &&& q &&& env_spatial_is_nil Δ1) (Esnoc Enil j P2) Δ2;
     Some (Δ1,Δ2') (* does not preserve position of [j] *)
   with
   | Some (Δ1,Δ2') =>
@@ -301,15 +302,21 @@ Lemma tac_specialize_assert Δ j q neg js R P1 P2 P1' Q :
   | None => False
   end → envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq. intros ??? HQ.
+  rewrite envs_entails_eq. intros ?? Hmod HQ.
   destruct (_ ≫= _) as [[Δ1 Δ2']|] eqn:?; last done.
   destruct HQ as [HP1 HQ].
   destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
     destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
   rewrite envs_lookup_sound // envs_split_sound //.
   rewrite (envs_app_singleton_sound Δ2) //; simpl.
-  rewrite HP1 (into_wand q false) /= -(add_modal P1' P1 Q). cancel [P1'].
-  apply wand_intro_l. by rewrite assoc !wand_elim_r.
+  rewrite -intuitionistically_if_idemp (into_wand q false) /=.
+  destruct (negb am &&& q &&& env_spatial_is_nil Δ1) eqn:Hp; simpl.
+  - move: Hp. rewrite !lazy_andb_true negb_true. intros [[-> ->] ?]; simpl.
+    destruct Hmod. rewrite env_spatial_is_nil_intuitionistically // HP1.
+    by rewrite assoc intuitionistically_sep_2 wand_elim_l wand_elim_r HQ.
+  - rewrite intuitionistically_if_elim HP1. destruct am; last destruct Hmod.
+    + by rewrite assoc -(comm _ P1') -assoc wand_trans HQ.
+    + by rewrite assoc wand_elim_l wand_elim_r HQ.
 Qed.
 
 Lemma tac_unlock_emp Δ Q : envs_entails Δ Q → envs_entails Δ (emp ∗ locked Q).
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index d9ff74e69..db77fe7dd 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -903,15 +903,13 @@ Ltac iSpecializePat_go H1 pats :=
        fail "iSpecialize: cannot select hypotheses for intuitionistic premise"
     | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
        let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
-       notypeclasses refine (tac_specialize_assert _ H1 _ lr Hs' _ _ _ _ _ _ _ _ _);
+       notypeclasses refine (tac_specialize_assert _ H1 _
+           (if m is GModal then true else false) lr Hs' _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H1 := pretty_ident H1 in
           fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
-         |lazymatch m with
-          | GSpatial => class_apply add_modal_id
-          | GModal => iSolveTC || fail "iSpecialize: goal not a modality"
-          end
+         |iSolveTC || fail "iSpecialize: goal not a modality"
          |pm_reduce;
           lazymatch goal with
           | |- False =>
-- 
GitLab