From eacc2cf96028c954b98d27bb0c4742ce238691cd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Jan 2019 13:27:05 +0100
Subject: [PATCH] Fix issue #206.
---
opam | 2 +-
tests/proofmode.v | 12 +++++
theories/proofmode/coq_tactics.v | 10 ++--
theories/proofmode/ltac_tactics.v | 86 +++++++++++++++++++------------
4 files changed, 71 insertions(+), 39 deletions(-)
diff --git a/opam b/opam
index bf1ea8241..290fb30a1 100644
--- a/opam
+++ b/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") }
]
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 477e4787e..c4566b7b4 100644
--- a/tests/proofmode.v
+++ b/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.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index d1321d83d..426f5263c 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/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
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 8d313f3bb..34763324e 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -862,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
--
GitLab