Skip to content

GitLab

I
Iris
Commit 8db4eba0 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Unify `iAlways` and `iModIntro`.

parent 69cf8016
Hide whitespace changes
Inline Side-by-side
Showing with 405 additions and 369 deletions
theories/proofmode/class_instances.v
View file @ 8db4eba0
......@@ -4,55 +4,100 @@ From iris.proofmode Require Export classes.
Set Default Proof Using "Type".
Import bi.
Section always_modalities.
Section bi_modalities.
Context {PROP : bi}.
Lemma always_modality_persistently_mixin :
always_modality_mixin (@bi_persistently PROP) AIEnvId AIEnvClear.
Lemma modality_persistently_mixin :
modality_mixin (@bi_persistently PROP) MIEnvId MIEnvClear.
Proof.
split; eauto using equiv_entails_sym, persistently_intro, persistently_mono,
persistently_sep_2 with typeclass_instances.
Qed.
Definition always_modality_persistently :=
AlwaysModality _ always_modality_persistently_mixin.
Definition modality_persistently :=
Modality _ modality_persistently_mixin.
Lemma always_modality_affinely_mixin :
always_modality_mixin (@bi_affinely PROP) AIEnvId (AIEnvForall Affine).
Lemma modality_affinely_mixin :
modality_mixin (@bi_affinely PROP) MIEnvId (MIEnvForall Affine).
Proof.
split; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
affinely_sep_2 with typeclass_instances.
Qed.
Definition always_modality_affinely :=
AlwaysModality _ always_modality_affinely_mixin.
Definition modality_affinely :=
Modality _ modality_affinely_mixin.
Lemma always_modality_affinely_persistently_mixin :
always_modality_mixin (λ P : PROP, □ P)%I AIEnvId AIEnvIsEmpty.
Lemma modality_affinely_persistently_mixin :
modality_mixin (λ P : PROP, □ P)%I MIEnvId MIEnvIsEmpty.
Proof.
split; eauto using equiv_entails_sym, affinely_persistently_emp,
affinely_mono, persistently_mono, affinely_persistently_idemp,
affinely_persistently_sep_2 with typeclass_instances.
Qed.
Definition always_modality_affinely_persistently :=
AlwaysModality _ always_modality_affinely_persistently_mixin.
Definition modality_affinely_persistently :=
Modality _ modality_affinely_persistently_mixin.
Lemma always_modality_plainly_mixin :
always_modality_mixin (@bi_plainly PROP) (AIEnvForall Plain) AIEnvClear.
Lemma modality_plainly_mixin :
modality_mixin (@bi_plainly PROP) (MIEnvForall Plain) MIEnvClear.
Proof.
split; split_and?; eauto using equiv_entails_sym, plainly_intro, plainly_mono,
plainly_and, plainly_sep_2 with typeclass_instances.
Qed.
Definition always_modality_plainly :=
AlwaysModality _ always_modality_plainly_mixin.
Definition modality_plainly :=
Modality _ modality_plainly_mixin.
Lemma always_modality_affinely_plainly_mixin :
always_modality_mixin (λ P : PROP, ■ P)%I (AIEnvForall Plain) AIEnvIsEmpty.
Lemma modality_affinely_plainly_mixin :
modality_mixin (λ P : PROP, ■ P)%I (MIEnvForall Plain) MIEnvIsEmpty.
Proof.
split; split_and?; eauto using equiv_entails_sym, affinely_plainly_emp, affinely_intro,
plainly_intro, affinely_mono, plainly_mono, affinely_plainly_idemp,
affinely_plainly_and, affinely_plainly_sep_2 with typeclass_instances.
Qed.
Definition always_modality_affinely_plainly :=
AlwaysModality _ always_modality_affinely_plainly_mixin.
End always_modalities.
Definition modality_affinely_plainly :=
Modality _ modality_affinely_plainly_mixin.
Lemma modality_absorbingly_mixin :
modality_mixin (@bi_absorbingly PROP) MIEnvId MIEnvId.
Proof.
split; eauto using equiv_entails_sym, absorbingly_intro,
absorbingly_mono, absorbingly_sep.
Qed.
Definition modality_absorbingly :=
Modality _ modality_absorbingly_mixin.
End bi_modalities.
Section sbi_modalities.
Context {PROP : sbi}.
Lemma modality_except_0_mixin :
modality_mixin (@sbi_except_0 PROP) MIEnvId MIEnvId.
Proof.
split; eauto using equiv_entails_sym,
except_0_intro, except_0_mono, except_0_sep.
Qed.
Definition modality_except_0 :=
Modality _ modality_except_0_mixin.
Lemma modality_laterN_mixin n :
modality_mixin (@sbi_laterN PROP n)
(MIEnvTransform (MaybeIntoLaterN false n)) (MIEnvTransform (MaybeIntoLaterN false n)).
Proof.
split; split_and?; eauto using equiv_entails_sym, laterN_intro, laterN_mono,
laterN_and, laterN_sep with typeclass_instances.
rewrite /MaybeIntoLaterN=> P Q ->. by rewrite laterN_affinely_persistently_2.
Qed.
Definition modality_laterN n :=
Modality _ (modality_laterN_mixin n).
Lemma modality_bupd_mixin `{BUpdFacts PROP} :
modality_mixin (@bupd PROP _) MIEnvId MIEnvId.
Proof. split; eauto using bupd_intro, bupd_mono, bupd_sep. Qed.
Definition modality_bupd `{BUpdFacts PROP} :=
Modality _ modality_bupd_mixin.
Lemma modality_fupd_mixin `{FUpdFacts PROP} E :
modality_mixin (@fupd PROP _ E E) MIEnvId MIEnvId.
Proof. split; eauto using fupd_intro, fupd_mono, fupd_sep. Qed.
Definition modality_fupd `{FUpdFacts PROP} E :=
Modality _ (modality_fupd_mixin E).
End sbi_modalities.
Section bi_instances.
Context {PROP : bi}.
......@@ -267,54 +312,54 @@ Global Instance into_persistent_persistent P :
Persistent P → IntoPersistent false P P | 100.
Proof. intros. by rewrite /IntoPersistent. Qed.
(* FromAlways *)
Global Instance from_always_affinely P :
FromAlways always_modality_affinely (bi_affinely P) P | 2.
Proof. by rewrite /FromAlways. Qed.
Global Instance from_always_persistently P :
FromAlways always_modality_persistently (bi_persistently P) P | 2.
Proof. by rewrite /FromAlways. Qed.
Global Instance from_always_affinely_persistently P :
FromAlways always_modality_affinely_persistently (□ P) P | 1.
Proof. by rewrite /FromAlways. Qed.
Global Instance from_always_affinely_persistently_affine_bi P :
BiAffine PROP → FromAlways always_modality_persistently (□ P) P | 0.
Proof. intros. by rewrite /FromAlways /= affine_affinely. Qed.
Global Instance from_always_plainly P :
FromAlways always_modality_plainly (bi_plainly P) P | 2.
Proof. by rewrite /FromAlways. Qed.
Global Instance from_always_affinely_plainly P :
FromAlways always_modality_affinely_plainly (■ P) P | 1.
Proof. by rewrite /FromAlways. Qed.
Global Instance from_always_affinely_plainly_affine_bi P :
BiAffine PROP → FromAlways always_modality_plainly (■ P) P | 0.
Proof. intros. by rewrite /FromAlways /= affine_affinely. Qed.
Global Instance from_always_affinely_embed `{BiEmbedding PROP PROP'} P Q :
FromAlways always_modality_affinely P Q →
FromAlways always_modality_affinely ⎡P⎤ ⎡Q⎤.
Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely. Qed.
Global Instance from_always_persistently_embed `{BiEmbedding PROP PROP'} P Q :
FromAlways always_modality_persistently P Q →
FromAlways always_modality_persistently ⎡P⎤ ⎡Q⎤.
Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_persistently. Qed.
Global Instance from_always_affinely_persistently_embed `{BiEmbedding PROP PROP'} P Q :
FromAlways always_modality_affinely_persistently P Q →
FromAlways always_modality_affinely_persistently ⎡P⎤ ⎡Q⎤.
Proof.
rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_persistently.
Qed.
Global Instance from_always_plainly_embed `{BiEmbedding PROP PROP'} P Q :
FromAlways always_modality_plainly P Q →
FromAlways always_modality_plainly ⎡P⎤ ⎡Q⎤.
Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_plainly. Qed.
Global Instance from_always_affinely_plainly_embed `{BiEmbedding PROP PROP'} P Q :
FromAlways always_modality_affinely_plainly P Q →
FromAlways always_modality_affinely_plainly ⎡P⎤ ⎡Q⎤.
Proof.
rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
(* FromModal *)
Global Instance from_modal_affinely P :
FromModal modality_affinely (bi_affinely P) P | 2.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_persistently P :
FromModal modality_persistently (bi_persistently P) P | 2.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_affinely_persistently P :
FromModal modality_affinely_persistently (□ P) P | 1.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_affinely_persistently_affine_bi P :
BiAffine PROP → FromModal modality_persistently (□ P) P | 0.
Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.
Global Instance from_modal_plainly P :
FromModal modality_plainly (bi_plainly P) P | 2.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_affinely_plainly P :
FromModal modality_affinely_plainly (■ P) P | 1.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_affinely_plainly_affine_bi P :
BiAffine PROP → FromModal modality_plainly (■ P) P | 0.
Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.
Global Instance from_modal_affinely_embed `{BiEmbedding PROP PROP'} P Q :
FromModal modality_affinely P Q →
FromModal modality_affinely ⎡P⎤ ⎡Q⎤.
Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_affinely. Qed.
Global Instance from_modal_persistently_embed `{BiEmbedding PROP PROP'} P Q :
FromModal modality_persistently P Q →
FromModal modality_persistently ⎡P⎤ ⎡Q⎤.
Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_persistently. Qed.
Global Instance from_modal_affinely_persistently_embed `{BiEmbedding PROP PROP'} P Q :
FromModal modality_affinely_persistently P Q →
FromModal modality_affinely_persistently ⎡P⎤ ⎡Q⎤.
Proof.
rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_persistently.
Qed.
Global Instance from_modal_plainly_embed `{BiEmbedding PROP PROP'} P Q :
FromModal modality_plainly P Q →
FromModal modality_plainly ⎡P⎤ ⎡Q⎤.
Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_plainly. Qed.
Global Instance from_modal_affinely_plainly_embed `{BiEmbedding PROP PROP'} P Q :
FromModal modality_affinely_plainly P Q →
FromModal modality_affinely_plainly ⎡P⎤ ⎡Q⎤.
Proof.
rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
Qed.
(* IntoWand *)
......@@ -1077,11 +1122,14 @@ Proof.
Qed.
(* FromModal *)
Global Instance from_modal_absorbingly P : FromModal (bi_absorbingly P) P.
Proof. apply absorbingly_intro. Qed.
Global Instance from_modal_absorbingly P :
FromModal modality_absorbingly (bi_absorbingly P) P.
Proof. by rewrite /FromModal. Qed.
(* FIXME
Global Instance from_modal_embed `{BiEmbedding PROP PROP'} P Q :
FromModal P Q → FromModal ⎡P⎤ ⎡Q⎤.
Proof. by rewrite /FromModal=> ->. Qed.
*)
(* AsValid *)
Global Instance as_valid_valid {PROP : bi} (P : PROP) : AsValid0 (bi_valid P) P | 0.
......@@ -1410,15 +1458,19 @@ Global Instance is_except_0_fupd `{FUpdFacts PROP} E1 E2 P :
Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
(* FromModal *)
Global Instance from_modal_later P : FromModal (▷ P) P.
Proof. apply later_intro. Qed.
Global Instance from_modal_except_0 P : FromModal (◇ P) P.
Proof. apply except_0_intro. Qed.
Global Instance from_modal_bupd `{BUpdFacts PROP} P : FromModal (|==> P) P.
Proof. apply bupd_intro. Qed.
Global Instance from_modal_fupd E P `{FUpdFacts PROP} : FromModal (|={E}=> P) P.
Proof. rewrite /FromModal. apply fupd_intro. Qed.
Global Instance from_modal_later P : FromModal (modality_laterN 1) (▷ P) P.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_laterN n P : FromModal (modality_laterN n) (▷^n P) P.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_except_0 P : FromModal modality_except_0 (◇ P) P.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_bupd `{BUpdFacts PROP} P :
FromModal modality_bupd (|==> P) P.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_fupd E P `{FUpdFacts PROP} :
FromModal (modality_fupd E) (|={E}=> P) P.
Proof. by rewrite /FromModal. Qed.
(* IntoInternalEq *)
Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
......
theories/proofmode/classes.v
View file @ 8db4eba0
......@@ -83,12 +83,11 @@ Arguments IntoPersistent {_} _ _%I _%I : simpl never.
Arguments into_persistent {_} _ _%I _%I {_}.
Hint Mode IntoPersistent + + ! - : typeclass_instances.
(* The `iAlways` tactic is not tied to `persistently` and `affinely`, but can be
instantiated with a variety of comonadic (always-style) modalities.
(* The `iModIntro` tactic is not tied the Iris modalities, but can be
instantiated with a variety of modalities.
In order to plug in an always-style modality, one has to decide for both the
persistent and spatial what action should be performed upon introducing the
modality:
In order to plug in a modality, one has to decide for both the persistent and
spatial what action should be performed upon introducing the modality:
- Introduction is only allowed when the context is empty.
- Introduction is only allowed when all hypotheses satisfy some predicate
......@@ -102,125 +101,124 @@ modality:
Formally, these actions correspond to the following inductive type: *)
Inductive always_intro_spec (PROP : bi) :=
| AIEnvIsEmpty
| AIEnvForall (C : PROP → Prop)
| AIEnvTransform (C : PROP → PROP → Prop)
| AIEnvClear
| AIEnvId.
Arguments AIEnvIsEmpty {_}.
Arguments AIEnvForall {_} _.
Arguments AIEnvTransform {_} _.
Arguments AIEnvClear {_}.
Arguments AIEnvId {_}.
Notation AIEnvFilter C := (AIEnvTransform (TCDiag C)).
(* An always-style modality is then a record packing together the modality with
the laws it should satisfy to justify the given actions for both contexts: *)
Record always_modality_mixin {PROP : bi} (M : PROP → PROP)
(pspec sspec : always_intro_spec PROP) := {
always_modality_mixin_persistent :
Inductive modality_intro_spec (PROP : bi) :=
| MIEnvIsEmpty
| MIEnvForall (C : PROP → Prop)
| MIEnvTransform (C : PROP → PROP → Prop)
| MIEnvClear
| MIEnvId.
Arguments MIEnvIsEmpty {_}.
Arguments MIEnvForall {_} _.
Arguments MIEnvTransform {_} _.
Arguments MIEnvClear {_}.
Arguments MIEnvId {_}.
Notation MIEnvFilter C := (MIEnvTransform (TCDiag C)).
(* A modality is then a record packing together the modality with the laws it
should satisfy to justify the given actions for both contexts: *)
Record modality_mixin {PROP : bi} (M : PROP → PROP)
(pspec sspec : modality_intro_spec PROP) := {
modality_mixin_persistent :
match pspec with
| AIEnvIsEmpty => True
| AIEnvForall C => (∀ P, C P → □ P ⊢ M (□ P)) ∧ (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
| AIEnvTransform C => (∀ P Q, C P Q → □ P ⊢ M (□ Q)) ∧ (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
| AIEnvClear => True
| AIEnvId => ∀ P, □ P ⊢ M (□ P)
| MIEnvIsEmpty => True
| MIEnvForall C => (∀ P, C P → □ P ⊢ M (□ P)) ∧ (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
| MIEnvTransform C => (∀ P Q, C P Q → □ P ⊢ M (□ Q)) ∧ (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
| MIEnvClear => True
| MIEnvId => ∀ P, □ P ⊢ M (□ P)
end;
always_modality_mixin_spatial :
modality_mixin_spatial :
match sspec with
| AIEnvIsEmpty => True
| AIEnvForall C => ∀ P, C P → P ⊢ M P
| AIEnvTransform C => (∀ P Q, C P Q → P ⊢ M Q)
| AIEnvClear => ∀ P, Absorbing (M P)
| AIEnvId => ∀ P, P ⊢ M P
| MIEnvIsEmpty => True
| MIEnvForall C => ∀ P, C P → P ⊢ M P
| MIEnvTransform C => (∀ P Q, C P Q → P ⊢ M Q)
| MIEnvClear => ∀ P, Absorbing (M P)
| MIEnvId => ∀ P, P ⊢ M P
end;
always_modality_mixin_emp : emp ⊢ M emp;
always_modality_mixin_mono P Q : (P ⊢ Q) → M P ⊢ M Q;
always_modality_mixin_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q)
modality_mixin_emp : emp ⊢ M emp;
modality_mixin_mono P Q : (P ⊢ Q) → M P ⊢ M Q;
modality_mixin_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q)
}.
Record always_modality (PROP : bi) := AlwaysModality {
always_modality_car :> PROP → PROP;
always_modality_persistent_spec : always_intro_spec PROP;
always_modality_spatial_spec : always_intro_spec PROP;
always_modality_mixin_of : always_modality_mixin
always_modality_car
always_modality_persistent_spec always_modality_spatial_spec
Record modality (PROP : bi) := Modality {
modality_car :> PROP → PROP;
modality_persistent_spec : modality_intro_spec PROP;
modality_spatial_spec : modality_intro_spec PROP;
modality_mixin_of :
modality_mixin modality_car modality_persistent_spec modality_spatial_spec
}.
Arguments AlwaysModality {_} _ {_ _} _.
Arguments always_modality_persistent_spec {_} _.
Arguments always_modality_spatial_spec {_} _.
Arguments Modality {_} _ {_ _} _.
Arguments modality_persistent_spec {_} _.
Arguments modality_spatial_spec {_} _.
Section always_modality.
Context {PROP} (M : always_modality PROP).
Section modality.
Context {PROP} (M : modality PROP).
Lemma always_modality_persistent_forall C P :
always_modality_persistent_spec M = AIEnvForall C → C P → □ P ⊢ M (□ P).
Lemma modality_persistent_forall C P :
modality_persistent_spec M = MIEnvForall C → C P → □ P ⊢ M (□ P).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma always_modality_and_forall C P Q :
always_modality_persistent_spec M = AIEnvForall C → M P ∧ M Q ⊢ M (P ∧ Q).
Lemma modality_and_forall C P Q :
modality_persistent_spec M = MIEnvForall C → M P ∧ M Q ⊢ M (P ∧ Q).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma always_modality_persistent_transform C P Q :
always_modality_persistent_spec M = AIEnvTransform C → C P Q → □ P ⊢ M (□ Q).
Lemma modality_persistent_transform C P Q :
modality_persistent_spec M = MIEnvTransform C → C P Q → □ P ⊢ M (□ Q).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma always_modality_and_transform C P Q :
always_modality_persistent_spec M = AIEnvTransform C → M P ∧ M Q ⊢ M (P ∧ Q).
Lemma modality_and_transform C P Q :
modality_persistent_spec M = MIEnvTransform C → M P ∧ M Q ⊢ M (P ∧ Q).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma always_modality_persistent_id P :
always_modality_persistent_spec M = AIEnvId → □ P ⊢ M (□ P).
Lemma modality_persistent_id P :
modality_persistent_spec M = MIEnvId → □ P ⊢ M (□ P).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma always_modality_spatial_forall C P :
always_modality_spatial_spec M = AIEnvForall C → C P → P ⊢ M P.
Lemma modality_spatial_forall C P :
modality_spatial_spec M = MIEnvForall C → C P → P ⊢ M P.
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma always_modality_spatial_transform C P Q :
always_modality_spatial_spec M = AIEnvTransform C → C P Q → P ⊢ M Q.
Lemma modality_spatial_transform C P Q :
modality_spatial_spec M = MIEnvTransform C → C P Q → P ⊢ M Q.
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma always_modality_spatial_clear P :
always_modality_spatial_spec M = AIEnvClear → Absorbing (M P).
Lemma modality_spatial_clear P :
modality_spatial_spec M = MIEnvClear → Absorbing (M P).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma always_modality_spatial_id P :
always_modality_spatial_spec M = AIEnvId → P ⊢ M P.
Lemma modality_spatial_id P :
modality_spatial_spec M = MIEnvId → P ⊢ M P.
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma always_modality_emp : emp ⊢ M emp.
Proof. eapply always_modality_mixin_emp, always_modality_mixin_of. Qed.
Lemma always_modality_mono P Q : (P ⊢ Q) → M P ⊢ M Q.
Proof. eapply always_modality_mixin_mono, always_modality_mixin_of. Qed.
Lemma always_modality_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q).
Proof. eapply always_modality_mixin_sep, always_modality_mixin_of. Qed.
Global Instance always_modality_mono' : Proper ((⊢) ==> (⊢)) M.
Proof. intros P Q. apply always_modality_mono. Qed.
Global Instance always_modality_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) M.
Proof. intros P Q. apply always_modality_mono. Qed.
Global Instance always_modality_proper : Proper ((≡) ==> (≡)) M.
Proof. intros P Q. rewrite !equiv_spec=> -[??]; eauto using always_modality_mono. Qed.
Lemma always_modality_persistent_forall_big_and C Ps :
always_modality_persistent_spec M = AIEnvForall C →
Lemma modality_emp : emp ⊢ M emp.
Proof. eapply modality_mixin_emp, modality_mixin_of. Qed.
Lemma modality_mono P Q : (P ⊢ Q) → M P ⊢ M Q.
Proof. eapply modality_mixin_mono, modality_mixin_of. Qed.
Lemma modality_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q).
Proof. eapply modality_mixin_sep, modality_mixin_of. Qed.
Global Instance modality_mono' : Proper ((⊢) ==> (⊢)) M.
Proof. intros P Q. apply modality_mono. Qed.
Global Instance modality_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) M.
Proof. intros P Q. apply modality_mono. Qed.
Global Instance modality_proper : Proper ((≡) ==> (≡)) M.
Proof. intros P Q. rewrite !equiv_spec=> -[??]; eauto using modality_mono. Qed.
Lemma modality_persistent_forall_big_and C Ps :
modality_persistent_spec M = MIEnvForall C →
Forall C Ps → □ [∧] Ps ⊢ M (□ [∧] Ps).
Proof.
induction 2 as [|P Ps ? _ IH]; simpl.
- by rewrite persistently_pure affinely_True_emp affinely_emp -always_modality_emp.
- rewrite affinely_persistently_and -always_modality_and_forall // -IH.
by rewrite {1}(always_modality_persistent_forall _ P).
- by rewrite persistently_pure affinely_True_emp affinely_emp -modality_emp.
- rewrite affinely_persistently_and -modality_and_forall // -IH.
by rewrite {1}(modality_persistent_forall _ P).
Qed.
Lemma always_modality_spatial_forall_big_sep C Ps :
always_modality_spatial_spec M = AIEnvForall C →
Lemma modality_spatial_forall_big_sep C Ps :
modality_spatial_spec M = MIEnvForall C →
Forall C Ps → [∗] Ps ⊢ M ([∗] Ps).
Proof.
induction 2 as [|P Ps ? _ IH]; simpl.
- by rewrite -always_modality_emp.
- by rewrite -always_modality_sep -IH {1}(always_modality_spatial_forall _ P).
- by rewrite -modality_emp.
- by rewrite -modality_sep -IH {1}(modality_spatial_forall _ P).
Qed.
End always_modality.
End modality.
Class FromAlways {PROP : bi} (M : always_modality PROP) (P Q : PROP) :=
from_always : M Q ⊢ P.
Arguments FromAlways {_} _ _%I _%I : simpl never.
Arguments from_always {_} _ _%I _%I {_}.
Hint Mode FromAlways + - ! - : typeclass_instances.
Class FromModal {PROP : bi} (M : modality PROP) (P Q : PROP) :=
from_modal : M Q ⊢ P.
Arguments FromModal {_} _ _%I _%I : simpl never.
Arguments from_modal {_} _ _%I _%I {_}.
Hint Mode FromModal + - ! - : typeclass_instances.
Class FromAffinely {PROP : bi} (P Q : PROP) :=
from_affinely : bi_affinely Q ⊢ P.
......@@ -338,11 +336,6 @@ Arguments IsExcept0 {_} _%I : simpl never.
Arguments is_except_0 {_} _%I {_}.
Hint Mode IsExcept0 + ! : typeclass_instances.
Class FromModal {PROP : bi} (P Q : PROP) := from_modal : Q ⊢ P.
Arguments FromModal {_} _%I _%I : simpl never.
Arguments from_modal {_} _%I _%I {_}.
Hint Mode FromModal + ! - : 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.
......@@ -645,8 +638,8 @@ Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
IntoExist P Φ → IntoExist (tc_opaque P) Φ := id.
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.
Instance from_modal_tc_opaque {PROP : bi} M (P Q : PROP) :
FromModal M P Q → FromModal M (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 into_inv_tc_opaque {PROP : bi} (P : PROP) N :
......
theories/proofmode/coq_tactics.v
View file @ 8db4eba0
......@@ -583,149 +583,7 @@ Qed.
Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ → Q) → (φ → envs_entails Δ Q).
Proof. rewrite envs_entails_eq. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
(** * Always modalities *)
(** Transforming *)
Class TransformPersistentEnv
(M : always_modality PROP) (C : PROP → PROP → Prop) (Γ1 Γ2 : env PROP) := {
transform_persistent_env :
(∀ P Q, C P Q → □ P ⊢ M (□ Q)) →
(∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q)) →
□ ([∧] Γ1) ⊢ M (□ ([∧] Γ2));
transform_persistent_env_wf : env_wf Γ1 → env_wf Γ2;
transform_persistent_env_dom i : Γ1 !! i = None → Γ2 !! i = None;
}.
Global Instance transform_persistent_env_nil M C : TransformPersistentEnv M C Enil Enil.
Proof.
split=> // HC /=. rewrite !persistently_pure !affinely_True_emp.
by rewrite affinely_emp -always_modality_emp.
Qed.
Global Instance transform_persistent_env_snoc M (C : PROP → PROP → Prop) Γ Γ' i P Q :
C P Q →