Merge branch 'modalities-doc' into 'master'

[documentation] Some more text about the modalities.

See merge request iris/iris!220

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 <affine> 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