From a23fbfe84a06e48728abe08d57b2c75ab80c054e Mon Sep 17 00:00:00 2001 From: Richard Zach Date: Sun, 17 Dec 2023 18:51:12 +0100 Subject: [PATCH] finalize v1.0 --- fitch.hacker.txt | 256 +++++++++++++++++++++++------------------------ fitch.sty | 18 ++-- fitchdoc.tex | 80 +++++++++------ 3 files changed, 189 insertions(+), 165 deletions(-) diff --git a/fitch.hacker.txt b/fitch.hacker.txt index df4af5c..9649a7b 100644 --- a/fitch.hacker.txt +++ b/fitch.hacker.txt @@ -5,7 +5,7 @@ which is provided in the file fitchdoc.tex. GENERAL -Global identifiers defined by this package start with '\nd*'. The only +Global identifiers defined by this package start with '\nd@'. The only exceptions are \ndref, \nddim, \ndindent, and the "nd" and "ndresume" latex environments. @@ -22,36 +22,36 @@ REFERENCES We start with some macros to facilitate automatic line numbering, and for referencing of lines by labels. The macros defined here are: -\nd*reset to reset the line number count. \nd*num{x}, to generate the -next line number and store it in reference x; \nd*ref{x} to print the +\nd@reset to reset the line number count. \nd@num{x}, to generate the +next line number and store it in reference x; \nd@ref{x} to print the line number referenced by x, \ndref{xxx} to parse a list of references, separated by commas, periods, and hyphens, and translate all references to line numbers. Note: \ndref ignores spaces in its argument, but puts a space after each comma or period in the -output. Also note: \nd*ref can be useful outside a natded environment, +output. Also note: \nd@ref can be useful outside a natded environment, and thus it has a user accessible name. Most general ``line numbers'' actually consist of a name (such as ``n'') and a number (such as -``2''), to produce output such as $n+2$. \nd*set{n}{m} is called to +``2''), to produce output such as $n+2$. \nd@set{n}{m} is called to set the letter to n and the number to m. As special cases, if the second argument is empty, it is not set, and if the first argument is \relax, it is not set. Example for references: -\nd*reset \nd*num{x}; \nd*num{y}; \nd*numopt{n+1}{z}; \nd*num{zz}; -\nd*ref{y}; \ndref{x, y-zz, z} +\nd@reset \nd@num{x}; \nd@num{y}; \nd@numopt{n+1}{z}; \nd@num{zz}; +\nd@ref{y}; \ndref{x, y-zz, z} will produce: 1; 2; n+1; 3; 2; 1, 2-3, n+1 LAYER A Layer A provides primitive picture elements which can be combined into -natural deduction derivations. These are: \nd*t to make a topmost -vertical line segment; \nd*v to make a continuation vertical line -segment, \nd*i to produce the indentation for a subproof, \nd*s to +natural deduction derivations. These are: \nd@t to make a topmost +vertical line segment; \nd@v to make a continuation vertical line +segment, \nd@i to produce the indentation for a subproof, \nd@s to produce the horizontal space between a vertical line and a formula, -\nd*u{x} to underline x with appropriate spacing for a -hypothesis. \nd*f{x} typesets the formula x with the appropriate -vertical spacing. \nd*g{x} is like \nd*i, except it puts a guard in +\nd@u{x} to underline x with appropriate spacing for a +hypothesis. \nd@f{x} typesets the formula x with the appropriate +vertical spacing. \nd@g{x} is like \nd@i, except it puts a guard in the space it creates. These elements are spaced so that they are appropriate as left-aligned array entries. Line numberings and justifications must be provided manually in this layer. All explicit @@ -62,91 +62,91 @@ Example of a derivation using layer A syntax: \[ \begin{array}{lll} - 1 & \nd*t\nd*s\nd*f {P\vee Q} \\ - 2 & \nd*v\nd*s\nd*u {\neg Q} \\ - 3 & \nd*v\nd*i\nd*t\nd*s\nd*u {P} \\ - 4 & \nd*v\nd*i\nd*v\nd*s\nd*f {P} & \mbox{by 3} \\ - 5 & \nd*v\nd*i\nd*t\nd*s\nd*u {Q} \\ - 6 & \nd*v\nd*i\nd*v\nd*s\nd*f {\neg Q} & \mbox{by 2} \\ - 7 & \nd*v\nd*i\nd*v\nd*s\nd*f {\bot} & \mbox{by 5, 6} \\ - 8 & \nd*v\nd*i\nd*v\nd*s\nd*f {P} & \mbox{by 7} \\ - 9 & \nd*v\nd*s\nd*f {P} & \mbox{by 1, 3-4, 5-8} \\ + 1 & \nd@t\nd@s\nd@f {P\vee Q} \\ + 2 & \nd@v\nd@s\nd@u {\neg Q} \\ + 3 & \nd@v\nd@i\nd@t\nd@s\nd@u {P} \\ + 4 & \nd@v\nd@i\nd@v\nd@s\nd@f {P} & \mbox{by 3} \\ + 5 & \nd@v\nd@i\nd@t\nd@s\nd@u {Q} \\ + 6 & \nd@v\nd@i\nd@v\nd@s\nd@f {\neg Q} & \mbox{by 2} \\ + 7 & \nd@v\nd@i\nd@v\nd@s\nd@f {\bot} & \mbox{by 5, 6} \\ + 8 & \nd@v\nd@i\nd@v\nd@s\nd@f {P} & \mbox{by 7} \\ + 9 & \nd@v\nd@s\nd@f {P} & \mbox{by 1, 3-4, 5-8} \\ \end{array} \] LISTS This is a bit of a hack. We implement linked lists as follows: a list -is either \nd*nil, or \nd*cons{T}{H}, where T is another list, and H +is either \nd@nil, or \nd@cons{T}{H}, where T is another list, and H is some arbitrary code. Note that lists grow to the right. The following macros operate on a list that is stored in a macro \list. -\nd*push\list{item} pushes the item onto the list -\nd*pop\list{item} pops and discards the last item from the list -\nd*item\list{command} applies command to each element of the list -\nd*modify\list\n{elt} modifies the \n-th element of the +\nd@push\list{item} pushes the item onto the list +\nd@pop\list{item} pops and discards the last item from the list +\nd@item\list{command} applies command to each element of the list +\nd@modify\list\n{elt} modifies the \n-th element of the list, if there is such an element. Here \n is a counter. Elements are counted from the right, starting from 1. -We use lists of items of the forms \nd*t, \nd*v, \nd*i, and \nd*g{...} +We use lists of items of the forms \nd@t, \nd@v, \nd@i, and \nd@g{...} to represent the current indentation level and format (see Layer A, -above). The function \nd*cont computes the indentation for the -following line by replacing all items of the form \nd*t by \nd*v and -\nd*g{...} by \nd*i. +above). The function \nd@cont computes the indentation for the +following line by replacing all items of the form \nd@t by \nd@v and +\nd@g{...} by \nd@i. With the list syntax, a derivation can be expressed like this: \[ \begin{array}{lll} - \gdef\stack{\nd*nil} + \gdef\stack{\nd@nil} \newcount\n - \nd*push\stack{\nd*t} - 1 & \nd*iter\stack\relax\nd*s\nd*u {\neg\exists xP(x)} \\ - \nd*cont\stack - \nd*push\stack{\nd*i} - \nd*push\stack{\nd*t} - \nd*n=2\nd*modify\stack\n{\nd*g{u}} - \nd*push\stack{\nd*i} - \nd*push\stack{\nd*t} - 2 & \nd*iter\stack\relax\nd*s\nd*u {P(u)} \\ - \nd*cont\stack - 3 & \nd*iter\stack\relax\nd*s\nd*f {\exists xP(x)} \\ - \nd*cont\stack - 4 & \nd*iter\stack\relax\nd*s\nd*f {\neg\exists xP(x)} \\ - \nd*cont\stack - 5 & \nd*iter\stack\relax\nd*s\nd*f {\bot} \\ - \nd*cont\stack - \nd*pop\stack - \nd*pop\stack - 6 & \nd*iter\stack\relax\nd*s\nd*f {\neg P(u)} \\ - \nd*cont\stack - \nd*pop\stack - \nd*pop\stack - 7 & \nd*iter\stack\relax\nd*s\nd*f {\forall y\neg P(y)} \\ - \nd*cont\stack + \nd@push\stack{\nd@t} + 1 & \nd@iter\stack\relax\nd@s\nd@u {\neg\exists xP(x)} \\ + \nd@cont\stack + \nd@push\stack{\nd@i} + \nd@push\stack{\nd@t} + \nd@n=2\nd@modify\stack\n{\nd@g{u}} + \nd@push\stack{\nd@i} + \nd@push\stack{\nd@t} + 2 & \nd@iter\stack\relax\nd@s\nd@u {P(u)} \\ + \nd@cont\stack + 3 & \nd@iter\stack\relax\nd@s\nd@f {\exists xP(x)} \\ + \nd@cont\stack + 4 & \nd@iter\stack\relax\nd@s\nd@f {\neg\exists xP(x)} \\ + \nd@cont\stack + 5 & \nd@iter\stack\relax\nd@s\nd@f {\bot} \\ + \nd@cont\stack + \nd@pop\stack + \nd@pop\stack + 6 & \nd@iter\stack\relax\nd@s\nd@f {\neg P(u)} \\ + \nd@cont\stack + \nd@pop\stack + \nd@pop\stack + 7 & \nd@iter\stack\relax\nd@s\nd@f {\forall y\neg P(y)} \\ + \nd@cont\stack \end{array} \] LAYER B Layer B is simply a wrapper around layer A. It provides commands -\nd*beginb, \nd*resumeb, \nd*endb, \nd*openb, \nd*closeb, \nd*guardb, -\nd*hypob, and \nd*haveb which abstract from the layer A +\nd@beginb, \nd@resumeb, \nd@endb, \nd@openb, \nd@closeb, \nd@guardb, +\nd@hypob, and \nd@haveb which abstract from the layer A primitives. This includes automatic line numbering, and automatic -indentation. \nd*hypocontb and \nd*havecontb are like \nd*hypob and -\nd*haveb, except that they introduce continuation lines that are -slightly indented and have no line number/label. \nd*beginb and -\nd*endb enclose a natural deduction in layer B syntax. \nd*resumeb is -like \nd*beginb, except that it resumes a deduction in progress (for -instance, after a manual page break). \nd*openb and \nd*closeb open, -respectively close, a subproof. \nd*guardb{n}{g} adds the guard g to +indentation. \nd@hypocontb and \nd@havecontb are like \nd@hypob and +\nd@haveb, except that they introduce continuation lines that are +slightly indented and have no line number/label. \nd@beginb and +\nd@endb enclose a natural deduction in layer B syntax. \nd@resumeb is +like \nd@beginb, except that it resumes a deduction in progress (for +instance, after a manual page break). \nd@openb and \nd@closeb open, +respectively close, a subproof. \nd@guardb{n}{g} adds the guard g to the nth enclosing subderivation (counted from 1 from the -inside). \nd*hypob introduces a hypothesis, and \nd*haveb introduces a +inside). \nd@hypob introduces a hypothesis, and \nd@haveb introduces a non-hypothesis line in a proof. Line numbering is integrated, but justifications must still be given manually. Also, proof lines must still be terminated by '\\'. An idiosyncracy of this layer is that in a list of several hypotheses, all but the last one must be called with -\nd*haveb, not \nd*hypob, to avoid drawing a horizontal line under +\nd@haveb, not \nd@hypob, to avoid drawing a horizontal line under each of them. Example of a derivation using layer B syntax. Note that the "line @@ -154,40 +154,40 @@ numbers" are really labels, which will be replaced by consecutive line numbers in the output. \[ - \nd*beginb - \nd*haveb {1}{P\vee Q} \\ - \nd*hypob {2}{\neg Q} \\ - \nd*openb - \nd*hypob {3}{P} \\ - \nd*haveb {4}{P} \mbox{by \ndref{3}} \\ - \nd*closeb - \nd*openb - \nd*hypob {5}{Q} \\ - \nd*haveb {6}{\neg Q} \mbox{by \ndref{2}} \\ - \nd*haveb {6a}{\bot} \mbox{by \ndref{5,6}} \\ - \nd*haveb {6b}{P} \mbox{by \ndref{6a}} \\ - \nd*closeb - \nd*haveb {8}{P} \mbox{by \ndref{1,3-4,5-6b}} \\ - \nd*endb + \nd@beginb + \nd@haveb {1}{P\vee Q} \\ + \nd@hypob {2}{\neg Q} \\ + \nd@openb + \nd@hypob {3}{P} \\ + \nd@haveb {4}{P} \mbox{by \ndref{3}} \\ + \nd@closeb + \nd@openb + \nd@hypob {5}{Q} \\ + \nd@haveb {6}{\neg Q} \mbox{by \ndref{2}} \\ + \nd@haveb {6a}{\bot} \mbox{by \ndref{5,6}} \\ + \nd@haveb {6b}{P} \mbox{by \ndref{6a}} \\ + \nd@closeb + \nd@haveb {8}{P} \mbox{by \ndref{1,3-4,5-6b}} \\ + \nd@endb \] Here is another example, using a guard. \[ - \nd*beginb - \nd*hypob {1}{\neg\exists xP(x)} \\ - \nd*openb - \nd*guardb {1}{u} - \nd*openb - \nd*hypob {2}{P(u)} \\ - \nd*haveb {3}{\exists xP(x)} \mbox{by \ndref{2}} \\ - \nd*haveb {4}{\neg\exists xP(x)} \mbox{by \ndref{1}} \\ - \nd*haveb {5}{\bot} \mbox{by \ndref{3,4}}\\ - \nd*closeb - \nd*haveb {6}{\neg P(u)} \mbox{by \ndref{2-5}}\\ - \nd*closeb - \nd*haveb {7}{\forall y\neg P(y)} \mbox{by \ndref{2-6}}\\ - \nd*endb + \nd@beginb + \nd@hypob {1}{\neg\exists xP(x)} \\ + \nd@openb + \nd@guardb {1}{u} + \nd@openb + \nd@hypob {2}{P(u)} \\ + \nd@haveb {3}{\exists xP(x)} \mbox{by \ndref{2}} \\ + \nd@haveb {4}{\neg\exists xP(x)} \mbox{by \ndref{1}} \\ + \nd@haveb {5}{\bot} \mbox{by \ndref{3,4}}\\ + \nd@closeb + \nd@haveb {6}{\neg P(u)} \mbox{by \ndref{2-5}}\\ + \nd@closeb + \nd@haveb {7}{\forall y\neg P(y)} \mbox{by \ndref{2-6}}\\ + \nd@endb \] LAYER C @@ -197,42 +197,42 @@ information and putting it correctly into an array. Specifically, in layer C, it is no more necessary to explicitly give '\\', and all hypotheses are denoted \hypo. Layer C also provides a convenient syntax for writing justification labels. Further, layer C provides -``multi-line'' commands, thus e.g. \nd*mhypoc{a}{x\\y\\z} is an -abbreviation for \nd*hypoc{a}{x}\nd*hypocontc{y}\nd*hypocontc{z}. In -addition there is a \nd*by command for writing justification labels, -in the style of \nd*by{$\vee$E}{1,2-4,5-6}. +``multi-line'' commands, thus e.g. \nd@mhypoc{a}{x\\y\\z} is an +abbreviation for \nd@hypoc{a}{x}\nd@hypocontc{y}\nd@hypocontc{z}. In +addition there is a \nd@by command for writing justification labels, +in the style of \nd@by{$\vee$E}{1,2-4,5-6}. -Commands exported by layer C are: \nd*hypoc, \nd*havec, \nd*hypocontc, -\nd*havecontc, \nd*mhypoc, \nd*mhavec, \nd*mhypocontc, \nd*mhavecontc, -\nd*by, \nd*beginc, \nd*resumec, \nd*endc, \nd*openc, \nd*closec, -\nd*guardc. +Commands exported by layer C are: \nd@hypoc, \nd@havec, \nd@hypocontc, +\nd@havecontc, \nd@mhypoc, \nd@mhavec, \nd@mhypocontc, \nd@mhavecontc, +\nd@by, \nd@beginc, \nd@resumec, \nd@endc, \nd@openc, \nd@closec, +\nd@guardc. The layer C macros work by storing each line in a data structure -\ppp,\nd*typ,\nd*byt. The line is ejected when the beginning of the +\ppp,\nd@typ,\nd@byt. The line is ejected when the beginning of the next line is read, and once at the very end. In this way, we can put in the correct line breaks (whether or not the line carries a justification), and a hypothesis does not get typeset until we know -whether it is followed by another hypothesis. \nd*sto stores a new -line, \nd*clr clears the current line, \nd*cmd outputs the current +whether it is followed by another hypothesis. \nd@sto stores a new +line, \nd@clr clears the current line, \nd@cmd outputs the current line. Example of layer C syntax: \[ - \nd*beginc - \nd*hypoc {1}{\neg\exists xP(x)} - \nd*openc - \nd*guardc {1}{u} - \nd*openc - \nd*hypoc {2}{P(u)} - \nd*havec {3}{\exists xP(x)} \nd*by{$\exists$I}{2} - \nd*havec {4}{\neg\exists xP(x)} \nd*by{R}{1} - \nd*havec {5}{\bot} \nd*by{$\neg$E}{3,4} - \nd*closec - \nd*havec {6}{\neg P(u)} \nd*by{$\neg$I}{2-5} - \nd*closec - \nd*havec {7}{\forall y\neg P(y)} \nd*by{$\forall$I}{2-6} - \nd*endc + \nd@beginc + \nd@hypoc {1}{\neg\exists xP(x)} + \nd@openc + \nd@guardc {1}{u} + \nd@openc + \nd@hypoc {2}{P(u)} + \nd@havec {3}{\exists xP(x)} \nd@by{$\exists$I}{2} + \nd@havec {4}{\neg\exists xP(x)} \nd@by{R}{1} + \nd@havec {5}{\bot} \nd@by{$\neg$E}{3,4} + \nd@closec + \nd@havec {6}{\neg P(u)} \nd@by{$\neg$I}{2-5} + \nd@closec + \nd@havec {7}{\forall y\neg P(y)} \nd@by{$\forall$I}{2-6} + \nd@endc \] LAYER D @@ -250,24 +250,24 @@ global name space. There is also an environment ndresume which is like nd, except that it continues a proof in progress (with continuous nesting and labeling). -The macros \nd*hypod, \nd*haved, \nd*opend, \nd*guardd are essentially +The macros \nd@hypod, \nd@haved, \nd@opend, \nd@guardd are essentially the user-level macros, but with all optional argument spelled-out. The versions without the final "d" allow the optional arguments to be omitted. -The functions \nd*optarg and \nd*optargg are used to handle optional -arguments. Usage: \nd*optarg{default}{continuation}xxx - reads an +The functions \nd@optarg and \nd@optargg are used to handle optional +arguments. Usage: \nd@optarg{default}{continuation}xxx - reads an optional argument, supplies default if necessary, then continues with continuation. Continuation expects optional argument between -[...]. I.e., \nd*optarg{d}{c}[xxx] => c[xxx], and \nd*optarg{d}{c}x => -c[d]x if x != '['. Behavior is undefined if x is {[...}. \nd*optargg +[...]. I.e., \nd@optarg{d}{c}[xxx] => c[xxx], and \nd@optarg{d}{c}x => +c[d]x if x != '['. Behavior is undefined if x is {[...}. \nd@optargg is similar except it takes two continuations: first one for optional argument present, second for not present. It takes no default value. -The function \nd*five{\a} reads five, partly optional arguments of the +The function \nd@five{\a} reads five, partly optional arguments of the shape [][]{}[]{}, then call \a with these arguments. -Finally, \nd*init puts all the commands which are visible inside an +Finally, \nd@init puts all the commands which are visible inside an nd-environment in the current name space. Example of a derivation using layer D syntax. As before, the "line diff --git a/fitch.sty b/fitch.sty index 0d7094e..a1dc1fc 100644 --- a/fitch.sty +++ b/fitch.sty @@ -18,9 +18,9 @@ % Original Author: Peter Selinger, Dalhousie University % Created: Jan 14, 2002 -% Modified: October 15, 2023 -% Version: 0.6 -% Copyright: (C) 2002-2005 Peter Selinger +% Modified: December 17, 2023 +% Version: 1.0 +% Copyright: (C) 2002-2005 Peter Selinger, Richard Zach % Filename: fitch.sty % Documentation: fitchdoc.tex % https://github.com/OpenLogicProject/fitch/ @@ -50,7 +50,7 @@ % \] \NeedsTeXFormat{LaTeX2e} -\ProvidesPackage{fitch}[2023-10-15 v1.0-beta2 Macros for Fitch-style natural deduction] +\ProvidesPackage{fitch}[2023-12-17 v1.0 Macros for Fitch-style natural deduction] % Define keyval options @@ -302,13 +302,13 @@ prefix = nd@ % prefix with nd@ for compatibility with old code \newenvironment{ndresume}[1][] {\begingroup \setkeys{fitch}{#1}% - \nd@init\nd@resumec} + \nd@init\nd@resumec\ignorespaces} {\nd@endc\endgroup} -\newenvironment{fitchproof}[1][arrayenv=tabular] - {\begin{list}{}{\setlength{\leftmargin}{0pt}}\item\begin{nd}[arrayenv=tabular,#1]} +\newenvironment{fitchproof}[1][] + {\begin{list}{}{\setlength{\leftmargin}{0pt}}\item\begin{nd}[#1]} {\end{nd}\end{list}} -\newenvironment{fitchproof*}[1][arrayenv=tabular] - {\begin{list}{}{\setlength{\leftmargin}{0pt}}\item\begin{ndresume}[arrayenv=tabular,#1]} +\newenvironment{fitchproof*}[1][] + {\begin{list}{}{\setlength{\leftmargin}{0pt}}\item\begin{ndresume}[#1]} {\end{ndresume}\end{list}} % End of file fitch.sty diff --git a/fitchdoc.tex b/fitchdoc.tex index 20dc29c..5a16d90 100644 --- a/fitchdoc.tex +++ b/fitchdoc.tex @@ -18,9 +18,9 @@ % Original Author: Peter Selinger, Dalhousie University % Created: Jan 14, 2002 -% Modified: Sep 30, 2023 +% Modified: Dec 17, 2023 % Version: 1.0 -% Copyright: (C) 2002-2023 Peter Selinger +% Copyright: (C) 2002-2023 Peter Selinger, Richard Zach % Filename: fitch.sty % Documentation: fitchdoc.tex % https://github.com/OpenLogicProject/fitch/ @@ -55,7 +55,7 @@ \href{https://github.com/OpenLogicProject/fitch/issues}{issues} with it.}} -\date{Version 1.0-beta2\\ October 15, 2023} +\date{Version 1.0\\ December 17, 2023} \begin{document} \maketitle @@ -63,15 +63,15 @@ \section{Overview} This document describes how to use the {\tt fitch.sty} macros for -typesetting Fitch-style natural deduction derivations. To load the macros, -simply put |\usepackage{fitch}| into the preamble of your +typesetting Fitch-style natural deduction derivations. To load the +macros, simply put |\usepackage{fitch}| into the preamble of your {\LaTeX} file. Here is a natural deduction derivation, together with the code that produced it: \begin{LTXexample} -\begin{fitchproof} +$\begin{nd} \hypo {1} {P\vee Q} \hypo {2} {\neg Q} \open @@ -85,7 +85,7 @@ \section{Overview} \have {8} {P} \be{7} \close \have {9} {P} \oe{1,3-4,aa-8} -\end{fitchproof} +\end{nd}$ \end{LTXexample} A derivation consists of \emph{lines}, and each line contains a {\em @@ -103,19 +103,27 @@ \section{Overview} shorthand macros used to produce rule names can be customized (see Section~\ref{sec-customization}). +\NewIn{1.0} Several new commands and customization options have been +introduced in v1.0. It is mostly backwards compatible with earlier +versions, but see section~\ref{compat}. In particular, if you +redefined any internal |fitch| commands, you will have to change |nd*| +to |nd@|. + \section{Usage}\label{sec-usage} -\DescribeEnv{nd}\DescribeEnv{fitchproof} Derivations are typeset +\DescribeEnv{nd}\DescribeEnv{nd} Derivations are typeset inside the |nd| environment. By default, the standard |array| environment is used to do this, so the |nd| environment must must be used in math mode, i.e., it should be surrounded by |$...$| or |\[...\]|. -\NewIn{1.0} The environment |fitchproof| typesets the proof on its -own. Proofs will be set flush left, with the default |\partopsep| -spacing surrounding lists added. You do not have to insert |$| to -switch to math mode for |fitchproof|---by default, it is generated -using a |tabular| environment. +\NewIn{1.0} The environment |fitchproof| typesets the proof on its own +in text, not math mode. Proofs will be set flush left, with the +default |\partopsep| spacing surrounding lists added. You do not have +to insert |$| to switch to math mode for |fitchproof|---by default. +However, it only works if you generate proofs using the |tabular| +environment, e.g., by loading |fitch| with the |arrayenv=tabular| +option. \DescribeMacro{\hypo}\DescribeMacro{\have} The commands |\hypo| and |\have| are used @@ -287,10 +295,11 @@ \subsection{Breaking it across pages}\label{subsec-break} derivation. \NewIn{1.0} The environment |fitchproof*| works the same way, except typesets the proof just like the |fitchproof| environment (no need for math mode, -flush left, spacing before and after). Here is an example: +flush left, spacing before and after). However, like |fitchproof|, it +requires the |arrayenv=tabular| option. Here is an example: \begin{LTXexample} -\begin{fitchproof} +\begin{fitchproof}[arrayenv=tabular] \hypo {1} {P\vee Q} \hypo {2} {\neg Q} \open @@ -303,7 +312,7 @@ \subsection{Breaking it across pages}\label{subsec-break} \end{fitchproof} Derivations can be interrupted and resumed at any point. -\begin{fitchproof*} +\begin{fitchproof*}[arrayenv=tabular] \have {7} {\bot} \ne{aa,6} \have {8} {P} \be{7} \close @@ -311,6 +320,17 @@ \subsection{Breaking it across pages}\label{subsec-break} \end{fitchproof*} \end{LTXexample} +\NewIn{1.0} You can also have derivations break across pages +automatically. In order to do this, you have to load the +\href{https://ctan.org/pkg/longtable}{|longtable|} package, and load +|fitch| with the |arrayenv=longtable| option. Since the |longtable| +environment works in text (not math) mode, you should then only use +|fitchproof|, or the |nd| environment but \emph{not} in text mode. +Note that the |longtable| package does not work in 2-column mode or +inside a |multicolumn| environment. You can always produce a proof +inside a |multicolumn| environment by passing |arrayenv=tabular| as an +option to the |nd| or |fitchproof| environment. + \subsection{Custom line numbers}\label{subsec-customline} @@ -434,13 +454,13 @@ \section{Customization}\label{sec-customization} \NewIn{1.0} To change these default dimensions, pass a list of key-value pairs as package options, as optional arguments to the -\cmd{\nd} or \cmd{\fitchproof} environment, or use the |\fitchset| +|nd| or |fitchproof| environment, or use the |\setkeys| command: \begin{verbatim} \usepackage[justsep=1em]{fitch} \begin{nd}[rules=myrules] \begin{fitchproof}[linethickness=1pt] - \fitchset{hsep=1em,indent=1em}\end{verbatim} + \setkeys{fitch}{hsep=1em,indent=1em}\end{verbatim} In addition, the macros used to generate the table containing the proof, to format justifications, format line number references, and to @@ -458,12 +478,15 @@ \section{Customization}\label{sec-customization} For compatibility with earlier versions of |fitch.sty|, the default for \meta{arrayenv} is |array|, i.e., the table containing the proof is generated using an |array| environment, and must therefore occur -inside math mode. The |fitchproof| and |fitchproof*| environments use -|tabular| instead, and hence should \emph{not} be in math mode. Any -other table environment that takes the same table format argument as -|array| and |tabular| can be used here, e.g., the |longtable| -environment from the |longtable| package (which must be loaded -separately). +inside math mode. The |fitchproof| and |fitchproof*| environments +assume that you use a text table command instead, such as |tabular|. +Hence, you should \emph{not} use |fitchproof| in math mode, and you +must use the option |arrayenv=tabular| (when loading |fitch|, as an +optional argument to |fitchproof|, or using +|\setkeys{fitch}{arrayenv=tabular}|. Any other table environment that +takes the same table format argument as |array| and |tabular| can be +used here, e.g., the |longtable| environment from the |longtable| +package (which must be loaded separately). The package defines the macros \DescribeMacro{\ndrules}\cmd{\ndrules}, which defines the rule @@ -549,7 +572,7 @@ \section{Customization}\label{sec-customization} $ \end{LTXexample} -\section{Obsolete commands and backwards compatibility} +\section{Obsolete commands and backwards compatibility}\label{compat} \DescribeMacro{\nddim} The dimensions can also be changed with the @@ -568,7 +591,8 @@ \section{Obsolete commands and backwards compatibility} The original code ``hid'' the internal macros by naming them |\nd*...|. In v1.0 this has been changed to the standard -|\nd@...|. +|\nd@...|. Any low-level redefinition of |fitch| internals that uses +|*| will break in v1.0. \section{Other comments} @@ -584,8 +608,8 @@ \section{Other comments} \section{Copyright and license} -This document and the accompanying |fitch.sty| macros -are {\copyright} 2002--2023 by Peter Selinger and distributed under +This document and the accompanying |fitch.sty| macros are {\copyright} +2002--2023 by Peter Selinger and Richard Zach and distributed under the terms of the \href{https://www.latex-project.org/lppl/}{LPPL}. \end{document}