Commit 3ecc71db authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 37db79b9 417e8297
Pipeline #313 passed with stage
...@@ -6,11 +6,11 @@ ...@@ -6,11 +6,11 @@
Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows: Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
\begin{align*} \begin{align*}
\monoid \eqdef{}& \setComp{(c, V) \in (\mathbb{N} \to T) \times \pset{\mathbb{N}}}{ \All n, m. n \geq m \Ra n \in V \Ra m \in V } \\ \monoid \eqdef{}& \recordComp{c : \mathbb{N} \to T , V : \pset{\mathbb{N}}}{ \All n, m. n \geq m \Ra n \in V \Ra m \in V } \\
& \text{quotiented by} \\ & \text{quotiented by} \\
(c_1, V_1) \equiv (c_1, V_2) \eqdef{}& V_1 = V_2 \land \All n. n \in V_1 \Ra c_1(n) \nequiv{n} c_2(n) \\ \melt \equiv \meltB \eqdef{}& \melt.V = \meltB.V \land \All n. n \in \melt.V \Ra \melt.c(n) \nequiv{n} \meltB.c(n) \\
(c_1, V_1) \nequiv{n} (c_1, V_2) \eqdef{}& (\All m \leq n. m \in V_1 \Lra m \in V_2) \land (\All m \leq n. m \in V_1 \Ra c_1(m) \nequiv{m} c_2(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{(c, V) \in \monoid}{ n \in V \land \All m \leq n. c(n) \nequiv{m} 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 \\ \melt \mdiv \meltB \eqdef{}& \melt \\
......
...@@ -59,6 +59,7 @@ ...@@ -59,6 +59,7 @@
\newcommand*\setComp[2]{\left\{#1\spac\middle|\spac#2\right\}} \newcommand*\setComp[2]{\left\{#1\spac\middle|\spac#2\right\}}
\newcommand*\set[1]{\left\{#1\right\}} \newcommand*\set[1]{\left\{#1\right\}}
\newcommand*\record[1]{\left\{\spac#1\spac\right\}} \newcommand*\record[1]{\left\{\spac#1\spac\right\}}
\newcommand*\recordComp[2]{\left\{\spac#1\spac\middle|\spac#2\spac\right\}}
\newenvironment{inbox}[1][]{ \newenvironment{inbox}[1][]{
\begin{array}[#1]{@{}l@{}} \begin{array}[#1]{@{}l@{}}
......
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