Commit fa0ed70a authored by Ralf Jung's avatar Ralf Jung

docs: unit -> core

parent 86bc5be1
Pipeline #285 passed with stage
......@@ -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} \\
......
......@@ -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.
......
......@@ -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}}
......
......@@ -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.}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment