Merge branch 'robbert/issue_206' into 'master'

Fix issue #206

Closes #206

See merge request FP/iris-coq!199

opam

@@ -11,5 +11,5 @@ install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { (>= "8.7.1" & < "8.10~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2018-12-12.0.9cbafb67") | (= "dev") }
+  "coq-stdpp" { (= "dev.2019-01-13.0.48758ab8") | (= "dev") }
 ]

tests/proofmode.v

@@ -60,6 +60,18 @@ Proof. iIntros "[#? _] [_ #?]". Show. auto. Qed.
 Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P → Q → P ∧ Q)%I.
 Proof. iIntros "H1 #H2". by iFrame "∗#". Qed.
 
+Lemma test_iDestruct_intuitionistic_1 P Q `{!Persistent P}:
+  Q ∗ □ (Q -∗ P) -∗ P ∗ Q.
+Proof. iIntros "[HQ #HQP]". iDestruct ("HQP" with "HQ") as "#HP". by iFrame. Qed.
+
+Lemma test_iDestruct_intuitionistic_2 P Q `{!Persistent P, !Affine P}:
+  Q ∗ (Q -∗ P) -∗ P.
+Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". done. Qed.
+
+Lemma test_iDestruct_intuitionistic_affine_bi `{BiAffine PROP} P Q `{!Persistent P}:
+  Q ∗ (Q -∗ P) -∗ P ∗ Q.
+Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". by iFrame. Qed.
+
 Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → (⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P)%I.
 Proof. iIntros (??) "H". auto. Qed.
 

theories/proofmode/coq_tactics.v

@@ -311,18 +311,20 @@ Qed.
 
 Lemma tac_specialize_intuitionistic_helper Δ Δ'' j q P R R' Q :
   envs_lookup j Δ = Some (q,P) →
+  (if q then TCTrue else BiAffine PROP) →
   envs_entails Δ (<absorb> R) →
   IntoPersistent false R R' →
-  (if q then TCTrue else BiAffine PROP) →
   envs_replace j q true (Esnoc Enil j R') Δ = Some Δ'' →
   envs_entails Δ'' Q → envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq => ? HR ? Hpos ? <-. rewrite -(idemp bi_and (of_envs Δ)) {1}HR.
+  rewrite envs_entails_eq => ?? HR ?? <-. rewrite -(idemp bi_and (of_envs Δ)) {1}HR.
   rewrite envs_replace_singleton_sound //; destruct q; simpl.
   - by rewrite (_ : R = <pers>?false R)%I // (into_persistent _ R)
-      absorbingly_elim_persistently sep_elim_r persistently_and_intuitionistically_sep_l wand_elim_r.
+      absorbingly_elim_persistently sep_elim_r
+      persistently_and_intuitionistically_sep_l wand_elim_r.
   - by rewrite (absorbing_absorbingly R) (_ : R = <pers>?false R)%I //
-       (into_persistent _ R) sep_elim_r persistently_and_intuitionistically_sep_l wand_elim_r.
+      (into_persistent _ R) sep_elim_r
+      persistently_and_intuitionistically_sep_l wand_elim_r.
 Qed.
 
 (* A special version of [tac_assumption] that does not do any of the

theories/proofmode/ltac_tactics.v

@@ -52,6 +52,9 @@ Ltac iTypeOf H :=
   let Δ := match goal with |- envs_entails ?Δ _ => Δ end in
   pm_eval (envs_lookup H Δ).
 
+Ltac iBiOfGoal :=
+  match goal with |- @envs_entails ?PROP _ _ => PROP end.
+
 Tactic Notation "iMatchHyp" tactic1(tac) :=
   match goal with
   | |- context[ environments.Esnoc _ ?x ?P ] => tac x P
@@ -859,40 +862,58 @@ Tactic Notation "iSpecializeCore" open_constr(H)
     | _ => H
     end in
   iSpecializeArgs H xs; [..|
-  lazymatch type of H with
-  | ident =>
-    (* The lemma [tac_specialize_intuitionistic_helper] allows one to use all
-    spatial hypotheses for both proving the premises of the lemma we
-    specialize as well as those of the remaining goal. We can only use it when
-    the result of the specialization is intuitionistic, and no modality is
-    eliminated. We do not use [tac_specialize_intuitionistic_helper] in the case
-    only universal quantifiers and no implications or wands are instantiated
-    (i.e [pat = []]) because it is a.) not needed, and b.) more efficient. *)
-    let pat := spec_pat.parse pat in
-    lazymatch eval compute in
-      (p && bool_decide (pat ≠ []) && negb (existsb spec_pat_modal pat)) with
-    | true =>
-       (* FIXME: do something reasonable when the BI is not affine *)
-       notypeclasses refine (tac_specialize_intuitionistic_helper _ _ H _ _ _ _ _ _ _ _ _ _ _);
-         [pm_reflexivity ||
-          let H := pretty_ident H in
-          fail "iSpecialize:" H "not found"
-         |iSpecializePat H pat;
-           [..
-           |notypeclasses refine (tac_specialize_intuitionistic_helper_done _ H _ _ _);
-            pm_reflexivity]
-         |iSolveTC ||
-          let Q := match goal with |- IntoPersistent _ ?Q _ => Q end in
-          fail "iSpecialize:" Q "not persistent"
-         |pm_reduce; iSolveTC ||
-          let Q := match goal with |- TCAnd _ (Affine ?Q) => Q end in
-          fail "iSpecialize:" Q "not affine"
-         |pm_reflexivity
-         |(* goal *)]
-    | false => iSpecializePat H pat
-    end
-  | _ => fail "iSpecialize:" H "should be a hypothesis, use iPoseProof instead"
-  end].
+    lazymatch type of H with
+    | ident =>
+       (* The lemma [tac_specialize_intuitionistic_helper] allows one to use the
+       whole spatial context for:
+       - proving the premises of the lemma we specialize, and,
+       - the remaining goal.
+
+       We can only use if all of the following properties hold:
+       - The result of the specialization is persistent.
+       - No modality is eliminated.
+       - If the BI is not affine, the hypothesis should be in the intuitionistic
+         context.
+
+       As an optimization, we do only use [tac_specialize_intuitionistic_helper]
+       if no implications nor wands are eliminated, i.e. [pat ≠ []]. *)
+       let pat := spec_pat.parse pat in
+       lazymatch eval compute in
+         (p && bool_decide (pat ≠ []) && negb (existsb spec_pat_modal pat)) with
+       | true =>
+          (* Check that if the BI is not affine, the hypothesis is in the
+          intuitionistic context. *)
+          lazymatch iTypeOf H with
+          | Some (?q, _) =>
+             let PROP := iBiOfGoal in
+             lazymatch eval compute in (q || tc_to_bool (BiAffine PROP)) with
+             | true =>
+                notypeclasses refine (tac_specialize_intuitionistic_helper _ _ H _ _ _ _ _ _ _ _ _ _ _);
+                  [pm_reflexivity
+                   (* This premise, [envs_lookup j Δ = Some (q,P)],
+                   holds because [iTypeOf] succeeded *)
+                  |pm_reduce; iSolveTC
+                   (* This premise, [if q then TCTrue else BiAffine PROP],
+                   holds because [q || TC_to_bool (BiAffine PROP)] is true *)
+                  |iSpecializePat H pat;
+                    [..
+                    |notypeclasses refine (tac_specialize_intuitionistic_helper_done _ H _ _ _);
+                     pm_reflexivity]
+                  |iSolveTC ||
+                   let Q := match goal with |- IntoPersistent _ ?Q _ => Q end in
+                   fail "iSpecialize:" Q "not persistent"
+                  |pm_reflexivity
+                  |(* goal *)]
+             | false => iSpecializePat H pat
+             end
+          | None =>
+             let H := pretty_ident H in
+             fail "iSpecialize:" H "not found"
+          end
+       | false => iSpecializePat H pat
+       end
+    | _ => fail "iSpecialize:" H "should be a hypothesis, use iPoseProof instead"
+    end].
 
 Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
   lazymatch type of t with