proof arch for the lr stuff

paper/gtt.tex

@@ -1710,7 +1710,7 @@ Note that since we are working with preorders and not posets, there
 may be more than one least element in this sense (for example in the
 $\precltdyn$ relation both $\diverge$ and $\err$ are least elements).
 
-\begin{definition}
+\begin{definition}{Finitized Preorder}
   Given a preorder on results $\apreorder$ such that $\diverge$ is a
   least element, we define the \emph{finitization} of $\apreorder$ to
   be, for each natural number $i$, a relation between programs and
@@ -1731,6 +1731,9 @@ makes the logical relation theorem stronger: it proves that diverging
 terms must use recursive types of some sort and so any term that does
 not use them terminates.
 
+% TODO: pole properties go here: down-closed, trivial at 0, indexed
+% anti-reduction (transitivity is later, error awareness is trivial!)
+
 Next, we define the \emph{logical} preorder by induction on types and
 the index $i$ in figure \ref{lr}.
 %
@@ -1739,11 +1742,63 @@ Specifically, for every value type $A$ we define a relation $\ilrof
 computation type $\u B$, we define a relation $\ilrof \apreorder i {\u
   B}$ between stacks \emph{from} $\u B$ to our type of results $\u F
 2$.
+%
+The definition is well-founded using the lexicographic ordering on
+$(i, A)$ and $(i, B)$: either the type reduces and the index stays the
+same or the index reduces.
+%
+We extend the definition to contexts point-wise.
+%
+%TODO: give more explanation about the cases, especially F, U and mu, nu.
+
+Next, analogous to the contextual preorder, we define the
+\emph{logical} preorder on terms, values and stacks.
+\begin{definition}{Logical Preorder}
+  Given a preorder on results $\apreorder$ with $\diverge$ a least
+  element, we define the step-indexed logical preorder as follows:
+  \begin{enumerate}
+  \item $\Gamma \vDash M_1 \ilrof\apreorder{i}{} M_2 \in \u B$ holds
+    when for every $\gamma_1 \ilrof\apreorder i {\Gamma} \gamma_2$ and $S_1
+    \ilrof\apreorder i {\u B} S_2$, $S_1[M_1[\gamma_1]] \ix\apreorder
+    i \result(S_2[M_2[\gamma_2]])$.
+  \item $\Gamma \vDash V_1 \ilrof\apreorder{i}{} V_2 \in A$ holds when
+    for every $\gamma_1 \ilrof\apreorder i {\Gamma} \gamma_2$, $V_1[\gamma_1] \ilrof\apreorder i A V_2[\gamma_2]$
+  \item $\Gamma \pipe \u B \vDash S_1 \ilrof\apreorder{i}{} S_2 \in \u B'$ holds
+    when for every $\gamma_1 \ilrof\apreorder i {\Gamma} \gamma_2$ and
+    $S_1' \ilrof\apreorder i {\u B'} S_2'$, $S_1'[S_1[\gamma_1]] \ilrof \apreorder
+    i {\u B} S_2'[S_2[\gamma_2]])$.
+  \end{enumerate}
+\end{definition}
+
+We next want to prove that the logical preorder is a congruence
+relation, i.e., the fundamental lemma of the logical relation.
+
+% TODO: downward closure lemma
+
+\begin{theorem}{Logical Preorder is a Congruence}
+  For any preorder on results with diverge least element, the logical
+  preorder $\ilrof\apreorder i {}$ is a congruence relation, i.e.,
+  closed under the congruence rules of figure TODO.
+\end{theorem}
+\begin{proof}
+  TODO: adapt from below
+\end{proof}
+
+\begin{corollary}{Reflexivity}
+  For any $\Gamma \vdash M : \u B$, and $i \in \mathbb{N}$,
+  \[\Gamma \vDash M \ilorof\apreorder i {} M \in \u B.\]
+\end{corollary}
+
+% Corollary: relation in the limit recovers the original ordering!
 
+% Lemma: relation is a module of the ordering/infinite relation
 
 \begin{figure}
   \begin{mathpar}
-    {\logty{i}{A}} \subseteq \{ \cdot \vdash V : A \}^2 \quad\qquad{\logty{i}{\u B}}\subseteq \{ \cdot \pipe \u B \vdash S : \u F (1 + 1) \}^2\quad\qquad {\logc{i}} \subseteq \{ \cdot \vdash M : \u F (1 + 1) \}^2\\
+    {\logty{i}{A}} \subseteq \{ \cdot \vdash V : A \}^2
+    \quad\qquad{\logty{i}{\u B}}\subseteq \{ \cdot \pipe \u B \vdash S
+    : \u F (1 + 1) \}^2\quad\qquad {\logc{i}} \subseteq \{ \cdot
+    \vdash M : \u F (1 + 1) \}^2\\
     \begin{array}{rcl}
       \Gamma \vDash M_1 \ltdyn M_2 \in \u B &=& \forall i \in \mathbb{N}, \gamma_1 \logty i \Gamma \gamma_2, S_1 \logty i {\u B} S_2.~ S_1[M_1[\gamma_1]] \logc i S_2[M_2[\gamma_2]]\\
       \Gamma \vDash V_1 \ltdyn V_2 \in A &=& \forall i \in \mathbb{N}, \gamma_1 \logty i \Gamma \gamma_2.~ V_1[\gamma_1] \logty i A V_2[\gamma_2]\\