summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/fitch/fitch.hacker.txt
blob: df4af5c4da688907c8d69b8ccd68b919cb147caf (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
This file describes the internals of the macros in fitch.sty. It is
intended for programmers who might want to hack this package. For
information on how to use the package, please see the user guide,
which is provided in the file fitchdoc.tex.

GENERAL

Global identifiers defined by this package start with '\nd*'. The only
exceptions are \ndref, \nddim, \ndindent, and the "nd" and "ndresume"
latex environments.

The macros provided by this package mix TeX and LaTeX primitives.
LaTeX is used for \rule, \settowidth, \addtolength, \hspace...  All
macros are assumed to be called in math mode.

Translation proceeds through several layers of macros. Each layer
consist of macros which expand into macros of the previous layer. Each
layer may have some global state and initialization functions. Only
the topmost layer (layer D) is directly user-accessible.

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
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,
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
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}
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
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
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
spacing information is contained in this layer; higher layers
manipulate only layer A primitives.

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}  \\
\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 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
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{...}
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.

With the list syntax, a derivation can be expressed like this:

\[ 
\begin{array}{lll}
  \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
\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
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
the nth enclosing subderivation (counted from 1 from the
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
each of them.

Example of a derivation using layer B syntax. Note that the "line
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
\]

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
\]

LAYER C

Layer C is a wrapper around layer B. It takes care of buffering
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}.

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
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
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
\]

LAYER D

Layer D is the syntax used by the end user. It is implemented as a
wrapper around layer C, providing three additional conveniences: (1) a
latex environment, (2) guard as optional argument to \have, \hypo, or
\open, (3) optional relabeling arguments. The user level commands are
similar to those of layer C: they are called \begin{nd}, \end{nd},
\open, \close, \hypo, \have, \guard, \by.  For convenience, a number
of abbreviations are also provided for writing justifications. For
instance \ie for \by{$\Rightarrow$E} etc. These commands are only
visible inside an nd-environment; thus they do not interfere with the
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 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
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
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
shape [][]{}[]{}, then call \a with these arguments.

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
numbers" are really labels, which will be replaced by consecutive line
numbers in the output.

\[
\begin{nd}
  \hypo{1}  {P\vee Q}   
  \hypo{2}  {\neg Q}                         
  \open                              
  \hypo{3a} {P}
  \have{3b} {P}        \r{3a}
  \close                   
  \open
  \hypo{4a} {Q}
  \have{4b} {\neg Q}   \r{2}
  \have{4c} {\bot}     \ne{4a,4b}
  \have{4d} {P}        \be{4c}
  \close                             
  \have{5}  {P}        \oe{1,3a-3b,4a-4d}                 
\end{nd}
\]

Another example of layer D syntax, using guards and relabelings:

\[
\begin{nd}
  \hypo          {1} {P\vee Q}
  \open[u]
  \hypo          {2} {P}
  \have [\vdots] {3} {\vdots}
  \have [n][-1]  {4} {A\wedge B}
  \close
  \open
  \hypo          {5} {Q}
  \have [\vdots] {6} {\vdots}
  \have [m]      {7} {A\wedge B}
  \close
  \have          {8} {A\wedge B}  \oe{1,2-(4),5-7}
  \have [\vdots] {9} {\vdots}
  \have [][100] {10} {A}          \ae{8}
\end{nd}
\]