reflect latest changes in coq in paper

jfla-paper/fereegooliglesiasvazquez2024.tex

@@ -7,7 +7,9 @@
 \def\BaseUrlCode{https://github.com/hferee/UIML}
 \newcommand{\coqdoc}[1]{\href{\BaseUrl/#1}{\raisebox{-.9mm}{\includegraphics[height=1em]{coql.png}}}}
 \def\CommitOrig{ebb461dd334ce10ceeb00ebaf6094778e2f03c4e} % Commit before the simplifications
-\def\CommitOpt{39b38d9d8c86672bea49bef5c342a24526914de9} % Last commit before deadline
+% \def\CommitOpt{39b38d9d8c86672bea49bef5c342a24526914de9} 
+\def\CommitOpt{44d4c8ed2ad8a725c4a5863d470b191063f29db8} % Last commit before deadline
+\def\CommitOptShort{44d4c8e}
 
 \usepackage[capitalise]{cleveref}
 \newcommand{\Ra}{\Rightarrow}
@@ -113,7 +115,7 @@ \section{Introduction}
 % \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} 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 under a clickable 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 under a clickable symbol \coqdoc{toc.html}. The reference commit for the code discussed in this paper is \href{https://github.com/hferee/UIML/tree/\CommitOpt}{\texttt{\CommitOptShort}}.
 
 \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}.
@@ -245,10 +247,7 @@ \section{Decision procedure}\label{sec:decision}
 	\Comment{$(\mathrm{IdP})$}
 	\CaseWhenEnd
 
-	\Case{$\_,\phi_1 \wedge \phi_2$}
-	$(\Gamma \vdash_? \phi_1) \;\band\; (\Gamma \vdash_? \phi_2)$
-	\Comment{$(\land\mathrm{R})$}
-	\CaseEnd
+
 
 	\Case{$\inside {\delta_1 \wedge \delta_2}$}
  	$\delta_1 \cons \delta_2 \cons \Delta_1 \cons \Delta_2 \vdash_? \phi$
@@ -275,6 +274,11 @@ \section{Decision procedure}\label{sec:decision}
 	\Comment{$(\lor\!\rightarrow\mathrm{L})$}
 	\CaseEnd
 
+	\Case{$\_,\phi_1 \wedge \phi_2$}
+	$(\Gamma \vdash_? \phi_1) \;\band\; (\Gamma \vdash_? \phi_2)$
+	\Comment{$(\land\mathrm{R})$}
+	\CaseEnd
+
     \Case{$\inside {\delta_1 \vee \delta_2},\_$}
 	$(\delta_1 \cons \Delta_1 \cons \Delta_2 \vdash_? \phi) \;\band\; (\delta_2 \cons \Delta_1 \cons \Delta_2 \vdash_? \phi)$
 	\Comment{$(\lor\mathrm{L})$}
@@ -427,7 +431,7 @@ \section{Examples, benchmarks and challenges}\label{sec:benchmarks}
 in the size of the output formulas (measured in weight) generated by Pitts' construction. These benchmarks allowed us to clearly evaluate the 
 effectiveness of each improvement.
 
-The example formulas used for our benchmark were of two kinds: First, we have two sequences of formulas $\phi_{\text{imp}}$ and $\phi_{\text{conj}}$ of increasing complexity, which we knew were treated inefficiently by our initial implementation; Second, our initial implementation drew the interest of researchers in intuitionistic logic, notably M. Jibladze (personal communication) and Z. Kocsis~\cite{Koc2023}, who provided us with a number of specific formulas of interest to them, for which the output of our initial implementation was highly complex, but for which one could prove `by hand' that the quantified formulas could be represented in a simple way. We include some of these examples as the formulas $\psi_1, \psi_2, \psi_3$, and $\psi_4$ below.
+The example formulas used for our benchmark were of two kinds: First, we have two sequences of formulas $\phi_{\text{imp}}$ and $\phi_{\text{conj}}$ of increasing complexity, which we knew were treated inefficiently by our initial implementation; Second, our initial implementation drew the interest of researchers in intuitionistic logic, notably M. Jibladze (personal communication) and Z. Kocsis~\cite{Koc2023}, who provided us with a number of specific formulas of interest to them, for which the output of our initial implementation was highly complex, but for which one could prove `by hand' that the quantified formulas could be represented in a simple way. We include some of these examples as the formulas $\psi_1, \psi_2, \psi_3$ (communicated to us by M.~Jibladze) and $\psi_4$~\cite[3.13]{Koc2023} below.
 
 
 \begin{itemize} \label{def:test-formulas}