Leaf Petersen
53345a6d6d
BUG= R=jmesserly@google.com, vsm@google.com Review URL: https://codereview.chromium.org/1205173003
260 lines
7.1 KiB
TeX
260 lines
7.1 KiB
TeX
% proof.sty (Proof Figure Macros)
|
|
%
|
|
% version 3.1 (for both LaTeX 2.09 and LaTeX 2e)
|
|
% Nov 24, 2005
|
|
% Copyright (C) 1990 -- 2005, 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.
|
|
|
|
% Special Fonts
|
|
|
|
\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
|
|
\vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
|
|
|
|
% 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{\@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{\@IFnextchar [{\@deduce{\@empty}}
|
|
{\@inferRulefalse \@infer[\@empty]}}
|
|
|
|
% \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
|
|
|
|
\def\@deduce#1[#2]#3#4{\@inferRulefalse
|
|
\@infer[\@empty]{#3}{\@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
|
|
\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
|
|
}
|