small corrections

jfla-paper/fereegooliglesiasvazquez2024.tex

@@ -12,7 +12,7 @@
 
 \usepackage[capitalise]{cleveref}
 \newcommand{\Ra}{\Rightarrow}
-
+\newcommand{\Coq}{{Coq/Rocq}}
 
 \theoremstyle{definition}
 \newtheorem{definition}{Definition}
@@ -104,22 +104,22 @@ \section{Introduction}
 Here, by a propositional \emph{formula} we mean any term built from variables, here denoted by letters $p, q, \dots$, using binary operations $\vee, \wedge, \to$, and a nullary operation $\bot$. Alternatively, one may think of such a formula as a type in a simply typed $\lambda$-calculus with zero, sum, and product types. Throughout the paper, by \emph{equivalence} of two formulas $\phi$ and $\phi'$ we mean that the formula $(\phi \to \phi') \wedge (\phi' \to \phi)$ is provable, or, on the other side of the Curry-Howard isomorphism, inhabited. The precise definition of the adjective `simpler' in (\ref{eq:question}) that we use here depends on a function associating to each formula a natural number, its \emph{weight}. We give the function in~\cref{dfn:weight} below; for now, it suffices to say that it satisfies the intuitive property that shorter formulas have lower weight.
 
 Since intuitionistic equivalence is decidable, there evidently exists a simplest formula in any equivalence class, and such a formula is computable by a brute-force enumeration. However, we here seek a practically feasible, and provably correct, answer to the question (\ref{eq:question}).
-The immediate origin of the question, for us, lies in a verified Coq/Rocq implementation by the first and second author~\cite{FerGoo2023} of Pitts' procedure~\cite{Pit1992} for computing propositional quantifiers in intuitionistic logic. Given a propositional formula $\phi$ and a propositional variable $p$, the formulas $\exists p. \phi$ and $\forall p. \phi$ are abstractly defined by the usual rules of quantification, see~\cref{dfn:prop-quantifiers}. The surprising result of~\cite{Pit1992} is that for any $\phi$, there actually exist \emph{propositional} formulas $\Ep{\phi}$ and $\Ap{\phi}$ that are equivalent to $\exists p. \phi$ and $\forall p. \phi$, respectively. This implies in particular that second-order propositional quantifiers may in fact be encoded, up to equivalence, in the zero-order fragment. Pitts' theorem has many consequences for higher-order intuitionistic logic, including a uniform interpolation theorem and the existence of a model completion for the class of Heyting algebras, further see~\cite{GhiZaw2002}. Since the implementation of~\cite{FerGoo2023}, researchers in intuitionistic logic have also become interested in computing the formulas $\Ep{\phi}$ and $\Ap{\phi}$ on specific examples; see for example~\cite{Koc2023} and also our remarks in Section~\ref{sec:benchmarks} below.
+The immediate origin of the question, for us, lies in a verified {\Coq} implementation by the first and second author~\cite{FerGoo2023} of Pitts' procedure~\cite{Pit1992} for computing propositional quantifiers in intuitionistic logic. Given a propositional formula $\phi$ and a propositional variable $p$, the formulas $\exists p. \phi$ and $\forall p. \phi$ are abstractly defined by the usual rules of quantification, see~\cref{dfn:prop-quantifiers}. The surprising result of~\cite{Pit1992} is that for any $\phi$, there actually exist \emph{propositional} formulas $\Ep{\phi}$ and $\Ap{\phi}$ that are equivalent to $\exists p. \phi$ and $\forall p. \phi$, respectively. This implies in particular that second-order propositional quantifiers may in fact be encoded, up to equivalence, in the zero-order fragment. Pitts' theorem has many consequences for higher-order intuitionistic logic, including a uniform interpolation theorem and the existence of a model completion for the class of Heyting algebras, further see~\cite{GhiZaw2002}. Since the implementation of~\cite{FerGoo2023}, researchers in intuitionistic logic have also become interested in computing the formulas $\Ep{\phi}$ and $\Ap{\phi}$ on specific examples; see for example~\cite{Koc2023} and also our remarks in Section~\ref{sec:benchmarks} below.
 
-A main issue that we already identified in~\cite{FerGoo2023} was that, even on relatively small inputs, the formulas that were output by our program were very large; we will quantify this in Table~\ref{tab:quant-improvements} below. In all specific cases of interest, one could show manually that the output would admit substantial simplifications, but developing an algorithm for applying such simplifications was both a conceptual and technical challenge. Our main contribution here is to give such a simplification algorithm for intuitionistic formulas, accompanied by a verified implementation in Coq/Rocq. Further, by interleaving Pitts' original recursive procedure with our simplification procedure, we obtain a program with much improved efficiency. This moreover allows us to simplify Pitts' procedure itself both on paper and in the verified implementation, building also on recent insights from work in~\cite{FGGS2024}. 
+A main issue that we already identified in~\cite{FerGoo2023} was that, even on relatively small inputs, the formulas that were output by our program were very large; we will quantify this in Table~\ref{tab:quant-improvements} below. In all specific cases of interest, one could show manually that the output would admit substantial simplifications, but developing an algorithm for applying such simplifications was both a conceptual and technical challenge. Our main contribution here is to give such a simplification algorithm for intuitionistic formulas, accompanied by a verified implementation in {\Coq}. Further, by interleaving Pitts' original recursive procedure with our simplification procedure, we obtain a program with much improved efficiency. This moreover allows us to simplify Pitts' procedure itself both on paper and in the verified implementation, building also on recent insights from work in~\cite{FGGS2024}. 
 
 Our approach, which we explain in more detail in the rest of this paper, relies on the sequent calculus $\Gfourip$, which was also used by Pitts in~\cite{Pit1992} and implemented in~\cite{FerGoo2023}. The first step is to use this calculus to obtain a decision procedure for the logic, for which we provide a verified implementation, that we further explain in \cref{sec:decision}. 
 We subsequently use the decision procedure to algorithmically simplify both the left and right hand side of a sequent.
-Both the decision and simplification procedures are guided by the invertible rules of the sequent calculus. To be able to use the decision procedure inside the simplification procedure, we use admissibility of cut and weakening. For this, we give a verified proof of cut admissibility for the sequent calculus $\Gfourip$, relying on the formally verified proof of~\cite{Shillito23}, by integrating the ideas developed there into our existing Coq/Rocq development.
+Both the decision and simplification procedures are guided by the invertible rules of the sequent calculus. To be able to use the decision procedure inside the simplification procedure, we use admissibility of cut and weakening. For this, we give a verified proof of cut admissibility for the sequent calculus $\Gfourip$, relying on the formally verified proof of~\cite{Shillito23}, by integrating the ideas developed there into our existing {\Coq} development.
 We give more details in \cref{sec:simplification}.
 
 
-In order to make our simplification algorithm usable for calculating propositional quantifiers, we first give a formal proof in Coq/Rocq that these simplification functions are correct, in the sense that they always compute equivalent formulas and contexts of lower weight. Given a correct simplification function, we interleave it with Pitts' calculation at each recursive call, and then show, with a relatively low amount of effort, that the newly calculated propositional quantifiers are still correct. This methodology means that one may still improve the simplification function later, without touching the rest of the correctness proof for the propositional quantifiers.
+In order to make our simplification algorithm usable for calculating propositional quantifiers, we first give a formal proof in {\Coq} that these simplification functions are correct, in the sense that they always compute equivalent formulas and contexts of lower weight. Given a correct simplification function, we interleave it with Pitts' calculation at each recursive call, and then show, with a relatively low amount of effort, that the newly calculated propositional quantifiers are still correct. This methodology means that one may still improve the simplification function later, without touching the rest of the correctness proof for the propositional quantifiers.
 
 % \sam{TODO It opens up a number of new questions: Complexity, Optimality of the simplification (and is it worth it, there may be a trade-off where simpler formulas can be very difficult to obtain and the one an algorithm obtains is already readable? Although maybe this is unlikely because if a formula is already readable it should be easy to simplify it further.) }
 
 
-The Coq/Rocq development is available online at \url{https://github.com/hferee/UIML/}. A web demo of the calculator is available at \url{https://hferee.github.io/UIML/}, which also links to online documentation of the Coq/Rocq code. Throughout this paper, we provide links to relevant Coq/Rocq declarations with the symbol \coqdoc{toc.html}. The reference commit for the code discussed in this paper is \href{https://github.com/hferee/UIML/tree/39b38d9d8c86672bea49bef5c342a24526914de9}{\texttt{39b38d9}}.
+The {\Coq} development is available online at \url{https://github.com/hferee/UIML/}. A web demo of the calculator is available at \url{https://hferee.github.io/UIML/}, which also links to online documentation of the {\Coq} code. Throughout this paper, we provide links to relevant {\Coq} declarations with the symbol \coqdoc{toc.html}. The reference commit for the code discussed in this paper is \href{https://github.com/hferee/UIML/tree/39b38d9d8c86672bea49bef5c342a24526914de9}{\texttt{39b38d9}}.
 
 \section{Sequents, proofs, and propositional quantifiers}\label{sec:prelims}
 A \emph{context} is a finite list of formulas, and is typically denoted with a capital Greek letter $\Gamma$ or $\Delta$. We denote the concatenation of contexts $\Gamma$ and $\Delta$ by $\Gamma, \Delta$, or occasionally $\Gamma \bullet \Delta$, and we abuse notation to write expressions like $\Gamma, \phi$ and $\Gamma \bullet \phi$ for the concatenation of $\Gamma$ with the one-element context containing only $\phi$. A \emph{sequent} is a pair of a context and a formula, denoted $\Gamma \Rightarrow \phi$. We now recall a notion of \emph{weight} on formulas and sequents~\cite{Pit1992}.
@@ -236,7 +236,7 @@ \section{Decision procedure}\label{sec:decision}
 
 To explain the intuition for this decision procedure, one may start from the idea of a naive proof search, which would explore all possible proof trees: Given an input sequent, for each applicable instance of a rule, one would recursively search for a proof for each of its premises.
 However, such a naive proof search is very inefficient.
-Our implementation, for which we give the pseudocode in \cref{fig:decision}, improves on this by applying the rules in a specific order, so as to avoid unnecessary branching as much as possible: (1) we first try to apply axioms to end the proof search; (2) if this is not possible, then we try to apply linear invertible rules, so as to obtain a single equivalent subsequent, and iterate; (3) if none of these apply, then we try to apply a duplicating invertible proof, leading to two successive proof searches; (4) finally, if no other rule is applicable, try each possible instance of a non-invertible rule and continue the search, in a depth-first-search manner. This leads to the following function, expressed in pseudocode as a pattern match in \cref{fig:decision}. For the reader's convenience, we annotate each case with the name of the corresponding $\Gfourip$-rule. When defining this function in Coq/Rocq, one needs to simultaneously prove termination, which we obtain from the fact that applying $\Gfourip$-rules upwards decreases the weight of a sequent. 
+Our implementation, for which we give the pseudocode in \cref{fig:decision}, improves on this by applying the rules in a specific order, so as to avoid unnecessary branching as much as possible: (1) we first try to apply axioms to end the proof search; (2) if this is not possible, then we try to apply linear invertible rules, so as to obtain a single equivalent subsequent, and iterate; (3) if none of these apply, then we try to apply a duplicating invertible proof, leading to two successive proof searches; (4) finally, if no other rule is applicable, try each possible instance of a non-invertible rule and continue the search, in a depth-first-search manner. This leads to the following function, expressed in pseudocode as a pattern match in \cref{fig:decision}. For the reader's convenience, we annotate each case with the name of the corresponding $\Gfourip$-rule. When defining this function in {\Coq}, one needs to simultaneously prove termination, which we obtain from the fact that applying $\Gfourip$-rules upwards decreases the weight of a sequent. 
 \begin{figure}[htp]
 \begin{algorithmic}[lines]
 	\Function{$\Gamma \vdash_? \phi $}{}
@@ -343,7 +343,7 @@ \subsection{Simplification of formulas in context}
 As an instructive example, let us run through a call of $\texttt{csimp} \; [] \; p \wedge (p \to q)$. The conjunction case defines $\phi\texttt{2'}$ with a recursive call to $\csimp$, with $\Delta = [p]$ and $\phi = p \to q$. In this recursive call, we are in the implication case, and we call $\csimp \; \Delta \; p$ and $\csimp \; \Delta \; q$, which both fall in the last case: The first returns $\top$, since $\Delta \vdash p$, and the second returns $q$, since $\Delta \not\vdash q$. According to the rules of $\texttt{choose\_impl}$, $\top \to q$ simplifies to $q$, which is propagated back to the original recursive call, and becomes the value of $\phi\texttt{2'}$. We then call $\csimp  \; [q] \; p$, but this immediately returns $p$. Finally, in this simple case, $\texttt{choose\_conj p q}$ just returns $p \wedge q$. For a slightly more complex example, the reader may verify that the simplification of the formula in \cref{eq:csimp-example} will lead to $p \wedge r \wedge q$, as expected.
 \end{example}
 
-We establish in Coq/Rocq the following correctness properties of the function $\csimp$. 
+We establish in {\Coq} the following correctness properties of the function $\csimp$. 
 \begin{proposition}
     For any context $\Delta$ and formula $\phi$, we have either $\csimp \; \Delta \; \phi = \top$ or $\weight(\csimp \; \Delta \; \phi) \leq \weight(\phi)$. \coqdoc{ISL.Simp_env.html\#contextual_simp_form_weight}
 \end{proposition}
@@ -388,7 +388,7 @@ \subsection{Simplification of contexts}
 \subsection{Simplifications specific to Pitts' algorithm}
 In earlier work~\cite{FerGoo2023} we gave a direct implementation of Pitts' algorithm~\cite{Pit1992} for computing propositional quantifiers. We briefly recall the general scheme of this algorithm. The goal is to compute, for any formula $\phi$, formulas $\exists p. \phi$ and $\forall p. \phi$ that satisfy the properties of \cref{dfn:prop-quantifiers}. The algorithm more generally computes, for any context $\Gamma$ and formula $\phi$, a formula $\Ep{\Gamma}$ and a formula $\Ap{\Gamma; \phi}$; the quantifiers are then defined as $\exists p. \phi := \Ep{[\phi]}$ and $\forall p. \phi := \Ap{[]; \phi}$.
 
-The formulas $\Ep{\Gamma}$ and $\Ap{\Gamma; \phi}$, in turn, are defined as the conjunction of a set of formulas $\callEp{\Gamma}$ and the disjunction of a set of formulas $\callAp{\Gamma; \phi}$, respectively. We do not recall in detail the definition of the sets of formulas $\callEp{\Gamma}$ and $\callAp{\Gamma; \phi}$ here; see \cite[Table 5]{Pit1992}, or the Coq/Rocq declarations \texttt{e\_rule} (\coqdoc{ISL.PropQuantifiers.html\#e_rule}), \texttt{a\_rule\_env} (\coqdoc{ISL.PropQuantifiers.html\#a_rule_env}), and \texttt{a\_rule\_form} (\coqdoc{ISL.PropQuantifiers.html\#a_rule_form}). 
+The formulas $\Ep{\Gamma}$ and $\Ap{\Gamma; \phi}$, in turn, are defined as the conjunction of a set of formulas $\callEp{\Gamma}$ and the disjunction of a set of formulas $\callAp{\Gamma; \phi}$, respectively. We do not recall in detail the definition of the sets of formulas $\callEp{\Gamma}$ and $\callAp{\Gamma; \phi}$ here; see \cite[Table 5]{Pit1992}, or the {\Coq} declarations \texttt{e\_rule} (\coqdoc{ISL.PropQuantifiers.html\#e_rule}), \texttt{a\_rule\_env} (\coqdoc{ISL.PropQuantifiers.html\#a_rule_env}), and \texttt{a\_rule\_form} (\coqdoc{ISL.PropQuantifiers.html\#a_rule_form}). 
 For the following discussion, it suffices to know that $\callAp{\Gamma; \phi}$ and $\callEp{\Gamma}$ are built by recursively computing $\mathsf{E}_p$ and $\mathsf{A}_p$ for the assumptions of any $\Gfourip$-rule that may be applied to the input; more precisely, at each stage of the computation, there are 8 different kinds of recursive calls for $\mathsf{E}$ and 13 different kinds of recursive calls for $\mathsf{A}$.
 
 The construction outlined above is practical for proving that the output formula is correct with respect to the specification.
@@ -441,7 +441,7 @@ \subsection{Simplifications specific to Pitts' algorithm}
 
 While one could use these observations to give a shorter correctness proof `from scratch' with fewer cases, we were able to re-use the correctness proofs that we had already formalized previously, with only slight modifications. Whenever the old version of the proof used an induction hypothesis about $\mathcal{A}_p(\Gamma; \phi)$ or $\mathcal{E}_p(\Gamma)$, in the new proof we are able to use the same induction hypothesis for $\mathcal{A}_p(\simpenv{\Gamma}; \phi)$ or $\mathcal{E}_p(\simpenv{\Gamma}$. To prove that this is indeed possible, one needs to observe that (i) $\simpenv{\Gamma}$ has lower weight than $\Gamma$, so the induction hypothesis used for $\Gamma$ \emph{a fortiori}  applies to $\simpenv{\Gamma}$; and (ii) the context $\simpenv{\Gamma}$ is equivalent to the context $\Gamma$, and may therefore be replaced by it in any hypothesis.
 
-A technical modification in the formalization of the proof that we had to make in order for this to go through was to change the induction principle. Our original implementation used an induction on the last rule in a hypothetical proof of a sequent of the form $\Gamma \vdash \cdot$ (when proving correctness for $\Ep{\Gamma}$) or of a sequent of the form $\Gamma \cup \cdot \vdash \phi$ (when proving correctness for $\Ap{\Gamma; \phi}$). In our new proof, we use an induction on the weight of the proved sequent.
+A technical modification in the formalization of the proof that we had to make in order for this to go through was to change the induction principle. Our original implementation used an induction on the last rule in a hypothetical proof of a sequent of the form $\Gamma \vdash \cdot$ (when proving correctness for $\Ep{\Gamma}$) or of a sequent of the form $\Gamma \cons \cdot \vdash \phi$ (when proving correctness for $\Ap{\Gamma; \phi}$). In our new proof, we use an induction on the weight of the sequent.