docs: timeless assertions

docs/algebra.tex

@@ -116,7 +116,7 @@ This operation is needed to prove that $\later$ commutes with existential quanti
   \item $\munit$ is valid: \\ $\All n. \munit \in \mval_n$
   \item $\munit$ is a left-identity of the operation: \\
     $\All \melt \in M. \munit \mtimes \melt = \melt$
-  \item $\munit$ is a discrete element
+  \item $\munit$ is a discrete COFE element
   \end{enumerate}
 \end{defn}
 

docs/derived.tex

@@ -15,6 +15,29 @@ Persistence is preserved by conjunction, disjunction, separating conjunction as
 
 In our proofs, we will implicitly add and remove $\always$ from persistent assertions as necessary, and generally treat them like normal, non-linear assumptions.
 
+\paragraph{Timeless assertions.}
+
+We can show that the following additional closure properties hold for timeless assertions:
+
+\begin{mathparpagebreakable}
+  \infer
+  {\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
+  {\vctx \proves \timeless{\prop \land \propB}}
+
+  \infer
+  {\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
+  {\vctx \proves \timeless{\prop \lor \propB}}
+
+  \infer
+  {\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
+  {\vctx \proves \timeless{\prop * \propB}}
+
+  \infer
+  {\vctx \proves \timeless{\prop}}
+  {\vctx \proves \timeless{\always\prop}}
+\end{mathparpagebreakable}
+
+
 \subsection{Program logic}
 
 \ralf{Sync this with Coq.}

docs/logic.tex

@@ -137,6 +137,11 @@ Note that $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $
 We will write $\pvs[\term] \prop$ for $\pvs[\term][\term] \prop$.
 If we omit the mask, then it is $\top$ for weakest precondition $\wpre\expr{\Ret\var.\prop}$ and $\emptyset$ for primitive view shifts $\pvs \prop$.
 
+Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
+This is a \emph{meta-level} assertions about propositions, defined as follows:
+
+\[ \vctx \proves \timeless{\prop} \eqdef \vctx\mid\later\prop \proves \prop \lor \later\FALSE \]
+
 
 \paragraph{Metavariable conventions.}
 We introduce additional metavariables ranging over terms and generally let the choice of metavariable indicate the term's type:
@@ -293,15 +298,6 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
 	}
 \end{mathparpagebreakable}
 
-\subsection{Timeless propositions}
-
-Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
-This is a \emph{meta-level} assertions about propositions, defined by the following judgment.
-
-\judgment{Timeless Propositions}{\timeless{P}}
-
-\ralf{Define a judgment that defines them.}
-
 \subsection{Proof rules}
 
 The judgment $\vctx \mid \pfctx \proves \prop$ says that with free variables $\vctx$, proposition $\prop$ holds whenever all assumptions $\pfctx$ hold.
@@ -311,7 +307,7 @@ Axioms $\prop \Ra \propB$ stand for judgments $\vctx \mid \cdot \proves \prop \R
 (Bi-implications are analogous.)
 
 \judgment{}{\vctx \mid \pfctx \proves \prop}
-\paragraph{Laws of intuitionistic higher-order logic.}
+\paragraph{Laws of intuitionistic higher-order logic with equality.}
 This is entirely standard.
 \begin{mathparpagebreakable}
 \infer[Asm]
@@ -418,10 +414,11 @@ This is entirely standard.
 \begin{mathpar}
 \begin{array}{rMcMl}
 \ownGGhost{\melt} * \ownGGhost{\meltB} &\Lra&  \ownGGhost{\melt \mtimes \meltB} \\
-\TRUE &\Ra&  \ownGGhost{\munit}\\
-\ownGGhost{\melt} &\Ra& \melt \in \mval % * \ownGGhost{\melt}
+\ownGGhost{\melt} &\Ra& \melt \in \mval \\
+\TRUE &\Ra&  \ownGGhost{\munit}
 \end{array}
 \and
+\and
 \begin{array}{c}
 \ownPhys{\state} * \ownPhys{\state'} \Ra \FALSE
 \end{array}
@@ -453,6 +450,36 @@ This is entirely standard.
 \end{array}
 \end{mathpar}
 
+\begin{mathpar}
+\infer
+{\text{$\term$ or $\term'$ is a discrete COFE element}}
+{\timeless{\term =_\type \term'}}
+
+\infer
+{\text{$\melt$ is a discrete COFE element}}
+{\timeless{\ownGGhost\melt}}
+
+\infer{}
+{}\timeless{\ownPhys\state}
+
+\infer
+{\vctx \proves \timeless{\propB}}
+{\vctx \proves \timeless{\prop \Ra \propB}}
+
+\infer
+{\vctx \proves \timeless{\propB}}
+{\vctx \proves \timeless{\prop \wand \propB}}
+
+\infer
+{\vctx,\var:\type \proves \timeless{\prop}}
+{\vctx \proves \timeless{\All\var:\type.\prop}}
+
+\infer
+{\vctx,\var:\type \proves \timeless{\prop}}
+{\vctx \proves \timeless{\Exists\var:\type.\prop}}
+\end{mathpar}
+
+
 \paragraph{Laws for the always modality.}
 \begin{mathpar}
 \infer[$\always$I]