diff --git a/docs/derived.tex b/docs/derived.tex index 29d2b230faac707ed0cd49714ad2d5efaaf3a42e..60afd02e53f6f1aa66fcf741eb840dad4507d6fd 100644 --- a/docs/derived.tex +++ b/docs/derived.tex @@ -47,7 +47,7 @@ We collect here some important and frequently used derived proof rules. \end{defn} Of course, $\always\prop$ is persistent for any $\prop$. -Furthermore, by the proof rules given above, $t = t'$ as well as $\ownGGhost{\mcore\melt}$ and $\knowInv\iname\prop$ are persistent. +Furthermore, by the proof rules given in \Sref{sec:proof-rules}, $t = t'$ as well as $\ownGGhost{\mcore\melt}$, $\mval(\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. diff --git a/docs/logic.tex b/docs/logic.tex index 53ba97a9bab28ec15c0559d37efcb7828fa071ec..6b3c37119d6f9e2780cca18bd9b40338aaa7c0a9 100644 --- a/docs/logic.tex +++ b/docs/logic.tex @@ -305,6 +305,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $\end{mathparpagebreakable} \subsection{Proof rules} +\label{sec:proof-rules} The judgment$\vctx \mid \pfctx \proves \prop$says that with free variables$\vctx$, proposition$\prop$holds whenever all assumptions$\pfctx$hold. We implicitly assume that an arbitrary variable context,$\vctx\$, is added to every constituent of the rules. @@ -516,6 +517,8 @@ This is entirely standard. { \knowInv\iname\prop \proves \always \knowInv\iname\prop} \and { \ownGGhost{\mcore\melt} \proves \always \ownGGhost{\mcore\melt}} +\and +{ \mval(\melt) \proves \always \mval(\melt)} \end{mathpar} \paragraph{Laws of primitive view shifts.}