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

Final edits

This commit is contained in:
Jonathan Chan 2025-04-22 12:34:42 -04:00
parent 98cfb5b7de
commit 4cdd0c233a
3 changed files with 24 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
cbpv.mng
View File

@ -725,9 +725,10 @@ traditional strong normalization of well typed terms holds as a corollary.
\subsection{Proof Structure of Strong Normalization} \subsection{Proof Structure of Strong Normalization}
Overall, the inductive characterization of strongly normal terms is convenient to work with. Overall, the inductive characterization of strongly normal terms is convenient to work with.
Its congruence and inversion properties are exactly what are needed Its congruence and inversion properties,
to show \nameref{lem:closure} and \nameref{lem:adequacy} of the logical relation, already built in by its inductive nature,
which are 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, Proving soundness itself relies mostly on the properties of the logical relation,
along with a few more congruence properties of strong head reduction. along with a few more congruence properties of strong head reduction.
Knowing the general recipe for constructing the inductive definition Knowing the general recipe for constructing the inductive definition
@ -737,7 +738,7 @@ There are only a few pitfalls related to simply typed CBPV specifically:
\begin{itemize}[rightmargin=\leftmargin] \begin{itemize}[rightmargin=\leftmargin]
\item I originally included a corresponding notion of reduction for values \item I originally included a corresponding notion of reduction for values
in the mutual inductive which reduced under subterms. in the mutual inductive which reduces under subterms.
This is unnecessary not only because values have no $\beta$-reductions, 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, but also because subterms of strongly normal values need to be strongly normal anyway,
so there is no need to reduce subterms. so there is no need to reduce subterms.
@ -772,13 +773,13 @@ require double or even triple induction.
\Rref{sn-App-bwd,sn-Let-bwd} are especially tricky, \Rref{sn-App-bwd,sn-Let-bwd} are especially tricky,
since their double inductions are on two auxiliary derivations since their double inductions are on two auxiliary derivations
produced from one of the actual premises, produced from one of the actual premises,
and that premise unintuitively needs to stick around over the course of the inductions. and the original premise unintuitively needs to stick around over the course of the inductions.
Without guidance from the POPLMark Reloaded paper, Without guidance from the POPLMark Reloaded paper,
I would have been stuck on these two particular lemmas for much longer. 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} The purpose of all the work done in \cref{sec:sn-acc}
is to show that $\kw{sn}$ satisfies properties that is to show that $\kw{sn}$ satisfies properties that
otherwise hold by definition for $\kw{SN}$ as a constructor. otherwise hold by definition for $\kw{SN}$ by construction.
If proving that the latter is sound with respect to the former 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, already requires all this work showing that the former behaves exactly like the latter,
then what is the point of using the inductive characterization? then what is the point of using the inductive characterization?
@ -808,7 +809,7 @@ to the particularities of the chosen reduction strategy.
The proof development involved in this report consists of nine files, The proof development involved in this report consists of nine files,
as mentioned throughout. as mentioned throughout.
\Cref{tab:loc} gives the number of non-blank, non-comment lines of code for each file, \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. which roughly reflects the amount of proof effort required.
The \texttt{Syntax.lean} file involves a lot of renaming and substitution proofs, 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. 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} The actual semantic proofs in \texttt{NormalInd.lean}, \texttt{OpenSemantics.lean}, and \texttt{Soundness.lean}
@ -850,7 +851,7 @@ each with motives for all mutual inductives,
similar to what \texttt{Scheme Induction for ... with Induction for ...} similar to what \texttt{Scheme Induction for ... with Induction for ...}
generates in Rocq. generates in Rocq.
Lean's induction tactic produces applications of the appropriate recursor, Lean's induction tactic applies the appropriate recursor,
but does not support mutual inductives. but does not support mutual inductives.
In cases where induction on only a single inductive from the mutual definitions is needed, 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, the induction tactic can be supplied with a custom recursor,
@ -867,7 +868,7 @@ However, this feature is currently a little buggy,
and fails on some more complex inductive types.% and fails on some more complex inductive types.%
\footnote{\url{https://github.com/leanprover/lean4/issues/1672}} \footnote{\url{https://github.com/leanprover/lean4/issues/1672}}
Futhermore, writing proofs as recursive functions is unconventional, Futhermore, writing proofs as recursive functions is unconventional,
and isn't amenable to even simple automation that can automatically apply induction hypotheses. 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. Of course, it's possible to manually apply the recursors that Lean generates for each mutual inductive.
This is inconvenient for several reasons: This is inconvenient for several reasons:
@ -905,7 +906,7 @@ Specifically, mutual theorems are first stated as some conjunction
$(\forall v, P \gap v) \wedge (\forall m, Q \gap m)$, $(\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, 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$. 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. 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, There are discussions underway for introducing top-level syntax for mutual theorems,
similar to Rocq's \texttt{Theorem ... with ...} vernacular, similar to Rocq's \texttt{Theorem ... with ...} vernacular,
so that multiple goals are introduced automatically with their hypotheses.% so that multiple goals are introduced automatically with their hypotheses.%

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

Binary file not shown.

21
cbpv.tex
View File

@ -725,9 +725,10 @@ traditional strong normalization of well typed terms holds as a corollary.
\subsection{Proof Structure of Strong Normalization} \subsection{Proof Structure of Strong Normalization}
Overall, the inductive characterization of strongly normal terms is convenient to work with. Overall, the inductive characterization of strongly normal terms is convenient to work with.
Its congruence and inversion properties are exactly what are needed Its congruence and inversion properties,
to show \nameref{lem:closure} and \nameref{lem:adequacy} of the logical relation, already built in by its inductive nature,
which are 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, Proving soundness itself relies mostly on the properties of the logical relation,
along with a few more congruence properties of strong head reduction. along with a few more congruence properties of strong head reduction.
Knowing the general recipe for constructing the inductive definition Knowing the general recipe for constructing the inductive definition
@ -737,7 +738,7 @@ There are only a few pitfalls related to simply typed CBPV specifically:
\begin{itemize}[rightmargin=\leftmargin] \begin{itemize}[rightmargin=\leftmargin]
\item I originally included a corresponding notion of reduction for values \item I originally included a corresponding notion of reduction for values
in the mutual inductive which reduced under subterms. in the mutual inductive which reduces under subterms.
This is unnecessary not only because values have no $\beta$-reductions, 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, but also because subterms of strongly normal values need to be strongly normal anyway,
so there is no need to reduce subterms. so there is no need to reduce subterms.
@ -772,13 +773,13 @@ require double or even triple induction.
\Rref{sn-App-bwd,sn-Let-bwd} are especially tricky, \Rref{sn-App-bwd,sn-Let-bwd} are especially tricky,
since their double inductions are on two auxiliary derivations since their double inductions are on two auxiliary derivations
produced from one of the actual premises, produced from one of the actual premises,
and that premise unintuitively needs to stick around over the course of the inductions. and the original premise unintuitively needs to stick around over the course of the inductions.
Without guidance from the POPLMark Reloaded paper, Without guidance from the POPLMark Reloaded paper,
I would have been stuck on these two particular lemmas for much longer. 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} The purpose of all the work done in \cref{sec:sn-acc}
is to show that $\kw{sn}$ satisfies properties that is to show that $\kw{sn}$ satisfies properties that
otherwise hold by definition for $\kw{SN}$ as a constructor. otherwise hold by definition for $\kw{SN}$ by construction.
If proving that the latter is sound with respect to the former 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, already requires all this work showing that the former behaves exactly like the latter,
then what is the point of using the inductive characterization? then what is the point of using the inductive characterization?
@ -808,7 +809,7 @@ to the particularities of the chosen reduction strategy.
The proof development involved in this report consists of nine files, The proof development involved in this report consists of nine files,
as mentioned throughout. as mentioned throughout.
\Cref{tab:loc} gives the number of non-blank, non-comment lines of code for each file, \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. which roughly reflects the amount of proof effort required.
The \texttt{Syntax.lean} file involves a lot of renaming and substitution proofs, 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. 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} The actual semantic proofs in \texttt{NormalInd.lean}, \texttt{OpenSemantics.lean}, and \texttt{Soundness.lean}
@ -850,7 +851,7 @@ each with motives for all mutual inductives,
similar to what \texttt{Scheme Induction for ... with Induction for ...} similar to what \texttt{Scheme Induction for ... with Induction for ...}
generates in Rocq. generates in Rocq.
Lean's induction tactic produces applications of the appropriate recursor, Lean's induction tactic applies the appropriate recursor,
but does not support mutual inductives. but does not support mutual inductives.
In cases where induction on only a single inductive from the mutual definitions is needed, 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, the induction tactic can be supplied with a custom recursor,
@ -867,7 +868,7 @@ However, this feature is currently a little buggy,
and fails on some more complex inductive types.% and fails on some more complex inductive types.%
\footnote{\url{https://github.com/leanprover/lean4/issues/1672}} \footnote{\url{https://github.com/leanprover/lean4/issues/1672}}
Futhermore, writing proofs as recursive functions is unconventional, Futhermore, writing proofs as recursive functions is unconventional,
and isn't amenable to even simple automation that can automatically apply induction hypotheses. 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. Of course, it's possible to manually apply the recursors that Lean generates for each mutual inductive.
This is inconvenient for several reasons: This is inconvenient for several reasons:
@ -905,7 +906,7 @@ Specifically, mutual theorems are first stated as some conjunction
$(\forall v, P \gap v) \wedge (\forall m, Q \gap m)$, $(\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, 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$. 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. 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, There are discussions underway for introducing top-level syntax for mutual theorems,
similar to Rocq's \texttt{Theorem ... with ...} vernacular, similar to Rocq's \texttt{Theorem ... with ...} vernacular,
so that multiple goals are introduced automatically with their hypotheses.% so that multiple goals are introduced automatically with their hypotheses.%