938 lines
42 KiB
Plaintext
938 lines
42 KiB
Plaintext
\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) \citep{cbpv}.
|
|
It follows work by Forster, Sch\"afer, Spies, and Stark \citep{cbpv-coq} 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.%
|
|
\footnote{\url{https://github.com/ionathanch/MutualInduction/tree/main/CBPV}}
|
|
\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 $[[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.
|
|
%
|
|
\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*}
|
|
|
|
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:
|
|
|
|
\clearpage
|
|
\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
|
|
with strongly normal subterms
|
|
or strongly neutral values.
|
|
\item Strongly normal computations are constructors
|
|
with strongly normal subterms,
|
|
strongly neutral computations,
|
|
or computations that 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, head 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 \fbox{$[[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 and set membership notation,
|
|
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 returned value 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{LR'-Arr}.
|
|
The alternate presentation can be interpreted as a function
|
|
matching 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{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} 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.
|
|
\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,
|
|
using \rref{SRs-Trans',SRs-App}.
|
|
\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 \fbox{$[[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.
|
|
|
|
\begingroup
|
|
\mprset{fraction={-~}{-~}{-}}
|
|
\drules[S]{$[[G ⊧ s]]$}{admissible semantic substitution well-formedness}{Nil,Cons}
|
|
\endgroup
|
|
|
|
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 \fbox{$[[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 \fbox{$[[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 a corollary.
|
|
|
|
\begingroup
|
|
\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,Lam,App,Ret,Let,Case}
|
|
\endgroup
|
|
|
|
\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}
|
|
|
|
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 $[[m ∈ SN]]$ if $[[m ⤳ m]]$,
|
|
which doesn't appear to violate any of the existing properties we require.
|
|
Then $[[(λx. (force x) x) (thunk (λx. (force x) 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 $[[m ∈ SN ∧ m ⤳* m]]$ is impossible.
|
|
However, this does not cover diverging terms that grow forever.
|
|
Furthermore, $[[m ⤳ 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{$[[v ⇝ w]]$}, \fbox{$[[m ⇝ 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,
|
|
with \fbox{$[[v ⇝* w]]$}, \fbox{$[[m ⇝* n]]$} denoting their reflexive, transitive closures.
|
|
|
|
Traditional strongly normal terms, defined below,
|
|
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 diverging terms, since they never stop stepping.
|
|
%
|
|
% \drules[sn]{$[[v ∈ sn]], [[m ∈ sn]]$}{strongly normal terms}{Val,Com}
|
|
\begin{mathpar}
|
|
\fbox{$[[v ∈ sn]]$} \quad \fbox{$[[m ∈ sn]]$} \hfill \textit{strongly normal 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 \fbox{$[[v ∈ ne]]$} to say that $[[v]]$ is a variable for symmetry.
|
|
|
|
\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{definition}[Strongly neutral computations]
|
|
A strongly neutral computation, written \fbox{$[[m ∈ sne]]$},
|
|
is a computation that is both neutral and strongly normalizing,
|
|
\ie $[[m ∈ ne]]$ and $[[m ∈ 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 $[[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}
|
|
|
|
\begingroup
|
|
\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}
|
|
\endgroup
|
|
|
|
\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 $[[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}
|
|
|
|
\begingroup
|
|
\mprset{fraction={-~}{-~}{-}}
|
|
\drules[sn]{$[[m ∈ sn]]$}{head expansion}{Force-Thunk,App-Lam,Let-Ret,Case-Inl,Case-Inr}
|
|
\endgroup
|
|
|
|
\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]]$ (or $[[n ∈ 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}
|
|
|
|
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 $[[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}
|
|
|
|
\begingroup
|
|
\setlength{\abovedisplayskip}{0pt}
|
|
\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}
|
|
\endgroup
|
|
|
|
\begin{proof}
|
|
First, use \rref{sn-App-inv1,sn-App-inv2,sn-Let-inv1,sn-Let-inv2}
|
|
to obtain $[[m ∈ sn]]$ and $[[v ∈ sn]]$/$[[n ∈ 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:commute}
|
|
to join the strong head 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 $[[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
|
|
\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 $[[m ∈ SNe]]$ then $[[m ∈ ne]]$.
|
|
\end{lemma}
|
|
|
|
\begin{proof}
|
|
By induction on the derivation of $[[m ∈ SNe]]$.
|
|
\end{proof}
|
|
|
|
\begin{theorem}[Soundness (\textsf{SN})] \label{thm:soundness-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-sn}.
|
|
The cases for strong head 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}
|
|
|
|
\subsection{Proof Structure of Strong Normalization}
|
|
|
|
Overall, the inductive characterization of strongly normal terms is convenient to work with.
|
|
Its congruence and inversion properties,
|
|
already built in by its inductive nature,
|
|
are exactly what are needed to show
|
|
\nameref{lem:closure} and \nameref{lem:adequacy} of the logical relation.
|
|
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 reduces 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 $[[F 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 the original 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}$ by construction.
|
|
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 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 applies 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 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 thrice for single induction
|
|
(\ie all other motives are trivial):
|
|
\rref{SN-Force-inv}, \nameref{cor:ext}, and \nameref{lem:closure}.
|
|
|
|
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 conjoined 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} |