Commit 5b489445 authored by Ralf Jung's avatar Ralf Jung

validity persists

parent 7ada3cbb
......@@ -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.
......
......@@ -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.}
......
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