Commit cf44ca8b authored by Ralf Jung's avatar Ralf Jung

Merge branch 'robbert/issue_154' into 'gen_proofmode'

Bring back side-conditionals for `iMod`

See merge request FP/iris-coq!113
parents c54e1692 10ce5481
......@@ -29,7 +29,7 @@ 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 (|==> P) P (|==> Q) (|==> Q).
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.
(** A bad recursive reference: "Assertion with name [i] does not hold" *)
......@@ -127,10 +127,10 @@ 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 (fupd E P) P (fupd E Q) (fupd E Q).
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_fupd0_fupd1 P Q : ElimModal (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
Global Instance elim_fupd0_fupd1 P Q : ElimModal True (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.
Qed.
......
......@@ -382,16 +382,16 @@ Section proofmode_classes.
Proof. by rewrite /IsExcept0 -{2}fupd_twp -except_0_fupd -fupd_intro. Qed.
Global Instance elim_modal_bupd_twp s E e P Φ :
ElimModal (|==> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
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_fupd_twp s E e P Φ :
ElimModal (|={E}=> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
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_atomic s E1 E2 e P Φ :
Atomic (stuckness_to_atomicity s) e
ElimModal (|={E1,E2}=> P) P
ElimModal True (|={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.
......
......@@ -376,16 +376,16 @@ Section proofmode_classes.
Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
Global Instance elim_modal_bupd_wp s E e P Φ :
ElimModal (|==> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
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 (|={E}=> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
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 Φ :
Atomic (stuckness_to_atomicity s) e
ElimModal (|={E1,E2}=> P) P
ElimModal True (|={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.
......
......@@ -801,29 +801,21 @@ Global Instance from_forall_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PR
Proof. by rewrite /FromForall -bi_embed_forall => <-. Qed.
(* 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' Q Q' R :
ElimModal φ P P' Q Q' ElimModal φ P P' (R - Q) (R - Q').
Proof.
rewrite /ElimModal=> H. apply wand_intro_r.
by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l.
rewrite /ElimModal=> H Hφ. apply wand_intro_r.
rewrite wand_curry -assoc (comm _ P') -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' (Φ Ψ : A PROP) :
( x, ElimModal φ P P' (Φ x) (Ψ x)) ElimModal φ P P' ( x, Φ x) ( x, Ψ x).
Proof.
rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
rewrite /ElimModal=> H ?. apply forall_intro=> a. rewrite (forall_elim a); auto.
Qed.
(* We use this proxy type class to make sure that the instance is only
used when we know that Pabs is not an existential, so that this
instance is only triggered when a [bi_absorbingly] modality
actually appears, thanks to the [Hint Mode] lower in this
file. Otherwise, this instance is too generic and gets used in
irrelevant contexts. *)
Class ElimModalAbsorbingly Pabs P Q :=
elim_modal_absorbingly :> ElimModal Pabs P Q Q.
Global Instance elim_modal_absorbingly_here P Q :
Absorbing Q ElimModalAbsorbingly (bi_absorbingly P) P Q.
Absorbing Q ElimModal True (bi_absorbingly P) P Q Q.
Proof.
rewrite /ElimModalAbsorbingly /ElimModal=> H.
rewrite /ElimModal=> H.
by rewrite absorbingly_sep_l wand_elim_r absorbing_absorbingly.
Qed.
......@@ -1075,13 +1067,13 @@ Proof. apply bupd_intro. Qed.
(* ElimModal *)
Global Instance elim_modal_bupd `{BUpdFacts PROP} P Q :
ElimModal (|==> P) P (|==> Q) (|==> 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_plain_goal `{BUpdFacts PROP} P Q :
Plain Q ElimModal (|==> P) P Q 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 `{BUpdFacts PROP} P Q :
Plain P ElimModal (|==> P) P Q Q.
Plain P ElimModal True (|==> P) P Q Q.
Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
(* AsValid *)
......@@ -1105,8 +1097,6 @@ Global Instance as_valid_embed `{BiEmbedding PROP PROP'} (φ : Prop) (P : PROP)
Proof. rewrite /AsValid0 /AsValid=> ->. rewrite bi_embed_valid //. Qed.
End bi_instances.
Hint Mode ElimModalAbsorbingly + ! - - : typeclass_instances.
Section sbi_instances.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
......@@ -1425,18 +1415,18 @@ Proof. rewrite /IntoExcept0=> ->. by rewrite sbi_embed_except_0. Qed.
(* ElimModal *)
Global Instance elim_modal_timeless P Q :
IntoExcept0 P P' IsExcept0 Q ElimModal P P' Q Q.
IntoExcept0 P P' IsExcept0 Q ElimModal True P P' Q Q.
Proof.
intros. rewrite /ElimModal (except_0_intro (_ - _)%I).
by rewrite (into_except_0 P) -except_0_sep wand_elim_r.
Qed.
Global Instance elim_modal_bupd_fupd `{FUpdFacts PROP} E1 E2 P Q :
ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
ElimModal True (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
Proof.
by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
Qed.
Global Instance elim_modal_fupd_fupd `{FUpdFacts PROP} E1 E2 E3 P Q :
ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> 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.
(* AddModal *)
......
......@@ -321,11 +321,11 @@ Arguments FromModal {_} _%I _%I : simpl never.
Arguments from_modal {_} _%I _%I {_}.
Hint Mode FromModal + ! - : typeclass_instances.
Class ElimModal {PROP : bi} (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.
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.
(* Used by the specialization pattern [ > ] in [iSpecialize] and [iAssert] to
add a modality to the goal corresponding to a premise/asserted proposition. *)
......@@ -473,7 +473,5 @@ Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
IntoForall P Φ IntoForall (tc_opaque P) Φ := id.
Instance from_modal_tc_opaque {PROP : bi} (P Q : PROP) :
FromModal P Q FromModal (tc_opaque P) Q := id.
(* Higher precedence than [elim_modal_timeless], so that [iAssert] does not
loop (see test [test_iAssert_modality] in proofmode.v). *)
Instance elim_modal_tc_opaque {PROP : bi} (P P' Q Q' : PROP) :
ElimModal P P' Q Q' ElimModal (tc_opaque P) P' Q Q' | 100 := 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.
......@@ -1138,14 +1138,15 @@ Lemma tac_modal_intro Δ P Q :
FromModal P Q envs_entails Δ Q envs_entails Δ P.
Proof. by rewrite /envs_entails /FromModal=> <- ->. Qed.
Lemma tac_modal_elim Δ Δ' i p P' P Q Q' :
Lemma tac_modal_elim Δ Δ' i p φ P' P Q Q' :
envs_lookup i Δ = Some (p, P)
ElimModal P P' Q Q'
ElimModal φ P P' Q Q'
φ
envs_replace i p false (Esnoc Enil i P') Δ = Some Δ'
envs_entails Δ' Q' envs_entails Δ Q.
Proof.
rewrite /envs_entails => ??? HΔ. rewrite envs_replace_singleton_sound //=.
rewrite HΔ affinely_persistently_if_elim. by apply elim_modal.
rewrite /envs_entails => ???? HΔ. rewrite envs_replace_singleton_sound //=.
rewrite HΔ affinely_persistently_if_elim. by eapply elim_modal.
Qed.
End bi_tactics.
......
......@@ -369,29 +369,29 @@ Global Instance from_modal_monPred_at i P Q 𝓠 :
FromModal P Q MakeMonPredAt i Q 𝓠 FromModal (P i) 𝓠.
Proof. by rewrite /FromModal /MakeMonPredAt=> <- <-. Qed.
Global Instance elim_modal_embed_bupd_goal `{BUpdFacts PROP} P P' 𝓠 𝓠' :
ElimModal P P' (|==> ⎡𝓠⎤)%I (|==> ⎡𝓠')%I
ElimModal P P' |==> 𝓠⎤ |==> 𝓠'.
Global Instance elim_modal_embed_bupd_goal `{BUpdFacts PROP} φ P P' 𝓠 𝓠' :
ElimModal φ P P' (|==> ⎡𝓠⎤)%I (|==> ⎡𝓠')%I
ElimModal φ P P' |==> 𝓠⎤ |==> 𝓠'.
Proof. by rewrite /ElimModal !monPred_bupd_embed. Qed.
Global Instance elim_modal_embed_bupd_hyp `{BUpdFacts PROP} 𝓟 P' Q Q' :
ElimModal (|==> ⎡𝓟⎤)%I P' Q Q'
ElimModal |==> 𝓟⎤ P' Q Q'.
Global Instance elim_modal_embed_bupd_hyp `{BUpdFacts PROP} φ 𝓟 P' Q Q' :
ElimModal φ (|==> ⎡𝓟⎤)%I P' Q Q'
ElimModal φ |==> 𝓟⎤ P' Q Q'.
Proof. by rewrite /ElimModal monPred_bupd_embed. Qed.
Global Instance add_modal_embed_bupd_goal `{BUpdFacts PROP} P P' 𝓠 :
AddModal P P' (|==> ⎡𝓠⎤)%I AddModal P P' |==> 𝓠⎤.
Proof. by rewrite /AddModal !monPred_bupd_embed. Qed.
Global Instance elim_modal_at_bupd_goal `{BUpdFacts PROP} 𝓟 𝓟' Q Q' i :
ElimModal 𝓟 𝓟' (|==> Q i) (|==> Q' i)
ElimModal 𝓟 𝓟' ((|==> Q) i) ((|==> Q') i).
Global Instance elim_modal_at_bupd_goal `{BUpdFacts PROP} φ 𝓟 𝓟' Q Q' i :
ElimModal φ 𝓟 𝓟' (|==> Q i) (|==> Q' i)
ElimModal φ 𝓟 𝓟' ((|==> Q) i) ((|==> Q') i).
Proof. by rewrite /ElimModal !monPred_at_bupd. Qed.
Global Instance elim_modal_at_bupd_hyp `{BUpdFacts PROP} P 𝓟' 𝓠 𝓠' i:
ElimModal (|==> P i) 𝓟' 𝓠 𝓠'
ElimModal ((|==> P) i) 𝓟' 𝓠 𝓠'.
Global Instance elim_modal_at_bupd_hyp `{BUpdFacts PROP} φ P 𝓟' 𝓠 𝓠' i:
ElimModal φ (|==> P i) 𝓟' 𝓠 𝓠'
ElimModal φ ((|==> P) i) 𝓟' 𝓠 𝓠'.
Proof. by rewrite /ElimModal monPred_at_bupd. Qed.
Global Instance add_modal_at_bupd_goal `{BUpdFacts PROP} 𝓟 𝓟' Q i :
Global Instance add_modal_at_bupd_goal `{BUpdFacts PROP} φ 𝓟 𝓟' Q i :
AddModal 𝓟 𝓟' (|==> Q i)%I AddModal 𝓟 𝓟' ((|==> Q) i).
Proof. by rewrite /AddModal !monPred_at_bupd. Qed.
End bi.
......@@ -470,26 +470,26 @@ Proof.
by rewrite monPred_at_later.
Qed.
Global Instance elim_modal_embed_fupd_goal `{FUpdFacts PROP} E1 E2 E3 P P' 𝓠 𝓠' :
ElimModal P P' (|={E1,E3}=> ⎡𝓠⎤)%I (|={E2,E3}=> ⎡𝓠')%I
ElimModal P P' |={E1,E3}=> 𝓠⎤ |={E2,E3}=> 𝓠'.
Global Instance elim_modal_embed_fupd_goal `{FUpdFacts PROP} φ E1 E2 E3 P P' 𝓠 𝓠' :
ElimModal φ P P' (|={E1,E3}=> ⎡𝓠⎤)%I (|={E2,E3}=> ⎡𝓠')%I
ElimModal φ P P' |={E1,E3}=> 𝓠⎤ |={E2,E3}=> 𝓠'.
Proof. by rewrite /ElimModal !monPred_fupd_embed. Qed.
Global Instance elim_modal_embed_fupd_hyp `{FUpdFacts PROP} E1 E2 𝓟 P' Q Q' :
ElimModal (|={E1,E2}=> ⎡𝓟⎤)%I P' Q Q'
ElimModal |={E1,E2}=> 𝓟⎤ P' Q Q'.
Global Instance elim_modal_embed_fupd_hyp `{FUpdFacts PROP} φ E1 E2 𝓟 P' Q Q' :
ElimModal φ (|={E1,E2}=> ⎡𝓟⎤)%I P' Q Q'
ElimModal φ |={E1,E2}=> 𝓟⎤ P' Q Q'.
Proof. by rewrite /ElimModal monPred_fupd_embed. Qed.
Global Instance add_modal_embed_fupd_goal `{FUpdFacts PROP} E1 E2 P P' 𝓠 :
AddModal P P' (|={E1,E2}=> ⎡𝓠⎤)%I AddModal P P' |={E1,E2}=> 𝓠⎤.
Proof. by rewrite /AddModal !monPred_fupd_embed. Qed.
Global Instance elim_modal_at_fupd_goal `{FUpdFacts 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 `{FUpdFacts 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).
Proof. by rewrite /ElimModal !monPred_at_fupd. Qed.
Global Instance elim_modal_at_fupd_hyp `{FUpdFacts PROP} E1 E2 P 𝓟' 𝓠 𝓠' i :
ElimModal (|={E1,E2}=> P i) 𝓟' 𝓠 𝓠'
ElimModal ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
Global Instance elim_modal_at_fupd_hyp `{FUpdFacts PROP} φ E1 E2 P 𝓟' 𝓠 𝓠' i :
ElimModal φ (|={E1,E2}=> P i) 𝓟' 𝓠 𝓠'
ElimModal φ ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
Proof. by rewrite /ElimModal monPred_at_fupd. Qed.
Global Instance add_modal_at_fupd_goal `{FUpdFacts PROP} E1 E2 𝓟 𝓟' Q i :
......
......@@ -944,12 +944,13 @@ Tactic Notation "iModIntro" :=
fail "iModIntro:" P "not a 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"
|apply _ ||
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|].
(** * Basic destruct tactic *)
......
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