add: discrete CMRAs

docs/algebra.tex

@@ -48,7 +48,7 @@ Note that $\COFEs$ is cartesian closed.
 \subsection{CMRA}
 
 \begin{defn}
-  A \emph{CMRA} is a tuple $(\monoid, (\mval_n \subseteq \monoid)_{n \in \mathbb{N}}, \mcore{-}: \monoid \to \monoid, (\mtimes) : \monoid \times \monoid \to \monoid, (\mdiv) : \monoid \times \monoid \to \monoid)$ satisfying
+  A \emph{CMRA} is a tuple $(\monoid : \COFEs, (\mval_n \subseteq \monoid)_{n \in \mathbb{N}}, \mcore{-}: \monoid \to \monoid, (\mtimes) : \monoid \times \monoid \to \monoid, (\mdiv) : \monoid \times \monoid \to \monoid)$ satisfying
   \begin{align*}
     \All n, m.& n \geq m \Ra V_n \subseteq V_m \tagH{cmra-valid-mono} \\
     \All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{cmra-assoc} \\
@@ -65,8 +65,6 @@ Note that $\COFEs$ is cartesian closed.
   \end{align*}
 \end{defn}
 
-Note that every RA is a CMRA, by picking the discrete COFE for the equivalence relation.
-
 \ralf{Copy the rest of the explanation from the paper, when that one is more polished.}
 
 \paragraph{The division operator $\mdiv$.}
@@ -115,10 +113,10 @@ This operation is needed to prove that $\later$ commutes with existential quanti
 \begin{defn}
   An element $\munit$ of a CMRA $\monoid$ is called the \emph{unit} of $\monoid$ if it satisfies the following conditions:
   \begin{enumerate}[itemsep=0pt]
-  \item $\munit$ is valid: \\ $\All n, \munit \in \mval_n$
-  \item $\munit$ is left-identity of the operation: \\
+  \item $\munit$ is valid: \\ $\All n. \munit \in \mval_n$
+  \item $\munit$ is a left-identity of the operation: \\
     $\All \melt \in M. \munit \mtimes \melt = \melt$
-  \item $\munit$ is discrete
+  \item $\munit$ is a discrete element
   \end{enumerate}
 \end{defn}
 
@@ -130,16 +128,27 @@ This operation is needed to prove that $\later$ commutes with existential quanti
 \end{defn}
 Note that for RAs, this and the RA-based definition of a frame-preserving update coincide.
 
-\ralf{Describe discrete CMRAs, and how they correspond to RAs.}
+\begin{defn}
+  A CMRA $\monoid$ is \emph{discrete} if it satisfies the following conditions:
+  \begin{enumerate}[itemsep=0pt]
+  \item $\monoid$ is a discrete COFE
+  \item $\val$ ignores the step-index: \\
+    $\All \melt \in \monoid. \melt \in \mval_0 \Ra \All n, \melt \in \mval_n$
+  \item $f$ preserves CMRA inclusion:\\
+    $\All \melt, \meltB. \melt \mincl \meltB \Ra f(\melt) \mincl f(\meltB)$
+  \end{enumerate}
+\end{defn}
+Note that every RA is a discrete CMRA, by picking the discrete COFE for the equivalence relation.
+Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE structure, as well as the step-index of $\mval$.
 
 \begin{defn}
   A function $f : M \to N$ between two CMRAs is \emph{monotone} if it satisfies the following conditions:
   \begin{enumerate}[itemsep=0pt]
   \item $f$ is non-expansive
   \item $f$ preserves validity: \\
-    $\All n, x \in M. x \in \mval_n \Ra f(x) \in \mval_n$
+    $\All n, \melt \in M. \melt \in \mval_n \Ra f(\melt) \in \mval_n$
   \item $f$ preserves CMRA inclusion:\\
-    $\All x, y. x \mincl y \Ra f(x) \mincl f(y)$
+    $\All \melt, \meltB. \melt \mincl \meltB \Ra f(\melt) \mincl f(\meltB)$
   \end{enumerate}
 \end{defn}
 

docs/iris.sty

@@ -70,6 +70,7 @@
 
 \newcommand{\pset}[1]{\wp(#1)} % Powerset
 \newcommand{\psetdown}[1]{\wp^\downarrow(#1)}
+\newcommand{\finpset}[1]{\wp^\mathrm{fin}(#1)}
 
 \newcommand{\Func}{F} % functor