Commit 15946faa authored by Ralf Jung's avatar Ralf Jung
Browse files

add pure precondition to FromModal

parent fd243450
......@@ -315,23 +315,23 @@ Proof. intros. by rewrite /IntoPersistent. Qed.
(** FromModal *)
Global Instance from_modal_affinely P :
FromModal modality_affinely (<affine> P) (<affine> P) P | 2.
FromModal True modality_affinely (<affine> P) (<affine> P) P | 2.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_persistently P :
FromModal modality_persistently (<pers> P) (<pers> P) P | 2.
FromModal True modality_persistently (<pers> P) (<pers> P) P | 2.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_intuitionistically P :
FromModal modality_intuitionistically ( P) ( P) P | 1.
FromModal True modality_intuitionistically ( P) ( P) P | 1.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_intuitionistically_affine_bi P :
BiAffine PROP FromModal modality_persistently ( P) ( P) P | 0.
BiAffine PROP FromModal True modality_persistently ( P) ( P) P | 0.
Proof.
intros. by rewrite /FromModal /= intuitionistically_into_persistently.
Qed.
Global Instance from_modal_absorbingly P :
FromModal modality_id (<absorb> P) (<absorb> P) P.
FromModal True modality_id (<absorb> P) (<absorb> P) P.
Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.
(** IntoWand *)
......
......@@ -33,26 +33,26 @@ Qed.
(* When having a modality nested in an embedding, e.g. [ ⎡|==> P⎤ ], we prefer
the embedding over the modality. *)
Global Instance from_modal_embed P :
FromModal (@modality_embed PROP PROP' _) P P P.
FromModal True (@modality_embed PROP PROP' _) P P P.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_id_embed `(sel : A) P Q :
FromModal modality_id sel P Q
FromModal modality_id sel P Q | 100.
Proof. by rewrite /FromModal /= =><-. Qed.
Global Instance from_modal_affinely_embed `(sel : A) P Q :
FromModal modality_affinely sel P Q
FromModal modality_affinely sel P Q | 100.
Proof. rewrite /FromModal /= =><-. by rewrite embed_affinely_2. Qed.
Global Instance from_modal_persistently_embed `(sel : A) P Q :
FromModal modality_persistently sel P Q
FromModal modality_persistently sel P Q | 100.
Proof. rewrite /FromModal /= =><-. by rewrite embed_persistently. Qed.
Global Instance from_modal_intuitionistically_embed `(sel : A) P Q :
FromModal modality_intuitionistically sel P Q
FromModal modality_intuitionistically sel P Q | 100.
Proof. rewrite /FromModal /= =><-. by rewrite embed_intuitionistically_2. Qed.
Global Instance from_modal_id_embed φ `(sel : A) P Q :
FromModal φ modality_id sel P Q
FromModal φ modality_id sel P Q | 100.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ. Qed.
Global Instance from_modal_affinely_embed φ `(sel : A) P Q :
FromModal φ modality_affinely sel P Q
FromModal φ modality_affinely sel P Q | 100.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // embed_affinely_2. Qed.
Global Instance from_modal_persistently_embed φ `(sel : A) P Q :
FromModal φ modality_persistently sel P Q
FromModal φ modality_persistently sel P Q | 100.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // embed_persistently. Qed.
Global Instance from_modal_intuitionistically_embed φ `(sel : A) P Q :
FromModal φ modality_intuitionistically sel P Q
FromModal φ modality_intuitionistically sel P Q | 100.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // embed_intuitionistically_2. Qed.
Global Instance into_wand_embed p q R P Q :
IntoWand p q R P Q IntoWand p q R P Q.
......@@ -139,16 +139,16 @@ Global Instance is_except_0_embed `{!BiEmbedLater PROP PROP'} P :
IsExcept0 P IsExcept0 P.
Proof. by rewrite /IsExcept0 -embed_except_0=>->. Qed.
Global Instance from_modal_later_embed `{!BiEmbedLater PROP PROP'} `(sel : A) n P Q :
FromModal (modality_laterN n) sel P Q
FromModal (modality_laterN n) sel P Q.
Proof. rewrite /FromModal /= =><-. by rewrite embed_laterN. Qed.
Global Instance from_modal_later_embed `{!BiEmbedLater PROP PROP'} φ `(sel : A) n P Q :
FromModal φ (modality_laterN n) sel P Q
FromModal φ (modality_laterN n) sel P Q.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // embed_laterN. Qed.
Global Instance from_modal_plainly_embed
`{!BiPlainly PROP, !BiPlainly PROP', !BiEmbedPlainly PROP PROP'} `(sel : A) P Q :
FromModal modality_plainly sel P Q
FromModal (PROP2:=PROP') modality_plainly sel P Q | 100.
Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed.
`{!BiPlainly PROP, !BiPlainly PROP', !BiEmbedPlainly PROP PROP'} φ `(sel : A) P Q :
FromModal φ modality_plainly sel P Q
FromModal φ (PROP2:=PROP') modality_plainly sel P Q | 100.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // embed_plainly. Qed.
Global Instance into_internal_eq_embed
`{!BiInternalEq PROP, !BiInternalEq PROP', !BiEmbedInternalEq PROP PROP'}
......
......@@ -17,7 +17,7 @@ Global Instance into_pure_eq {A : ofe} (a b : A) :
Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
Global Instance from_modal_Next {A : ofe} (x y : A) :
FromModal (PROP1:=PROP) (PROP2:=PROP) (modality_laterN 1)
FromModal (PROP1:=PROP) (PROP2:=PROP) True (modality_laterN 1)
(^1 (x y) : PROP)%I (Next x Next y) (x y).
Proof. by rewrite /FromModal /= later_equivI. Qed.
......@@ -47,4 +47,4 @@ Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
Global Instance into_internal_eq_persistently {A : ofe} (x y : A) P :
IntoInternalEq P x y IntoInternalEq (<pers> P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
End class_instances_internal_eq.
\ No newline at end of file
End class_instances_internal_eq.
......@@ -205,12 +205,13 @@ Proof. by rewrite /IsExcept0 except_0_later. Qed.
(** FromModal *)
Global Instance from_modal_later P :
FromModal (modality_laterN 1) (^1 P) ( P) P.
FromModal True (modality_laterN 1) (^1 P) ( P) P.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_laterN n P :
FromModal (modality_laterN n) (^n P) (^n P) P.
FromModal True (modality_laterN n) (^n P) (^n P) P.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_except_0 P : FromModal modality_id ( P) ( P) P.
Global Instance from_modal_except_0 P :
FromModal True modality_id ( P) ( P) P.
Proof. by rewrite /FromModal /= -except_0_intro. Qed.
(** IntoExcept0 *)
......
......@@ -88,7 +88,7 @@ Global Instance from_forall_plainly {A} P (Φ : A → PROP) name :
Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
Global Instance from_modal_plainly P :
FromModal modality_plainly ( P) ( P) P | 2.
FromModal True modality_plainly ( P) ( P) P | 2.
Proof. by rewrite /FromModal. Qed.
Global Instance into_except_0_plainly `{!BiPlainlyExist PROP} P Q :
......
......@@ -124,10 +124,10 @@ Global Instance is_except_0_fupd `{!BiFUpd PROP} E1 E2 P :
Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
Global Instance from_modal_bupd `{!BiBUpd PROP} P :
FromModal modality_id (|==> P) (|==> P) P.
FromModal True modality_id (|==> P) (|==> P) P.
Proof. by rewrite /FromModal /= -bupd_intro. Qed.
Global Instance from_modal_fupd E P `{!BiFUpd PROP} :
FromModal modality_id (|={E}=> P) (|={E}=> P) P.
FromModal True modality_id (|={E}=> P) (|={E}=> P) P.
Proof. by rewrite /FromModal /= -fupd_intro. Qed.
Global Instance elim_modal_bupd `{!BiBUpd PROP} p P Q :
......
......@@ -96,8 +96,9 @@ Global Arguments IntoPersistent {_} _ _%I _%I : simpl never.
Global Arguments into_persistent {_} _ _%I _%I {_}.
Global Hint Mode IntoPersistent + + ! - : typeclass_instances.
(** The [FromModal M sel P Q] class is used by the [iModIntro] tactic to transform
a goal [P] into a modality [M] and proposition [Q].
(** The [FromModal M sel P Q] class is used by the [iModIntro] tactic to
transform a goal [P] into a modality [M] and proposition [Q], under additional
pure assumptions [φ].
The inputs are [P] and [sel] and the outputs are [M] and [Q].
......@@ -113,11 +114,11 @@ instance only imposes the proof obligation [P ⊢ N P]. Examples of such
modalities [N] are [bupd], [fupd], [except_0], [monPred_subjectively] and
[bi_absorbingly]. *)
Class FromModal {PROP1 PROP2 : bi} {A}
(M : modality PROP1 PROP2) (sel : A) (P : PROP2) (Q : PROP1) :=
from_modal : M Q P.
Global Arguments FromModal {_ _ _} _ _%I _%I _%I : simpl never.
Global Arguments from_modal {_ _ _} _ _ _%I _%I {_}.
Global Hint Mode FromModal - + - - - ! - : typeclass_instances.
(φ : Prop) (M : modality PROP1 PROP2) (sel : A) (P : PROP2) (Q : PROP1) :=
from_modal : φ M Q P.
Global Arguments FromModal {_ _ _} _ _ _%I _%I _%I : simpl never.
Global Arguments from_modal {_ _ _} _ _ _ _%I _%I {_}.
Global Hint Mode FromModal - + - - - - ! - : typeclass_instances.
(** The [FromAffinely P Q] class is used to add an [<affine>] modality to the
proposition [Q].
......@@ -645,8 +646,8 @@ Global Instance from_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PRO
Global Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A PROP) :
IntoForall P Φ IntoForall (tc_opaque P) Φ := id.
Global Instance from_modal_tc_opaque {PROP1 PROP2 : bi} {A}
M (sel : A) (P : PROP2) (Q : PROP1) :
FromModal M sel P Q FromModal M sel (tc_opaque P) Q := id.
φ M (sel : A) (P : PROP2) (Q : PROP1) :
FromModal φ M sel P Q FromModal φ M sel (tc_opaque P) Q := id.
Global Instance elim_modal_tc_opaque {PROP : bi} φ p p' (P P' Q Q' : PROP) :
ElimModal φ p p' P P' Q Q' ElimModal φ p p' (tc_opaque P) P' Q Q' := id.
Global Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
......
......@@ -1029,14 +1029,15 @@ Section tac_modal_intro.
Qed.
(** The actual introduction tactic *)
Lemma tac_modal_intro {A} (sel : A) Γp Γs n Γp' Γs' Q Q' fi :
FromModal M sel Q' Q
Lemma tac_modal_intro {A} φ (sel : A) Γp Γs n Γp' Γs' Q Q' fi :
FromModal φ M sel Q' Q
IntoModalIntuitionisticEnv M Γp Γp' (modality_intuitionistic_action M)
IntoModalSpatialEnv M Γs Γs' (modality_spatial_action M) fi
(if fi then Absorbing Q' else TCTrue)
φ
envs_entails (Envs Γp' Γs' n) Q envs_entails (Envs Γp Γs n) Q'.
Proof.
rewrite envs_entails_eq /FromModal !of_envs_eq => HQ' HΓp HΓs ? HQ.
rewrite envs_entails_eq /FromModal !of_envs_eq => HQ' HΓp HΓs ? Hφ HQ.
apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs' n)) as Hwf.
{ split; simpl in *.
- destruct HΓp as [| |????? []| |]; eauto using Enil_wf.
......@@ -1060,19 +1061,19 @@ Section tac_modal_intro.
move: HQ'; rewrite -HQ pure_True // left_id HMp=> HQ' {HQ Hwf HMp}.
remember (modality_spatial_action M).
destruct HΓs as [? M|M C Γs ?%TCForall_Forall|? M C Γs Γs' fi []|? M Γs|M Γs]; simpl.
- by rewrite -HQ' /= !right_id.
- rewrite -HQ' {1}(modality_spatial_forall_big_sep _ _ Γs) //.
- by rewrite -HQ' //= !right_id.
- rewrite -HQ' // {1}(modality_spatial_forall_big_sep _ _ Γs) //.
by rewrite modality_sep.
- destruct fi.
+ rewrite -(absorbing Q') /bi_absorbingly -HQ' (comm _ True%I).
+ rewrite -(absorbing Q') /bi_absorbingly -HQ' // (comm _ True%I).
rewrite -modality_sep -assoc. apply sep_mono_r.
eauto using modality_spatial_transform.
+ rewrite -HQ' -modality_sep. apply sep_mono_r.
+ rewrite -HQ' // -modality_sep. apply sep_mono_r.
rewrite -(right_id emp%I bi_sep (M _)).
eauto using modality_spatial_transform.
- rewrite -HQ' /= right_id comm -{2}(modality_spatial_clear M) //.
- rewrite -HQ' //= right_id comm -{2}(modality_spatial_clear M) //.
by rewrite (True_intro ([] Γs)).
- rewrite -HQ' {1}(modality_spatial_id M ([] Γs)) //.
- rewrite -HQ' // {1}(modality_spatial_id M ([] Γs)) //.
by rewrite -modality_sep.
Qed.
End tac_modal_intro.
......
......@@ -1385,7 +1385,7 @@ Local Tactic Notation "iExistDestruct" constr(H)
(** * Modality introduction *)
Tactic Notation "iModIntro" uconstr(sel) :=
iStartProof;
notypeclasses refine (tac_modal_intro _ sel _ _ _ _ _ _ _ _ _ _ _ _ _);
notypeclasses refine (tac_modal_intro _ _ sel _ _ _ _ _ _ _ _ _ _ _ _ _ _);
[iSolveTC ||
fail "iModIntro: the goal is not a modality"
|iSolveTC ||
......@@ -1402,6 +1402,7 @@ Tactic Notation "iModIntro" uconstr(sel) :=
end
|pm_reduce; iSolveTC ||
fail "iModIntro: cannot filter spatial context when goal is not absorbing"
|iSolveSideCondition
|pm_prettify (* reduce redexes created by instantiation *)
(* subgoal *) ].
Tactic Notation "iModIntro" := iModIntro _.
......
......@@ -55,35 +55,40 @@ Implicit Types φ : Prop.
Implicit Types i j : I.
Global Instance from_modal_objectively P :
FromModal modality_objectively (<obj> P) (<obj> P) P | 1.
FromModal True modality_objectively (<obj> P) (<obj> P) P | 1.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_subjectively P :
FromModal modality_id (<subj> P) (<subj> P) P | 1.
FromModal True modality_id (<subj> P) (<subj> P) P | 1.
Proof. by rewrite /FromModal /= -monPred_subjectively_intro. Qed.
Global Instance from_modal_affinely_monPred_at `(sel : A) P Q 𝓠 i :
FromModal modality_affinely sel P Q MakeMonPredAt i Q 𝓠
FromModal modality_affinely sel (P i) 𝓠 | 0.
Global Instance from_modal_affinely_monPred_at φ `(sel : A) P Q 𝓠 i :
FromModal φ modality_affinely sel P Q
MakeMonPredAt i Q 𝓠
FromModal φ modality_affinely sel (P i) 𝓠 | 0.
Proof.
rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_affinely.
rewrite /FromModal /MakeMonPredAt /==> HPQ <- ?.
by rewrite -HPQ // monPred_at_affinely.
Qed.
Global Instance from_modal_persistently_monPred_at `(sel : A) P Q 𝓠 i :
FromModal modality_persistently sel P Q MakeMonPredAt i Q 𝓠
FromModal modality_persistently sel (P i) 𝓠 | 0.
Global Instance from_modal_persistently_monPred_at φ `(sel : A) P Q 𝓠 i :
FromModal φ modality_persistently sel P Q
MakeMonPredAt i Q 𝓠
FromModal φ modality_persistently sel (P i) 𝓠 | 0.
Proof.
rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_persistently.
rewrite /FromModal /MakeMonPredAt /==> HPQ <- ?.
by rewrite -HPQ // monPred_at_persistently.
Qed.
Global Instance from_modal_intuitionistically_monPred_at `(sel : A) P Q 𝓠 i :
FromModal modality_intuitionistically sel P Q MakeMonPredAt i Q 𝓠
FromModal modality_intuitionistically sel (P i) 𝓠 | 0.
Global Instance from_modal_intuitionistically_monPred_at φ `(sel : A) P Q 𝓠 i :
FromModal φ modality_intuitionistically sel P Q
MakeMonPredAt i Q 𝓠
FromModal φ modality_intuitionistically sel (P i) 𝓠 | 0.
Proof.
rewrite /FromModal /MakeMonPredAt /==> <- <-.
by rewrite monPred_at_affinely monPred_at_persistently.
rewrite /FromModal /MakeMonPredAt /==> HPQ <- ?.
by rewrite -HPQ // monPred_at_affinely monPred_at_persistently.
Qed.
Global Instance from_modal_id_monPred_at `(sel : A) P Q 𝓠 i :
FromModal modality_id sel P Q MakeMonPredAt i Q 𝓠
FromModal modality_id sel (P i) 𝓠.
Proof. by rewrite /FromModal /MakeMonPredAt=> <- <-. Qed.
Global Instance from_modal_id_monPred_at φ `(sel : A) P Q 𝓠 i :
FromModal φ modality_id sel P Q MakeMonPredAt i Q 𝓠
FromModal φ modality_id sel (P i) 𝓠.
Proof. rewrite /FromModal /MakeMonPredAt=> HPQ <- ?. by rewrite -HPQ. Qed.
Global Instance make_monPred_at_pure φ i : MakeMonPredAt i ⌜φ⌝ ⌜φ⌝.
Proof. by rewrite /MakeMonPredAt monPred_at_pure. Qed.
......@@ -511,11 +516,13 @@ Proof.
rewrite /IntoLaterN /MaybeIntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
by rewrite monPred_at_later.
Qed.
Global Instance from_later_monPred_at i `(sel : A) n P Q 𝓠 :
FromModal (modality_laterN n) sel P Q MakeMonPredAt i Q 𝓠
FromModal (modality_laterN n) sel (P i) 𝓠.
Global Instance from_later_monPred_at i φ `(sel : A) n P Q 𝓠 :
FromModal φ (modality_laterN n) sel P Q
MakeMonPredAt i Q 𝓠
FromModal φ (modality_laterN n) sel (P i) 𝓠.
Proof.
rewrite /FromModal /MakeMonPredAt=> <- <-. elim n=>//= ? ->.
rewrite /FromModal /MakeMonPredAt=> HPQ <- ?. rewrite -HPQ //.
elim n=>//= ? ->.
by rewrite monPred_at_later.
Qed.
......
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