From cfa6acb017b874d81cabbb850d69ca2c122fecf1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 17 Oct 2016 14:41:32 +0200
Subject: [PATCH] Define macro for singleton map and use it.
---
docs/constructions.tex | 8 ++++----
docs/ghost-state.tex | 2 +-
docs/iris.sty | 2 ++
docs/model.tex | 12 ++++++------
docs/program-logic.tex | 12 ++++++++++--
5 files changed, 23 insertions(+), 13 deletions(-)
diff --git a/docs/constructions.tex b/docs/constructions.tex
index e7607889b..433361253 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -55,7 +55,7 @@ Frame-preserving updates on the $M_i$ lift to the product:
\begin{mathpar}
\inferH{prod-update}
{\melt \mupd_{M_i} \meltsB}
- {f[i \mapsto \melt] \mupd \setComp{ f[i \mapsto \meltB]}{\meltB \in \meltsB}}
+ {\mapinsert i \melt f \mupd \setComp{ \mapinsert i \meltB f}{\meltB \in \meltsB}}
\end{mathpar}
\subsection{Sum}
@@ -96,15 +96,15 @@ We obtain the following frame-preserving updates:
\begin{mathpar}
\inferH{fpfn-alloc-strong}
{\text{$G$ infinite} \and \melt \in \mval}
- {\emptyset \mupd \setComp{[\gname \mapsto \melt]}{\gname \in G}}
+ {\emptyset \mupd \setComp{\mapsingleton \gname \melt}{\gname \in G}}
\inferH{fpfn-alloc}
{\melt \in \mval}
- {\emptyset \mupd \setComp{[\gname \mapsto \melt]}{\gname \in K}}
+ {\emptyset \mupd \setComp{\mapsingleton \gname \melt}{\gname \in K}}
\inferH{fpfn-update}
{\melt \mupd_\monoid \meltsB}
- {f[i \mapsto \melt] \mupd \setComp{ f[i \mapsto \meltB]}{\meltB \in \meltsB}}
+ {\mapinsert i \melt f] \mupd \setComp{ \mapinsert i \meltB f}{\meltB \in \meltsB}}
\end{mathpar}
Above, $\mval$ refers to the validity of $\monoid$.
diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index d5226a1ec..0d7da30da 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -197,7 +197,7 @@ This is best demonstrated by giving some proof rules.
So let us first define the notion of ghost ownership that we use in this logic.
Assuming that the family of functors contains the functor $\Sigma_i$ at index $i$, and furthermore assuming that $\monoid_i = \Sigma_i(\iPreProp, \iPreProp)$, given some $\melt \in \monoid_i$ we define:
-\[ \ownGhost\gname{\melt:\monoid_i} \eqdef \ownM{(\ldots, \emptyset, i:\set{\gname \mapsto \melt}, \emptyset, \ldots)} \]
+\[ \ownGhost\gname{\melt:\monoid_i} \eqdef \ownM{(\ldots, \emptyset, i:\mapsingleton \gname \melt, \emptyset, \ldots)} \]
This is ownership of the pair (element of the product over all the functors) that has the empty finite partial function in all components \emph{except for} the component corresponding to index $i$, where we own the element $\melt$ at index $\gname$ in the finite partial function.
We can show the following properties for this form of ownership:
diff --git a/docs/iris.sty b/docs/iris.sty
index 656e45861..4100a6592 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -85,6 +85,8 @@
\newcommand{\subst}[3]{{#1}[{#3} / {#2}]}
\newcommand{\mapinsert}[3]{#3[#1:=#2]}
+\newcommand{\mapsingleton}[2]{[#1:=#2]}
+\newcommand{\mapsingletonComp}[3]{\left[ #1 := #2 \spac\middle|\spac #3 \right]}
\newcommand{\nil}{\epsilon}
diff --git a/docs/model.tex b/docs/model.tex
index bb91207bb..4a97f7a0a 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -42,10 +42,10 @@ We are thus going to define the assertions as mapping CMRA elements to sets of s
\Lam \melt. \setComp{n}{\begin{aligned}
\All m, \meltB.& m \leq n \land \melt \mincl \meltB \land \meltB \in \mval_m \Ra {} \\
& m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\meltB)\end{aligned}}\\
- \Sem{\vctx \proves \All x : \type. \prop : \Prop}_\gamma &\eqdef
- \Lam \melt. \setComp{n}{ \All v \in \Sem{\type}. n \in \Sem{\vctx, x : \type \proves \prop : \Prop}_{\gamma[x \mapsto v]}(\melt) } \\
- \Sem{\vctx \proves \Exists x : \type. \prop : \Prop}_\gamma &\eqdef
- \Lam \melt. \setComp{n}{ \Exists v \in \Sem{\type}. n \in \Sem{\vctx, x : \type \proves \prop : \Prop}_{\gamma[x \mapsto v]}(\melt) } \\
+ \Sem{\vctx \proves \All \var : \type. \prop : \Prop}_\gamma &\eqdef
+ \Lam \melt. \setComp{n}{ \All v \in \Sem{\type}. n \in \Sem{\vctx, \var : \type \proves \prop : \Prop}_{\mapinsert \var v \gamma}(\melt) } \\
+ \Sem{\vctx \proves \Exists \var : \type. \prop : \Prop}_\gamma &\eqdef
+ \Lam \melt. \setComp{n}{ \Exists v \in \Sem{\type}. n \in \Sem{\vctx, \var : \type \proves \prop : \Prop}_{\mapinsert \var v \gamma}(\melt) } \\
~\\
\Sem{\vctx \proves \prop * \propB : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}\Exists \meltB_1, \meltB_2. &\melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \land {}\\& n \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB_1) \land n \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\meltB_2)\end{aligned}}
\\
@@ -72,11 +72,11 @@ For every definition, we have to show all the side-conditions: The maps have to
\Sem{\vctx \proves x : \type}_\gamma &\eqdef \gamma(x) \\
\Sem{\vctx \proves \sigfn(\term_1, \dots, \term_n) : \type_{n+1}}_\gamma &\eqdef \Sem{\sigfn}(\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \dots, \Sem{\vctx \proves \term_n : \type_n}_\gamma) \\
\Sem{\vctx \proves \Lam \var:\type. \term : \type \to \type'}_\gamma &\eqdef
- \Lam \termB : \Sem{\type}. \Sem{\vctx, \var : \type \proves \term : \type}_{\gamma[\var \mapsto \termB]} \\
+ \Lam \termB : \Sem{\type}. \Sem{\vctx, \var : \type \proves \term : \type}_{\mapinsert \var \termB \gamma]} \\
\Sem{\vctx \proves \term(\termB) : \type'}_\gamma &\eqdef
\Sem{\vctx \proves \term : \type \to \type'}_\gamma(\Sem{\vctx \proves \termB : \type}_\gamma) \\
\Sem{\vctx \proves \MU \var:\type. \term : \type}_\gamma &\eqdef
- \mathit{fix}(\Lam \termB : \Sem{\type}. \Sem{\vctx, x : \type \proves \term : \type}_{\gamma[x \mapsto \termB]}) \\
+ \mathit{fix}(\Lam \termB : \Sem{\type}. \Sem{\vctx, x : \type \proves \term : \type}_{\mapinsert \var \termB \gamma}) \\
~\\
\Sem{\vctx \proves () : 1}_\gamma &\eqdef () \\
\Sem{\vctx \proves (\term_1, \term_2) : \type_1 \times \type_2}_\gamma &\eqdef (\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \Sem{\vctx \proves \term_2 : \type_2}_\gamma) \\
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 77f010aea..c292b837a 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -85,12 +85,20 @@ Furthermore, we assume that instances named $\gname_{\textmon{State}}$, $\gname_
\paragraph{World Satisfaction.}
We can now define the assertion $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
\begin{align*}
- W \eqdef{}& \Exists I : \mathbb N \fpfn \Prop. \ownGhost{\gname_{\textmon{Inv}}}{\authfull \setComp{\iname \mapsto \aginj(\latertinj(\wIso(I(\iname))))}{\iname \in \dom(I)}} * \Sep_{\iname \in \dom(I)} \left( \later I(\iname) * \ownGhost{\gname_{\textmon{Dis}}}{\set{\iname}} \lor \ownGhost{\gname_{\textmon{En}}}{\set{\iname}} \right)
+ W \eqdef{}& \Exists I : \mathbb N \fpfn \Prop.
+ \begin{array}{@{} l}
+ \ownGhost{\gname_{\textmon{Inv}}}{\authfull
+ \mapsingletonComp {\iname}
+ {\aginj(\latertinj(\wIso(I(\iname))))}
+ {\iname \in \dom(I)}} * \\
+ \Sep_{\iname \in \dom(I)} \left( \later I(\iname) * \ownGhost{\gname_{\textmon{Dis}}}{\set{\iname}} \lor \ownGhost{\gname_{\textmon{En}}}{\set{\iname}} \right)
+ \end{array}
\end{align*}
\paragraph{Invariants.}
The following assertion states that an invariant with name $\iname$ exists and maintains assertion $\prop$:
-\[ \knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}}{\authfrag\set{\iname \mapsto \aginj(\latertinj(\wIso(\prop)))}} \]
+\[ \knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}}
+ {\authfrag \mapsingleton \iname {\aginj(\latertinj(\wIso(\prop)))}} \]
\paragraph{View Updates and View Shifts.}
Next, we define \emph{view updates}, which are essentially the same as the resource updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants:
--
GitLab