diff options
author | Norbert Preining <norbert@preining.info> | 2019-09-02 13:46:59 +0900 |
---|---|---|
committer | Norbert Preining <norbert@preining.info> | 2019-09-02 13:46:59 +0900 |
commit | e0c6872cf40896c7be36b11dcc744620f10adf1d (patch) | |
tree | 60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/lkproof |
Initial commit
Diffstat (limited to 'macros/latex/contrib/lkproof')
-rw-r--r-- | macros/latex/contrib/lkproof/lkproof-doc.pdf | bin | 0 -> 256379 bytes | |||
-rw-r--r-- | macros/latex/contrib/lkproof/lkproof-doc.tex | 106 | ||||
-rw-r--r-- | macros/latex/contrib/lkproof/proof.sty | 259 | ||||
-rw-r--r-- | macros/latex/contrib/lkproof/proofeg.tex | 143 |
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 Binary files differnew file mode 100644 index 0000000000..56afe708b6 --- /dev/null +++ b/macros/latex/contrib/lkproof/lkproof-doc.pdf 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} |