Commit d6dba217 authored by Ralf Jung's avatar Ralf Jung

docs: get rid of division :)

parent 417e8297
...@@ -49,7 +49,7 @@ Note that $\COFEs$ is cartesian closed. ...@@ -49,7 +49,7 @@ Note that $\COFEs$ is cartesian closed.
\subsection{CMRA} \subsection{CMRA}
\begin{defn} \begin{defn}
A \emph{CMRA} is a tuple $(\monoid : \COFEs, (\mval_n \subseteq \monoid)_{n \in \mathbb{N}}, \mcore{-}: \monoid \nfn \monoid, (\mtimes) : \monoid \times \monoid \nfn \monoid, (\mdiv) : \monoid \times \monoid \nfn \monoid)$ satisfying A \emph{CMRA} is a tuple $(\monoid : \COFEs, (\mval_n \subseteq \monoid)_{n \in \mathbb{N}}, \mcore{-}: \monoid \nfn \monoid, (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying
\begin{align*} \begin{align*}
\All n, \melt, \meltB.& \melt \nequiv{n} \meltB \land \melt\in\mval_n \Ra \meltB\in\mval_n \tagH{cmra-valid-ne} \\ \All n, \melt, \meltB.& \melt \nequiv{n} \meltB \land \melt\in\mval_n \Ra \meltB\in\mval_n \tagH{cmra-valid-ne} \\
\All n, m.& n \geq m \Ra V_n \subseteq V_m \tagH{cmra-valid-mono} \\ \All n, m.& n \geq m \Ra V_n \subseteq V_m \tagH{cmra-valid-mono} \\
...@@ -59,7 +59,6 @@ Note that $\COFEs$ is cartesian closed. ...@@ -59,7 +59,6 @@ Note that $\COFEs$ is cartesian closed.
\All \melt.& \mcore{\mcore\melt} = \mcore\melt \tagH{cmra-core-idem} \\ \All \melt.& \mcore{\mcore\melt} = \mcore\melt \tagH{cmra-core-idem} \\
\All \melt, \meltB.& \melt \mincl \meltB \Ra \mcore\melt \mincl \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 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 {}$} \\ \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} \\ &\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\\ \text{where}\qquad\qquad\\
...@@ -70,8 +69,6 @@ Note that $\COFEs$ is cartesian closed. ...@@ -70,8 +69,6 @@ Note that $\COFEs$ is cartesian closed.
This is a natural generalization of RAs over COFEs. This is a natural generalization of RAs over COFEs.
All operations have to be non-expansive, and the validity predicate $\mval$ can now also depend on the step-index. All operations have to be non-expansive, and the validity predicate $\mval$ can now also depend on the step-index.
\ralf{TODO: Get rid of division.}
\paragraph{The extension axiom (\ruleref{cmra-extend}).} \paragraph{The extension axiom (\ruleref{cmra-extend}).}
Notice that the existential quantification in this axiom is \emph{constructive}, \ie it is a sigma type in Coq. Notice that the existential quantification in this axiom is \emph{constructive}, \ie it is a sigma type in Coq.
The purpose of this axiom is to compute $\melt_1$, $\melt_2$ completing the following square: The purpose of this axiom is to compute $\melt_1$, $\melt_2$ completing the following square:
......
...@@ -12,8 +12,7 @@ Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows: ...@@ -12,8 +12,7 @@ Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
\melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.V \Lra m \in \meltB.V) \land (\All m \leq n. m \in \melt.V \Ra \melt.c(m) \nequiv{m} \meltB.c(m)) \\ \melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.V \Lra m \in \meltB.V) \land (\All m \leq n. m \in \melt.V \Ra \melt.c(m) \nequiv{m} \meltB.c(m)) \\
\mval_n \eqdef{}& \setComp{\melt \in \monoid}{ n \in \melt.V \land \All m \leq n. \melt.c(n) \nequiv{m} \melt.c(m) } \\ \mval_n \eqdef{}& \setComp{\melt \in \monoid}{ n \in \melt.V \land \All m \leq n. \melt.c(n) \nequiv{m} \melt.c(m) } \\
\mcore\melt \eqdef{}& \melt \\ \mcore\melt \eqdef{}& \melt \\
\melt \mtimes \meltB \eqdef{}& (\melt.c, \setComp{n}{n \in \melt.V \land n \in \meltB.V_2 \land \melt \nequiv{n} \meltB }) \\ \melt \mtimes \meltB \eqdef{}& (\melt.c, \setComp{n}{n \in \melt.V \land n \in \meltB.V_2 \land \melt \nequiv{n} \meltB })
\melt \mdiv \meltB \eqdef{}& \melt \\
\end{align*} \end{align*}
$\agm(-)$ is a locally non-expansive bifunctor from $\COFEs$ to $\CMRAs$. $\agm(-)$ is a locally non-expansive bifunctor from $\COFEs$ to $\CMRAs$.
......
...@@ -140,7 +140,6 @@ ...@@ -140,7 +140,6 @@
\newcommand{\munit}{\varepsilon} \newcommand{\munit}{\varepsilon}
\newcommand{\mcore}[1]{\lfloor#1\rfloor} \newcommand{\mcore}[1]{\lfloor#1\rfloor}
\newcommand{\mtimes}{\mathbin{\cdot}} \newcommand{\mtimes}{\mathbin{\cdot}}
\newcommand{\mdiv}{\mathbin{\div}}
\newcommand{\mupd}{\rightsquigarrow} \newcommand{\mupd}{\rightsquigarrow}
\newcommand{\mincl}[1][]{\ensuremath{\mathrel{\stackrel{#1}{\preccurlyeq}}}} \newcommand{\mincl}[1][]{\ensuremath{\mathrel{\stackrel{#1}{\preccurlyeq}}}}
......
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