\documentclass{article}

\usepackage[supertabular]{ottalt}
\let\newlist\relax
\let\renewlist\relax
\usepackage[T1]{fontenc}
\usepackage{mlmodern}
\usepackage[margin=1in]{geometry}
\usepackage{enumitem,float,booktabs,xspace,doi}
\usepackage{amsmath,amsthm,amssymb}
\usepackage[capitalize,nameinlink]{cleveref}
\usepackage{mathpartir,mathtools,stmaryrd}

\setlist{nosep}
\hypersetup{
  colorlinks=true,
  urlcolor=blue,
  linkcolor=magenta,
  citecolor=teal
}
\urlstyle{tt}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}{Definition}

\newcommand{\ie}{\textit{i.e.}\@\xspace}
\newcommand{\ala}{\textit{\`a la}\@\xspace}
\newcommand{\apriori}{\textit{a priori}\@\xspace}
\newcommand{\aposteriori}{\textit{a posteriori}\@\xspace}

\title{Strong Normalization for \\ Simply Typed Call-by-Push-Value}
\author{Jonathan Chan}
\date{}

\inputott{rules}

\begin{document}
\maketitle

\section{Introduction}

The goal of this project is to mechanize a proof of strong normalization for call-by-push-value (CBPV).
It follows work by Forster, Sch\"afer, Spies, and Stark (TODO: cite) on mechanizing the metatheory of CBPV in Rocq,
but instead adapts the proof technique from POPLMark Reloaded (TODO: cite).

Both proofs, and mine, follow the same sequence of steps:
we define a logical relation that semantically interpret types as sets of terms,
show that these sets are backward closed by reduction and that they contain only strongly normalizing terms,
prove a fundamental soundness theorem that places well typed terms in the semantic interpretations of their types,
and conclude that well typed terms must be strongly normalizing.
The difference lies in \emph{how strong normalization} (and reduction) is defined.
The Rocq mechanization uses a traditional definition of strong normalization as an accessibility relation,
while POPLMark Reloaded and this project use an inductive characterization of strong normalization,
then prove it sound with respect to the traditional definition.

In contrast to both prior works, which use Rocq, Agda, or Beluga,
this project is mechanized in Lean.
A secondary purpose of this project is to assess the capabilities of Lean for PL metatheory,
especially when making heavy use of mutually defined inductive types.
I have implemented a mutual induction tactic for Lean (TODO: link),
and the mutual values and computations of CBPV,
combined with the even more complex mutual inductives from POPLMark Reloaded,
make it an attractive test case to test the tactic's robustness.

This report is divided in roughly the same shape as the proof development.
\Cref{sec:syntax} introduces the syntax and the typing rules for CBPV (\texttt{Syntax.lean}, \texttt{Typing.lean}).
Then the inductive characterization of strong normalization is defined in \cref{sec:sn-ind} (\texttt{NormalInd.lean}),
followed by the logical relation in \cref{sec:lr} (\texttt{OpenSemantics.lean}).
The central theorem of strong normalization is proven in \cref{sec:soundness}
as a corollary of the fundamental theorem for the logical relation (\texttt{Soundness.lean}, \texttt{Normalization.lean}).
To ensure that the inductive characterization is correct,
\cref{sec:sn-acc} shows that it implies the traditional definition of strong normalization (\texttt{NormalAcc.lean}).
This latter definition and proof depends on small-step reduction on open terms,
whose properties are omitted here (\texttt{Reduction.lean}).
In general, I gloss over details about substitution and reduction,
since I'm interested in presenting the structure of the strong normalization proof
and not the minutiae of syntax and binding.
Finally, I discuss the merits of this proof technique
and the challenges posed by using Lean in \cref{sec:discussion}.

\section{Syntax and Typing} \label{sec:syntax}

\begin{align*}
  [[A]] &\Coloneqq [[Unit]] \mid [[A1 + A2]] \mid [[U B]] & \textit{value types} \\
  [[B]] &\Coloneqq [[A → B]] \mid [[F A]] & \textit{computation types} \\
  [[v]], [[w]] &\Coloneqq [[x]] \mid [[unit]] \mid [[inl v]] \mid [[inr v]] \mid [[thunk m]] & \textit{values} \\
  [[m]], [[n]] &\Coloneqq [[force v]] \mid [[λx. m]] \mid [[m v]] \mid [[ret v]] & \textit{computations} \\
  & \mid [[let x m n]] \\
  & \mid [[case v | y.m | z.n]] \\
  [[G]] &\Coloneqq [[•]] \mid [[G, x : A]] & \textit{typing contexts} \\
  [[s]] &\Coloneqq [[•]] \mid [[s, x ↦ v]] & \textit{simultaneous substitutions}
\end{align*}

The grammar of the CBPV for this project is given above.
Terms and their types are divided between \emph{values} and \emph{computations}.
Values are variables, unit, injections into a sum type, or a thunked computation,
while computations are forcing thunks,
functions, applications, returning values, binding returned values,
and case analysis on sums.
There are only value variables and no computation variables,
since they represent terms that require no more work to be done on them ready to be substituted in,
and typing contexts similarly only contain value types.
I use $t$ to refer to terms that may be either values or computations.

Although the syntax is presented nominally,
the mechanization uses an unscoped de Bruijn indexed representation of variables,
along with simultaneous substitutions $[[s]]$ mapping variables to values,
with $[[•]]$ as the identity substitution.
Applying a substitution is represented as $[[v{s}]]$ and $[[m{s}]]$,
and implemented in terms of renamings,
which are mappings from variables to other variables.

This is not the usual complete CBPV language,
since it's missing both value tuples and computation tuples.
I exclude them because they are syntactically not much more interesting than returns,
whose eliminator is shaped like pattern matching on a singleton value tuple,
and than thunks,
whose eliminator is shaped like projection on a singleton computation tuple.
In contrast, I do include sums, which represent the only way a computation can branch.

The typing rules below are standard for the values and computations included.
The judgements for values and computations are defined mutually,
just as are the types and the terms.

\drules[T]{$[[G ⊢ v : A]]$}{value typing}{Var,Unit,Inl,Inr,Thunk}
\drules[T]{$[[G ⊢ m : B]]$}{computation typing}{Force,Lam,App,Ret,Let,Case}

\section{Strong Normalization as an Inductive Definition} \label{sec:sn-ind}

The idea behind the inductive characterization of strong normalization
is to describe case by case when a term is strongly normal,
rather than showing \aposteriori which terms are strongly normal.
This is done in conjunction with defining strongly neutral terms,
which are blocked from $\beta$-reduction,
and strong head reduction,
which expands the set from normal forms
to terms which must reduce to normal forms.

The general recipe for defining these for CBPV is as follows:
\begin{itemize}[rightmargin=\leftmargin]
  \item The only strongly neutral values are variables.
  \item Strongly neutral computations are eliminators
    whose head positions are strongly neutral,
    while all other subterms are strongly normal.
  \item Strongly normal values are constructors
    whose subterms are strongly normal,
    or strongly neutral values, \ie variables.
  \item Strongly normal computations are constructors
    whose subterms are strongly normal,
    or strongly neutral computations,
    or computations which reduce to strongly normal computations
    (backward closure).
  \item Strong head reduction consists of $\beta$ reductions
    for all eliminators around the corresponding constructors,
    and congruent reductions in head positions.
\end{itemize}

Additionally, strong reduction requires premises asserting that
the subterms that may ``disappear'' after reduction be strongly normal
so that backward closure actually closes over strongly normal terms.
These subterms are the values that get substituted into a computation,
which may disappear if the computation never actually uses the binding,
as well as computation branches not taken.

Because we're dealing with CBPV, values have no $\beta$ reductions,
so there's no need for head reduction of values as there are no heads.
Furthermore, there is only one strongly neutral value,
so we inline the definition as a variable where needed,
but also write it as $[[v ∈ SNe]]$ for symmetry as appropriate.
Otherwise, the remaining four judgements are defined mutually below.

\drules[SNe]{$[[m ∈ SNe]]$}{strongly neutral computations}{Force,App,Let,Case}
\drules[SN]{$[[v ∈ SN]]$}{strongly normal values}{Var,Unit,Inl,Inr,Thunk}
\drules[SN]{$[[m ∈ SN]]$}{strongly normal computations}{Lam,Ret,SNe,Red}
\drules[SR]{$[[m ⤳ n]]$}{strong head reduction}{Thunk,Lam,Ret,Inl,Inr,App,Let}
\drules[SRs]{$[[m ⤳* n]]$}{reflexive, transitive closure of head reduction}{Refl,Trans}

We also need the reflexive, transitive closure of head reduction,
defined as a separate inductive above.
Now we show a few simple lemmas about it,
along with an inversion lemma for forcing
(other inversion lemmas hold, but this is the only one we need).
I present them below as judgement pseudorules
using a dashed line to indicate that they are admissible rules.
These are all proven either by construction
or by induction on the first premise.

\begin{mathpar}
\mprset{fraction={-~}{-~}{-}}
\drule[]{SRs-Once}
\drule[]{SRs-TransPP}
\drule[]{SRs-App}
\drule[]{SRs-Let}
\drule[]{SN-Reds}
\drule[]{SN-Force-inv}
\end{mathpar}

The most important property of strongly normal terms that we need is antirenaming,
which states that undoing a renaming does not change the term's
normalization or reduction behaviour.
A crucial property that follows is extensionality of applications,
which is an inversion lemma specifically when the application argument is a variable.

\begin{lemma}[Antirenaming] \label{thm:antisubst}
  Let $[[s]]$ be a renaming,
  \ie a substitution mapping variables to variables.
  Then the following hold:
  \begin{enumerate}
    \item If $[[m{s} ∈ SNe]]$ then $[[m ∈ SNe]]$.
    \item If $[[v{s} ∈ SN]]$ then $[[v ∈ SN]]$.
    \item If $[[m{s} ∈ SN]]$ then $[[m ∈ SN]]$.
    \item If $[[m{s} ⤳ n]]$ then there exists some $[[n']]$
      such that $[[n]] = [[n'{s}]]$ and $[[m ⤳ n']]$.
  \end{enumerate}
\end{lemma}

\begin{proof}
  By mutual induction on the four derivations of
  $[[m{s} ∈ SNe]]$, $[[v{s} ∈ SN]]$, $[[m{s} ∈ SN]]$, and $[[m{s} ⤳ n]]$.
\end{proof}

\begin{corollary}[Extensionality] \label{cor:ext}
  If $[[m x ∈ SN]]$ then $[[m ∈ SN]]$.
\end{corollary}

\begin{proof}
  By induction on the derivation of strongly normal values.
  The possible cases are \rref*{SN-SNe,SN-Red}.
  Destructing the premise of the former gives $[[m ∈ SNe]]$,
  and we conclude using \rref{SN-SNe} again.
  In the latter case, we have $[[m x ⤳ n]]$ and $[[n ∈ SN]]$;
  destructing on the reduction yields the possible cases
  \rref{SR-Lam,SR-App}.
  In the first case, we have $[[m{x ↦ v} ∈ SN]]$,
  so the goal holds by \nameref{thm:antisubst}.
  In the second case, we have $[[m ⤳ n]]$ and $[[n x ∈ SN]]$,
  so by the induction hypothesis, we have $[[n ∈ SN]]$,
  and we conclude using \rref{SN-Red}.
\end{proof}

\section{Logical Relation on Open Terms} \label{sec:lr}

The next step is to define a logical relation that semantically interprets types
as sets of open terms.
The key property we need from these sets is that they contain only strongly normal terms.
Because we are working with open terms to prove normalization
and not just termination of evaluation of closed terms,
we need to consider variables and strongly neutral terms.
Having no other information about them other than their strong neutrality,
we require that the interpretation sets always contain all strongly neutral terms.

The logical relation on simple types can be defined by induction on the structure of the type.
However, I want to maximize the amount of mutual inductives used in this project,
so we instead define the logical relation as an inductive binary relation
between the type and the set of terms of its interpretation,
denoted as $[[⟦A⟧ ↘ P]]$ and $[[⟦B⟧ ↘ P]]$ below.
I use set builder notation to define the sets and set membership,
but they are implemented in the mechanization as functions
that take terms and return propositions and as function applications.
Here, the conjunctions ($\wedge$), disjunctions ($\vee$), equalities ($=$), implications ($\Rightarrow$),
and universal ($\forall$) and existential ($\exists$) quantifiers
are part of the metatheory, not part of the object language.

\drules[LR]{$[[⟦A⟧ ↘ P]]$}{semantic interpretation of value types}{Unit,U,Sum}
\drules[LR]{$[[⟦B⟧ ↘ P]]$}{semantic interpretation of computation types}{F,Arr}

The terms in the interpretation of a type can be characterized in two different ways:
by what constructor of that type they reduce to,
or by how they act when eliminated by an eliminator for that type.
For the former, we need to explicitly include the possibility of the term being strongly neutral.
I chose the following characterizations because they seemed the simplest to me,
but the alternate choices likely work as well.

\begin{itemize}[noitemsep,rightmargin=\leftmargin]
  \item Values in the interpretation of the unit type
    are either variables or the unit value.
  \item Values are in the interpretation of the $[[U B]]$ type
    if they can be forced to computations in the interpretation of the $[[B]]$ type.
  \item Values in the interpretation of the sum type $[[A1 + A2]]$ are either variables,
    left injections whose values are in the interpretation of $[[A1]]$,
    or right injections whose values are in that of $[[A2]]$.
  \item Computations in the interpretation of the $[[F A]]$ type
    reduce to either a neutral computation
    or a return whose value is in the interpretation of $[[A]]$.
  \item Computations are in the interpretation of the function type $[[A → B]]$
    if applying them to values in the interpretation of $[[A]]$
    yields computations in the interpretation of $[[B]]$.
\end{itemize}

By this description, it sounds like the logical relation can be presented
directly as a relation between a type and a term;
this presentation is given in \cref{fig:lr-alt}.
Unfortunately, this is not well defined,
since the logical relation appears in a negative position
(to the left of an implication) in the premise of \rref{LRPP-Arr}.
The alternate presentation can be interpreted as a function
match on the term and the type and returning the conjunction of its premises,
but I wanted to use a mutually defined inductive definition.

\begin{figure}[H]
\fbox{$[[v ∈ ⟦A⟧]]$} \quad \fbox{$[[m ∈ ⟦B⟧]]$} \hfill \textit{} \\
\begin{mathpar}
\drule[]{LRPP-Unit-var}
\drule[]{LRPP-Unit-unit}
\drule[]{LRPP-Sum-var}
\drule[]{LRPP-Sum-inl}
\drule[]{LRPP-Sum-inr}
\drule[]{LRPP-Force}
\drule[]{LRPP-F-var}
\drule[]{LRPP-F-ret}
\drule[]{LRPP-Arr}
\end{mathpar}
\caption{Alternate presentation of the logical relation}
\label{fig:lr-alt}
\end{figure}

Using the inductive presentation of the logical relation,
there are three easy properties to show:
interpretability, which states that all types have an interpretation;
determinism, which states that the interpretation indeed behaves like a function
from types to sets of terms;
and backward closure, which states that the interpretations of computation types
are backward closed under multi-step head reduction.
The last property is why \rref{LRPP-F-var} needs to include
computations that \emph{reduce to} strongly neutral terms or returns,
not merely ones that are such terms.

\begin{lemma}[Interpretability] \label{lem:interp} \leavevmode
  \begin{enumerate}
    \item Given $[[A]]$, there exists $[[P]]$ such that $[[⟦A⟧ ↘ P]]$.
    \item Given $[[B]]$, there exists $[[P]]$ such that $[[⟦B⟧ ↘ P]]$.
  \end{enumerate}
\end{lemma}

\begin{proof}
  By mutual induction on the types $[[A]]$ and $[[B]]$.
\end{proof}

\begin{lemma}[Determinism] \label{lem:det} \leavevmode
  \begin{enumerate}
    \item If $[[⟦A⟧ ↘ P]]$ and $[[⟦A⟧ ↘ Q]]$ then $[[P]] = [[Q]]$.
    \item If $[[⟦B⟧ ↘ P]]$ and $[[⟦B⟧ ↘ Q]]$ then $[[P]] = [[Q]]$.
  \end{enumerate}
\end{lemma}

\begin{proof}
  By mutual induction on the first derivations of the logical relation,
  then by cases on the second derivations.
\end{proof}

\begin{lemma}[Backward closure] \label{lem:closure}
  Given $[[⟦B⟧ ↘ P]]$ and $[[m ⤳* n]]$,
  if $[[n ∈ P]]$ then $[[m ∈ P]]$.
\end{lemma}

\begin{proof}
  By induction on the derivation of the logical relation.
\end{proof}

The final key property is adequacy,
which states that the interpretations of types
must contain all strongly neutral terms
and must contain only strongly normal terms.
Such sets are said to be \emph{reducibility candidates}.

\begin{definition}[Reducibility candidates]
  A reducibility candidate is a set of terms $[[P]]$ where,
  given a term $[[t]]$,
  if $[[t ∈ SNe]]$ then $[[t ∈ P]]$, and
  if $[[t ∈ P]]$ then $[[t ∈ SN]]$.
\end{definition}

\begin{lemma}[Adequacy] \label{lem:adequacy} \leavevmode
  \begin{enumerate}
    \item If $[[⟦A⟧ ↘ P]]$ then $[[P]]$ is a reducibility candidate.
    \item If $[[⟦B⟧ ↘ P]]$ then $[[P]]$ is a reducibility candidate.
  \end{enumerate}
\end{lemma}

\begin{proof}
  By mutual induction on the derivations of the logical relation.
  \Rref{SN-Force-inv} is used in the \rref*{S-U} case,
  while \rref{SN-Reds} is used in the \rref{S-F} case.
  In the \rref*{S-Arr} case on $[[A → B]]$,
  where $[[⟦A⟧ ↘ P]]$ and $[[⟦B⟧ ↘ Q]]$,
  to show the second part of its interpretation being a reducibility candidate,
  we are given $[[m]]$ such that for every $[[v ∈ P]]$, $[[m v ∈ Q]]$,
  and the goal is to show that $[[m ∈ SN]]$.
  By the induction hypotheses, picking an arbitrary variable $[[x]]$,
  we have that $[[x ∈ P]]$ (since it is neutral) and that $[[m x ∈ SN]]$.
  Then the goal holds by \nameref{cor:ext}.
\end{proof}

\section{Semantic Typing and the Fundamental Theorem} \label{sec:soundness}

Now that we know that the interpretations contain only strongly normal terms,
our goal is to show that well typed terms inhabit the interpretations of their types.
We first define what it means for a substitution to be
semantically well formed with respect to a context.

\begin{definition}[Semantic well-formedness of substitutions]
  A substitution $[[s]]$ is well formed with respect to a context $[[G]]$,
  written $[[G ⊧ s]]$, if for every $[[x : A ∈ G]]$ and $[[⟦A⟧ ↘ P]]$,
  we have $[[x{s} ∈ P]]$.
  In short, the substitution maps variables in the context
  to values in the interpretations of their types.
\end{definition}

These judgements can be built up inductively,
as demonstrated by the below admissible rules,
which are proven by cases.

{\mprset{fraction={-~}{-~}{-}}
\drules[S]{$[[G ⊧ s]]$}{admissible semantic substitution well-formedness}{Nil,Cons}
}

Then we can define semantic typing in terms of the logical relation,
using semantic well formedness of substitutions to handle the context.

\begin{definition}[Semantic typing]
  \begin{enumerate}[rightmargin=\leftmargin] \leavevmode
    \item $[[v]]$ semantically has type $[[A]]$ under context $[[G]]$,
      written $[[G ⊧ v : A]]$, if for every $[[s]]$ such that $[[G ⊧ s]]$,
      there exists an interpretation $[[⟦A⟧ ↘ P]]$ such that $[[v{s} ∈ P]]$.
    \item $[[m]]$ semantically has type $[[B]]$ under context $[[G]]$,
      written $[[G ⊧ m : B]]$, if for every $[[s]]$ such that $[[G ⊧ s]]$,
      there exists an interpretation $[[⟦B⟧ ↘ P]]$ such that $[[m{s} ∈ P]]$.
  \end{enumerate}
\end{definition}

Semantic typing follows exactly the same shape of rules as syntactic typing,
so I present them here as admissible rules.
All the hard work happens in these lemmas;
the fundamental theorem of soundness of syntactic typing with respect to semantic typing
then follows directly.
Normalization holds as an easy corollary.

{\mprset{fraction={-~}{-~}{-}}
\drules[S]{$[[G ⊧ v : A]]$}{admissible semantic value typing}{Var,Unit,Inl,Inr,Thunk}
\drules[S]{$[[G ⊧ m : B]]$}{admissible semantic computation typing}{Force,Arr,App,Ret,Let,Case}
}

\begin{proof}
  By construction using prior lemmas,
  in particular \rref{SRs-Let} in case \rref*{S-Let};
  \nameref{lem:interp} in cases \rref*{S-Var,S-Inl,S-Inr,S-Lam};
  \nameref{lem:det} in cases \rref*{S-Lam,S-App};
  \nameref{lem:closure} in cases \rref*{S-Thunk,S-Lam,S-Let,S-Case}; and
  \nameref{lem:adequacy} in cases \rref*{S-Lam,S-Let,S-Case}.
\end{proof}

\begin{theorem}[Soundness] \label{thm:soundness} \leavevmode
  \begin{enumerate}
    \item If $[[G ⊢ v : A]]$ then $[[G ⊧ v : A]]$.
    \item If $[[G ⊢ m : B]]$ then $[[G ⊧ m : B]]$.
  \end{enumerate}
\end{theorem}

\begin{proof}
  By mutual induction on the syntactic typing derivations,
  using the admissible semantic typing rules.
\end{proof}

\begin{corollary}[Normalization] \leavevmode
  \begin{enumerate}
    \item If $[[G ⊢ v : A]]$ then $[[v ∈ SN]]$.
    \item If $[[G ⊢ m : B]]$ then $[[m ∈ SN]]$.
  \end{enumerate}
\end{corollary}

\begin{proof}
  By \nameref{thm:soundness},
  using the identity substitution and \rref{S-Nil},
  the well typed terms inhabit the semantic interpretations of their types.
  Then by \nameref{lem:adequacy},
  they are also strongly normalizing.
\end{proof}

\section{Strong Normalization as an Accessibility Relation} \label{sec:sn-acc}

\drules[sn]{$[[v ∈ sn]], [[m ∈ sn]]$}{strongly normalizing terms}{Val,Com}
\drules[sr]{$[[m ⤳' n]]$}{strong head reduction}{Thunk,Lam,Ret,Inl,Inr,App,Let}
\drules[ne]{$[[m ∈ ne]]$}{neutral computations}{Force,App,Let,Case}

\begin{mathpar}
\mprset{fraction={-~}{-~}{-}}
\drule[]{sn-App-invOne}
\drule[]{sn-App-invTwo}
\drule[]{sn-Let-invOne}
\drule[]{sn-Let-invTwo}
\end{mathpar}

\begin{proof}
  By induction on the premises of strongly normal terms,
  using congruence of single-step reduction.
\end{proof}

\begin{definition}[Neutral values]
  A value is neutral, written $[[v ∈ ne]]$, if it is a variable.
\end{definition}

\begin{lemma}[Preservation] \label{lem:preservation} \leavevmode
  \begin{enumerate}
    \item If $[[v ⇝ w]]$ and $[[v ∈ ne]]$ then $[[w ∈ ne]]$.
    \item If $[[m ⇝ n]]$ and $[[m ∈ ne]]$ then $[[n ∈ ne]]$.
  \end{enumerate}
\end{lemma}

\begin{proof}
  By mutual induction on the single-step reductions.
\end{proof}

\begin{definition}[Strongly neutral computations]
  A strongly neutral computation, written $[[m ∈ sne]]$,
  is a computation that is both neutral and strongly normalizing,
  \ie $[[m ∈ ne]]$ and $[[m ∈ sn]]$.
\end{definition}

{\mprset{fraction={-~}{-~}{-}}
\drules[sn]{$[[v ∈ sn]]$}{admissible strongly normal values}{Var,Unit,Inl,Inr,Thunk}
\drules[sn]{$[[m ∈ sn]]$}{admissible strongly normal computations}{Lam,Ret,Force,App,Let,Case}
}

\begin{proof}
  \Rref{sn-App,sn-Let,sn-Case} are proven by double induction
  on the two derivations of strongly normal terms.
  Intuitively, we want to show that if the conclusion steps,
  then it steps to a strongly normal term,
  knowing by the induction hypotheses that if their subterms reduce,
  then they also reduce to strongly normal terms.
  Neutrality of the term in head position eliminates cases where the conclusion $\beta$-reduces,
  leaving only the congruent reductions.
  Because single-step reduction only steps in one subterm,
  we only need the induction hypothesis for that reducing subterm,
  so the double induction is really a lexicographic induction on the two derivations.
  We additionally require \nameref{lem:preservation} to carry along neutrality
  when the heads reduce in cases \rref*{sn-App,sn-Let}.
  All other cases are direct by construction
  or by induction on their sole premise.
\end{proof}

% admissible rules missing backward closure \rref{SN-Red}

\begin{lemma}[Antisubstitution (\textsf{sn})] \label{lem:antisubst-sn}
  If $[[m{x ↦ v} ∈ sn]]$ and $[[v ∈ sn]]$ then $[[m ∈ sn]]$.
\end{lemma}

\begin{proof}
  By induction on the derivation of $[[m{x ↦ v} ∈ sn]]$.
\end{proof}

{\mprset{fraction={-~}{-~}{-}}
\drules[sn]{$[[m ∈ sn]]$}{head expansion}{Force-Thunk,App-Lam,Let-Ret,Case-Inl,Case-Inr}
}

\begin{proof}
  \Rref{sn-Force-Thunk} holds directly by induction on the premise;
  the remaining proofs are more complex.
  First, given the premise $[[m{x ↦ v} ∈ sn]]$ (or $[[n{z ↦ v}]]$),
  use \nameref{lem:antisubst-sn} to obtain $[[m ∈ sn]]$.
  Then proceed by double (or triple) induction on the derivations of
  $[[v ∈ sn]]$ and $[[m ∈ sn]]$ (and $[[n ∈ sn]]$ for the case rules).
  Similarly to the admissible strongly normal rules,
  these are lexicographic inductions,
  except $[[m{x ↦ v} ∈ sn]]$ (or $[[n{z ↦ v}]]$)
  is used to satisfy the $\beta$-reduction cases.
\end{proof}

\begin{lemma}[Confluence] \label{lem:confluence}
  If $[[m ⇝ n1]]$ and $[[m ⤳' n2]]$, then either $[[n1]] = [[n2]]$,
  or there exists some $[[m']]$ such that
  $[[n1 ⤳' m']]$ and $[[n2 ⇝ m']]$.
\end{lemma}

\begin{proof}
  By induction on the derivation of $[[m ⤳' n2]]$,
  then by cases on the derivation of $[[m ⇝ n1]]$.
\end{proof}

\begin{mathpar}
\mprset{fraction={-~}{-~}{-}}
\fbox{$[[m ∈ sn]]$} \hfill \textit{backward closure in head position} \\
\drule[width=0.45\textwidth]{sn-App-bwd}
\drule[width=0.55\textwidth]{sn-Let-bwd}
\end{mathpar}

\begin{proof}
  First, use \rref{sn-App-inv,sn-Let-inv} to obtain $[[m ∈ sn]]$.
  Then proceed by double induction on the derivations of
  $[[m ∈ sn]]$ and $[[v ∈ sn]]$/$[[n ∈ sn]]$,
  again as lexicographic induction.
  We want to show that if the conclusion steps,
  then it steps to a strongly normal term.
  Strong reduction of the head position eliminates the cases of $\beta$-reduction,
  leaving the cases where the head position steps or the other position steps.
  If the head position steps, we use \nameref{lem:confluence}
  to join the strong reduction and the single-step reduction together,
  then use the first induction hypothesis.
  Otherwise, we use the second induction hypothesis.
  We need the last premise to step through either of the subterms,
  since we have no congruence rule for when the head position is not neutral.
\end{proof}

\begin{lemma}[Backward closure] \label{lem:closure}
  If $[[m ⤳' n]]$ and $[[n ∈ sn]]$ then $[[m ∈ sn]]$.
\end{lemma}

\begin{proof}
  By induction on the derivation of $[[m ⤳' n]]$.
  The cases correspond exactly to each of
  \rref{sn-Force-Thunk,sn-App-Lam,sn-Let-Ret,sn-Case-Inl,sn-Case-Inr,sn-App-bwd,sn-Let-bwd}.
\end{proof}

\begin{lemma}[Soundness (\textsf{SNe})] \label{lem:sound-sne}
  If $[[m ∈ SNe]]$ then $[[m ∈ ne]]$.
\end{lemma}

\begin{proof}
  By induction on the derivation of $[[m ∈ SNe]]$.
\end{proof}

\begin{theorem}[Soundness (\textsf{SN})] \leavevmode
  \begin{enumerate}
    \item If $[[m ∈ SNe]]$ then $[[m ∈ sn]]$.
    \item If $[[v ∈ SN]]$ then $[[v ∈ sn]]$.
    \item If $[[m ∈ SN]]$ then $[[m ∈ sn]]$.
    \item If $[[m ⤳ n]]$ then $[[m ⤳' n]]$.
  \end{enumerate}
\end{theorem}

\begin{proof}
  By mutual induction on the derivations of
  $[[m ∈ SNe]]$, $[[v ∈ SN]]$, $[[m ∈ SN]]$, and $[[m ⤳ n]]$.
  The cases for the first three correspond to the admissible strongly normal rules,
  using \nameref{lem:sound-sne} as needed,
  except for the \rref*{SN-Red} case, which uses \nameref{lem:closure}.
  The cases for strong reduction hold by construction.
\end{proof}

\begin{corollary}
  If $[[G ⊢ v : A]]$ then $[[v ∈ sn]]$,
  and if $[[G ⊢ m : B]]$ then $[[m ∈ sn]]$.
\end{corollary}

\section{Discussion} \label{sec:discussion}

\end{document}