Commit 30890193 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make `[#]` produce goal with `<pers>` modality if premise is not persistent.

This is an alternative for !216. This closes issue #186.
parent 628000da
......@@ -98,8 +98,17 @@ The command has indeed failed with message:
Tactic failure: iSpecialize: Q not persistent.
"test_iAssert_intuitionistic"
: string
The command has indeed failed with message:
Tactic failure: iSpecialize: (|==> P)%I not persistent.
1 subgoal
PROP : bi
BiBUpd0 : BiBUpd PROP
P : PROP
============================
"HP" : P
"HPupd1" : |==> P
--------------------------------------□
<pers> (|==> P)
The command has indeed failed with message:
Tactic failure: iSpecialize: cannot instantiate (∀ _ : φ, P -∗ False)%I with
P.
......
......@@ -239,8 +239,10 @@ Proof.
iIntros "#HP".
(* Test that [HPupd1] ends up in the intuitionistic context *)
iAssert (|==> P)%I with "[]" as "#HPupd1"; first done.
(* This should not work, [|==> P] is not persistent. *)
Fail iAssert (|==> P)%I with "[#]" as "#HPupd2"; first done.
(* Since [|==> P] is not persistent, this should create a goal with a <pers>
modality. *)
iAssert (|==> P)%I with "[#]" as "#HPupd2".
{ Show. done. }
done.
Qed.
......
......@@ -393,21 +393,20 @@ Qed.
Lemma tac_specialize_assert_intuitionistic Δ j q P1 P1' P2 R Q :
envs_lookup j Δ = Some (q, R)
IntoWand q true R P1 P2
Persistent P1
IntoAbsorbingly P1' P1
MakePersistently P1 P1'
envs_entails (envs_delete true j q Δ) P1'
match envs_simple_replace j q (Esnoc Enil j P2) Δ with
| Some Δ'' => envs_entails Δ'' Q
| None => False
end envs_entails Δ Q.
Proof.
rewrite envs_entails_eq => ???? HP1 HQ.
rewrite /MakePersistently envs_entails_eq => ?? HP HΔ HQ.
destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:?; last done.
rewrite -HQ envs_lookup_sound //.
rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))).
rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
rewrite {1}HP1 (into_absorbingly P1' P1) (persistent_persistently_2 P1).
rewrite absorbingly_elim_persistently persistently_and_intuitionistically_sep_l assoc.
rewrite {1}HΔ -HP.
rewrite persistently_and_intuitionistically_sep_l assoc.
rewrite -intuitionistically_if_idemp -intuitionistically_idemp.
rewrite (intuitionistically_intuitionistically_if q).
by rewrite intuitionistically_if_sep_2 (into_wand q true) wand_elim_l wand_elim_r.
......
......@@ -911,14 +911,11 @@ Ltac iSpecializePat_go H1 pats :=
|pm_reduce;
iSpecializePat_go H1 pats]
| SGoal (SpecGoal GIntuitionistic false ?Hs_frame [] ?d) :: ?pats =>
notypeclasses refine (tac_specialize_assert_intuitionistic _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
notypeclasses refine (tac_specialize_assert_intuitionistic _ H1 _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity ||
let H1 := pretty_ident H1 in
fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|iSolveTC ||
let Q := match goal with |- Persistent ?Q => Q end in
fail "iSpecialize:" Q "not persistent"
|iSolveTC
|pm_reduce; iFrame Hs_frame; solve_done d (*goal*)
|pm_reduce; iSpecializePat_go H1 pats]
......
Supports Markdown
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