path: root/macros/latex/contrib/logicproof/logicproof.dtx

% \iffalse meta-comment
%
% Copyright (C) 2014 by Alan Davidson <alan.davidson@gmail.com>
% ---------------------------------------------------------------------------
% This work may be distributed and/or modified under the
% conditions of the LaTeX Project Public License, either version 1.3
% of this license or (at your option) any later version.
% The latest version of this license is in
%   http://www.latex-project.org/lppl.txt
% and version 1.3 or later is part of all distributions of LaTeX
% version 2005/12/01 or later.
%
% This work has the LPPL maintenance status `maintained'.
%
% The Current Maintainer of this work is Alan Davidson.
%
% This work consists of the files logicproof.dtx and logicproof.ins
% and the derived filebase logicproof.sty.
%
% \fi
%
% \iffalse
%<*driver>
\ProvidesFile{logicproof.dtx}
%</driver>
%<package>\NeedsTeXFormat{LaTeX2e}
%<package>\ProvidesPackage{logicproof}[2014/03/20 v1.0 Box proofs for propositional logic]
%
%<*driver>
\documentclass{ltxdoc}
\usepackage{logicproof}[2014/03/20]
\EnableCrossrefs
\CodelineIndex
\RecordChanges
\begin{document}
  \DocInput{logicproof.dtx}
  \PrintChanges
  \PrintIndex
\end{document}
%</driver>
% \fi
%
% \CheckSum{0}
%
% \CharacterTable
%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
%   Digits        \0\1\2\3\4\5\6\7\8\9
%   Exclamation   \!     Double quote  \"     Hash (number) \#
%   Dollar        \$     Percent       \%     Ampersand     \&
%   Acute accent  \'     Left paren    \(     Right paren   \)
%   Asterisk      \*     Plus          \+     Comma         \,
%   Minus         \-     Point         \.     Solidus       \/
%   Colon         \:     Semicolon     \;     Less than     \<
%   Equals        \=     Greater than  \>     Question mark \?
%   Commercial at \@     Left bracket  \[     Backslash     \\
%   Right bracket \]     Circumflex    \^     Underscore    \_
%   Grave accent  \`     Left brace    \{     Vertical bar  \|
%   Right brace   \}     Tilde         \~}
%
%
% \changes{1.0}{2014/03/20}{First version for public release}
% \changes{0.1}{2004/12/05}{Initial version created}
% \GetFileInfo{logicproof.dtx}
%
% \DoNotIndex{\newcommand,\newenvironment}
%
% \providecommand*{\url}{\texttt}
% \title{The \textsf{logicproof} package}
% \author{Alan Davidson \\ \url{alan.davidson@gmail.com}}
% \date{20 March 2014}
%
% \maketitle
%
% \section{Introduction}
%
% This package provides support for Fitch-style box proofs, intended to be used
% for proofs in propositional logic and predicate logic. In this proof style,
% each statement of the proof is accompanied by a justification, and subproofs
% or lemmata within a larger proof are enclosed in boxes to separate them from
% the rest of the proof.
%
% \section{Usage}
%
% \DescribeEnv{logicproof}
% The |logicproof| environment takes a single argument, which should be a
% nonnegative integer describing the maximum number of nested subproofs that
% this proof will contain. Each line of the proof consists of two main
% columns: the proof statement of the current line, followed by an ampersand
% (|&|), followed by the justification for the statement.
% Lines should be separated from each other by a |\\|.
% The column of proof statements defaults to
% math mode, while the justification column defaults to normal text.
%
% If you add a |\label| within a proof, the corresponding |\ref| will be the
% current line number.
%
% \DescribeEnv{subproof}
% Within these logic proofs, it is often necessary to make subproofs which begin
% by making some sort of assumption that does not necessarily hold in the
% broader proof. To delineate the scope of these assumptions, use the |subproof|
% environment, which will draw a box around the statements of the proof for
% which these assumptions should hold. Subproofs can be nested within each
% other, up to the maximum level provided as an argument to the |logicproof|
% environment.
%
% Within a subproof, the format of each line is exactly the same as in the
% |logicproof| environment: a proof statement, followed by an ampersand (|&|),
% followed by a justification for the statement, with |\\| at the end of every
% line except the last one (which instead ends with |\end{subproof}|).
%
% If a statement has an empty justification, it is still important to put in the
% |&| to separate out the column in which the justification would go, or else
% the right sides of the subproof boxes will be misaligned for this statement.
%
% The previous line before a subproof begins should end in either |\\| or
% |\end{subproof}|.
%
% A warning for advanced \LaTeX~users: although most environments make their own
% groups (such that changes made within an environment go out of scope at the
% end of it), the |subproof| environment does not! Any changes made within a
% |subproof|
% environment will not go out of scope until the enclosing |logicproof|
% environment ends. This was done because groups cannot cross alignment tabs,
% but the |subproof| environment needs to use the same alignment as the
% enclosing |logicproof| environment does (or else they won't line up together).
% An inconvenient side effect of this is that when you forget to put in a
% |\end{subproof}|, the error message about mismatched environments points to
% the line number where the enclosing |logicproof| environment started, rather
% than the offending |subproof| environment.
%
% \section{Example}
%
% This example proves the validity of the sequent
% $(p\lor q)\lor r\vdash p\lor (q\lor r)$. There are many different styles that
% can be used for the justification of each step; we are using the style found
% in \emph{Logic in Computer Science: Modelling and Reasoning about Systems} by
% Huth and Ryan.
%
%\begin{verbatim}
%\begin{logicproof}{2}
%  (p\lor q)\lor r & premise\\
%  \begin{subproof}
%    (p\lor q) & assumption\\
%    \begin{subproof}
%      p & assumption\\
%      p\lor (q\lor r) & $\lor\mathrm{i}_1$, 3
%    \end{subproof}
%    \begin{subproof}
%      q & assumption\\
%      q\lor r & $\lor\mathrm{i}_1$, 5\\
%      p\lor (q\lor r) & $\lor\mathrm{i}_2$, 6
%    \end{subproof}
%    p\lor (q\lor r) & $\lor$e, 2, 3--4, 5--7
%  \end{subproof}
%  \begin{subproof}
%    r & assumption\\
%    q\lor r & $\lor\mathrm{i}_2$, 9\\
%    p\lor (q\lor r) & $\lor\mathrm{i}_2$, 10
%  \end{subproof}
%  p\lor (q\lor r) & $\lor$e, 1, 2--8, 9--11
%\end{logicproof}
%\end{verbatim}
% This compiles into the following:
%\begin{logicproof}{2}
%  (p\lor q)\lor r & premise\\
%  \begin{subproof}
%    (p\lor q) & assumption\\
%    \begin{subproof}
%      p & assumption\\
%      p\lor (q\lor r) & $\lor\mathrm{i}_1$, 3
%    \end{subproof}
%    \begin{subproof}
%      q & assumption\\
%      q\lor r & $\lor\mathrm{i}_1$, 5\\
%      p\lor (q\lor r) & $\lor\mathrm{i}_2$, 6
%    \end{subproof}
%    p\lor (q\lor r) & $\lor$e, 2, 3--4, 5--7
%  \end{subproof}
%  \begin{subproof}
%    r & assumption\\
%    q\lor r & $\lor\mathrm{i}_2$, 9\\
%    p\lor (q\lor r) & $\lor\mathrm{i}_2$, 10
%  \end{subproof}
%  p\lor (q\lor r) & $\lor$e, 1, 2--8, 9--11
%\end{logicproof}
%
% \section{Advanced Configuration}
%
% There are two lengths that can be configured manually if desired. 
%
% \DescribeMacro{\subproofhorizspace}
% The
% horizontal distance between the sides of nested boxes is the length stored in 
% |\subproofhorizspace|. If you have many nested subproofs, it might be
% desirable to make this space larger so that it is easier to distinguish
% between them.
%
% \DescribeMacro{\intersubproofvertspace}
% An extra vertical space of length
% |\intersubproofvertspace| is added after each statement in the proof. The
% intention here is to have this much space between consecutive subproofs. This
% is to say, when one subproof ends
% and the next subproof begins immediately, this is the distance between the
% bottom edge of the ending subproof and the top edge of the beginning subproof.
% This space is inserted after each line, however, so that the vertical spacing
% between them is consistent regardless of whether subproofs are begun or ended.
% If you want more compact proofs and you never use consecutive
% subproofs, it might be useful to reduce or remove this extra space.
%
% \section{Constraints}
% The environments in this package might not work properly if any of the
% following constraints are violated. These should not be difficult burdens;
% they are listed here mainly for completeness.
% \begin{itemize}
% \item Each proof and each subproof must be at least 1 statement long.
% \item Each subproof must start with at least 1 statement before containing
% another subproof inside itself. You should not have a subproof that
% immediately begins with a nested subproof.
% \item The end of each subproof must have at least 1 statement (or
% a new subproof) following
% it; a single proof statement cannot end multiple subproofs at once.
% Consequently, the last
% statement of the top-level proof must be outside of all subproofs. It is okay
% to immediately start a new subproof after ending a previous subproof.
% \end{itemize}
%
% \StopEventually{\PrintIndex\PrintChanges}
%
% \section{Summary of Implementation}
%
% The |logicproof| environment is built on the |tabular| environment. It has a
% column for the line number, a column for each possible nested subproof, a
% column for the statement, a column for the justification, and then a second
% column for each possible nested subproof.
% The columns corresponding to nested subproofs either contain a |\vline| if the
% subproof is currently being used, or nothing if the subproof is not being
% used.
% When a subproof is begun or ended, a |\cline| is used to draw
% horizontal lines between the columns corresponding to that subproof. In order
% to prevent multiple |\cline|'s from overlapping when one subproof is ended and
% another is immediately begun, each statement in the proof actually ends with
% a negative vertical space backing up to the previous line, then a space down
% |\intersubproofvertspace| and a redrawing of the subproof lines again to cover
% the extra space.
%
% \section{Implementation}
%
% \iffalse
%<*package>
% \fi
%
%    \begin{macrocode}
\RequirePackage{array}
\RequirePackage{ifthen}
%    \end{macrocode}
%    \begin{macro}{\subproofhorizspace}
%    \begin{macro}{\intersubproofvertspace}
% We allow the user to configure the horizontal and vertical distance between
% the edges of the boxes.
%    \begin{macrocode}
\newlength{\subproofhorizspace}
\setlength{\subproofhorizspace}{0.5em}
\newlength{\intersubproofvertspace}
\setlength{\intersubproofvertspace}{0.333em}
%    \end{macrocode}
%    \end{macro}
%    \end{macro}
% We use a variety of counters to keep track of the state.
%    \begin{macrocode}
\newcounter{lp@line}% Current line number on the proof
\newcounter{lp@nested}% Number of nested subproofs we're currently in
\newcounter{lp@total@nests}% Maximum number of nested subproofs allowed
\newcounter{lp@cline@1}% Used to draw horizontal lines in subproofs
\newcounter{lp@cline@2}% Also used to draw horizontal lines in subproofs
\newcounter{lp@temp}% Temporary storage counter
%    \end{macrocode}
%
% \begin{environment}{logicproof}
% Use this to make a logic proof. The argument it takes is the
% maximum number of nested subproofs you will use. 
%    \begin{macrocode}
\newenvironment{logicproof}[1]{%
  \setcounter{lp@line}{0}%
  \setcounter{lp@nested}{0}%
  \setcounter{lp@total@nests}{#1}%
  \setlength{\tabcolsep}{0mm}%
%    \end{macrocode}
% When using the array package, the tabular environment contains the statement
% |\let\\\@arraycr| (note that with the array package, |\@tabularcr| is replaced
% with |\@arraycr| even within the tabular environment). So, to modify the
% behavior of |\\|, we're actually going to modify |\@arraycr|. Save a copy of the
% original definition first, so that we can use it inside our new definition.
% Remember that when the logicproof environment finishes, this redefinition
% will go out of scope and revert to the previous version, so we won't ruin
% any future uses of the tabular environment.
%    \begin{macrocode}
  \let\lp@orig@arraycr\@arraycr%
  \renewcommand{\@arraycr}{\lp@cr}%
%    \end{macrocode}
% Get labels to work in proofs by defining |\@currentlabel| to always be the
% line number, regardless of where we are in the proof. Note that the usual
% approach of using
% |\refstepcounter{lp@line}| doesn't work because it goes out of scope by the
% time we get to the next cell in the tabular environment.
%    \begin{macrocode}
  \renewcommand{\@currentlabel}{\p@lp@line\thelp@line}%
%    \end{macrocode}
% If the maximum number of nested subproofs is 0, we need a slightly different
% column format, because the array environment doesn't like it when you repeat a
% formatting group 0 times.
%    \begin{macrocode}
  \ifthenelse{%
    0=#1%
  }{%
    \def\lp@tab@format{{r@{~~~}>{$}l<{$}@{~~~~}l}}%
  }{%
%    \end{macrocode}
% Although we could use the |array| package's |>{...}| and |<{...}| features to
% have automatic placement of the vertical lines on the sides of subproofs,
% we would not be able to get the horizontal lines at the tops and bottoms
% of the subproofs to line up properly. Consequently, we go with the ``old
% school'' approach of putting subproofs in their own columns, so that we
% can use |\cline| to put the horizontal lines in their proper places.
%    \begin{macrocode}
    \def\lp@tab@format%
        {{r@{~~~}*{#1}{l}@{~}>{$}l<{$}@{~~~~}l@{~}*{#1}{r}}}
  }%
  \center%
%    \end{macrocode}
% We use the |tabular| environment instead of the |array| environment because
% we want
% to be able to have labels on individual lines. Since the entirety of the
% |array| environment is in math mode, it does not support more than one label
% per array.
%    \begin{macrocode}
  \expandafter\tabular\lp@tab@format%
  \lp@start@proof@line%
}{%
  \lp@stop@proof@line%
  \endtabular%
  \endcenter%
%    \end{macrocode}
% To ensure that no one tries using the subproof environment outside of the
% logicproof environment, set the maximum number of nested subproofs to 0.
%    \begin{macrocode}
  \setcounter{lp@total@nests}{0}%
%    \end{macrocode}
% Finally, make sure that all open subproofs have been closed. We do this last
% because if a subproof is still open, we need to set |\@currenvir| properly
% for |\end| to check and throw errors on, but previous commands have
% |\endgroup|'s that make it revert to previous definitions.
%    \begin{macrocode}
  \ifthenelse{%
    0=\value{lp@nested}
  }{% All is well.
  }{% There are still open subproofs.
    \def\@currenvir{subproof}%
  }
}
%    \end{macrocode}
% \end{environment}
% \begin{environment}{subproof}
% This environment puts a box around the lines of the proof within it. It
% should come right after either a |\\| or a |\end{subproof}|.
%    \begin{macrocode}
\newenvironment{subproof}{%
%    \end{macrocode}
% Make sure we don't start more nested subproofs than the current logicproof
% environment can handle.
%    \begin{macrocode}
  \ifthenelse{%
    \value{lp@total@nests}>\value{lp@nested}%
  }{% All is well; don't do anything.
  }{%
    \PackageError{logicproof}{Too many nested subproofs!}{%
      Increase the maximum number of nested subproofs allowed
      in the current logicproof environment.%
    }%
  }%
%    \end{macrocode}
% The |\begin| and |\end| parts of an environment start and end a group, so that
% macros defined within them have local scope. However, a group cannot cross
% alignment tabs (|&|'s), which means that this subproof environment, which must
% cross them, needs to get rid of those extra groups first. So, we immediately
% end the group that |\begin| created before going on with the subproof. Note
% that this means any redefinitions of any macros we might have will persist
% outside this subproof and will not go out of scope until the entire
% logicproof environment is over. Note also that this approach is slightly
% brittle: if the implementation of |\begin| and |\end| ever changes, this
% subproof environment is likely to break.
%    \begin{macrocode}
  \endgroup%
  \lp@stop@proof@line%
%    \end{macrocode}
% Ideally, we'd use |\lp@extend@space| here. However, we first need to end the
% current line, which means putting in |\lp@orig@arraycr| and then going up an
% extra line in the tabular environment via |\lp@add@space|.
%    \begin{macrocode}
  \lp@orig@arraycr%
  \lp@add@space%
  \lp@go@up@a@line%
  \stepcounter{lp@nested}%
  \lp@cr@clines%
%    \end{macrocode}
% The current line number was added in before this subproof was started. Do
% not add it in again now; just skip over the line number entry and go
% straight on to the subproof-drawing stuff.
%    \begin{macrocode}
  &%
  \lp@continue@proof@line%
}{%
%    \end{macrocode}
% If we try ending a subproof that has not yet begun, we will run into trouble
% with |\cline| trying to draw a horizontal line to a column past the end of the
% tabular environment. This happens before |\end| actually checks whether we're
% ending the right environment. In order to get a more useful error message,
% we first check that there is at least 1 open subproof.
%    \begin{macrocode}
  \ifthenelse{%
    0<\value{lp@nested}%
  }{% All is well; don't do anything.
  }{%
    \PackageError{logicproof}{Cannot end a subproof before it begins}{%
      You must have a \protect\begin{subproof} before you can use %
      \protect\end{subproof}.%
    }%
  }%
  \lp@stop@proof@line%
  \lp@cr@clines%
  \addtocounter{lp@nested}{-1}%
  \lp@extend@space%
  \lp@start@proof@line%
%    \end{macrocode}
% Now that we're done with the subproof, we need to create a group because
% |\end| is expecting us to still be in the group that was started in |\begin|. We
% also must redefine |\@currenvir| within that group, or the error-checking in
% |\end| will think we've ended the wrong environment (its previous redefinition
% went out of scope when we ended the group created by |\begin|).
%    \begin{macrocode}
  \begingroup%
  \def\@currenvir{subproof}%
}
%    \end{macrocode}
% \end{environment}
% \begin{macro}{\lp@cr}
% This is what the |\\| will be defined as inside the logicproof environment.
%    \begin{macrocode}
\newcommand{\lp@cr}{%
  \lp@stop@proof@line%
  \lp@orig@arraycr%
  \lp@extend@space%
  \lp@start@proof@line%
}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\lp@go@up@a@line}
% This moves up one entire line in the proof.
%    \begin{macrocode}
\newcommand{\lp@go@up@a@line}{%
  \vspace{-\ht\@arstrutbox}%
  \vspace{-\dp\@arstrutbox}%
  \vspace{-\intersubproofvertspace}%
}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\lp@add@space}
% Extends the vertical lines at the sides of the proof down slightly, so that
% the horizontal lines at the end of the previous subproof and the start of the
% next one don't overlap. This basically inserts a blank row in the proof (no
% line number, no statement, no justification; just the subproof lines), then
% backs up part of a line.
%    \begin{macrocode}
\newcommand{\lp@add@space}{%
  \lp@extend@space%
%    \end{macrocode}
% The |\@arstrutbox| is a box containing the minimum array height. Remember that
% the height of the strut is spread between the height above the baseline and
% the depth below it!
%    \begin{macrocode}
  \vspace{-\ht\@arstrutbox}%
  \vspace{-\dp\@arstrutbox}%
%    \end{macrocode}
% Uncommenting this would line things up exactly where they started.
%    \begin{macrocode}
  %\vspace{-\intersubproofvertspace}%
}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\lp@extend@space}
% This extends the vertical lines at the sides of the subproofs down by
% an extra |\intersubproofvertspace.| This is done so that two subproofs in a
% row don't have their horizontal lines overlap each other.
%    \begin{macrocode}
\newcommand{\lp@extend@space}{%
  \vspace{-\ht\@arstrutbox}%
  \vspace{-\dp\@arstrutbox}%
  \vspace{\intersubproofvertspace}%
%    \end{macrocode}
% Now, insert a row that has vertical lines for the subproofs but no line
% number, proof statement, or justification.
%    \begin{macrocode}
  &%
  \lp@continue@proof@line%
  &%
  \lp@stop@proof@line%
  \lp@orig@arraycr%
}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\lp@amper}
% You can't have a |&| in a |\whiledo| loop, but this works instead. 
%    \begin{macrocode}
\newcommand{\lp@amper}{&}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\lp@start@proof@line}
% This macro does everything on a proof line before the statement itself: it
% increments and prints the line number, then calls
% |\lp@continue@proof@line| to put in the vertical lines of any subproofs we're
% currently in.
%    \begin{macrocode}
\newcommand{\lp@start@proof@line}{%
%    \end{macrocode}
% We use |\stepcounter| instead of |\refstepcounter| here because the changes made
% by |\refstepcounter| to how labels get made would go out of scope by the time
% we got to the next cell of the tabular environment (i.e., 2 lines from
% here). Instead, we redefined |\@currentlabel| at the beginning of the
% environment to always contain the current value of the |lp@line| counter.
%    \begin{macrocode}
  \stepcounter{lp@line}%
  \arabic{lp@line}.%
  &%
  \lp@continue@proof@line%
}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\lp@continue@proof@line}
% This macro makes the vertical lines of the subproof boxes on the left side of
% the proof (i.e., the ones that come between the line numbers and the proof
% statements). We use |\lp@amper| here because the raw |&| token doesn't play
% well with |\whiledo| loops.
%    \begin{macrocode}
\newcommand{\lp@continue@proof@line}{%
  \setcounter{lp@temp}{0}%
  \whiledo{\value{lp@temp}<\value{lp@nested}}{%
    \vline%
    \hspace*{\subproofhorizspace}%
    \lp@amper%
    \stepcounter{lp@temp}%
  }%
  \whiledo{\value{lp@temp}<\value{lp@total@nests}}{%
    \hspace*{\subproofhorizspace}%
    \lp@amper%
    \stepcounter{lp@temp}%
  }%
}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\lp@stop@proof@line}
% This macro makes the vertical lines of the subproof boxes on the right side
% of the proof (i.e., the ones that come after the justifications for each
% step). It basically does the same thing as |\lp@continue@proof@line|, but in
% reverse order. We use |\lp@amper| here because the raw |&| token doesn't play
% well with |\whiledo| loops.
%    \begin{macrocode}
\newcommand{\lp@stop@proof@line}{%
  \whiledo{\value{lp@temp}>\value{lp@nested}}{%
    \addtocounter{lp@temp}{-1}%
    \lp@amper%
    \hspace*{\subproofhorizspace}%
  }%
  \whiledo{\value{lp@temp}>0}{%
    \addtocounter{lp@temp}{-1}%
    \lp@amper%
    \hspace*{\subproofhorizspace}%
    \vline%
  }%
}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\lp@subtract@from@counter}
% Subtraction by a value in another counter is annoying, but with this we can
% use |\expandafter| and make it easier.
%    \begin{macrocode}
\newcommand{\lp@subtract@from@counter}[2]{%
  \addtocounter{#2}{-#1}%
}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\lp@set@clines}
% This macro sets up where the horizontal bars go for subproofs.
%    \begin{macrocode}
\newcommand{\lp@set@clines}{%
%    \end{macrocode}
% |lp@cline@1 = lp@nested + 1|
%    \begin{macrocode}
  \setcounter{lp@cline@1}{\value{lp@nested}}%
  \stepcounter{lp@cline@1}% 
%    \end{macrocode}
% |lp@cline@2 = 2 * lp@total@nests + 4 - lp@nested|
%    \begin{macrocode}
  \setcounter{lp@cline@2}{\value{lp@total@nests}}%
  \addtocounter{lp@cline@2}{\value{lp@total@nests}}%
  \addtocounter{lp@cline@2}{4}%
%    \end{macrocode}
% Subtracting one counter from another is tricky. We need to expand the value
% of the counter being subtracted first.
%    \begin{macrocode}
  \expandafter\lp@subtract@from@counter\expandafter{%
      \value{lp@nested}}{lp@cline@2}%
}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\lp@cr@clines}
% This macro goes to the next line of the tabular environment and puts in a
% horizontal line for the beginning or end of the current subproof.
%    \begin{macrocode}
\newcommand{\lp@cr@clines}{%
  \lp@set@clines%
%    \end{macrocode}
% We put the |\lp@orig@arraycr| here instead of in |\lp@stop@proof@line| because
% |\cline| doesn't seem to work properly unless it's right after the carriage
% return. Even moving it up above |\lp@set@clines| on the previous line messes
% it up.
%    \begin{macrocode}
  \lp@orig@arraycr%
  \cline{\value{lp@cline@1}-\value{lp@cline@2}}%
}
%    \end{macrocode}
% \end{macro}
%
% \iffalse
%</package>
% \fi
%
% \Finale
\endinput