Commit 44c5c039 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'robbert/ElimModal' into 'gen_proofmode'

Extend ElimModal with Boolean flags to specify whether it operates on the…

See merge request FP/iris-coq!129
parents 9bdda372 e65f83ad
......@@ -93,12 +93,12 @@ Section proofs.
Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N.
Global Instance elim_inv_cinv p γ E N P Q Q' :
( R, ElimModal True (|={E,E∖↑N}=> R) R Q Q')
( R, ElimModal True false false (|={E,E∖↑N}=> R) R Q Q')
ElimInv (N E) (cinv N γ P) (cinv_own γ p)
( P cinv_own γ p) ( P ={E∖↑N,E}= True) Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&Hown&H2)".
iApply Helim; [done|]. iSplitR "H2"; [|done].
iApply Helim; [done|]; simpl. iSplitR "H2"; [|done].
iMod (cinv_open E N γ p P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto.
by iFrame.
Qed.
......
......@@ -110,11 +110,11 @@ Qed.
Global Instance into_inv_inv N P : IntoInv (inv N P) N.
Global Instance elim_inv_inv E N P Q Q' :
( R, ElimModal True (|={E,E∖↑N}=> R) R Q Q')
( R, ElimModal True false false (|={E,E∖↑N}=> R) R Q Q')
ElimInv (N E) (inv N P) True ( P) ( P ={E∖↑N,E}= True) Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&_&H2)".
iApply (Helim with "[H2]"); [done|]. iSplitR "H2"; [|done].
iApply (Helim with "[H2]"); [done|]; simpl. iSplitR "H2"; [|done].
iMod (inv_open _ N with "[#]") as "(HP&Hclose)"; auto with iFrame.
Qed.
......
......@@ -113,12 +113,12 @@ Section proofs.
Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N.
Global Instance elim_inv_na p F E N P Q Q':
( R, ElimModal True (|={E}=> R)%I R Q Q')
( R, ElimModal True false false (|={E}=> R)%I R Q Q')
ElimInv (N E N F) (na_inv p N P) (na_own p F)
( P na_own p (F∖↑N)) ( P na_own p (F∖↑N) ={E}= na_own p F) Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim (?&?)) "(#H1&Hown&H2)".
iApply Helim; [done|]. iSplitR "H2"; [|done].
iApply Helim; [done|]; simpl. iSplitR "H2"; [|done].
iMod (na_inv_open p E F N P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto.
by iFrame.
Qed.
......
......@@ -29,8 +29,11 @@ Module savedprop. Section savedprop.
Instance bupd_mono' : Proper (() ==> ()) bupd.
Proof. intros P Q ?. by apply bupd_mono. Qed.
Instance elim_modal_bupd P Q : ElimModal True (|==> P) P (|==> Q) (|==> Q).
Proof. by rewrite /ElimModal bupd_frame_r bi.wand_elim_r bupd_trans. Qed.
Instance elim_modal_bupd p P Q : ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
Proof.
by rewrite /ElimModal bi.intuitionistically_if_elim
bupd_frame_r bi.wand_elim_r bupd_trans.
Qed.
(** A bad recursive reference: "Assertion with name [i] does not hold" *)
Definition A (i : ident) : PROP := ( P, ¬ P saved i P)%I.
......@@ -127,12 +130,18 @@ Module inv. Section inv.
Lemma fupd_frame_r E P Q : fupd E P Q fupd E (P Q).
Proof. by rewrite comm fupd_frame_l comm. Qed.
Global Instance elim_fupd_fupd E P Q : ElimModal True (fupd E P) P (fupd E Q) (fupd E Q).
Proof. by rewrite /ElimModal fupd_frame_r bi.wand_elim_r fupd_fupd. Qed.
Global Instance elim_fupd_fupd p E P Q :
ElimModal True p false (fupd E P) P (fupd E Q) (fupd E Q).
Proof.
by rewrite /ElimModal bi.intuitionistically_if_elim
fupd_frame_r bi.wand_elim_r fupd_fupd.
Qed.
Global Instance elim_fupd0_fupd1 P Q : ElimModal True (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
Global Instance elim_fupd0_fupd1 p P Q :
ElimModal True p false (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
Proof.
by rewrite /ElimModal fupd_frame_r bi.wand_elim_r fupd_mask_mono fupd_fupd.
by rewrite /ElimModal bi.intuitionistically_if_elim
fupd_frame_r bi.wand_elim_r fupd_mask_mono fupd_fupd.
Qed.
Global Instance exists_split_fupd0 {A} E P (Φ : A PROP) :
......
......@@ -384,19 +384,28 @@ Section proofmode_classes.
Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E [{ Φ }]).
Proof. by rewrite /IsExcept0 -{2}fupd_twp -except_0_fupd -fupd_intro. Qed.
Global Instance elim_modal_bupd_twp s E e P Φ :
ElimModal True (|==> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r wand_elim_r fupd_twp. Qed.
Global Instance elim_modal_bupd_twp p s E e P Φ :
ElimModal True p false (|==> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
Proof.
by rewrite /ElimModal intuitionistically_if_elim
(bupd_fupd E) fupd_frame_r wand_elim_r fupd_twp.
Qed.
Global Instance elim_modal_fupd_twp s E e P Φ :
ElimModal True (|={E}=> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_twp. Qed.
Global Instance elim_modal_fupd_twp p s E e P Φ :
ElimModal True p false (|={E}=> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
Proof.
by rewrite /ElimModal intuitionistically_if_elim
fupd_frame_r wand_elim_r fupd_twp.
Qed.
Global Instance elim_modal_fupd_twp_atomic s E1 E2 e P Φ :
Global Instance elim_modal_fupd_twp_atomic p s E1 E2 e P Φ :
Atomic (stuckness_to_atomicity s) e
ElimModal True (|={E1,E2}=> P) P
ElimModal True p false (|={E1,E2}=> P) P
(WP e @ s; E1 [{ Φ }]) (WP e @ s; E2 [{ v, |={E2,E1}=> Φ v }])%I.
Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r twp_atomic. Qed.
Proof.
intros. by rewrite /ElimModal intuitionistically_if_elim
fupd_frame_r wand_elim_r twp_atomic.
Qed.
Global Instance add_modal_fupd_twp s E e P Φ :
AddModal (|={E}=> P) P (WP e @ s; E [{ Φ }]).
......
......@@ -378,19 +378,28 @@ Section proofmode_classes.
Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E {{ Φ }}).
Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
Global Instance elim_modal_bupd_wp s E e P Φ :
ElimModal True (|==> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp. Qed.
Global Instance elim_modal_fupd_wp s E e P Φ :
ElimModal True (|={E}=> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
Global Instance elim_modal_fupd_wp_atomic s E1 E2 e P Φ :
Global Instance elim_modal_bupd_wp p s E e P Φ :
ElimModal True p false (|==> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
Proof.
by rewrite /ElimModal intuitionistically_if_elim
(bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp.
Qed.
Global Instance elim_modal_fupd_wp p s E e P Φ :
ElimModal True p false (|={E}=> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
Proof.
by rewrite /ElimModal intuitionistically_if_elim
fupd_frame_r wand_elim_r fupd_wp.
Qed.
Global Instance elim_modal_fupd_wp_atomic p s E1 E2 e P Φ :
Atomic (stuckness_to_atomicity s) e
ElimModal True (|={E1,E2}=> P) P
ElimModal True p false (|={E1,E2}=> P) P
(WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I.
Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
Proof.
intros. by rewrite /ElimModal intuitionistically_if_elim
fupd_frame_r wand_elim_r wp_atomic.
Qed.
Global Instance add_modal_fupd_wp s E e P Φ :
AddModal (|={E}=> P) P (WP e @ s; E {{ Φ }}).
......
......@@ -763,37 +763,40 @@ Global Instance into_inv_embed {PROP' : bi} `{BiEmbed PROP PROP'} P N :
IntoInv P N IntoInv P N.
(* ElimModal *)
Global Instance elim_modal_wand φ P P' Q Q' R :
ElimModal φ P P' Q Q' ElimModal φ P P' (R - Q) (R - Q').
Global Instance elim_modal_wand φ p p' P P' Q Q' R :
ElimModal φ p p' P P' Q Q' ElimModal φ p p' P P' (R - Q) (R - Q').
Proof.
rewrite /ElimModal=> H Hφ. apply wand_intro_r.
rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l; auto.
rewrite wand_curry -assoc (comm _ (?p' _)%I) -wand_curry wand_elim_l; auto.
Qed.
Global Instance elim_modal_forall {A} φ P P' (Φ Ψ : A PROP) :
( x, ElimModal φ P P' (Φ x) (Ψ x)) ElimModal φ P P' ( x, Φ x) ( x, Ψ x).
Global Instance elim_modal_forall {A} φ p p' P P' (Φ Ψ : A PROP) :
( x, ElimModal φ p p' P P' (Φ x) (Ψ x)) ElimModal φ p p' P P' ( x, Φ x) ( x, Ψ x).
Proof.
rewrite /ElimModal=> H ?. apply forall_intro=> a. rewrite (forall_elim a); auto.
Qed.
Global Instance elim_modal_absorbingly_here P Q :
Absorbing Q ElimModal True (<absorb> P) P Q Q.
Global Instance elim_modal_absorbingly_here p P Q :
Absorbing Q ElimModal True p false (<absorb> P) P Q Q.
Proof.
rewrite /ElimModal=> H.
by rewrite absorbingly_sep_l wand_elim_r absorbing_absorbingly.
rewrite /ElimModal=> ? _. by rewrite intuitionistically_if_elim
absorbingly_sep_l wand_elim_r absorbing_absorbingly.
Qed.
Global Instance elim_modal_bupd `{BiBUpd PROP} P Q :
ElimModal True (|==> P) P (|==> Q) (|==> Q).
Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
Global Instance elim_modal_bupd `{BiBUpd PROP} p P Q :
ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
Proof.
by rewrite /ElimModal
intuitionistically_if_elim bupd_frame_r wand_elim_r bupd_trans.
Qed.
Global Instance elim_modal_embed_bupd_goal `{BiEmbedBUpd PROP PROP'}
φ (P P' : PROP') (Q Q' : PROP) :
ElimModal φ P P' (|==> Q)%I (|==> Q')%I
ElimModal φ P P' |==> Q |==> Q'.
p p' φ (P P' : PROP') (Q Q' : PROP) :
ElimModal φ p p' P P' (|==> Q)%I (|==> Q')%I
ElimModal φ p p' P P' |==> Q |==> Q'.
Proof. by rewrite /ElimModal !embed_bupd. Qed.
Global Instance elim_modal_embed_bupd_hyp `{BiEmbedBUpd PROP PROP'}
φ (P : PROP) (P' Q Q' : PROP') :
ElimModal φ (|==> P)%I P' Q Q'
ElimModal φ |==> P P' Q Q'.
p p' φ (P : PROP) (P' Q Q' : PROP') :
ElimModal φ p p' (|==> P)%I P' Q Q'
ElimModal φ p p' |==> P P' Q Q'.
Proof. by rewrite /ElimModal !embed_bupd. Qed.
(* AddModal *)
......
......@@ -474,38 +474,45 @@ Global Instance into_except_0_embed `{SbiEmbed PROP PROP'} P Q :
Proof. rewrite /IntoExcept0=> ->. by rewrite embed_except_0. Qed.
(* ElimModal *)
Global Instance elim_modal_timeless P Q :
IntoExcept0 P P' IsExcept0 Q ElimModal True P P' Q Q.
Global Instance elim_modal_timeless p P Q :
IntoExcept0 P P' IsExcept0 Q ElimModal True p p P P' Q Q.
Proof.
intros. rewrite /ElimModal (except_0_intro (_ - _)%I).
by rewrite (into_except_0 P) -except_0_sep wand_elim_r.
intros. rewrite /ElimModal (except_0_intro (_ - _)%I) (into_except_0 P).
by rewrite except_0_intuitionistically_if_2 -except_0_sep wand_elim_r.
Qed.
Global Instance elim_modal_bupd_plain_goal `{BiBUpdPlainly PROP} P Q :
Plain Q ElimModal True (|==> P) P Q Q.
Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
Global Instance elim_modal_bupd_plain `{BiBUpdPlainly PROP} P Q :
Plain P ElimModal True (|==> P) P Q Q.
Global Instance elim_modal_bupd_plain_goal `{BiBUpdPlainly PROP} p P Q :
Plain Q ElimModal True p false (|==> P) P Q Q.
Proof.
intros. by rewrite /ElimModal intuitionistically_if_elim
bupd_frame_r wand_elim_r bupd_plain.
Qed.
Global Instance elim_modal_bupd_plain `{BiBUpdPlainly PROP} p P Q :
Plain P ElimModal True p p (|==> P) P Q Q.
Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
Global Instance elim_modal_bupd_fupd `{BiBUpdFUpd PROP} E1 E2 P Q :
ElimModal True (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
Global Instance elim_modal_bupd_fupd `{BiBUpdFUpd PROP} p E1 E2 P Q :
ElimModal True p false (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
Proof.
by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
by rewrite /ElimModal intuitionistically_if_elim
(bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
Qed.
Global Instance elim_modal_fupd_fupd `{BiFUpd PROP} E1 E2 E3 P Q :
ElimModal True (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
Global Instance elim_modal_fupd_fupd `{BiFUpd PROP} p E1 E2 E3 P Q :
ElimModal True p false (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
Proof.
by rewrite /ElimModal intuitionistically_if_elim
fupd_frame_r wand_elim_r fupd_trans.
Qed.
Global Instance elim_modal_embed_fupd_goal `{BiEmbedFUpd PROP PROP'}
φ E1 E2 E3 (P P' : PROP') (Q Q' : PROP) :
ElimModal φ P P' (|={E1,E3}=> Q)%I (|={E2,E3}=> Q')%I
ElimModal φ P P' |={E1,E3}=> Q |={E2,E3}=> Q'.
p p' φ E1 E2 E3 (P P' : PROP') (Q Q' : PROP) :
ElimModal φ p p' P P' (|={E1,E3}=> Q)%I (|={E2,E3}=> Q')%I
ElimModal φ p p' P P' |={E1,E3}=> Q |={E2,E3}=> Q'.
Proof. by rewrite /ElimModal !embed_fupd. Qed.
Global Instance elim_modal_embed_fupd_hyp `{BiEmbedFUpd PROP PROP'}
φ E1 E2 (P : PROP) (P' Q Q' : PROP') :
ElimModal φ (|={E1,E2}=> P)%I P' Q Q'
ElimModal φ |={E1,E2}=> P P' Q Q'.
p p' φ E1 E2 (P : PROP) (P' Q Q' : PROP') :
ElimModal φ p p' (|={E1,E2}=> P)%I P' Q Q'
ElimModal φ p p' |={E1,E2}=> P P' Q Q'.
Proof. by rewrite /ElimModal embed_fupd. Qed.
(* AddModal *)
......
......@@ -234,11 +234,30 @@ Arguments IsExcept0 {_} _%I : simpl never.
Arguments is_except_0 {_} _%I {_}.
Hint Mode IsExcept0 + ! : typeclass_instances.
Class ElimModal {PROP : bi} (φ : Prop) (P P' : PROP) (Q Q' : PROP) :=
elim_modal : φ P (P' - Q') Q.
Arguments ElimModal {_} _ _%I _%I _%I _%I : simpl never.
Arguments elim_modal {_} _ _%I _%I _%I _%I {_}.
Hint Mode ElimModal + - ! - ! - : typeclass_instances.
(** The [ElimModal φ p p' P P' Q Q'] class is used by the [iMod] tactic.
The inputs are [p], [P] and [Q], and the outputs are [φ], [p'], [P'] and [Q'].
The class is used to transform a hypothesis [P] into a hypothesis [P'], given
a goal [Q], which is simultaniously transformed into [Q']. The Booleans [p]
and [p'] indicate whether the original, respectively, updated hypothesis reside
in the persistent context (iff [true]). The proposition [φ] can be used to
express a side-condition that [iMod] will generate (if not [True]).
An example instance is:
ElimModal True p false (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
This instance expresses that to eliminate [|={E1,E2}=> P] the goal is
transformed from [|={E1,E3}=> Q] into [|={E2,E3}=> Q], and the resulting
hypothesis is moved into the spatial context (regardless of where it was
originally). A corresponding [ElimModal] instance for the Iris 1/2-style update
modality, would have a side-condition [φ] on the masks. *)
Class ElimModal {PROP : bi} (φ : Prop) (p p' : bool) (P P' : PROP) (Q Q' : PROP) :=
elim_modal : φ ?p P (?p' P' - Q') Q.
Arguments ElimModal {_} _ _ _ _%I _%I _%I _%I : simpl never.
Arguments elim_modal {_} _ _ _ _%I _%I _%I _%I {_}.
Hint Mode ElimModal + - ! - ! - ! - : typeclass_instances.
(* Used by the specialization pattern [ > ] in [iSpecialize] and [iAssert] to
add a modality to the goal corresponding to a premise/asserted proposition. *)
......@@ -556,8 +575,8 @@ Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
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.
Instance elim_modal_tc_opaque {PROP : bi} φ (P P' Q Q' : PROP) :
ElimModal φ P P' Q Q' ElimModal φ (tc_opaque P) P' Q Q' := id.
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.
Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
IntoInv P N IntoInv (tc_opaque P) N := id.
Instance elim_inv_tc_opaque {PROP : bi} φ (Pinv Pin Pout Pclose Q Q' : PROP) :
......
......@@ -1054,15 +1054,15 @@ Proof.
Qed.
(** * Modalities *)
Lemma tac_modal_elim Δ Δ' i p φ P' P Q Q' :
Lemma tac_modal_elim Δ Δ' i p p' φ P' P Q Q' :
envs_lookup i Δ = Some (p, P)
ElimModal φ P P' Q Q'
ElimModal φ p p' P P' Q Q'
φ
envs_replace i p false (Esnoc Enil i P') Δ = Some Δ'
envs_replace i p p' (Esnoc Enil i P') Δ = Some Δ'
envs_entails Δ' Q' envs_entails Δ Q.
Proof.
rewrite envs_entails_eq => ???? HΔ. rewrite envs_replace_singleton_sound //=.
rewrite HΔ intuitionistically_if_elim. by eapply elim_modal.
rewrite HΔ. by eapply elim_modal.
Qed.
(** * Invariants *)
......
......@@ -359,14 +359,14 @@ Proof.
by rewrite {1}(objective_objectively P) monPred_objectively_unfold.
Qed.
Global Instance elim_modal_at_bupd_goal `{BiBUpd PROP} φ 𝓟 𝓟' Q Q' i :
ElimModal φ 𝓟 𝓟' (|==> Q i) (|==> Q' i)
ElimModal φ 𝓟 𝓟' ((|==> Q) i) ((|==> Q') i).
Global Instance elim_modal_at_bupd_goal `{BiBUpd PROP} φ p p' 𝓟 𝓟' Q Q' i :
ElimModal φ p p' 𝓟 𝓟' (|==> Q i) (|==> Q' i)
ElimModal φ p p' 𝓟 𝓟' ((|==> Q) i) ((|==> Q') i).
Proof. by rewrite /ElimModal !monPred_at_bupd. Qed.
Global Instance elim_modal_at_bupd_hyp `{BiBUpd PROP} φ P 𝓟 𝓟' 𝓠 𝓠' i:
Global Instance elim_modal_at_bupd_hyp `{BiBUpd PROP} φ p p' P 𝓟 𝓟' 𝓠 𝓠' i:
MakeMonPredAt i P 𝓟
ElimModal φ (|==> 𝓟) 𝓟' 𝓠 𝓠'
ElimModal φ ((|==> P) i) 𝓟' 𝓠 𝓠'.
ElimModal φ p p' (|==> 𝓟) 𝓟' 𝓠 𝓠'
ElimModal φ p p' ((|==> P) i) 𝓟' 𝓠 𝓠'.
Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_bupd=><-. Qed.
Global Instance add_modal_at_bupd_goal `{BiBUpd PROP} φ 𝓟 𝓟' Q i :
......@@ -465,14 +465,14 @@ Proof.
by rewrite monPred_at_later.
Qed.
Global Instance elim_modal_at_fupd_goal `{BiFUpd PROP} φ E1 E2 E3 𝓟 𝓟' Q Q' i :
ElimModal φ 𝓟 𝓟' (|={E1,E3}=> Q i) (|={E2,E3}=> Q' i)
ElimModal φ 𝓟 𝓟' ((|={E1,E3}=> Q) i) ((|={E2,E3}=> Q') i).
Global Instance elim_modal_at_fupd_goal `{BiFUpd PROP} φ p p' E1 E2 E3 𝓟 𝓟' Q Q' i :
ElimModal φ p p' 𝓟 𝓟' (|={E1,E3}=> Q i) (|={E2,E3}=> Q' i)
ElimModal φ p p' 𝓟 𝓟' ((|={E1,E3}=> Q) i) ((|={E2,E3}=> Q') i).
Proof. by rewrite /ElimModal !monPred_at_fupd. Qed.
Global Instance elim_modal_at_fupd_hyp `{BiFUpd PROP} φ E1 E2 P 𝓟 𝓟' 𝓠 𝓠' i :
Global Instance elim_modal_at_fupd_hyp `{BiFUpd PROP} φ p p' E1 E2 P 𝓟 𝓟' 𝓠 𝓠' i :
MakeMonPredAt i P 𝓟
ElimModal φ (|={E1,E2}=> 𝓟) 𝓟' 𝓠 𝓠'
ElimModal φ ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
ElimModal φ p p' (|={E1,E2}=> 𝓟) 𝓟' 𝓠 𝓠'
ElimModal φ p p' ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_fupd=><-. Qed.
Global Instance add_modal_at_fupd_goal `{BiFUpd PROP} E1 E2 𝓟 𝓟' Q i :
......
......@@ -1012,11 +1012,11 @@ Tactic Notation "iNext" := iModIntro (▷^_ _)%I.
(** * Update modality *)
Tactic Notation "iModCore" constr(H) :=
eapply tac_modal_elim with _ H _ _ _ _ _;
eapply tac_modal_elim with _ H _ _ _ _ _ _;
[env_reflexivity || fail "iMod:" H "not found"
|iSolveTC ||
let P := match goal with |- ElimModal _ ?P _ _ _ => P end in
let Q := match goal with |- ElimModal _ _ _ ?Q _ => Q end in
let P := match goal with |- ElimModal _ _ _ ?P _ _ _ => P end in
let Q := match goal with |- ElimModal _ _ _ _ _ ?Q _ => Q end in
fail "iMod: cannot eliminate modality " P "in" Q
|try fast_done (* optional side-condition *)
|env_reflexivity|].
......
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