docs: define plainly

docs/base-logic.tex

@@ -63,12 +63,13 @@ Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$.
 %\\&
     \ownM{\term} \mid \mval(\term) \mid
     \always\prop \mid
+    \plainly\prop \mid
     {\later\prop} \mid
     \upd \prop
 \end{align*}
 Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality.
 
-Note that the modalities $\upd$, $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
+Note that the modalities $\upd$, $\always$, $\plainly$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
 
 
 \paragraph{Variable conventions.}
@@ -175,6 +176,9 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
 \and
 	\infer{\vctx \proves \wtt{\prop}{\Prop}}
 		{\vctx \proves \wtt{\always\prop}{\Prop}}
+\and
+	\infer{\vctx \proves \wtt{\prop}{\Prop}}
+		{\vctx \proves \wtt{\plainly\prop}{\Prop}}
 \and
 	\infer{\vctx \proves \wtt{\prop}{\Prop}}
 		{\vctx \proves \wtt{\later\prop}{\Prop}}

docs/iris.sty

@@ -260,6 +260,7 @@
 \newcommand{\later}{\mathop{{\triangleright}}}
 \newcommand*{\lateropt}[1]{\mathop{{\later}^{#1}}}
 \newcommand{\always}{\mathop{\Box}}
+\newcommand{\plainly}{\mathop{\blacksquare}}
 
 %% Invariants and Ghost ownership
 % PDS: Was 0pt inner, 2pt outer.

docs/model.tex

@@ -54,10 +54,11 @@ 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\mtimes\meltB \in \mval_m \Ra {} \\
             & m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt\mtimes\meltB)\end{aligned}} \\
-	\Sem{\vctx \proves \always{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\mcore\melt) \\
-	\Sem{\vctx \proves \later{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{n = 0 \lor n-1 \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt)}\\
         \Sem{\vctx \proves \ownM{\term} : \Prop}_\gamma &\eqdef \Lam\meltB. \setComp{n}{\Sem{\vctx \proves \term : \textlog{M}}_\gamma \mincl[n] \meltB}  \\
         \Sem{\vctx \proves \mval(\term) : \Prop}_\gamma &\eqdef \Lam\any. \setComp{n}{\Sem{\vctx \proves \term : \textlog{M}}_\gamma \in \mval_n} \\
+	\Sem{\vctx \proves \always{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\mcore\melt) \\
+	\Sem{\vctx \proves \plainly{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\munit) \\
+	\Sem{\vctx \proves \later{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{n = 0 \lor n-1 \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt)}\\
         \Sem{\vctx \proves \upd\prop : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}
             \All m, \melt'. & m \leq n \land (\melt \mtimes \melt') \in \mval_m \Ra {}\\& \Exists \meltB. (\meltB \mtimes \melt') \in \mval_m \land m \in \Sem{\vctx \proves \prop :\Prop}_\gamma(\meltB)
           \end{aligned}