Commit 325ccb75 authored by Ralf Jung's avatar Ralf Jung
Browse files

tac_specialize_assert_pure: do not assume that pure things are persistent

This improves our support for BIs without a persistence modality.
IntoWand needs to be made a bit smarter, but it seems to still work for the cases in the repo.
parent 95b66417
Pipeline #66088 passed with stage
in 6 minutes and 50 seconds
......@@ -1437,6 +1437,13 @@ Qed.
Lemma persistent_and_sep_assoc P `{!Persistent P, !Absorbing P} Q R :
P (Q R) (P Q) R.
Proof. by rewrite -(persistent_persistently P) persistently_and_sep_assoc. Qed.
Lemma persistent_impl_wand_affinely P `{!Persistent P, !Absorbing P} Q :
(P Q) (<affine> P - Q).
Proof.
apply (anti_symm _).
- apply wand_intro_l. rewrite -persistent_and_affinely_sep_l impl_elim_r //.
- apply impl_intro_l. rewrite persistent_and_affinely_sep_l wand_elim_r //.
Qed.
Lemma impl_wand_2 P `{!Persistent P} Q : (P - Q) P Q.
Proof. apply impl_intro_l. by rewrite persistent_and_sep_1 wand_elim_r. Qed.
......
......@@ -432,30 +432,48 @@ Global Instance into_wand_wand p q P Q P' :
Proof.
rewrite /FromAssumption /IntoWand=> HP. by rewrite HP intuitionistically_if_elim.
Qed.
(** Implication instances
Generally we assume [P → ...] is written in cases where that would be
equivalent to [<affine> P -∗ ...], i.e., [P] is absorbing and persistent. The
workhorse of the [IntoWand false] instances (i.e., the implication being taken
from the spatial context) is [persistent_impl_wand_affinely].
If the premise does not come from the intuitionistic context (second parameter [false]),
we add an affinely modality, as if the user had written the magic wand form. *)
(** To make sure this always applies for affine BIs, we also allow [BiAffine] here. *)
Global Instance into_wand_impl_false_false P Q P' :
Absorbing P' Absorbing (P' Q)
FromAssumption false P P' IntoWand false false (P' Q) P Q.
Absorbing P'
TCOr (Persistent P') (BiAffine PROP)
MakeAffinely P' P
IntoWand false false (P' Q) P Q.
Proof.
rewrite /FromAssumption /IntoWand /= => ?? ->. apply wand_intro_r.
by rewrite sep_and impl_elim_l.
rewrite /MakeAffinely /IntoWand /= => ? Hpers <-. apply wand_intro_l.
destruct Hpers.
- rewrite persistent_impl_wand_affinely wand_elim_r //.
- rewrite impl_wand_1 affinely_elim wand_elim_r //.
Qed.
Global Instance into_wand_impl_false_true P Q P' :
Absorbing P' FromAssumption true P P'
Absorbing P'
FromAssumption true P P'
IntoWand false true (P' Q) P Q.
Proof.
rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
rewrite -(persistently_elim P').
rewrite persistent_impl_wand_affinely.
rewrite -(intuitionistically_idemp P) HP.
by rewrite -persistently_and_intuitionistically_sep_l persistently_elim impl_elim_r.
apply wand_elim_r.
Qed.
Global Instance into_wand_impl_true_false P Q P' :
Affine P' FromAssumption false P P'
(* FIXME: use FromAssumption instead of MakeAffinely?
But then needless <affine> modalities get added. *)
MakeAffinely P' P
IntoWand true false (P' Q) P Q.
Proof.
rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
rewrite HP sep_and intuitionistically_elim impl_elim_l //.
rewrite /MakeAffinely /IntoWand /= => <-. apply wand_intro_r.
rewrite sep_and intuitionistically_elim affinely_elim impl_elim_l //.
Qed.
Global Instance into_wand_impl_true_true P Q P' :
FromAssumption true P P' IntoWand true true (P' Q) P Q.
FromAssumption true P P'
IntoWand true true (P' Q) P Q.
Proof.
rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
rewrite sep_and [( (_ _))%I]intuitionistically_elim impl_elim_r //.
......
......@@ -378,7 +378,7 @@ Qed.
Lemma tac_specialize_assert_pure Δ j q a R P1 P2 φ Q :
envs_lookup j Δ = Some (q, R)
IntoWand q true R P1 P2
IntoWand q false R P1 P2
FromPure a P1 φ
φ
match envs_simple_replace j q (Esnoc Enil j P2) Δ with
......@@ -389,10 +389,10 @@ Lemma tac_specialize_assert_pure Δ j q a R P1 P2 φ Q :
Proof.
destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done.
rewrite envs_entails_unseal=> ?????. rewrite envs_simple_replace_singleton_sound //=.
rewrite -intuitionistically_if_idemp (into_wand q true) /=.
rewrite -intuitionistically_if_idemp (into_wand q false) /=.
rewrite -(from_pure a P1) pure_True //.
rewrite -affinely_affinely_if affinely_True_emp.
by rewrite intuitionistically_emp left_id wand_elim_r.
by rewrite left_id wand_elim_r.
Qed.
Lemma tac_specialize_assert_intuitionistic Δ j q P1 P1' P2 R Q :
......
......@@ -210,6 +210,9 @@ Global Instance make_affinely_emp : @KnownMakeAffinely PROP emp emp | 0.
Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_emp. Qed.
Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0.
Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed.
Global Instance make_affinely_default_affine_bi P :
BiAffine PROP MakeAffinely P P | 99.
Proof. intros. by rewrite /MakeAffinely affine_affinely. Qed.
Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
Proof. by rewrite /MakeAffinely. Qed.
......
......@@ -143,6 +143,29 @@ The command has indeed failed with message:
Tactic failure: iSpecialize: cannot solve P using done.
The command has indeed failed with message:
Tactic failure: iSpecialize: Q not persistent.
"test_iSpecialize_impl_pure"
: string
1 goal
PROP : bi
φ : Prop
P, Q : PROP
H : φ
============================
--------------------------------------∗
<affine> ⌜φ⌝
"test_iSpecialize_impl_pure_affine"
: string
1 goal
PROP : bi
BiAffine0 : BiAffine PROP
φ : Prop
P, Q : PROP
H : φ
============================
--------------------------------------∗
⌜φ⌝
"test_iAssert_intuitionistic"
: string
The command has indeed failed with message:
......
......@@ -427,6 +427,36 @@ Proof.
by iFrame "#".
Qed.
Check "test_iSpecialize_impl_pure".
Lemma test_iSpecialize_impl_pure (φ : Prop) P Q :
φ (⌜φ⌝ P) - (⌜φ⌝ Q) - P Q.
Proof.
iIntros (?) "#H1 H2".
(* Adds an affine modality *)
iSpecialize ("H1" with "[]"). { Show. done. }
Restart.
iIntros (?) "#H1 H2".
(* Solving it directly as a pure goal also works. *)
iSpecialize ("H1" with "[% //]").
iSpecialize ("H2" with "[% //]").
by iFrame.
Abort.
Check "test_iSpecialize_impl_pure_affine".
Lemma test_iSpecialize_impl_pure_affine `{!BiAffine PROP} (φ : Prop) P Q :
φ (⌜φ⌝ P) - (⌜φ⌝ Q) - P Q.
Proof.
iIntros (?) "#H1 H2".
(* Does not add an affine modality *)
iSpecialize ("H1" with "[]"). { Show. done. }
Restart.
iIntros (?) "#H1 H2".
(* Solving it directly as a pure goal also works. *)
iSpecialize ("H1" with "[% //]").
iSpecialize ("H2" with "[% //]").
by iFrame.
Abort.
Check "test_iAssert_intuitionistic".
Lemma test_iAssert_intuitionistic `{!BiBUpd PROP} P :
P - |==> P.
......
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