agda/notes/talks/MetaVars/proof.sty

%       proof.sty       (Proof Figure Macros)
%
%       version 3.0 (for both LaTeX 2.09 and LaTeX 2e)
%       Mar 6, 1997
%       Copyright (C) 1990 -- 1997, Makoto Tatsuta (tatsuta@nii.ac.jp)
% 
% This program is free software; you can redistribute it or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation; either versions 1, or (at your option)
% any later version.
% 
% This program is distributed in the hope that it will be useful
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
% GNU General Public License for more details.
%
%       Usage:
%               In \documentstyle, specify an optional style `proof', say,
%                       \documentstyle[proof]{article}.
%
%       The following macros are available:
%
%       In all the following macros, all the arguments such as
%       <Lowers> and <Uppers> are processed in math mode.
%
%       \infer<Lower><Uppers>
%               draws an inference.
%
%               Use & in <Uppers> to delimit upper formulae.
%               <Uppers> consists more than 0 formulae.
%
%               \infer returns \hbox{ ... } or \vbox{ ... } and
%               sets \@LeftOffset and \@RightOffset globally.
%
%       \infer[<Label>]<Lower><Uppers>
%               draws an inference labeled with <Label>.
%
%       \infer*<Lower><Uppers>
%               draws a many step deduction.
%
%       \infer*[<Label>]<Lower><Uppers>
%               draws a many step deduction labeled with <Label>.
%
%       \infer=<Lower><Uppers>
%               draws a double-ruled deduction.
%
%       \infer=[<Label>]<Lower><Uppers>
%               draws a double-ruled deduction labeled with <Label>.
%
%       \deduce<Lower><Uppers>
%               draws an inference without a rule.
%
%       \deduce[<Proof>]<Lower><Uppers>
%               draws a many step deduction with a proof name.
%
%       Example:
%               If you want to write
%                           B C
%                          -----
%                      A     D
%                     ----------
%                         E
%       use
%               \infer{E}{
%                       A
%                       &
%                       \infer{D}{B & C}
%               }
%

%       Style Parameters

\newdimen\inferLineSkip         \inferLineSkip=2pt
\newdimen\inferLabelSkip        \inferLabelSkip=5pt
\def\inferTabSkip{\quad}

%       Variables

\newdimen\@LeftOffset   % global
\newdimen\@RightOffset  % global
\newdimen\@SavedLeftOffset      % safe from users

\newdimen\UpperWidth
\newdimen\LowerWidth
\newdimen\LowerHeight
\newdimen\UpperLeftOffset
\newdimen\UpperRightOffset
\newdimen\UpperCenter
\newdimen\LowerCenter
\newdimen\UpperAdjust
\newdimen\RuleAdjust
\newdimen\LowerAdjust
\newdimen\RuleWidth
\newdimen\HLabelAdjust
\newdimen\VLabelAdjust
\newdimen\WidthAdjust

\newbox\@UpperPart
\newbox\@LowerPart
\newbox\@LabelPart
\newbox\ResultBox

%       Flags

\newif\if@inferRule     % whether \@infer draws a rule.
\newif\if@DoubleRule    % whether \@infer draws doulbe rules.
\newif\if@ReturnLeftOffset      % whether \@infer returns \@LeftOffset.
\newif\if@MathSaved     % whether inner math mode where \infer or
                        % \deduce appears.

%       Special Fonts

\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
    \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}

%       Math Save Macros
%
%       \@SaveMath is called in the very begining of toplevel macros
%       which are \infer and \deduce.
%       \@RestoreMath is called in the very last before toplevel macros end.
%       Remark \infer and \deduce ends calling \@infer.

\def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner
        \relax $\relax \@MathSavedtrue \fi\fi }

\def\@RestoreMath{\if@MathSaved \relax $\relax\fi }

%       Macros

% Renaming @ifnextchar and @ifnch of LaTeX2e to @IFnextchar and @IFnch.

\def\@IFnextchar#1#2#3{%
  \let\reserved@e=#1\def\reserved@a{#2}\def\reserved@b{#3}\futurelet
    \reserved@c\@IFnch}
\def\@IFnch{\ifx \reserved@c \@sptoken \let\reserved@d\@xifnch
      \else \ifx \reserved@c \reserved@e\let\reserved@d\reserved@a\else
          \let\reserved@d\reserved@b\fi
      \fi \reserved@d}

\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
        \ifx \@tempa \@tempb #2\else #3\fi }

\def\infer{\@SaveMath \@IFnextchar *{\@inferSteps}{\relax
        \@IFnextchar ={\@inferDoubleRule}{\@inferOneStep}}}

\def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse
        \@IFnextchar [{\@infer}{\@infer[\@empty]}}

\def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue
        \@IFnextchar [{\@infer}{\@infer[\@empty]}}

\def\@inferSteps*{\@IFnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}

\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}

\def\deduce{\@SaveMath \@IFnextchar [{\@deduce{\@empty}}
        {\@inferRulefalse \@infer[\@empty]}}

%       \@deduce<Proof Label>[<Proof>]<Lower><Uppers>

\def\@deduce#1[#2]#3#4{\@inferRulefalse
        \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}

%       \@infer[<Label>]<Lower><Uppers>
%               If \@inferRuletrue, it draws a rule and <Label> is right to
%               a rule. In this case, if \@DoubleRuletrue, it draws
%               double rules.
%
%               Otherwise, draws no rule and <Label> is right to <Lower>.

\def\@infer[#1]#2#3{\relax
% Get parameters
        \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
        \setbox\@LabelPart=\hbox{$#1$}\relax
        \setbox\@LowerPart=\hbox{$#2$}\relax
%
        \global\@LeftOffset=0pt
        \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
                \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
                \inferTabSkip
                \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
                #3\cr}}\relax
%                       Here is a little trick.
%                       \@ReturnLeftOffsettrue(false) influences on \infer or
%                       \deduce placed in ## locally
%                       because of \@SaveMath and \@RestoreMath.
        \UpperLeftOffset=\@LeftOffset
        \UpperRightOffset=\@RightOffset
% Calculate Adjustments
        \LowerWidth=\wd\@LowerPart
        \LowerHeight=\ht\@LowerPart
        \LowerCenter=0.5\LowerWidth
%
        \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
        \advance\UpperWidth by -\UpperRightOffset
        \UpperCenter=\UpperLeftOffset
        \advance\UpperCenter by 0.5\UpperWidth
%
        \ifdim \UpperWidth > \LowerWidth
                % \UpperCenter > \LowerCenter
        \UpperAdjust=0pt
        \RuleAdjust=\UpperLeftOffset
        \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
        \RuleWidth=\UpperWidth
        \global\@LeftOffset=\LowerAdjust
%
        \else   % \UpperWidth <= \LowerWidth
        \ifdim \UpperCenter > \LowerCenter
%
        \UpperAdjust=0pt
        \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
        \LowerAdjust=\RuleAdjust
        \RuleWidth=\LowerWidth
        \global\@LeftOffset=\LowerAdjust
%
        \else   % \UpperWidth <= \LowerWidth
                % \UpperCenter <= \LowerCenter
%
        \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
        \RuleAdjust=0pt
        \LowerAdjust=0pt
        \RuleWidth=\LowerWidth
        \global\@LeftOffset=0pt
%
        \fi\fi
% Make a box
        \if@inferRule
%
        \setbox\ResultBox=\vbox{
                \moveright \UpperAdjust \box\@UpperPart
                \nointerlineskip \kern\inferLineSkip
                \if@DoubleRule
                \moveright \RuleAdjust \vbox{\hrule width\RuleWidth
                        \kern 1pt\hrule width\RuleWidth}\relax
                \else
                \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
                \fi
                \nointerlineskip \kern\inferLineSkip
                \moveright \LowerAdjust \box\@LowerPart }\relax
%
        \@ifEmpty{#1}{}{\relax
%
        \HLabelAdjust=\wd\ResultBox     \advance\HLabelAdjust by -\RuleAdjust
        \advance\HLabelAdjust by -\RuleWidth
        \WidthAdjust=\HLabelAdjust
        \advance\WidthAdjust by -\inferLabelSkip
        \advance\WidthAdjust by -\wd\@LabelPart
        \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
%
        \VLabelAdjust=\dp\@LabelPart
        \advance\VLabelAdjust by -\ht\@LabelPart
        \VLabelAdjust=0.5\VLabelAdjust  \advance\VLabelAdjust by \LowerHeight
        \advance\VLabelAdjust by \inferLineSkip
%
        \setbox\ResultBox=\hbox{\box\ResultBox
                \kern -\HLabelAdjust \kern\inferLabelSkip
                \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
%
        }\relax % end @ifEmpty
%
        \else % \@inferRulefalse
%
        \setbox\ResultBox=\vbox{
                \moveright \UpperAdjust \box\@UpperPart
                \nointerlineskip \kern\inferLineSkip
                \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
                        \@ifEmpty{#1}{}{\relax
                        \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
        \fi
%
        \global\@RightOffset=\wd\ResultBox
        \global\advance\@RightOffset by -\@LeftOffset
        \global\advance\@RightOffset by -\LowerWidth
        \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
%
        \box\ResultBox
        \@RestoreMath
}