From b7e38f0686232dbecee5d93bdabbdfcbee625610 Mon Sep 17 00:00:00 2001 From: Karl Berry Date: Tue, 2 Jul 2013 23:21:33 +0000 Subject: lplfitch (30jun13) git-svn-id: svn://tug.org/texlive/trunk@31077 c570f23f-e606-0410-a88d-b1316a301751 --- Master/texmf-dist/doc/latex/lplfitch/README | 42 ++ Master/texmf-dist/doc/latex/lplfitch/lplfitch.pdf | Bin 0 -> 226982 bytes .../texmf-dist/source/latex/lplfitch/lplfitch.dtx | 796 +++++++++++++++++++++ .../texmf-dist/source/latex/lplfitch/lplfitch.ins | 59 ++ Master/texmf-dist/tex/latex/lplfitch/lplfitch.sty | 131 ++++ Master/tlpkg/bin/tlpkg-ctan-check | 2 +- Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc | 1 + Master/tlpkg/tlpsrc/lplfitch.tlpsrc | 0 8 files changed, 1030 insertions(+), 1 deletion(-) create mode 100644 Master/texmf-dist/doc/latex/lplfitch/README create mode 100644 Master/texmf-dist/doc/latex/lplfitch/lplfitch.pdf create mode 100644 Master/texmf-dist/source/latex/lplfitch/lplfitch.dtx create mode 100644 Master/texmf-dist/source/latex/lplfitch/lplfitch.ins create mode 100644 Master/texmf-dist/tex/latex/lplfitch/lplfitch.sty create mode 100644 Master/tlpkg/tlpsrc/lplfitch.tlpsrc diff --git a/Master/texmf-dist/doc/latex/lplfitch/README b/Master/texmf-dist/doc/latex/lplfitch/README new file mode 100644 index 00000000000..c89659a03b8 --- /dev/null +++ b/Master/texmf-dist/doc/latex/lplfitch/README @@ -0,0 +1,42 @@ +lplfitch +======== + +LaTeX package for typesetting Fitch-style proofs a la Language, Proof, +and Logic, a logic textbook by Jon Barwise and John Etchemendy. It was +originally written by John Etchemendy, with modifications by +Dave Barker-Plummer and Richard Zach. + +https://github.com/rzach/lplfitch + +Installation +------------ + +Run latex on lplfitch.ins to produce lplfitch.sty + +Run latex on lplfitch.dxt to produce the documentation. + +License +------- + +Copyright 2013 by John Etchemendy, Dave Barker-Plummer, and Richard Zach + +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 Richard Zach. + +This work consists of the files lplfitch.dtx and lplfitch.ins +and the derived files lplfitch.sty and lplfitch.pdf. + +Versions +-------- + +0.9 (2013/05/16) First public beta + diff --git a/Master/texmf-dist/doc/latex/lplfitch/lplfitch.pdf b/Master/texmf-dist/doc/latex/lplfitch/lplfitch.pdf new file mode 100644 index 00000000000..58a7f7ac174 Binary files /dev/null and b/Master/texmf-dist/doc/latex/lplfitch/lplfitch.pdf differ diff --git a/Master/texmf-dist/source/latex/lplfitch/lplfitch.dtx b/Master/texmf-dist/source/latex/lplfitch/lplfitch.dtx new file mode 100644 index 00000000000..e0f8bb4741e --- /dev/null +++ b/Master/texmf-dist/source/latex/lplfitch/lplfitch.dtx @@ -0,0 +1,796 @@ +% \iffalse meta-comment +% +% Copyright (C) 2013 by John Etchemendy, Dave Barker-Plummer, +% and Richard Zach +% ------------------------------------------------------- +% +% 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. +% +% \fi +% +% \iffalse +%<*driver> +\ProvidesFile{lplfitch.dtx} +% +%\NeedsTeXFormat{LaTeX2e}[1999/12/01] +%\ProvidesPackage{lplfitch} +%<*package> + [2013/05/16 v0.9 LPL Fitch style] +% +% +%<*driver> +\documentclass{ltxdoc} +\usepackage{lplfitch}[2013/05/16] +\usepackage{hyperref} +\EnableCrossrefs +\CodelineIndex +\RecordChanges +\begin{document} + \DocInput{lplfitch.dtx} + \PrintChanges + \PrintIndex +\end{document} +% +% \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{v0.1}{Aeons ago}{Initial version} +% \changes{v0.9}{2012/05/16}{First public beta} +% +% \GetFileInfo{lplfitch.dtx} +% +% \DoNotIndex{\newcommand,\newenvironment} +% +% \title{The \textsf{lplfitch} package\thanks{This document +% corresponds to \textsf{lplproof}~\fileversion, dated \filedate.}} +% \author{John Etchemendy \and Dave Barker-Plummer \and Richard Zach} +% +% \maketitle +% +% \section{Introduction} +% +% The package |lplfitch| provides macros for typesetting natural +% deduction proofs in ``Fitch'' style, with subproofs indented and +% offset by scope lines. It produces proofs in the format used in the +% textbook \href{http://lpl.stanford.edu/}{\textit{Language, Proof, +% and Logic}} by Dave Barker-Plummer, Jon Barwise, and John +% Etchemendy. The package was originally written by John +% Etchemendy. The current version incorporates changes by Dave +% Barker-Plummer and Richard Zach. +% +% \section{Fitch Proofs by Example} +% \label{sect:proofs-by-example} +% +% In this section we will describe how to typeset the Fitch-style +% natural deduction proof shown in figure~\ref{fig:example-proof}. +% This proof uses all of the macros that we have developed for +% typesetting proofs and therefore serves as a good illustration. +% +% \begin{figure} +% \fitchprf{}{ +% \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{ +% \subproof{\pline[2.]{\exi{x}{Cube(x)}}}{ +% \boxedsubproof[3.]{a}{Cube(a)}{ +% \pline[4.]{Cube(a)\lif Small(a)}[\lalle{1}]\\ +% \pline[5.]{Small(a)}[\life{4}{3}]\\ +% \pline[6.]{\exi{x}{Small(x)}}[\lexii{5}] +% } +% \pline[7.]{\exi{x}{Small(x)}}[\lexie{2}{3--6}] +% } +% \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}[\lifi{2--7}] +% } +% \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{ +% \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}[\lifi{1--8}] +% } +% \caption{An Example Proof} +% \label{fig:example-proof} +% \end{figure} +% +% The commands for producing this proof are given in +% figure~\ref{fig:proof-eg-cmds}. This proof is a little hard to take +% in all at once, and so in the remainder of this section we will +% describe the development of this proof, which we hope is of use to +% readers. +% +%\begin{figure} +%\begin{verbatim} +% \fitchprf{}{ +% \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{ +% \subproof{\pline[2.]{\exi{x}{Cube(x)}}}{ +% \boxedsubproof[3.]{a}{Cube(a)}{ +% \pline[4.]{Cube(a)\lif Small(a)}[\lalle{1}]\\ +% \pline[5.]{Small(a)}[\life{4}{3}]\\ +% \pline[6.]{\exi{x}{Small(x)}}[\lexii{5}] +% } +% \pline[7.]{\exi{x}{Small(x)}}[\lexie{2}{3--6}] +% } +% \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}[\lifi{2--7}] +% } +% \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{ +% \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}[\lifi{1--8}] +% } +% \end{verbatim} +% \caption{The commands for producing the proof of +% figure~\ref{fig:example-proof}} +% \label{fig:proof-eg-cmds} +% \end{figure} +% +% We recommend developing the commands to typeset a proof from the +% inside out, starting with the most deeply nested subproof. We also +% recommend ignoring justifications until the proof is complete, +% primarily for simplicity but also because the line numbers are not +% known until the complete proof structure is present. +% +% We begin by writing the lines of the innermost subproof (lines 3--6 +% of the main proof). +% +% \begin{quote} +% \begin{tabular}{ll} +% |\pline{Cube(a)}| & \formula{Cube(a)}\\ +% |\pline{Cube(a)\lif Small(a)}| & \formula{Cube(a)\lif Small(a)}\\ +% |\pline{Small(a)}| & \formula{Small(a)}\\ +% |\pline{\exi{x}{Small(x)}}| & \formula{\exi{x}{Small(x)}} +% \end{tabular} +% \end{quote} +% +% The macro |\pline| produces a single line of the proof. The +% mandatory argument to |\pline| is the formula to appear within the +% step. You will notice that we have used the macro |\lif| to produce +% an conditional arrow, and |\exi| to produce an existentially +% quantified formula. These are members of a suite of macros that we +% find convenient for producing formulae. These are described in +% section~\ref{sect:formulae}. +% +% The |\pline| macro may only be used inside a proof context. We +% construct such a context by using the |\fitchprf| macro. This macro +% has two mandatory arguments, corresponding to the premises and the +% body of the proof. Each argument is a list of lines, separated by a +% newline (|\\|) command. We therefore embed the lines of our example +% proof like this: +% +% \begin{verbatim} +% \fitchprf{\pline{Cube(a)}}{ +% \pline{Cube(a) \lif Small(a)}\\ +% \pline{Small(a)}\\ +% \pline{\exi{x}{Small(x)}} +% }\end{verbatim} +% +% Typesetting a document containing this command results in +% the proof: +% \begin{quote} +% \fitchprf{\pline{Cube(a)}}{ +% \pline{Cube(a) \lif Small(a)}\\ +% \pline{Small(a)}\\ +% \pline{\exi{x}{Small(x)}} +% } +% \end{quote} +% +% Our next step is to embed this proof as a subproof within the larger +% proof. This is simply achieved. We first change the use of +% |\fitchprf| to a |\subproof| command, and then treat this as a line +% of the body of another |\fitchprf| command. The result of doing +% this is: +% +% \begin{verbatim} +% \fitchprf{\pline{\exi{x}{Cube(x)}}}{ +% \subproof{\pline{Cube(a)}}{ +% \pline{Cube(a)\lif Small(a)}\\ +% \pline{Small(a)}\\ +% \pline{\exi{x}{Small(x)}} +% } +% \pline{\exi{x}{Small(x)}} +% }\end{verbatim} +% +% \noindent which yields the proof: +% +% \begin{quote} +% \fitchprf{\pline{\exi{x}{Cube(x)}}}{ +% \subproof{\pline{Cube(a)}}{ +% \pline{Cube(a)\lif Small(a)}\\ +% \pline{Small(a)}\\ +% \pline{\exi{x}{Small(x)}} +% } +% \pline{\exi{x}{Small(x)}} +% } +% \end{quote} +% +% \noindent The new outer |\fitchprf| has two elements in the second +% argument, one of which is the subproof that we just wrote and the +% second is a formula. As we embedded the subproof in the body of the +% main proof we changed the command from |\fitchprf| to |\subproof|, +% the definitions of these two macros are almost identical but for the +% adjustment of vertical spacing after the use of a |\subproof| +% command. Note that no |\\| command is required after the use of a +% |\subproof| command. +% +% Two further applications of this technique give us the command: +% +% \begin{verbatim} +% \fitchprf{}{ +% \subproof{\pline{\uni{x}{(Cube(x)\lif Small(x))}}}{ +% \subproof{\pline{\exi{x}{Cube(x)}}}{ +% \subproof{\pline{Cube(a)}}{ +% \pline{Cube(a)\lif Small(a)}\\ +% \pline{Small(a)}\\ +% \pline{\exi{x}{Small(x)}} +% } +% \pline{\exi{x}{Small(x)}} +% } +% \pline{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}} +% } +% \pline{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{ +% \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}} +% } +% \end{verbatim} +% +% \noindent which produces the proof +% +% \begin{quote} +% \fitchprf{}{ +% \subproof{\pline{\uni{x}{(Cube(x)\lif Small(x))}}}{ +% \subproof{\pline{\exi{x}{Cube(x)}}}{ +% \subproof{\pline{Cube(a)}}{ +% \pline{Cube(a)\lif Small(a)}\\ +% \pline{Small(a)}\\ +% \pline{\exi{x}{Small(x)}} +% } +% \pline{\exi{x}{Small(x)}} +% } +% \pline{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}} +% } +% \pline{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{ +% \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}} +% } +% \end{quote} +% +% Notice that the last line contains a long formula, and we have used +% the |\brokenform| command to typeset this formula. The +% |\brokenform| command takes two arguments, the first is the first +% part of the formula, which will be typeset left justified in the +% space available, while the second argument contains the remaining +% pieces of the formula which will appear in subsequent lines. These +% lines should be separated by uses of the |\\| command, and each line +% should (usually) be a |\formula|. These lines will be typeset right +% justified in the available space. +% +% \subsection{Adding Line Numbers} +% +% The |\pline| command takes an optional argument which is the number +% of the line within the proof. We can simply add these now that we +% have all of the lines of the proof. +% +% \begin{verbatim} +% \fitchprf{}{ +% \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{ +% \subproof{\pline[2.]{\exi{x}{Cube(x)}}}{ +% \subproof{\pline[3.]{Cube(a)}}{ +% \pline[4.]{Cube(a)\lif Small(a)}\\ +% \pline[5.]{Small(a)}\\ +% \pline[6.]{\exi{x}{Small(x)}} +% } +% \pline[7.]{\exi{x}{Small(x)}} +% } +% \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}} +% } +% \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{ +% \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}} +% }\end{verbatim} +% \noindent which results in the proof: +% \begin{quote} +% \fitchprf{}{ +% \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{ +% \subproof{\pline[2.]{\exi{x}{Cube(x)}}}{ +% \subproof{\pline[3.]{Cube(a)}}{ +% \pline[4.]{Cube(a)\lif Small(a)}\\ +% \pline[5.]{Small(a)}\\ +% \pline[6.]{\exi{x}{Small(x)}} +% } +% \pline[7.]{\exi{x}{Small(x)}} +% } +% \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}} +% } +% \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{ +% \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}} +% } +% \end{quote} +% +% In the eventual proof, a boxed constant is introduced at line~3. We +% can convert the simple subproof into a boxed subproof. We use the +% |\boxedsubproof| macro to achieve this. The conversion is +% straightforward, we replace the first argument of the |\subproof| +% command which was |{\pline[3.]{Cube(a)}}}| by the three arguments +% |[3.]{a}{Cube(a)}| obtaining +% +% \begin{verbatim} +% \boxedsubproof[3.]{a}{Cube(a)}{ +% \pline[4.]{Cube(a)\lif Small(a)}\\ +% \pline[5.]{Small(a)}\\ +% \pline[6.]{\exi{x}{Small(x)}} +% }\end{verbatim} +% +% \subsection{Adding Justifications} +% +% The final thing that we need to do to complete the desired proof is +% the addition of justifications. To produce a justified line we need +% to then add the optional justification argument. +% +% \begin{verbatim}\pline[5.]{Small(a)}[\ife{4}{3}]\end{verbatim} +% +% \noindent The \verb|\ife| macro produces a justification using the +% $\lif$-elimination rule of the logic. This is one of a suite of +% macros that we developed to produce justifications in a uniform +% manner. These are described in section~\ref{sect:justifications}. +% +% \subsection{Command Reference} +% +% The |\pline| command can be used to typeset proof lines. It takes +% the formula as a mandatory argument, and line number and +% justification as optional arguments: |\pline|\oarg{line +% number}\marg{formula}\oarg{justification}. The variant |\fpline| +% works the same, except it produces a focus slider. In case you want +% to typeset a line in an argument or proof that is not typeset as a +% formula (e.g., plain text), use the |\tline| command. It takes a +% line number as optional argument. +% +% \subsection{Obsolete Commands} +% +% The original version of |lplfitch| set lines of proofs using two +% separate macros, the |\nline| and |\jline| commands. They are +% superceded by the |\pline| command and are included for backward +% compatibility only. +% +% A numbered line is produced by |\nline|, with the optional argument +% the line number. A justified line is produced using the +% \verb|\jline| macro, which has one mandatory and one optional +% argument. The optional argument contains the justification, while +% the mandatory argument must contain {\em all} of the arguments +% previously given to \verb|\nline|. So the command +% +% \begin{verbatim}\nline[5.]{Small(a)}\end{verbatim} +% +% \noindent produces exactly the same output as +% +% \begin{verbatim}\jline{[5.]{Small(a)}}\end{verbatim} +% +% \noindent but notice that both the arguments to \verb|\nline| are +% passed within the single argument to \verb|\jline|. To produce a +% justified line using |\jline|, you would also include the +% justification as an optional argument, say, +% +% \begin{verbatim}\jline{[5.]{Small(a)}}[\life{2}{3}]\end{verbatim} +% +% \section{Logical Formulae} +% \label{sect:formulae} +% +% We set our formulae using sans-serif font and we also need to be in +% math mode because the use of logical connectives. The +% \verb|\formula| command takes a formula to set as its argument, and +% handles both font and mode change. If the LPL convention of sans-serif +% formulas is not desired, you can simly redefine |\formula| as +% \begin{verbatim}\renewcommand{\formula}[1]{\ensuremath{#1}}\end{verbatim} +% +% Many of the commands that follow require that they are used in a +% formula, or math, context. +% +% \subsection{Connectives} +% +% We introduce our own (usually) shorter names for logical +% connectives. All of these commands require a formula context. +% +% \begin{center} +% \begin{tabular}{lc} +% \bf Usage & \bf Output\\ +% \hline\\ +% \verb|\land| & \formula{\land}\\ +% \verb|\lor| & \formula{\lor}\\ +% \verb|\lif| & \formula{\lif}\\ +% \verb|\liff| & \formula{\liff}\\ +% \verb|\lnot| & \formula{\lnot}\\ +% \verb|\lfalse| & \formula{\lfalse}\\ +% \verb|\lall| & \formula{\lall}\\ +% \verb|\lis| & \formula{\lis} +% \end{tabular} +% \end{center} +% +% \subsection{Quantified Formulae} +% +% So that we don't have to think about spacing when setting quantified +% formulae, we defined the commands |\exi| and |\uni|. Use +% |\exi{x}{P(x)}| to obtain \formula{\exi{x}{P(x)}}, and +% |\uni{x}{\exi{y}{(P(x)\lif Q(x,y))}}| for +% \formula{\uni{x}{\exi{y}{(P(x)\lif Q(x,y))}}}, for example. |\exi| +% and |\uni| require a formula context. +% +% \section{Justifications} +% \label{sect:justifications} +% +% Here are the macros that we have developed to typeset justifications +% within a proof. These do not require a formula context. +% +% \begin{center} +% \begin{tabular}{ll} +% \bf Usage & \bf Output\\ +% \hline\\ +% |\landi{2, 3}| &\landi{2, 3}\\ +% |\lande{4}|&\lande{4}\\ +% |\lori{5}| & \lori{5}\\ +% |\lore{6}{7--9}{11--13}| &\lore{6}{7--9}{11--13}\\ +% |\lnoti{14--15}| &\lnoti{14-15}\\ +% |\lnote{16}| &\lnote{16}\\ +% |\lfalsei{17}{19}| &\lfalsei{17}{19}\\ +% |\lfalsee{20}|&\lfalsee{20}\\ +% |\lifi{21--25}| &\lifi{21--25}\\ +% |\life{27}{30}| &\life{27}{30}\\ +% |\liffi{33--37}{40-50}|&\liffi{33--37}{40--50}\\ +% |\liffe{55}{57}| &\liffe{55}{57}\\ +% |\reit{4}|&\reit{4}\\ +% |\eqi| &\eqi\\ +% |\eqe{7}{11}|&\eqe{7}{11}\\ +% |\lalli{9--12}|&\lalli{9--12}\\ +% |\lalle{13}|&\lalle{13}\\ +% |\lexii{15}| &\lexii{15}\\ +% |\lexie{17}{18-30}| &\lexie{17}{18--30}\\ +% \end{tabular} +% \end{center} +% +% \section{Other Macros} +% \label{sect:other-macros} +% +% \subsection{Arguments} +% +% When you want to typeset an argument, for example when setting an +% exercise requiring the proof of some conclusion from a collection of +% premises, you should use the |\fitcharg| command. This command +% takes two arguments, both mandatory, the premise lines which are set +% above the Fitch bar, and the conclusion lines, which go below. +% Here's an example. The argument +% +%\begin{quote} +% \fitcharg{\formula{P(a)}\\ \formula{Q(a)}}{\formula{S(a)}} +%\end{quote} +% +%\noindent is typeset by the command: +%\begin{verbatim}\fitcharg{ +% \formula{P(a)}\\ +% \formula{Q(a)} +% }{ +% \formula{S(a)} +% }\end{verbatim} +% \noindent Notice that multiple lines are separated by a use of the +% \LaTeX\ command |\\|. +% +% \subsection{Fitch Contexts} +% +% The |\fitchctx| command is used for setting proof fragments which do +% not include the horizontal Fitch bar. We use these, for example, +% when formally describing the inference rules of our logic. The +% command below, for example, typesets our description of the rule of +% conditional proof. +% +% Notice here that we use the command |\ellipsesline| to produce a +% line of the ``proof'' containing a vertical ellipses (using the +% |\pline{\vdots}| results in the ellipses not being centered on the +% line). +% +% Another new feature of this situation is the use of the |\fpline| +% command. This command works just like the |\pline| command and +% produces exactly what the |\pline| command would, except that a +% focus slider appears to the left of the Fitch bar in question. The +% |\fpline| command does not work in the argument lines of +% |\fitchprf| or |\fitcharg|. +% +% \begin{verbatim} +% \fitchctx{ +% \subproof{\pline[$n$.]{P}}{ +% \ellipsesline\\ +% \pline[$m$.]{Q} +% } +% \fpline{P \lif Q}[\lifi{$n$--$m$}] +% } +% \end{verbatim} +% +% \begin{quote} +% \fitchctx{ +% \subproof{\pline[$n$.]{P}}{ +% \ellipsesline\\ +% \pline[$m$.]{Q} +% } +% \fpline{P \lif Q}[\lifi{$n$--$m$}] +% } +% \end{quote} +% +% \section{Other Packages} +% +% Two other \LaTeX{} packages provide functionality to typeset +% Fitch-style proofs. They differ from |lplfitch| in that they set the +% line numbers close to the left edge of the proof, while |lplfitch| +% sets them close to the formula. Another difference is that subroofs +% can easily be copied and work the same regardless of the depth of +% nesting. +% +% Peter Selinger's package is +% available at +%\begin{quote} +% \href{http://www.mathstat.dal.ca/~selinger/fitch/}{|http://www.mathstat.dal.ca/\~{ +% }selinger/fitch/|}, +% \end{quote} +% and that by Johan Kl\"uwer at +% \begin{quote} +% \href{http://folk.uio.no/johanw/FitchSty.html}{|http://folk.uio.no/johanw/FitchSty.html|}. +% \end{quote} +% +% \StopEventually{} +% +% \section{Implementation} +% +% \begin{macrocode} +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{lplfitch}[2013/05/07 -- Fitch Proofs a la LPL] +% \end{macrocode} +% +% \begin{macro}{\formula} +% Typesets a formula (in math mode, letters typeset in sans-serif as in LPL +% \begin{macrocode} +\newcommand*{\formula}[1]{\ensuremath{\sf{#1}}} +% \end{macrocode} +% \end{macro} +% +% \subsection{Connectives and Quantifiers} +% We provide convenient and short commands for logical symbols. +% \begin{macrocode} +\newcommand*\lif{\rightarrow} +\newcommand*\liff{\leftrightarrow} +\newcommand*\lfalse{\bot} +\newcommand*\lall{\forall} +\newcommand*\lis{\exists} +% \end{macrocode} +% The following provide for commands for setting quantified formulae, inserting correct space +% between variable and formula. It can be redifined using |\renewcommand| if you want to use them but +% want quantifiers set differently (e.g., with parentheses) +% \begin{macrocode} +\newcommand*{\quant}[3]{#1 #2\;#3} +\newcommand*{\exi}[2]{\quant{\lis}{#1}{#2}} +\newcommand*{\uni}[2]{\quant{\lall}{#1}{#2}} +% \end{macrocode} +% \subsection{Justifications} +% +% The folowing commands are used to generate justifications, e.g., +% |\landi{1, 2}| produces ``\landi{1, 2}''. +% \begin{macrocode} +\newcommand*\intro[1]{\formula{#1\,}{\bf Intro:}} +\newcommand*\elim[1]{\formula{#1\,}{\bf Elim:}} + +\newcommand*\landi[1]{\intro{\land} #1} +\newcommand*\lande[1]{\elim{\land} #1} +\newcommand*\lori[1]{\intro{\lor} #1} +\newcommand*\lore[3]{\elim{\lor} #1, #2, #3} +\newcommand*\lnoti[1]{\intro{\lnot} #1} +\newcommand*\lnote[1]{\elim{\lnot} #1} + +\newcommand*\lfalsei[2]{\intro{\lfalse} #1, #2} +\newcommand*\lfalsee[1]{\elim{\lfalse} #1} + +\newcommand*\lifi[1]{\intro{\lif} #1} +\newcommand*\life[2]{\elim{\lif} #1, #2} + +\newcommand*\liffi[2]{\intro{\liff} #1, #2} +\newcommand*\liffe[2]{\elim{\liff} #1, #2} + +\newcommand*\reit[1]{{\bf Reit:} #1} + +\newcommand*\eqi[0]{$=\,${\bf Intro}} +\newcommand*\eqe[2]{\elim{=} #1, #2} + +\newcommand*\lalli[1]{\intro{\lall} #1} +\newcommand*\lalle[1]{\elim{\lall} #1} + +\newcommand*\lexii[1]{\intro{\lis} #1} +\newcommand*\lexie[2]{\elim{\lis} #1, #2} +% \end{macrocode} +% +% \subsection{Dimensions} +% +% The following dimensions can be redefined with |\setlength| +% +% \begin{macro}{\fitchargwidth} +% Width of formulas in arguments +% \begin{macrocode} +\newlength{\fitchargwidth} +\setlength{\fitchargwidth}{3.5in} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\fitchprfwidth} +% Width of formulas in proofs +% \begin{macrocode} +\newlength{\fitchprfwidth} +\setlength{\fitchprfwidth}{3.0in} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\fitchctxwidth} +% Width of formulas in Fitch contexts +% \begin{macrocode} +\newlength{\fitchctxwidth} +\setlength{\fitchctxwidth}{1in} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\fitchsep} +% Distance between scope line and formula +% \begin{macrocode} +\newlength{\fitchsep} +\setlength{\fitchsep}{10pt} +% \end{macrocode} +% \end{macro} +% +% \subsection{Contexts, Arguments, Proofs} +% +% \begin{macro}{\fitchctx} Typesets a Fitch context, e.g., specification of +% a rule, in which a focus slider is typeset to the left of the conclusion +% \begin{macrocode} +\newcommand{\fitchctx}[1]{% + \advance \fitchctxwidth by -\fitchsep% + \advance \fitchctxwidth by .5pt% + \begin{tabular}[t]{r@{}|p{\fitchctxwidth}@{}l} + \phantom{\slider} \\[-1.75ex] + #1 \\[-1.75ex] & & + \end{tabular} + \advance \fitchctxwidth by \fitchsep% + \advance \fitchctxwidth by -.5pt% +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\fitchprf} Typesets a fitch proof +% \begin{macrocode} +\newcommand{\fitchprf}[2]{% + \advance \fitchprfwidth by -\fitchsep% + \advance \fitchprfwidth by .5pt% + \hspace*{.35em}% + \begin{tabular}[t]{|p{0pt}@{}p{\fitchprfwidth}@{\hspace*{\fitchsep}}l} + \multicolumn{3}{@{}l@{}}{\ }\\[-2.35ex] + #1 \\ + \ \\[-2.5ex] \cline{1-1}\\[-2ex] + #2 \\ \multicolumn{3}{@{}l@{}} \ \\[-2.35ex] + \end{tabular} + \advance \fitchprfwidth by \fitchsep% +} +% \end{macrocode} +% \end{macro} +% \begin{macro}{\fitcharg} Typesets an argument (without line +% numbers). Takes two arguments, the premises and conclusion lines of +% the argument. +% \begin{macrocode} +\newcommand{\fitcharg}[2]{ + \advance \fitchargwidth by -\fitchsep% + \hspace*{.35em} + \begin{tabular}[t]{|p{\fitchsep}@{}p{\fitchargwidth}@{}} + \multicolumn{2}{@{}l@{}}{\ }\\[-2.35ex] + #1 \\ + \ \\[-2.5ex] \cline{1-1}\\[-2ex] + #2 \\ \multicolumn{2}{@{}l@{}} \ \\[-2.35ex] + \end{tabular} +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\slider} Typesets the focus arrow. +% \begin{macrocode} +\newcommand*{\slider}{\mbox{$\triangleright \;$}} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\pline} Typesets a proof line with an optional line +% number (before the formula argument) and an optional justification +% (after the formula argument) +% \begin{macrocode} +\def\pline{\@ifnextchar[\@plinenum{\@plinenum[\@empty]}} +\def\@plinenum[#1]#2{\@ifnextchar[{\@plinex{#1}{#2}}{% + \@plinex{#1}{#2}[\@empty]}} +\def\@plinex#1#2[#3]{ & #1\formula{\; #2} & #3} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\fpline} Like |pline| except produces a focus slider +% on the left +% \begin{macrocode} +\newcommand*\fpline{\slider\pline} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\tline} Typesets proof line containing text with an +% optional line number. +% \begin{macrocode} +\newcommand*{\tline}[2][{}]{ & #1\hspace{.6em}{#2}} +% \end{macrocode} +% \end{macro} +% +% The following macros |\nline|, |\jline|, and |\fline| +% are the commands provided in the original version +% of |lplfitch| and are included for backwards compatibility. +% \begin{macrocode} +\newcommand*{\nline}[2][{}]{ & #1\formula{\;#2}} +% \end{macrocode} +% justified line (justification optional) +% |\jline[justification]{args for line}| +% \begin{macrocode} +\newcommand*{\jline}[2][{}]{\nline#2 & #1} +% \end{macrocode} +% focused line +% \begin{macrocode} +\newcommand*{\fline}[1]{\slider \jline#1} +% \end{macrocode} +% +% \begin{macro}{\ellipsesline} +% Producing vertical ellipses in a line on their own. +% This takes care of centering the ellipses in their line. +% \begin{macrocode} +\newcommand*{\ellipsesline}[0]{\nline{\;\raise.65ex\hbox{\vdots}}} +% \end{macrocode} +% \end{macro} +% \begin{macro}{\subproof} +% This command sets a subproof within a proof. +% The arguments are the line before, and the lines after +% the horizontal fitch bar. +% \begin{macrocode} +\newcommand{\subproof}[2]{&\fitchprf{#1}{#2}\\} +% \end{macrocode} +% \end{macro} +% \begin{macro}{\boxedsubproof} +% Produces a new boxed subproof. +% |\boxedsubproof|\oarg{n}\marg{c}\marg{premise}\marg{body}, where +% \meta{n} is the number of the premise line, \meta{c} is the +% constant(s) to be boxed, \meta{premise} is the premise of the +% subproof, and \meta{body} contains the lines of the subproof. +% \begin{macrocode} +\newcommand{\boxedsubproof}[4][{}]{ + \subproof{\nline[#1]{\fbox{\formula{#2}}\;#3}}{#4} +} +% \end{macrocode} +% \end{macro} +% \begin{macro}{\brokenform} +% A crude attempt at dealing with a formula which need to be broken to +% fit in the proof. We take two arguments, the first line of the +% formula which is left justified, and the remainder of the lines, +% which are right justified. The first argument is set as a +% |\formula| but the second is not (as it may contain line breaks +% itself). +% \begin{macrocode} +\newcommand{\brokenform}[2]{ + \advance\fitchprfwidth by-\fitchsep + \begin{tabular}[c]{rp{\fitchprfwidth}} + \multicolumn{1}{p{\fitchprfwidth}@{}}{\formula{#1}}\\ + \formula{#2} + \end{tabular} + \advance\fitchprfwidth by\fitchsep +} +% \end{macrocode} +% \end{macro} +% +% \Finale +\endinput diff --git a/Master/texmf-dist/source/latex/lplfitch/lplfitch.ins b/Master/texmf-dist/source/latex/lplfitch/lplfitch.ins new file mode 100644 index 00000000000..5de9a57126c --- /dev/null +++ b/Master/texmf-dist/source/latex/lplfitch/lplfitch.ins @@ -0,0 +1,59 @@ +%% +%% Copyright (C) 2013 by Dave Barker-Plummer and Richard Zach +%% +%% This file may be distributed and/or modified under the conditions of +%% the LaTeX Project Public License, either version 1.2 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.2 or later is part of all distributions of LaTeX version +%% 1999/12/01 or later. +%% + +\input docstrip.tex +\keepsilent + +\usedir{tex/latex/lplfitch} + +\preamble + +This is a generated file. + +Copyright (C) 2013 by John Etchemendy, Dave Barker-Plummer and Richard Zach + +This file may be distributed and/or modified under the conditions of +the LaTeX Project Public License, either version 1.2 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.2 or later is part of all distributions of LaTeX version +1999/12/01 or later. + +\endpreamble + +\generate{\file{lplfitch.sty}{\from{lplfitch.dtx}{package}}} + +\obeyspaces +\Msg{*************************************************************} +\Msg{* *} +\Msg{* To finish the installation you have to move the following *} +\Msg{* file into a directory searched by TeX: *} +\Msg{* *} +\Msg{* lplfitch.sty *} +\Msg{* *} +\Msg{* To produce the documentation, do *} +\Msg{* *} +\Msg{* pdflatex lplfitch.dtx *} +\Msg{* makeindex -s gglo.ist -o lplfitch.gls lplfitch.glo *} +\Msg{* pdflatex lplfitch.dtx *} +\Msg{* pdflatex lplfitch.dtx *} +\Msg{* *} +\Msg{* Happy TeXing! *} +\Msg{* *} +\Msg{*************************************************************} + +\endbatchfile diff --git a/Master/texmf-dist/tex/latex/lplfitch/lplfitch.sty b/Master/texmf-dist/tex/latex/lplfitch/lplfitch.sty new file mode 100644 index 00000000000..1ca3f348de3 --- /dev/null +++ b/Master/texmf-dist/tex/latex/lplfitch/lplfitch.sty @@ -0,0 +1,131 @@ +%% +%% This is file `lplfitch.sty', +%% generated with the docstrip utility. +%% +%% The original source files were: +%% +%% lplfitch.dtx (with options: `package') +%% +%% This is a generated file. +%% +%% Copyright (C) 2013 by John Etchemendy, Dave Barker-Plummer and Richard Zach +%% +%% This file may be distributed and/or modified under the conditions of +%% the LaTeX Project Public License, either version 1.2 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.2 or later is part of all distributions of LaTeX version +%% 1999/12/01 or later. +%% +\NeedsTeXFormat{LaTeX2e}[1999/12/01] +\ProvidesPackage{lplfitch} + [2013/05/16 v0.9 LPL Fitch style] +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{lplfitch}[2013/05/07 -- Fitch Proofs a la LPL] +\newcommand*{\formula}[1]{\ensuremath{\sf{#1}}} +\newcommand*\lif{\rightarrow} +\newcommand*\liff{\leftrightarrow} +\newcommand*\lfalse{\bot} +\newcommand*\lall{\forall} +\newcommand*\lis{\exists} +\newcommand*{\quant}[3]{#1 #2\;#3} +\newcommand*{\exi}[2]{\quant{\lis}{#1}{#2}} +\newcommand*{\uni}[2]{\quant{\lall}{#1}{#2}} +\newcommand*\intro[1]{\formula{#1\,}{\bf Intro:}} +\newcommand*\elim[1]{\formula{#1\,}{\bf Elim:}} + +\newcommand*\landi[1]{\intro{\land} #1} +\newcommand*\lande[1]{\elim{\land} #1} +\newcommand*\lori[1]{\intro{\lor} #1} +\newcommand*\lore[3]{\elim{\lor} #1, #2, #3} +\newcommand*\lnoti[1]{\intro{\lnot} #1} +\newcommand*\lnote[1]{\elim{\lnot} #1} + +\newcommand*\lfalsei[2]{\intro{\lfalse} #1, #2} +\newcommand*\lfalsee[1]{\elim{\lfalse} #1} + +\newcommand*\lifi[1]{\intro{\lif} #1} +\newcommand*\life[2]{\elim{\lif} #1, #2} + +\newcommand*\liffi[2]{\intro{\liff} #1, #2} +\newcommand*\liffe[2]{\elim{\liff} #1, #2} + +\newcommand*\reit[1]{{\bf Reit:} #1} + +\newcommand*\eqi[0]{$=\,${\bf Intro}} +\newcommand*\eqe[2]{\elim{=} #1, #2} + +\newcommand*\lalli[1]{\intro{\lall} #1} +\newcommand*\lalle[1]{\elim{\lall} #1} + +\newcommand*\lexii[1]{\intro{\lis} #1} +\newcommand*\lexie[2]{\elim{\lis} #1, #2} +\newlength{\fitchargwidth} +\setlength{\fitchargwidth}{3.5in} +\newlength{\fitchprfwidth} +\setlength{\fitchprfwidth}{3.0in} +\newlength{\fitchctxwidth} +\setlength{\fitchctxwidth}{1in} +\newlength{\fitchsep} +\setlength{\fitchsep}{10pt} +\newcommand{\fitchctx}[1]{% +\advance \fitchctxwidth by -\fitchsep% +\advance \fitchctxwidth by .5pt% +\begin{tabular}[t]{r@{}|p{\fitchctxwidth}@{}l} + \phantom{\slider} \\[-1.75ex] + #1 \\[-1.75ex] & & + \end{tabular} +\advance \fitchctxwidth by \fitchsep% +\advance \fitchctxwidth by -.5pt% +} +\newcommand{\fitchprf}[2]{% +\advance \fitchprfwidth by -\fitchsep% +\advance \fitchprfwidth by .5pt% +\hspace*{.35em}% +\begin{tabular}[t]{|p{0pt}@{}p{\fitchprfwidth}@{\hspace*{\fitchsep}}l} + \multicolumn{3}{@{}l@{}}{\ }\\[-2.35ex] + #1 \\ + \ \\[-2.5ex] \cline{1-1}\\[-2ex] + #2 \\ \multicolumn{3}{@{}l@{}} \ \\[-2.35ex] + \end{tabular} +\advance \fitchprfwidth by \fitchsep% +} +\newcommand{\fitcharg}[2]{ +\advance \fitchargwidth by -\fitchsep% +\hspace*{.35em} +\begin{tabular}[t]{|p{\fitchsep}@{}p{\fitchargwidth}@{}} +\multicolumn{2}{@{}l@{}}{\ }\\[-2.35ex] +#1 \\ +\ \\[-2.5ex] \cline{1-1}\\[-2ex] + #2 \\ \multicolumn{2}{@{}l@{}} \ \\[-2.35ex] +\end{tabular} +} +\newcommand*{\slider}{\mbox{$\triangleright \;$}} +\def\pline{\@ifnextchar[\@plinenum{\@plinenum[\@empty]}} +\def\@plinenum[#1]#2{\@ifnextchar[{\@plinex{#1}{#2}}{% + \@plinex{#1}{#2}[\@empty]}} +\def\@plinex#1#2[#3]{ & #1\formula{\; #2} & #3} +\newcommand*\fpline{\slider\pline} +\newcommand*{\tline}[2][{}]{ & #1\hspace{.6em}{#2}} +\newcommand*{\nline}[2][{}]{ & #1\formula{\;#2}} +\newcommand*{\jline}[2][{}]{\nline#2 & #1} +\newcommand*{\fline}[1]{\slider \jline#1} +\newcommand*{\ellipsesline}[0]{\nline{\;\raise.65ex\hbox{\vdots}}} +\newcommand{\subproof}[2]{&\fitchprf{#1}{#2}\\} +\newcommand{\boxedsubproof}[4][{}]{ + \subproof{\nline[#1]{\fbox{\formula{#2}}\;#3}}{#4} +} +\newcommand{\brokenform}[2]{ + \advance\fitchprfwidth by-\fitchsep + \begin{tabular}[c]{rp{\fitchprfwidth}} + \multicolumn{1}{p{\fitchprfwidth}@{}}{\formula{#1}}\\ + \formula{#2} + \end{tabular} + \advance\fitchprfwidth by\fitchsep +} +\endinput +%% +%% End of file `lplfitch.sty'. diff --git a/Master/tlpkg/bin/tlpkg-ctan-check b/Master/tlpkg/bin/tlpkg-ctan-check index ffc64cf8612..94e952982af 100755 --- a/Master/tlpkg/bin/tlpkg-ctan-check +++ b/Master/tlpkg/bin/tlpkg-ctan-check @@ -272,7 +272,7 @@ my @TLP_working = qw( listbib listing listings listings-ext listliketab listofsymbols lithuanian liturg lkproof lm lm-math lmake locality localloc logbox logical-markup-utils logicpuzzle logpap logreq - longnamefilelist loops lpic lps lsc + longnamefilelist loops lpic lplfitch lps lsc lshort-bulgarian lshort-chinese lshort-czech lshort-dutch lshort-english lshort-finnish lshort-french lshort-german lshort-italian lshort-japanese lshort-korean lshort-mongol lshort-persian diff --git a/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc b/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc index 0932966fb4f..9e74d6d7072 100644 --- a/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc +++ b/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc @@ -23,6 +23,7 @@ depend faktor depend interval depend ionumbers depend isomath +depend lplfitch depend mathcomp depend mattens depend mhequ diff --git a/Master/tlpkg/tlpsrc/lplfitch.tlpsrc b/Master/tlpkg/tlpsrc/lplfitch.tlpsrc new file mode 100644 index 00000000000..e69de29bb2d -- cgit v1.2.3