diff --git a/theories/proofmode/modalities.v b/theories/proofmode/modalities.v index 4ed0b68fd75540be3b470890bd53bcfb061fdda9..36e54a347087d5a31943bfafc85d788ac80826d0 100644 --- a/theories/proofmode/modalities.v +++ b/theories/proofmode/modalities.v @@ -6,8 +6,21 @@ Import bi. (** The `iModIntro` tactic is not tied the Iris modalities, but can be instantiated with a variety of modalities. -In order to plug in a modality, one has to decide for both the intuitionistic and -spatial context what action should be performed upon introducing the modality: +For the purpose of MoSeL, a modality is a mapping of propositions +`M : PROP1 → PROP2` (where `PROP1` and `PROP2` are BI-algebras, although usually +it is the same algebra) that is monotone and distributes over finite products. +Specifically, the following rules have to be satisfied: + + P ⊢ Q emp ⊢ M emp + ---------- + M P ⊢ M Q M P ∗ M Q ⊢ M (P ∗ Q) + +Together those conditions allow one to introduce the modality in the +goal, while stripping away the modalities in the context. + +Additionally, upon introducing a modality one can perform a number of +associated actions on the intuitionistic and spatial contexts. +Such an action can be one of the following: - Introduction is only allowed when the context is empty. - Introduction is only allowed when all hypotheses satisfy some predicate @@ -19,7 +32,22 @@ spatial context what action should be performed upon introducing the modality: - Introduction will clear the context. - Introduction will keep the context as-if. -Formally, these actions correspond to the following inductive type: *) +Formally, these actions correspond to the inductive type [modality_action]. +For each of those actions you have to prove that the transformation is valid. + +To instantiate the modality you have to define: 1) a mixin `modality_mixin`, +2) a record `modality`, 3) a `FromModal` type class instance from `classes.v`. + +For examples consult `modality_id` at the end of this file, or the instances +in the `modality_instances.v` file. + +Note that in MoSeL modalities can map the propositions between two different +BI-algebras. Most of the modalities in Iris operate on the same type of +assertions. For example, the modality can potentially maps propositions +of an arbitrary BI-algebra into the sub-BI-algebra of affine propositions, but +it is implemented as an endomapping. On the other hand, the embedding modality +⎡-⎤ is a mapping between propositions of different BI-algebras. +*) Inductive modality_action (PROP1 : bi) : bi → Type := | MIEnvIsEmpty {PROP2 : bi} : modality_action PROP1 PROP2