From 5b489445b8afa149d617d388fd958f692b595b66 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 16 Mar 2016 13:10:21 +0100
Subject: [PATCH] validity persists
---
docs/derived.tex | 2 +-
docs/logic.tex | 3 +++
2 files changed, 4 insertions(+), 1 deletion(-)
diff --git a/docs/derived.tex b/docs/derived.tex
index 29d2b230f..60afd02e5 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 53ba97a9b..6b3c37119 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.}
--
GitLab