\documentclass{article}

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

\setlist{noitemsep}
\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 \\[0.5\baselineskip]
\large CIS 6700: Type Systems}
\author{Jonathan Chan}
\date{8 May 2025}

\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 \citep{cbpv} on mechanizing the metatheory of CBPV in Rocq,
but instead adapts the proof technique from POPLMark Reloaded \citep{poplmark}.

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%
\footnote{\url{https://github.com/ionathanch/MutualInduction}},
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}

The grammar of the CBPV for this project is given below.
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 $\sigma$ mapping variables to values,
with $ \cdot $ as the identity substitution.
Applying a substitution is represented as $ \ottnt{v} [  \sigma  ] $ and $ \ottnt{m} [  \sigma  ] $,
and implemented in terms of renamings,
which are mappings from variables to other variables.
%
\begin{align*}
  \ottnt{A} &\Coloneqq  \kw{Unit}  \mid  \ottnt{A_{{\mathrm{1}}}}  +  \ottnt{A_{{\mathrm{2}}}}  \mid  \kw{U} \gap  \ottnt{B}  & \textit{value types} \\
  \ottnt{B} &\Coloneqq  \ottnt{A}  \rightarrow  \ottnt{B}  \mid  \kw{F} \gap  \ottnt{A}  & \textit{computation types} \\
  \ottnt{v}, \ottnt{w} &\Coloneqq \ottmv{x} \mid  \kw{unit}  \mid  \kw{inl} \gap  \ottnt{v}  \mid  \kw{inr} \gap  \ottnt{v}  \mid  \kw{thunk} \gap  \ottnt{m}  & \textit{values} \\
  \ottnt{m}, \ottnt{n} &\Coloneqq  \kw{force} \gap  \ottnt{v}  \mid  \lambda  \ottmv{x}  \mathpunct{.}  \ottnt{m}  \mid  \ottnt{m}  \gap  \ottnt{v}  \mid  \kw{return} \gap  \ottnt{v}  & \textit{computations} \\
  & \mid  \kw{let} \gap  \ottmv{x}  \leftarrow  \ottnt{m}  \gap \kw{in} \gap  \ottnt{n}  \\
  & \mid  \kw{case} \gap  \ottnt{v}  \gap \kw{of} \gap \lbrace \kw{inl} \gap  \ottmv{y}  \Rightarrow  \ottnt{m}  \mathrel{;} \kw{inr} \gap  \ottmv{z}  \Rightarrow  \ottnt{n}  \rbrace  \\
  \Gamma &\Coloneqq  \cdot  \mid  \Gamma ,  \ottmv{x}  \mathbin{:}  \ottnt{A}  & \textit{typing contexts} \\
  \sigma &\Coloneqq  \cdot  \mid  \sigma ,  \ottmv{x}  \mapsto  \ottnt{v}  & \textit{simultaneous substitutions}
\end{align*}

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]{$ \Gamma  \vdash  \ottnt{v}  :  \ottnt{A} $}{value typing}{Var,Unit,Inl,Inr,Thunk}
\drules[T]{$ \Gamma  \vdash  \ottnt{m}  :  \ottnt{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 $ \ottnt{v}  \in \kw{SNe} $ for symmetry as appropriate.
Otherwise, the remaining four judgements are defined mutually below.

\drules[SNe]{$ \ottnt{m}  \in \kw{SNe} $}{strongly neutral computations}{Force,App,Let,Case}
\drules[SN]{$ \ottnt{v}  \in \kw{SN} $}{strongly normal values}{Var,Unit,Inl,Inr,Thunk}
\drules[SN]{$ \ottnt{m}  \in \kw{SN} $}{strongly normal computations}{Lam,Ret,SNe,Red}
\drules[SR]{$ \ottnt{m}  \leadsto  \ottnt{n} $}{strong head reduction}{Thunk,Lam,Ret,Inl,Inr,App,Let}
\drules[SRs]{$ \ottnt{m}  \leadsto^*  \ottnt{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 $\sigma$ be a renaming,
  \ie a substitution mapping variables to variables.
  Then the following hold:
  \begin{enumerate}
    \item If $  \ottnt{m} [  \sigma  ]   \in \kw{SNe} $ then $ \ottnt{m}  \in \kw{SNe} $.
    \item If $  \ottnt{v} [  \sigma  ]   \in \kw{SN} $ then $ \ottnt{v}  \in \kw{SN} $.
    \item If $  \ottnt{m} [  \sigma  ]   \in \kw{SN} $ then $ \ottnt{m}  \in \kw{SN} $.
    \item If $  \ottnt{m} [  \sigma  ]   \leadsto  \ottnt{n} $ then there exists some $\ottnt{n'}$
      such that $\ottnt{n} =  \ottnt{n'} [  \sigma  ] $ and $ \ottnt{m}  \leadsto  \ottnt{n'} $.
  \end{enumerate}
\end{lemma}

\begin{proof}
  By mutual induction on the four derivations of
  $  \ottnt{m} [  \sigma  ]   \in \kw{SNe} $, $  \ottnt{v} [  \sigma  ]   \in \kw{SN} $, $  \ottnt{m} [  \sigma  ]   \in \kw{SN} $, and $  \ottnt{m} [  \sigma  ]   \leadsto  \ottnt{n} $.
\end{proof}

\begin{corollary}[Extensionality] \label{cor:ext}
  If $  \ottnt{m}  \gap  \ottmv{x}   \in \kw{SN} $ then $ \ottnt{m}  \in \kw{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 $ \ottnt{m}  \in \kw{SNe} $,
  and we conclude using \rref{SN-SNe} again.
  In the latter case, we have $  \ottnt{m}  \gap  \ottmv{x}   \leadsto  \ottnt{n} $ and $ \ottnt{n}  \in \kw{SN} $;
  destructing on the reduction yields the possible cases
  \rref{SR-Lam,SR-App}.
  In the first case, we have $  \ottnt{m} [   \ottmv{x}  \mapsto  \ottnt{v}   ]   \in \kw{SN} $,
  so the goal holds by \nameref{thm:antisubst}.
  In the second case, we have $ \ottnt{m}  \leadsto  \ottnt{n} $ and $  \ottnt{n}  \gap  \ottmv{x}   \in \kw{SN} $,
  so by the induction hypothesis, we have $ \ottnt{n}  \in \kw{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 $ \mathopen{\llbracket}  \ottnt{A}  \mathclose{\rrbracket} \searrow  \ottnt{P} $ and $ \mathopen{\llbracket}  \ottnt{B}  \mathclose{\rrbracket} \searrow  \ottnt{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]{$ \mathopen{\llbracket}  \ottnt{A}  \mathclose{\rrbracket} \searrow  \ottnt{P} $}{semantic interpretation of value types}{Unit,U,Sum}
\drules[LR]{$ \mathopen{\llbracket}  \ottnt{B}  \mathclose{\rrbracket} \searrow  \ottnt{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 $ \kw{U} \gap  \ottnt{B} $ type
    if they can be forced to computations in the interpretation of the $\ottnt{B}$ type.
  \item Values in the interpretation of the sum type $ \ottnt{A_{{\mathrm{1}}}}  +  \ottnt{A_{{\mathrm{2}}}} $ are either variables,
    left injections whose values are in the interpretation of $\ottnt{A_{{\mathrm{1}}}}$,
    or right injections whose values are in that of $\ottnt{A_{{\mathrm{2}}}}$.
  \item Computations in the interpretation of the $ \kw{F} \gap  \ottnt{A} $ type
    reduce to either a neutral computation
    or a return whose value is in the interpretation of $\ottnt{A}$.
  \item Computations are in the interpretation of the function type $ \ottnt{A}  \rightarrow  \ottnt{B} $
    if applying them to values in the interpretation of $\ottnt{A}$
    yields computations in the interpretation of $\ottnt{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{LR'-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{$ \ottnt{v}  \in \mathopen{\llbracket}  \ottnt{A}  \mathclose{\rrbracket} $} \quad \fbox{$ \ottnt{m}  \in \mathopen{\llbracket}  \ottnt{B}  \mathclose{\rrbracket} $} \hfill \textit{semantic inhabitance of types} \\
\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{LR'-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 $\ottnt{A}$, there exists $\ottnt{P}$ such that $ \mathopen{\llbracket}  \ottnt{A}  \mathclose{\rrbracket} \searrow  \ottnt{P} $.
    \item Given $\ottnt{B}$, there exists $\ottnt{P}$ such that $ \mathopen{\llbracket}  \ottnt{B}  \mathclose{\rrbracket} \searrow  \ottnt{P} $.
  \end{enumerate}
\end{lemma}

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

\begin{lemma}[Determinism] \label{lem:det} \leavevmode
  \begin{enumerate}
    \item If $ \mathopen{\llbracket}  \ottnt{A}  \mathclose{\rrbracket} \searrow  \ottnt{P} $ and $ \mathopen{\llbracket}  \ottnt{A}  \mathclose{\rrbracket} \searrow  \ottnt{Q} $ then $\ottnt{P} = \ottnt{Q}$.
    \item If $ \mathopen{\llbracket}  \ottnt{B}  \mathclose{\rrbracket} \searrow  \ottnt{P} $ and $ \mathopen{\llbracket}  \ottnt{B}  \mathclose{\rrbracket} \searrow  \ottnt{Q} $ then $\ottnt{P} = \ottnt{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 $ \mathopen{\llbracket}  \ottnt{B}  \mathclose{\rrbracket} \searrow  \ottnt{P} $ and $ \ottnt{m}  \leadsto^*  \ottnt{n} $,
  if $ \ottnt{n}  \in  \ottnt{P} $ then $ \ottnt{m}  \in  \ottnt{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 $\ottnt{P}$ where,
  given a term $t$,
  if $ t  \in \kw{SNe} $ then $ t  \in  \ottnt{P} $, and
  if $ t  \in  \ottnt{P} $ then $ t  \in \kw{SN} $.
\end{definition}

\begin{lemma}[Adequacy] \label{lem:adequacy} \leavevmode
  \begin{enumerate}
    \item If $ \mathopen{\llbracket}  \ottnt{A}  \mathclose{\rrbracket} \searrow  \ottnt{P} $ then $\ottnt{P}$ is a reducibility candidate.
    \item If $ \mathopen{\llbracket}  \ottnt{B}  \mathclose{\rrbracket} \searrow  \ottnt{P} $ then $\ottnt{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 $ \ottnt{A}  \rightarrow  \ottnt{B} $,
  where $ \mathopen{\llbracket}  \ottnt{A}  \mathclose{\rrbracket} \searrow  \ottnt{P} $ and $ \mathopen{\llbracket}  \ottnt{B}  \mathclose{\rrbracket} \searrow  \ottnt{Q} $,
  to show the second part of its interpretation being a reducibility candidate,
  we are given $\ottnt{m}$ such that for every $ \ottnt{v}  \in  \ottnt{P} $, $  \ottnt{m}  \gap  \ottnt{v}   \in  \ottnt{Q} $,
  and the goal is to show that $ \ottnt{m}  \in \kw{SN} $.
  By the induction hypotheses, picking an arbitrary variable $\ottmv{x}$,
  we have that $ \ottmv{x}  \in  \ottnt{P} $ (since it is neutral) and that $  \ottnt{m}  \gap  \ottmv{x}   \in \kw{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 $\sigma$ is well formed with respect to a context $\Gamma$,
  written $ \Gamma  \vDash  \sigma $, if for every $ \ottmv{x}  :  \ottnt{A}  \in  \Gamma $ and $ \mathopen{\llbracket}  \ottnt{A}  \mathclose{\rrbracket} \searrow  \ottnt{P} $,
  we have $  \ottmv{x} [  \sigma  ]   \in  \ottnt{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]{$ \Gamma  \vDash  \sigma $}{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 $\ottnt{v}$ semantically has type $\ottnt{A}$ under context $\Gamma$,
      written $ \Gamma  \vDash  \ottnt{v}  :  \ottnt{A} $, if for every $\sigma$ such that $ \Gamma  \vDash  \sigma $,
      there exists an interpretation $ \mathopen{\llbracket}  \ottnt{A}  \mathclose{\rrbracket} \searrow  \ottnt{P} $ such that $  \ottnt{v} [  \sigma  ]   \in  \ottnt{P} $.
    \item $\ottnt{m}$ semantically has type $\ottnt{B}$ under context $\Gamma$,
      written $ \Gamma  \vDash  \ottnt{m}  :  \ottnt{B} $, if for every $\sigma$ such that $ \Gamma  \vDash  \sigma $,
      there exists an interpretation $ \mathopen{\llbracket}  \ottnt{B}  \mathclose{\rrbracket} \searrow  \ottnt{P} $ such that $  \ottnt{m} [  \sigma  ]   \in  \ottnt{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 a corollary.

{\mprset{fraction={-~}{-~}{-}}
\drules[S]{$ \Gamma  \vDash  \ottnt{v}  :  \ottnt{A} $}{admissible semantic value typing}{Var,Unit,Inl,Inr,Thunk}
\drules[S]{$ \Gamma  \vDash  \ottnt{m}  :  \ottnt{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 $ \Gamma  \vdash  \ottnt{v}  :  \ottnt{A} $ then $ \Gamma  \vDash  \ottnt{v}  :  \ottnt{A} $.
    \item If $ \Gamma  \vdash  \ottnt{m}  :  \ottnt{B} $ then $ \Gamma  \vDash  \ottnt{m}  :  \ottnt{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 $ \Gamma  \vdash  \ottnt{v}  :  \ottnt{A} $ then $ \ottnt{v}  \in \kw{SN} $.
    \item If $ \Gamma  \vdash  \ottnt{m}  :  \ottnt{B} $ then $ \ottnt{m}  \in \kw{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}

How do we know that our definition of strongly normal terms is correct?
What are the properties that define its correctness?
It seems to be insufficient to talk about strongly neutral and normal terms alone.

For instance, we could add another rule asserting that $ \ottnt{m}  \in \kw{SN} $ if $ \ottnt{m}  \leadsto  \ottnt{m} $,
which doesn't appear to violate any of the existing properties we require.
Then $  (   \lambda  \ottmv{x}  \mathpunct{.}   (  \kw{force} \gap  \ottmv{x}  )    \gap  \ottmv{x}  )   \gap   (  \kw{thunk} \gap   (   \lambda  \ottmv{x}  \mathpunct{.}   (  \kw{force} \gap  \ottmv{x}  )    \gap  \ottmv{x}  )   )  $,
which reduces to itself, would be considered a ``strongly normal'' term,
and typing rules that can type this term (perhaps with a recursive type)
would still be sound with respect to our logical relation.

To try to rule out this kind of mistake in the definition,
we might want to prove that strongly normal terms never loop,
\ie $  \ottnt{m}  \in \kw{SN}   \wedge   \ottnt{m}  \leadsto^*  \ottnt{m}  $ is impossible.
However, this does not cover diverging terms that grow forever.
Furthermore, $ \ottnt{m}  \leadsto  \ottnt{n} $ isn't really a full reduction relation on its own,
since it's defined mutually with strongly normal terms,
and it doesn't describe reducing anywhere other than in the head position.

The solution we take from POPLMark Reloaded is to prove that $\kw{SN}$ is sound
with respect to a traditional presentation of strongly normal terms
based on full small-step reduction \fbox{$ \ottnt{v}  \rightsquigarrow  \ottnt{w} $}, \fbox{$ \ottnt{m}  \rightsquigarrow  \ottnt{n} $} of values and computations.
I omit here the definitions of these reductions,
but they encompass all $\beta$-reduction rules and are congruent over all subterms,
including under binders.
Traditional strongly normal terms, written $ \ottnt{v}  \in \kw{sn} $, $ \ottnt{m}  \in \kw{sn} $,
are accessibility relations with respect to small-step reduction.
Terms are inductively defined as strongly normal if they step to strongly normal terms,
so terms which don't step are trivially normal.
This rules out looping and diverging terms, since they never stop stepping.
%
% \drules[sn]{$ \ottnt{v}  \in \kw{sn} ,  \ottnt{m}  \in \kw{sn} $}{strongly normalizing terms}{Val,Com}
\begin{mathpar}
\fbox{$ \ottnt{v}  \in \kw{sn} $} \quad \fbox{$ \ottnt{m}  \in \kw{sn} $} \hfill \textit{strongly normalizing terms} \\
\drule[]{sn-Val}
\drule[]{sn-Com}
\end{mathpar}

The inversion lemmas we need are easily proven by induction.

\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}

In contrast, while congruence rules for $\kw{SN}$ hold by definition,
they require some work to prove for $\kw{sn}$.
The strategy is to mirror the inductive characterization,
and define corresponding notions of neutral terms and head reduction,
with strongly neutral terms being those both neutral and strongly normal.
As before, variables are the only neutral value,
but we write $ \ottnt{v}  \in \kw{ne} $ to say that $\ottnt{v}$ is a variable for symmetry.

\drules[sr]{$ \ottnt{m}  \leadsto_{ \kw{sn} }  \ottnt{n} $}{strong head reduction}{Thunk,Lam,Ret,Inl,Inr,App,Let}
\drules[ne]{$ \ottnt{m}  \in \kw{ne} $}{neutral computations}{Force,App,Let,Case}

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

The admissible congruence rules for $\kw{sn}$
mirror exactly the congruence constructors for $\kw{SNe}$ and $\kw{SN}$,
replacing these by $\kw{sne}$ and $\kw{sn}$ in each premise.
Proving them additionally requires showing that small-step reduction preserves neutrality.

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

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

{\mprset{fraction={-~}{-~}{-}}
\drules[sn]{$ \ottnt{v}  \in \kw{sn} $}{admissible strongly normal values}{Var,Unit,Inl,Inr,Thunk}
\drules[sn]{$ \ottnt{m}  \in \kw{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}

The only missing correponding rule is that for \rref{SN-Red},
which backward closes strongly normal terms under head reduction.
Proving this for $\kw{sn}$ requires much more work and many more intermediate lemmas.
To show backward closure under $\beta$-reduction, or \emph{head expansion},
we first need antisubstitution to be able to undo substitutions.

\begin{lemma}[Antisubstitution (\textsf{sn})] \label{lem:antisubst-sn}
  If $  \ottnt{m} [   \ottmv{x}  \mapsto  \ottnt{v}   ]   \in \kw{sn} $ and $ \ottnt{v}  \in \kw{sn} $ then $ \ottnt{m}  \in \kw{sn} $.
\end{lemma}

\begin{proof}
  By induction on the derivation of $  \ottnt{m} [   \ottmv{x}  \mapsto  \ottnt{v}   ]   \in \kw{sn} $.
\end{proof}

{\mprset{fraction={-~}{-~}{-}}
\drules[sn]{$ \ottnt{m}  \in \kw{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 $  \ottnt{m} [   \ottmv{x}  \mapsto  \ottnt{v}   ]   \in \kw{sn} $ (or $ \ottnt{n} [   \ottmv{z}  \mapsto  \ottnt{v}   ] $),
  use \nameref{lem:antisubst-sn} to obtain $ \ottnt{m}  \in \kw{sn} $.
  Then proceed by double (or triple) induction on the derivations of
  $ \ottnt{v}  \in \kw{sn} $ and $ \ottnt{m}  \in \kw{sn} $ (and $ \ottnt{n}  \in \kw{sn} $ for the case rules).
  Similarly to the admissible strongly normal rules,
  these are lexicographic inductions,
  except $  \ottnt{m} [   \ottmv{x}  \mapsto  \ottnt{v}   ]   \in \kw{sn} $ (or $ \ottnt{n} [   \ottmv{z}  \mapsto  \ottnt{v}   ] $)
  is used to satisfy the $\beta$-reduction cases.
\end{proof}

Now remains backward closure under congruent reduction in head position.
Because showing that a term is strongly normal involves single-step reduction,
we need to ensure that head reduction and single-step reduction commute
and behave nicely with each other.
Proving commutativity is a lengthy proof that involves careful analysis
of the structure of both reductions.

\begin{lemma}[Commutativity] \label{lem:commute}
  If $ \ottnt{m}  \rightsquigarrow  \ottnt{n_{{\mathrm{1}}}} $ and $ \ottnt{m}  \leadsto_{ \kw{sn} }  \ottnt{n_{{\mathrm{2}}}} $, then either $\ottnt{n_{{\mathrm{1}}}} = \ottnt{n_{{\mathrm{2}}}}$,
  or there exists some $\ottnt{m'}$ such that
  $ \ottnt{n_{{\mathrm{1}}}}  \leadsto_{ \kw{sn} }  \ottnt{m'} $ and $ \ottnt{n_{{\mathrm{2}}}}  \rightsquigarrow  \ottnt{m'} $.
\end{lemma}

\begin{proof}
  By induction on the derivation of $ \ottnt{m}  \leadsto_{ \kw{sn} }  \ottnt{n_{{\mathrm{2}}}} $,
  then by cases on the derivation of $ \ottnt{m}  \rightsquigarrow  \ottnt{n_{{\mathrm{1}}}} $.
\end{proof}

\begin{mathpar}
\mprset{fraction={-~}{-~}{-}}
\fbox{$ \ottnt{m}  \in \kw{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-inv1,sn-App-inv2,sn-Let-inv1,sn-Let-inv2}
  to obtain $ \ottnt{m}  \in \kw{sn} $ and $ \ottnt{v}  \in \kw{sn} $/$ \ottnt{n}  \in \kw{sn} $.
  Then proceed by double induction on the derivations of
  $ \ottnt{m}  \in \kw{sn} $ and $ \ottnt{v}  \in \kw{sn} $/$ \ottnt{n}  \in \kw{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:commute}
  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}

All of these lemmas at last give us backward closure.

\begin{lemma}[Backward closure] \label{lem:closure-sn}
  If $ \ottnt{m}  \leadsto_{ \kw{sn} }  \ottnt{n} $ and $ \ottnt{n}  \in \kw{sn} $ then $ \ottnt{m}  \in \kw{sn} $.
\end{lemma}

\begin{proof}
  By induction on the derivation of $ \ottnt{m}  \leadsto_{ \kw{sn} }  \ottnt{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}

This gives us all the pieces to show that the inductive characterization
is sound with respect to the traditional presentation of strongly normal terms,
using neutral terms and head reduction as intermediate widgets to strengthen the induction hypotheses,
although we can show soundness for neutrality independently.
With soundness of strongly normal terms combined with soundness of syntactic typing,
traditional strong normalization of well typed terms holds as a corollary.

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

\begin{proof}
  By induction on the derivation of $ \ottnt{m}  \in \kw{SNe} $.
\end{proof}

\begin{theorem}[Soundness (\textsf{SN})] \label{thm:soundness-sn} \leavevmode
  \begin{enumerate}
    \item If $ \ottnt{m}  \in \kw{SNe} $ then $ \ottnt{m}  \in \kw{sn} $.
    \item If $ \ottnt{v}  \in \kw{SN} $ then $ \ottnt{v}  \in \kw{sn} $.
    \item If $ \ottnt{m}  \in \kw{SN} $ then $ \ottnt{m}  \in \kw{sn} $.
    \item If $ \ottnt{m}  \leadsto  \ottnt{n} $ then $ \ottnt{m}  \leadsto_{ \kw{sn} }  \ottnt{n} $.
  \end{enumerate}
\end{theorem}

\begin{proof}
  By mutual induction on the derivations of
  $ \ottnt{m}  \in \kw{SNe} $, $ \ottnt{v}  \in \kw{SN} $, $ \ottnt{m}  \in \kw{SN} $, and $ \ottnt{m}  \leadsto  \ottnt{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-sn}.
  The cases for strong reduction hold by construction.
\end{proof}

\begin{corollary}
  If $ \Gamma  \vdash  \ottnt{v}  :  \ottnt{A} $ then $ \ottnt{v}  \in \kw{sn} $,
  and if $ \Gamma  \vdash  \ottnt{m}  :  \ottnt{B} $ then $ \ottnt{m}  \in \kw{sn} $.
\end{corollary}

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

\subsection{Proof Structure of Strong Normalization}

Overall, the inductive characterization of strongly normal terms is convenient to work with.
Its congruence and inversion properties are exactly what are needed
to show \nameref{lem:closure} and \nameref{lem:adequacy} of the logical relation,
which are already built in by its inductive nature.
Proving soundness itself relies mostly on the properties of the logical relation,
along with a few more congruence properties of strong head reduction.
Knowing the general recipe for constructing the inductive definition
and for the structure of a proof by logical relations
makes it easy to adapt the proof of strong normalization to simply typed CBPV.
There are only a few pitfalls related to simply typed CBPV specifically:

\begin{itemize}[rightmargin=\leftmargin]
  \item I originally included a corresponding notion of reduction for values
    in the mutual inductive which reduced under subterms.
    This is unnecessary not only because values have no $\beta$-reductions,
    but also because subterms of strongly normal values need to be strongly normal anyway,
    so there is no need to reduce subterms.
    Having reduction for values therefore probably characterizes the same set of strongly normal terms,
    but made proofs unnecessarily difficult to complete.
  \item Similarly, I originally included premises asserting other subterms of head reduction
    must be strongly normal even if they appear in the reduced term on the right-hand side.
    This changes what terms may reduce,
    but not what is included in the set of strongly normal terms,
    since \rref{SN-Red} requires that the right-hand term is strongly normal anyway.
    The soundness proof still went through,
    but this design is hard to justify by first principles,
    and adds proof burden to the lemmas for the traditional presentation
    of strongly normal terms later on.
  \item The lack of a notion of reduction for values creates an asymmetry
    that initially led me to omit the fact that the computations
    in the interpretation of $ \kw{F} \gap  \ottnt{A} $ in \rref{LR-F} must \emph{reduce}
    to strongly neutral terms instead of merely \emph{being} strongly neutral.
    This makes \nameref{lem:closure} impossible to prove,
    since strongly neutral terms are not backward closed.
\end{itemize}

The inductive characterization is easy to work with
because all the hard work seems to lie in showing it sound
with respect to the traditional presentation of strongly normal terms.
This proof took about as much time as the entire rest of the development.
Not only does it require setting up an entire single-step reduction relation
and proving all of its tedious congruence, renaming, substitution, and commutativity lemmas,
the intermediate lemmas for \nameref{thm:soundness-sn} are long and tricky.
In particular, the congruence, head expansion, and backward closure lemmas
require double or even triple induction.
\Rref{sn-App-bwd,sn-Let-bwd} are especially tricky,
since their double inductions are on two auxiliary derivations
produced from one of the actual premises,
and that premise unintuitively needs to stick around over the course of the inductions.
Without guidance from the POPLMark Reloaded paper,
I would have been stuck on these two particular lemmas for much longer.

The purpose of all the work done in \cref{sec:sn-acc}
is to show that $\kw{sn}$ satisfies properties that
otherwise hold by definition for $\kw{SN}$ as a constructor.
If proving that the latter is sound with respect to the former
already requires all this work showing that the former behaves exactly like the latter,
then what is the point of using the inductive characterization?
All constructions of $\kw{SN}$ could be directly replaced
by the congruence and backward closure lemmas we have proven for $\kw{sn}$.

Using the inductive characterization is beneficial only if we don't care
about its soundness with respect to the traditional presentation,
where strong normalization is not the end goal.
For example, in the metatheory of dependent type theory,
we care about normalization because we want to know
that the type theory is consistent,
and that definitional equality is decidable
so that a type checker can actually be implemented.
For the latter purpose,
all we require is \emph{weak normalization}:
that there exists \emph{some} reduction strategy that reduces terms to normal form.
The shape of the inductive characterization makes it easy to show
that a leftmost-outermost reduction strategy does so (\texttt{LeftmostOutermost.lean}).
While weak normalization can be proven directly using the logical relation,
generalizing to the inductive strong normalization is actually easier,
in addition to being more modular and not tying the logical relation
to the particularities of the chosen reduction strategy.

\subsection{Lean for PL Metatheory}

The proof development involved in this report consists of nine files,
as mentioned throughout.
\Cref{tab:loc} gives the number of non-blank, non-comment lines of code for each file,
which roughly reflects the amount of proof effort I required.
The \texttt{Syntax.lean} file involves a lot of renaming and substitution proofs,
but I copied these from prior proof developments with minimal changes to adapt them to CBPV.
The actual semantic proofs in \texttt{NormalInd.lean}, \texttt{OpenSemantics.lean}, and \texttt{Soundness.lean}
took roughly equal amounts of time to complete.
As said in \cref{sec:sn-acc}, the proofs in \texttt{NormalAcc.lean}
along with its dependency on \texttt{Reduction.lean} took nearly as much time to complete
as the rest of the semantic proofs,
while \texttt{LeftmostOutermost.lean} mostly mirrors \texttt{Reduction.lean}.
The entire project, excluding this report, took about a week to complete.

\begin{table}[H]
\centering
\begin{tabular}{lr}
  \toprule
  File & LOC \\
  \midrule
  \texttt{Syntax.lean}            & 252 \\
  \texttt{Typing.lean}            &  48 \\
  \texttt{NormalInd.lean}         & 192 \\
  \texttt{OpenSemantics.lean}     & 107 \\
  \texttt{Soundness.lean}         & 114 \\
  \texttt{Normalization.lean}     &  48 \\
  \texttt{Reduction.lean}         & 187 \\
  \texttt{NormalAcc.lean}         & 291 \\
  \texttt{LeftmostOutermost.lean} & 276 \\
  \bottomrule
\end{tabular}
\caption{Lean development files and lines of code}
\label{tab:loc}
\end{table}

One of the main technical challenges in mechanizing CBPV in Lean is dealing with mutual induction.
While Lean currently supports mutually defined inductive types,
the options for eliminating them are somewhat buggy and restricted.
At the lower level,
Lean generates independent eliminators (which they call \emph{recursors})
for each of the mutual inductives,
each with motives for all mutual inductives,
similar to what \texttt{Scheme Induction for ... with Induction for ...}
generates in Rocq.

Lean's induction tactic produces applications of the appropriate recursor,
but does not support mutual inductives.
In cases where induction on only a single inductive from the mutual definitions is needed,
the induction tactic can be supplied with a custom recursor,
in this case the appropriate inductive's recursor with all other motives
instantiated to trivial propositions.
Unfortunately, this fails because the tactic cannot handle induction cases
with different numbers of indices in the inductive type,
even if those other cases are eventually trivial.

Lean supports structural recursion on mutual inductives,
which is implemented via a recursor on an auxiliary inductive
that enables strong induction.
However, this feature is currently a little buggy,
and fails on some more complex inductive types.%
\footnote{\url{https://github.com/leanprover/lean4/issues/1672}}
Futhermore, writing proofs as recursive functions is unconventional,
and isn't amenable to even simple automation that can automatically apply induction hypotheses.

Of course, it's possible to manually apply the recursors that Lean generates for each mutual inductive.
This is inconvenient for several reasons:
motives need to be explicitly specified, even when they're inferrable from the goals;
cases with trivial motives still need to be explicitly proven;
and induction cases are duplicated across the recursors.
A partial solution, especially for the last inconvenience,
is to generate the same kind of combined recursor that \texttt{Combined Scheme ...}
does for Rocq, but it still requires explicit application.
The mutual induction tactic I had implemented (outside of this project)
aims to solve these issues.

In short, my mutual induction tactic targets multiple goals at a time.
Applying the tactic on targets in mutually defined inductives from different goals
applies their respective recursors, inferring motives from those goals,
but deduplicates the induction cases, and introduces these cases as new subgoals.
If a target and goal for a particular inductive is missing,
the motive for that inductive is set as a trivially inhabited type,
and all cases for that motive are automatically solved.

The mutual induction tactic has worked very well for this project.
The mutual inductives involved are the value and computation terms and types (2 and 2),
their typing judgements (2), the logical relation (2),
the small-step reduction relation (2),
and the mutually inductive definition of strongly neutral and normal terms and head reduction (4).
The tactic was used for every proof by mutual induction mentioned here.
Additionally, it was used twice for single induction
(\ie all other motives are trivial): \rref{SN-Force-inv} and \nameref{cor:ext}.

Because the mutual induction tactic is merely a tactic and not a top-level construct,
some amount of manipulation is still required to massage the proof state
into one where the tactic can be used.
Specifically, mutual theorems are first stated as some conjunction
$(\forall v, P \gap v) \wedge (\forall m, Q \gap m)$,
then split into two separate goals with targets $v, m$ introduced into the context,
before mutual induction is applied to $v$ and $m$ with inferred motives $P$ and $Q$.
This means that using the theorems individually requires projecting from the conjunction.
There are discussions underway for introducing top-level syntax for mutual theorems,
similar to Rocq's \texttt{Theorem ... with ...} vernacular,
so that multiple goals are introduced automatically with their hypotheses.%
\footnote{\url{https://leanprover.zulipchat.com/\#narrow/channel/239415-metaprogramming-.2F-tactics/topic/mutual.20induction.20tactic/near/504421657}}

Aside from mutual induction,
the other technical challenge is proving all the renaming and substitution lemmas.
There is no library like Autosubst 2 \citep{autosubst2} to automate defining and proving these lemmas.
In multiple places, substitutions need to be massaged into different propositionally equal forms,
and this massaging requires knowing exactly what equality is needed.
For PL metatheory that doesn't involve mutual definitions
but does involve some notion of binding and abstraction,
the lack of a library for substitution automation is perhaps the biggest barrier
to Lean being used for PL.

\bibliographystyle{abbrvnat}
\bibliography{cbpv.bib}

\end{document}