From fa0ed70a2b22841bc460b4640f3b61920ac25e9a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 8 Mar 2016 14:48:40 +0100
Subject: [PATCH] docs: unit -> core
---
docs/algebra.tex | 10 +++++-----
docs/derived.tex | 2 +-
docs/iris.sty | 2 +-
docs/logic.tex | 6 +++---
4 files changed, 10 insertions(+), 10 deletions(-)
diff --git a/docs/algebra.tex b/docs/algebra.tex
index 522d15e97..9fde12b07 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -48,15 +48,15 @@ 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}}, \munit: \monoid \to \monoid, (\mtimes) : \monoid \times \monoid \to \monoid, (\mdiv) : \monoid \times \monoid \to \monoid)$ satisfying
+ 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
\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} \\
\All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{cmra-comm} \\
- \All \melt.& \munit(\melt) \mtimes \melt = \melt \tagH{cmra-unit-id} \\
- \All \melt.& \munit(\munit(\melt)) = \munit(\melt) \tagH{cmra-unit-idem} \\
- \All \melt, \meltB.& \melt \leq \meltB \Ra \munit(\melt) \leq \munit(\meltB) \tagH{cmra-unit-mono} \\
- \All n, \melt, \meltB.& (\melt \mtimes \meltB) \in \mval_n \Ra \melt \in \mval_n \tagH{cmra-unit-op} \\
+ \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 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} \\
diff --git a/docs/derived.tex b/docs/derived.tex
index c36708093..8d8a4ea36 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -10,7 +10,7 @@
\end{defn}
Of course, $\always\prop$ is persistent for any $\prop$.
-Furthermore, by the proof rules given above, $t = t'$ as well as $\ownGGhost{\munit(\melt)}$ and $\knowInv\iname\prop$ are persistent.
+Furthermore, by the proof rules given above, $t = t'$ as well as $\ownGGhost{\mcore\melt}$ and $\knowInv\iname\prop$ are persistent.
Persistence is preserved by conjunction, disjunction, separating conjunction as well as universal and existential quantification.
In our proofs, we will implicitly add and remove $\always$ from persistent assertions as necessary, and generally treat them like normal, non-linear assumptions.
diff --git a/docs/iris.sty b/docs/iris.sty
index 275b5d77c..b761d4cf4 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -129,7 +129,7 @@
\newcommand{\mcar}[1]{|#1|}
\newcommand{\mcarp}[1]{\mcar{#1}^{+}}
-\newcommand{\munit}{\mathord{\varepsilon}}
+\newcommand{\mcore}[1]{\lfloor#1\rfloor}
\newcommand{\mtimes}{\mathbin{\cdot}}
\newcommand{\mdiv}{\mathbin{\div}}
diff --git a/docs/logic.tex b/docs/logic.tex
index ecebd3f4b..fb80799be 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -107,7 +107,7 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\t
\pi_i\; \term \mid
\Lam \var:\type.\term \mid
\term(\term) \mid
- \munit \mid
+ \mcore\term \mid
\term \mtimes \term \mid
\\&
\FALSE \mid
@@ -214,7 +214,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
{\vctx \proves \wtt{\term(\termB)}{\type'}}
%%% monoids
\and
- \infer{}{\vctx \proves \wtt{\munit}{\textlog{M} \to \textlog{M}}}
+ \infer{\vctx \proves \wtt\melt{\textlog{M}}}{\vctx \proves \wtt{\mcore\melt}{\textlog{M}}}
\and
\infer{\vctx \proves \wtt{\melt}{\textlog{M}} \and \vctx \proves \wtt{\meltB}{\textlog{M}}}
{\vctx \proves \wtt{\melt \mtimes \meltB}{\textlog{M}}}
@@ -477,7 +477,7 @@ This is entirely standard.
\and
{ \knowInv\iname\prop \Ra \always \knowInv\iname\prop}
\and
-{ \ownGGhost{\munit(\melt)} \Ra \always \ownGGhost{\munit(\melt)}}
+{ \ownGGhost{\mcore\melt} \Ra \always \ownGGhost{\mcore\melt}}
\end{mathpar}
\paragraph{Laws of primitive view shifts.}
--
GitLab