docs: describe more algebra stuff

algebra/cofe.v

@@ -89,6 +89,8 @@ Section cofe_mixin.
 End cofe_mixin.
 
 (** Discrete COFEs and Timeless elements *)
+(* TODO RJ: On paper, I called these "discrete elements". I think that makes
+   more sense. *)
 Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
 Arguments timeless {_} _ {_} _ _.
 Class Discrete (A : cofeT) := discrete_timeless (x : A) :> Timeless x.

docs/algebra.tex

@@ -18,7 +18,28 @@
 
 \ralf{Copy the explanation from the paper, when that one is more polished.}
 
-\ralf{Describe non-expansive, contractive, category $\COFEs$, later, locally non-expansive/contractive, black later, discrete elements, discrete CMRAs.}
+\begin{defn}
+  An element $x \in A$ of a COFE is called \emph{discrete} if
+  \[ \All y \in A. x \nequiv{0} y \Ra x = y\]
+  A COFE $A$ is called \emph{discrete} if all its elements are discrete.
+\end{defn}
+
+\begin{defn}
+  A function $f : A \to B$ between two COFEs is \emph{non-expansive} if
+  \[\All n, x \in A, y \in A. x \nequiv{n} y \Ra f(x) \nequiv{n} f(y) \]
+  It is \emph{contractive} if
+  \[ \All n, x \in A, y \in A. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(x) \]
+\end{defn}
+
+\begin{defn}
+  The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows.
+\end{defn}
+Note that $\COFEs$ is cartesian closed.
+
+\begin{defn}
+  A functor $F : \COFEs \to COFEs$ is called \emph{locally non-expansive} if its actions $F_1$ on arrows is itself a non-expansive map.
+  Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map.
+\end{defn}
 
 \subsection{RA}
 
@@ -91,17 +112,33 @@ This operation is needed to prove that $\later$ commutes with existential quanti
 \end{mathpar}
 (This assumes that the type $\type$ is non-empty.)
 
-\ralf{Describe monotone, category $\CMRAs$.}
-
 \begin{defn}
   It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if
   \[ \All n, \melt_f. \melt \mtimes \melt_f \in \mval_n \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \melt_f \in \mval_n \]
 
   We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$.
 \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 function $f : M \to N$ between two CMRAs is \emph{monotone} if it satisfies the following conditions:
+  \begin{enumerate}
+  \item $f$ is non-expansive
+  \item $f$ preserves validity: \\
+    $\All n, x \in M. x \in \mval_n \Ra f(x) \in \mval_n$
+  \item $f$ preserves CMRA inclusion:\\
+    $\All x, y. x \mincl y \Ra f(x) \mincl f(y)$
+  \end{enumerate}
+\end{defn}
+
+\begin{defn}
+  The category $\CMRAs$ consists of CMRAs as objects, and monotone functions as arrows.
+\end{defn}
+Note that $\CMRAs$ is a subcategory of $\COFEs$.
+The notion of a locally non-expansive (or contractive) functor naturally generalizes to functors between these categories.
+
 
 %%% Local Variables: 
 %%% mode: latex

docs/logic.tex

@@ -25,12 +25,15 @@ It does not matter whether they fork off an arbitrary expression.
 \end{itemize}
 
 \begin{defn}[Context]
-  A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied
-  \begin{align*}
-  \All\expr.& \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot \tagH{lang-ctx-not-val}\\
-  \All \expr_1, \state_1, \expr_2, \state_2, \expr'.& \expr_1, \state_1 \step \expr_2,\state_2,\expr' \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\expr' \tagH{lang-ctx-step}\\
-  \All \expr_1', \state_1, \expr_2, \state_2, \expr'.& \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\expr' \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\expr' \tagH{lang-ctx-step-inv}
-  \end{align*}
+  A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied:
+  \begin{enumerate}
+  \item $\lctx$ does not turn non-values into values:\\
+    $\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot $
+  \item One can perform reductions below $\lctx$:\\
+    $\All \expr_1, \state_1, \expr_2, \state_2, \expr'. \expr_1, \state_1 \step \expr_2,\state_2,\expr' \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\expr' $
+  \item Reductions stay below $\lctx$ until there is a value in the hole:\\
+    $\All \expr_1', \state_1, \expr_2, \state_2, \expr'. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\expr' \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\expr' $
+  \end{enumerate}
 \end{defn}
 
 \subsection{The concurrent language}
@@ -62,6 +65,7 @@ To instantiate Iris, you need to define the following parameters:
 \begin{itemize}
 \item A language $\Lang$
 \item A locally contractive functor $\iFunc : \COFEs \to \CMRAs$ defining the ghost state
+  \ralf{$\iFunc$ also needs to have a single-unit.}
 \end{itemize}
 
 \noindent

docs/model.tex

 \section{Model and semantics}
 
+\ralf{What also needs to be done here: Define uPred and its later function; define black later; define the resource CMRA}
+
 The semantics closely follows the ideas laid out in~\cite{catlogic}.
 We just repeat some of the most important definitions here.