summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/lkproof
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
committerNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
commite0c6872cf40896c7be36b11dcc744620f10adf1d (patch)
tree60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/lkproof
Initial commit
Diffstat (limited to 'macros/latex/contrib/lkproof')
-rw-r--r--macros/latex/contrib/lkproof/lkproof-doc.pdfbin0 -> 256379 bytes
-rw-r--r--macros/latex/contrib/lkproof/lkproof-doc.tex106
-rw-r--r--macros/latex/contrib/lkproof/proof.sty259
-rw-r--r--macros/latex/contrib/lkproof/proofeg.tex143
4 files changed, 508 insertions, 0 deletions
diff --git a/macros/latex/contrib/lkproof/lkproof-doc.pdf b/macros/latex/contrib/lkproof/lkproof-doc.pdf
new file mode 100644
index 0000000000..56afe708b6
--- /dev/null
+++ b/macros/latex/contrib/lkproof/lkproof-doc.pdf
Binary files differ
diff --git a/macros/latex/contrib/lkproof/lkproof-doc.tex b/macros/latex/contrib/lkproof/lkproof-doc.tex
new file mode 100644
index 0000000000..7a134ab413
--- /dev/null
+++ b/macros/latex/contrib/lkproof/lkproof-doc.tex
@@ -0,0 +1,106 @@
+\documentclass[pagesize=auto, fontsize=12pt, DIV=9, parskip=half]{scrartcl}
+
+\usepackage{fixltx2e}
+\usepackage{etex}
+\usepackage{lmodern}
+\usepackage[T1]{fontenc}
+\usepackage{textcomp}
+\usepackage[svgnames]{xcolor}
+\usepackage{proof}
+\usepackage{microtype}
+\usepackage{hyperref}
+
+\newcommand*{\mail}[1]{\href{mailto:#1}{\texttt{#1}}}
+\newcommand*{\pkg}[1]{\textsf{#1}}
+\newcommand*{\cs}[1]{\texttt{\textbackslash#1}}
+\makeatletter
+\newcommand*{\cmd}[1]{\cs{\expandafter\@gobble\string#1}}
+\makeatother
+\newcommand*{\opt}[1]{\texttt{#1}}
+\newcommand*{\meta}[1]{\textlangle\textsl{#1}\textrangle}
+\newcommand*{\marg}[1]{\texttt{\{}\meta{#1}\texttt{\}}}
+\newcommand*{\oarg}[1]{\texttt{[}\meta{#1}\texttt{]}}
+
+\addtokomafont{title}{\rmfamily}
+\addtokomafont{descriptionlabel}{\mdseries}
+
+\title{The \pkg{proof} package\thanks{This manual corresponds to \pkg{proof.sty}~v3.1 (for both \LaTeX\,2.09 and \LaTeXe), dated~Nov 24, 2005.}}
+\subtitle{Proof figure macros}
+\author{Makoto Tatsuta\thanks{\mail{tatsuta@nii.ac.jp}}}
+\date{Nov 24, 2005}
+
+
+\begin{document}
+
+\righthyphenmin=2
+
+\maketitle
+
+\section{Usage:}
+
+In \cmd{\documentstyle}, specify an optional style `\opt{proof}', say,\\
+\verb+\documentstyle[proof]{article}+.
+
+The following macros are available:
+
+In all the following macros, all the arguments such as
+\meta{Lowers} and \meta{Uppers} are processed in math mode.
+%
+\begin{description}
+\item[\cmd{\infer}\marg{Lower}\marg{Uppers}]
+ draws an inference.
+
+ Use \verb+&+ in \meta{Uppers} to delimit upper formulae.
+ \meta{Uppers} consists more than 0 formulae.
+
+ \cmd{\infer} returns \verb+\hbox{ ... }+ or \verb+\vbox{ ... }+ and
+ sets \cmd{\@LeftOffset} and \cmd{\@RightOffset} globally.
+
+\item[\cmd{\infer}\oarg{Label}\marg{Lower}\marg{Uppers}]
+ draws an inference labeled with~\meta{Label}.
+
+\item[\cmd{\infer*}\marg{Lower}\marg{Uppers}]
+ draws a many step deduction.
+
+\item[\cmd{\infer*}\oarg{Label}\marg{Lower}\marg{Uppers}]
+ draws a many step deduction labeled with~\meta{Label}.
+
+\item[\cmd{\infer=}\marg{Lower}\marg{Uppers}]
+ draws a double-ruled deduction.
+
+\item[\cmd{\infer=}\oarg{Label}\marg{Lower}\marg{Uppers}]
+ \begingroup
+ \spaceskip=\fontdimen2\font plus \fontdimen3\font minus 1.2\fontdimen4\font
+ draws a double-ruled deduction labeled with~\meta{Label}.
+ \endgroup
+
+\item[\cmd{\deduce}\marg{Lower}\marg{Uppers}]
+ draws an inference without a rule.
+
+\item[\cmd{\deduce}\oarg{Proof}\marg{Lower}\marg{Uppers}]
+ draws a many step deduction with a proof~name.
+\end{description}
+
+
+\section{Example:}
+
+If you want to write
+
+\medskip
+\infer{E}{
+ A
+ &
+ \infer{D}{B & C}
+}
+
+use
+%
+\begin{verbatim}
+\infer{E}{
+ A
+ &
+ \infer{D}{B & C}
+}
+\end{verbatim}
+
+\end{document}
diff --git a/macros/latex/contrib/lkproof/proof.sty b/macros/latex/contrib/lkproof/proof.sty
new file mode 100644
index 0000000000..c272a8103f
--- /dev/null
+++ b/macros/latex/contrib/lkproof/proof.sty
@@ -0,0 +1,259 @@
+% 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
+}
diff --git a/macros/latex/contrib/lkproof/proofeg.tex b/macros/latex/contrib/lkproof/proofeg.tex
new file mode 100644
index 0000000000..98020e82ee
--- /dev/null
+++ b/macros/latex/contrib/lkproof/proofeg.tex
@@ -0,0 +1,143 @@
+% proofeg.tex (An example file for proof.sty)
+%
+% Mar 6, 1997
+% Makoto Tatsuta
+%
+% I hope you can learn how to use proof figure macros easily
+% by these examples.
+
+\def\imp{\to}
+\def\land{\mathbin\&}
+
+\documentstyle[proof]{article}
+
+% for LaTeX 2e naitive mode.
+%\documentclass[]{article}
+%\usepackage{proof}
+
+\begin{document}
+\section*{Examples of proof.sty}
+
+\verb|\infer| draws beautiful proof figures easily:
+
+\noindent (1)
+$$
+\infer{A}{
+ \infer{B}{
+ B11\land B12\land B13
+ &
+ B21\land B22\land B23
+ }
+ &
+ C
+}
+$$
+
+\noindent (2)
+$$
+\infer{A1\land A2\land A3\land A4\land A5\land A6}{
+ \infer{B}{
+ B11\land B12\land B13
+ &
+ B21\land B22\land B23
+ }
+ &
+ C
+}
+$$
+
+\noindent (3)
+$$
+\infer{A1\land A2\land A3\land A4\land A5\land A6}{
+ C
+ &
+ \infer{B}{
+ B11\land B12\land B13
+ &
+ B21\land B22\land B23
+ }
+}
+$$
+
+You can use also some variations:
+
+\noindent (4)
+$$
+\infer[(1)]{A}{
+ \infer*{B}{
+ B11\land B12\land B13
+ &
+ B21\land B22\land B23
+ }
+ &
+ C
+}
+$$
+
+\noindent (5)
+$$
+\infer*[(1)]{A1\land A2\land A3\land A4\land A5\land A6}{
+ \deduce[{\displaystyle \sum}]{B}{
+ B11\land B12\land B13
+ &
+ B21\land B22\land B23
+ }
+ &
+ \deduce{C}{(2)}
+}
+$$
+
+\noindent (6)
+$$
+\infer={A}{A \land B \land C}
+$$
+
+Here are more practical examples:
+
+\noindent (7)
+$$
+\infer[(\land I)]{A \land B}{A & B}
+\qquad
+\infer[(\land E_l)]A{A\land B}
+\qquad
+\infer[(\land E_r)]B{A\land B}
+$$
+
+$$
+\infer[(\imp I)]{A \imp B}{
+ \infer*{B}{[A]}
+}
+\qquad
+\infer[(\imp E)]{B}{
+ A \imp B
+ &
+ A
+}
+$$
+
+Some techniques:
+Use \verb|\vcenter| for an equation of proofs.
+
+\noindent (8)
+$$
+\pi = \vcenter{
+\infer{E}{
+ A
+ &
+ \infer{D}{B & C}
+}
+}
+$$
+
+Use \verb|\kern| to adjust the form of a proof.
+
+\noindent (9)
+$$
+\infer{E}{
+ A
+ &
+ \infer{D}{B & C} \kern 0.5cm
+}
+$$
+
+\end{document}