ionchy
/
CIS6700-Spring2025
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Finished Discussion

This commit is contained in:
Jonathan Chan 2025-04-21 14:29:59 -04:00
parent f9a4db5a53
commit 5d4df59b92
4 changed files with 301 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
cbpv.bib
View File

@ -0,0 +1,41 @@
@inproceedings{cbpv,
author = {Forster, Yannick and Sch\"{a}fer, Steven and Spies, Simon and Stark, Kathrin},
title = {{Call-by-push-value in Coq: operational, equational, and denotational theory}},
year = 2019,
isbn = {9781450362221},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
doi = {10.1145/3293880.3294097},
booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs},
pages = {118--131},
numpages = {14},
location = {Cascais, Portugal},
series = {CPP 2019}
}
@article{poplmark,
title = {{POPLMark reloaded: Mechanizing proofs by logical relations}},
volume = 29,
DOI = {10.1017/S0956796819000170},
journal = {Journal of Functional Programming},
publisher = {Cambridge University Press},
author = {Abel, Andreas and Allais, Guillaume and Hameer, Aliya and Pientka, Brigitte and Momigliano, Alberto and Schäfer, Steven and Stark, Kathrin},
year = 2019,
pages = {e19}
}
@inproceedings{autosubst2,
author = {Stark, Kathrin and Sch\"{a}fer, Steven and Kaiser, Jonas},
title = {{Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions}},
year = 2019,
isbn = {9781450362221},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
doi = {10.1145/3293880.3294101},
booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs},
pages = {166--180},
numpages = 15,
keywords = {de Bruijn repersentation, multi-sorted terms, parallel substiutions, sigma-calculus},
location = {Cascais, Portugal},
series = {CPP 2019}
}

136
cbpv.mng
View File

@ -3,13 +3,14 @@
\usepackage[supertabular]{ottalt}
\let\newlist\relax
\let\renewlist\relax
\usepackage[margin=1in]{geometry}
\usepackage[T1]{fontenc}
\usepackage{mlmodern}
\usepackage[margin=1in]{geometry}
\usepackage{enumitem,float,booktabs,xspace,doi}
\usepackage{enumitem,float,booktabs,xspace,xcolor,doi}
\usepackage{amsmath,amsthm,amssymb}
\usepackage[capitalize,nameinlink,noabbrev]{cleveref}
\usepackage{mathpartir,mathtools,stmaryrd,latexsym}
\usepackage[capitalize,nameinlink,noabbrev]{cleveref}
\usepackage[numbers]{natbib}
\setlist{noitemsep}
\hypersetup{
@ -43,8 +44,8 @@
\section{Introduction}
The goal of this project is to mechanize a proof of strong normalization for call-by-push-value (CBPV).
It follows work by Forster, Sch\"afer, Spies, and Stark (TODO: cite) on mechanizing the metatheory of CBPV in Rocq,
but instead adapts the proof technique from POPLMark Reloaded (TODO: cite).
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,
@ -60,7 +61,8 @@ In contrast to both prior works, which use Rocq, Agda, or Beluga,
this project is mechanized in Lean.
A secondary purpose of this project is to assess the capabilities of Lean for PL metatheory,
especially when making heavy use of mutually defined inductive types.
I have implemented a mutual induction tactic for Lean (TODO: link),
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.
@ -301,7 +303,7 @@ match on the term and the type and returning the conjunction of its premises,
but I wanted to use a mutually defined inductive definition.
\begin{figure}[H]
\fbox{$[[v ∈ ⟦A⟧]]$} \quad \fbox{$[[m ∈ ⟦B⟧]]$} \hfill \textit{} \\
\fbox{$[[v ∈ ⟦A⟧]]$} \quad \fbox{$[[m ∈ ⟦B⟧]]$} \hfill \textit{semantic inhabitance of types} \\
\begin{mathpar}
\drule[]{LRPP-Unit-var}
\drule[]{LRPP-Unit-unit}
@ -716,6 +718,8 @@ traditional strong normalization of well typed terms holds as a 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,
@ -797,4 +801,122 @@ 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}

BIN
cbpv.pdf (Stored with Git LFS)
View File

Binary file not shown.

136
cbpv.tex
View File

@ -3,13 +3,14 @@
\usepackage[supertabular]{ottalt}
\let\newlist\relax
\let\renewlist\relax
\usepackage[margin=1in]{geometry}
\usepackage[T1]{fontenc}
\usepackage{mlmodern}
\usepackage[margin=1in]{geometry}
\usepackage{enumitem,float,booktabs,xspace,doi}
\usepackage{enumitem,float,booktabs,xspace,xcolor,doi}
\usepackage{amsmath,amsthm,amssymb}
\usepackage[capitalize,nameinlink,noabbrev]{cleveref}
\usepackage{mathpartir,mathtools,stmaryrd,latexsym}
\usepackage[capitalize,nameinlink,noabbrev]{cleveref}
\usepackage[numbers]{natbib}
\setlist{noitemsep}
\hypersetup{
@ -43,8 +44,8 @@
\section{Introduction}
The goal of this project is to mechanize a proof of strong normalization for call-by-push-value (CBPV).
It follows work by Forster, Sch\"afer, Spies, and Stark (TODO: cite) on mechanizing the metatheory of CBPV in Rocq,
but instead adapts the proof technique from POPLMark Reloaded (TODO: cite).
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,
@ -60,7 +61,8 @@ In contrast to both prior works, which use Rocq, Agda, or Beluga,
this project is mechanized in Lean.
A secondary purpose of this project is to assess the capabilities of Lean for PL metatheory,
especially when making heavy use of mutually defined inductive types.
I have implemented a mutual induction tactic for Lean (TODO: link),
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.
@ -301,7 +303,7 @@ 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{} \\
\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}
@ -716,6 +718,8 @@ traditional strong normalization of well typed terms holds as a 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,
@ -797,4 +801,122 @@ 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}