Commit eacc2cf9 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix issue #206.

parent e76659e6
......@@ -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") }
]
......@@ -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.
......
......@@ -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
......
......@@ -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
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment