From 1244778247f8b44da2a5f176bd26761095c0c336 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 11 Mar 2016 09:57:21 +0100
Subject: [PATCH] docs: align CMRA inclusion notation with Coq
---
docs/algebra.tex | 8 +++-----
docs/iris.sty | 7 ++++---
2 files changed, 7 insertions(+), 8 deletions(-)
diff --git a/docs/algebra.tex b/docs/algebra.tex
index 32060a7df..bd6613468 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -57,13 +57,13 @@ Note that $\COFEs$ is cartesian closed.
\All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{cmra-comm} \\
\All \melt.& \mcore\melt \mtimes \melt = \melt \tagH{cmra-core-id} \\
\All \melt.& \mcore{\mcore\melt} = \mcore\melt \tagH{cmra-core-idem} \\
- \All \melt, \meltB.& \melt \leq \meltB \Ra \mcore\melt \leq \mcore\meltB \tagH{cmra-core-mono} \\
+ \All \melt, \meltB.& \melt \mincl \meltB \Ra \mcore\melt \mincl \mcore\meltB \tagH{cmra-core-mono} \\
\All n, \melt, \meltB.& (\melt \mtimes \meltB) \in \mval_n \Ra \melt \in \mval_n \tagH{cmra-valid-op} \\
\All \melt, \meltB.& \melt \leq \meltB \Ra \melt \mtimes (\meltB \mdiv \melt) = \meltB \tagH{cmra-div-op} \\
\All n, \melt, \meltB_1, \meltB_2.& \omit\rlap{$\melt \in \mval_n \land \melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \Ra {}$} \\
&\Exists \meltC_1, \meltC_2. \melt = \meltC_1 \mtimes \meltC_2 \land \meltC_1 \nequiv{n} \meltB_1 \land \meltC_2 \nequiv{n} \meltB_2 \tagH{cmra-extend} \\
\text{where}\qquad\qquad\\
- \melt \leq \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{cmra-incl}
+ \melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{cmra-incl}
\end{align*}
\end{defn}
@@ -122,8 +122,6 @@ Note that for RAs, this and the RA-based definition of a frame-preserving update
\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 \in \monoid, \meltB \in \monoid. \melt \leq \meltB \Ra f(\melt) \leq f(\meltB)$
\end{enumerate}
\end{defn}
Note that every RA is a discrete CMRA, by picking the discrete COFE for the equivalence relation.
@@ -136,7 +134,7 @@ Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE struct
\item $f$ preserves validity: \\
$\All n, \melt \in \monoid_1. \melt \in \mval_n \Ra f(\melt) \in \mval_n$
\item $f$ preserves CMRA inclusion:\\
- $\All \melt \in \monoid_1, \meltB \in \monoid_1. \melt \leq \meltB \Ra f(\melt) \leq f(\meltB)$
+ $\All \melt \in \monoid_1, \meltB \in \monoid_1. \melt \mincl \meltB \Ra f(\melt) \mincl f(\meltB)$
\end{enumerate}
\end{defn}
diff --git a/docs/iris.sty b/docs/iris.sty
index 46af1619d..3cfdedd63 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -51,13 +51,14 @@
\newcommand{\ra}{\rightarrow}
\newcommand{\Ra}{\Rightarrow}
\newcommand{\Lra}{\Leftrightarrow}
-\newcommand\monra{\xrightarrow{\kern-0.25ex\textrm{mon}\kern-0.25ex}}
-\newcommand\nfn{\xrightarrow{\kern-0.15ex\textrm{n}\kern-0.05ex}}
+\newcommand\monra{\xrightarrow{\kern-0.15ex\textrm{mon}\kern-0.05ex}}
+\newcommand\nfn{\xrightarrow{\kern-0.15ex\textrm{ne}\kern-0.05ex}}
\newcommand{\eqdef}{\triangleq}
\newcommand{\bnfdef}{\vcentcolon\vcentcolon=}
\newcommand*\setComp[2]{\left\{#1\spac\middle|\spac#2\right\}}
\newcommand*\set[1]{\left\{#1\right\}}
+\newcommand*\record[1]{\left\{\spac#1\spac\right\}}
\newenvironment{inbox}[1][]{
\begin{array}[#1]{@{}l@{}}
@@ -141,7 +142,7 @@
\newcommand{\mdiv}{\mathbin{\div}}
\newcommand{\mupd}{\rightsquigarrow}
-\newcommand{\mincl}[1]{\ensuremath{\mathrel{\stackrel{#1}{\leq}}}}
+\newcommand{\mincl}[1][]{\ensuremath{\mathrel{\stackrel{#1}{\preccurlyeq}}}}
\newcommand{\CMRAs}{\mathcal{R}} % category of CMRAs
--
GitLab