Merge branch 'ralf/masks' into 'master'

mention that masks in Coq are a bit different than on paper

Closes #211

See merge request iris/iris!394

tex/program-logic.tex

@@ -47,6 +47,9 @@ The following proposition states that an invariant with name $\iname$ exists and
 Next, we define \emph{fancy updates}, which are essentially the same as the basic updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants:
 \[ \pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textmon{En}}}{\mask_1} \wand \upd\diamond (W * \ownGhost{\gname_{\textmon{En}}}{\mask_2} * \prop) \]
 Here, $\mask_1$ and $\mask_2$ are the \emph{masks} of the view update, defining which invariants have to be (at least!) available before and after the update.
+Masks are sets of natural numbers, \ie they are subsets of $\mathbb{N}$.%
+\footnote{Actually, in the Coq development masks are restricted to a class of sets of natural numbers that contains all finite sets and is closed under union, intersection, difference and complement.
+The restriction is necessary for engineering reasons to still obtain representation independence: two masks should be \emph{definitionally} equal iff they contain the same invariant names.}
 We use $\top$ as symbol for the largest possible mask, $\nat$, and $\bot$ for the smallest possible mask $\emptyset$.
 We will write $\pvs[\mask] \prop$ for $\pvs[\mask][\mask]\prop$.
 %