Commit a9c7a69d authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/mask-errors' into 'master'

better error when iMod/iModIntro fails due to mask mismatch

See merge request iris/iris!691
parents d18de58d faf185c4
......@@ -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,11 +124,17 @@ 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 from_modal_fupd_wrong_mask E1 E2 P `{!BiFUpd PROP} :
FromModal
(pm_error "Only non-mask-changing update modalities can be introduced directly.
Use [iApply fupd_mask_intro] to introduce mask-changing update modalities")
modality_id (|={E1,E2}=> P) (|={E1,E2}=> P) P | 100.
Proof. by intros []. Qed.
Global Instance elim_modal_bupd `{!BiBUpd PROP} p P Q :
ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
......@@ -161,6 +167,13 @@ Proof.
by rewrite /ElimModal intuitionistically_if_elim
fupd_frame_r wand_elim_r fupd_trans.
Qed.
Global Instance elim_modal_fupd_fupd_wrong_mask `{!BiFUpd PROP} p E0 E1 E2 E3 P Q :
ElimModal
(pm_error "Goal and eliminated modality must have the same mask.
Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]")
p false
(|={E1,E2}=> P) False (|={E0,E3}=> Q) False | 100.
Proof. intros []. Qed.
Global Instance add_modal_bupd `{!BiBUpd PROP} P Q : AddModal (|==> P) P (|==> Q).
Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.
......
......@@ -5,6 +5,11 @@ From iris.proofmode Require Export ident_name modalities.
From iris.prelude Require Import options.
Import bi.
(** Use this as precondition on "failing" instances of typeclasses that have
pure preconditions (such as [ElimModal]), if you want a nice error to be shown
when this instances is picked as part of some proof mode tactic. *)
Inductive pm_error (s : string) := .
Class FromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
from_assumption : ?p P Q.
Global Arguments FromAssumption {_} _ _%I _%I : simpl never.
......@@ -91,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].
......@@ -108,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].
......@@ -640,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.
......
......@@ -28,7 +28,10 @@ Ltac iSolveTC :=
(** Tactic used for solving side-conditions arising from TC resolution in [iMod]
and [iInv]. *)
Ltac iSolveSideCondition :=
split_and?; try solve [ fast_done | solve_ndisj | iSolveTC ].
lazymatch goal with
| |- pm_error ?err => fail "" err
| _ => split_and?; try solve [ fast_done | solve_ndisj | iSolveTC ]
end.
(** Used for printing [string]s and [ident]s. *)
Ltac pretty_ident H :=
......@@ -1382,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 ||
......@@ -1399,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.
......
......@@ -707,6 +707,26 @@ Tactic failure: iRevert: k is used in hypothesis "Hk".
: string
The command has indeed failed with message:
Tactic failure: iLöb: no 'BiLöb' instance found.
"iMod_mask_mismatch"
: string
The command has indeed failed with message:
Tactic failure:
"Goal and eliminated modality must have the same mask.
Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]".
The command has indeed failed with message:
Tactic failure:
"Goal and eliminated modality must have the same mask.
Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]".
"iModIntro_mask_mismatch"
: string
The command has indeed failed with message:
Tactic failure:
"Only non-mask-changing update modalities can be introduced directly.
Use [iApply fupd_mask_intro] to introduce mask-changing update modalities".
The command has indeed failed with message:
Tactic failure:
"Only non-mask-changing update modalities can be introduced directly.
Use [iApply fupd_mask_intro] to introduce mask-changing update modalities".
"test_pure_name"
: string
1 goal
......
......@@ -1389,16 +1389,28 @@ Proof. intros Hk. Fail iRevert (k). Abort.
Check "iRevert_dep_var".
Lemma iRevert_dep_var (k : nat) (Φ : nat PROP) : Φ k - Φ (S k).
Proof. iIntros "Hk". Fail iRevert (k). Abort.
End error_tests.
Section error_tests_bi.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Check "iLöb_no_BiLöb".
Lemma iLöb_no_BiLöb P : P.
Proof. Fail iLöb as "IH". Abort.
End error_tests_bi.
Check "iMod_mask_mismatch".
Lemma iMod_mask_mismatch `{!BiFUpd PROP} E1 E2 (P : PROP) :
(|={E2}=> P) |={E1}=> P.
Proof.
Fail iIntros ">HP".
iIntros "HP". Fail iMod "HP".
Abort.
Check "iModIntro_mask_mismatch".
Lemma iMod_mask_mismatch `{!BiFUpd PROP} E1 E2 (P : PROP) :
|={E1,E2}=> P.
Proof.
Fail iModIntro.
Fail iIntros "!>".
Abort.
End error_tests.
Section pure_name_tests.
Context {PROP : bi}.
......
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