diff --git a/cbpv.mng b/cbpv.mng index f19dece..94a151e 100644 --- a/cbpv.mng +++ b/cbpv.mng @@ -725,9 +725,10 @@ traditional strong normalization of well typed terms holds as a corollary. \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. +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 @@ -737,7 +738,7 @@ 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. + 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. @@ -772,13 +773,13 @@ 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. +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}$ as a constructor. +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? @@ -808,7 +809,7 @@ to the particularities of the chosen reduction strategy. 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. +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} @@ -850,7 +851,7 @@ 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, +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, @@ -867,7 +868,7 @@ 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. +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: @@ -905,7 +906,7 @@ 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. +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.% diff --git a/cbpv.pdf b/cbpv.pdf index 18e9590..64377d9 100644 --- a/cbpv.pdf +++ b/cbpv.pdf @@ -1,3 +1,3 @@ version https://git-lfs.github.com/spec/v1 -oid sha256:7524bf83211e81eebb1b2b53487d46a1255122a95492499cd24b1c7631a02694 -size 326980 +oid sha256:168965f631854952bfb76e480f8671ea55d6b644ac7583b2e3d37d10664e805d +size 327003 diff --git a/cbpv.tex b/cbpv.tex index c03ed34..ecd5e10 100644 --- a/cbpv.tex +++ b/cbpv.tex @@ -725,9 +725,10 @@ traditional strong normalization of well typed terms holds as a corollary. \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. +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 @@ -737,7 +738,7 @@ 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. + 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. @@ -772,13 +773,13 @@ 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. +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}$ as a constructor. +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? @@ -808,7 +809,7 @@ to the particularities of the chosen reduction strategy. 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. +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} @@ -850,7 +851,7 @@ 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, +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, @@ -867,7 +868,7 @@ 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. +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: @@ -905,7 +906,7 @@ 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. +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.%