summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/stex/doc/packages/stex-proofs.tex
blob: 9e6e44f5ca28e0aa70516b9b471589eb8d617844 (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
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
\begin{sfragment}{Proofs}

The \pkg{stex-proof} package supplies macros and environment that allow to annotate the
structure of mathematical proofs in \sTeX document. This structure can be used by MKM
systems for added-value services, either directly from the \sTeX sources, or after
translation.

Its central component is the |sproof|-environment, whose body consists
of:
\begin{itemize}
  \item \emph{subproofs} via the |subproof|-environment,
  \item \emph{proof steps} via the |\spfstep|, |\eqstep|
    |\assumption|, and |\conclude| macros, and
  \item \emph{comments}, via normal text without special markup.
\end{itemize}

|sproof|, |subproof| and the various proof step macros take the following
optional arguments:
\begin{itemize}
  \item[|id|] (\meta{string}) for referencing,
  \item[|method|] (\meta{string}) the proof method (e.g. contradiction, induction,...)
  \item[|term|] (\meta{token list}) the (ideally semantically-marked up)
    proposition that is derived/proven by this proof/subproof/proof step.
\end{itemize}
Additionally, they take one mandatory argument for the document text
to be annotated, or (in the case of the environments)
as an introductory description of the proof itself. Since
the latter often contains the |term| to be derived
as text, alternatively to providing it as 
an optional argument, the mandatory argument can use the
|\yield|-macro to mark it up in the text.

The |sproof| and |subproof| environments additionally take
two optional arguments:
\begin{itemize}
  \item[|for|] the symbol identifier/name corresponding to the |sassertion|
    to be proven. This too subsumes |\yield| and the |term|-argument.
  \item[|hide|] In the pdf, this only shows the mandatory argument text
    and hides the body of the environment. In the HTML (as served by \mmt),
    the bodies of all |proof| and |subproof| environments are \emph{collapsible},
    and |hide| collapses the body by default.
\end{itemize}

\begin{smodule}{sproofs}
  \symdef{coprime}[args=2]{#1 \comp\bot #2}
  \symdef{realroot}[args=1]{\sqrt{#1}}
  \symdecl{irrational}[args=1]
  \symdecl{rational}[args=1]
  \symdef{eq}[args=2]{#1 \comp= #2}
  \symdef{ratfrac}[args=2,prec=1]{\frac{#1}{#2}}
  \symdef{intpow}[args=2,prec=-1]{{#1}^{#2}}
  \symdef{ratpow}[args=2]{{#1}^{#2}}
  \symdef{inset}[args=ai]{#1\comp\in#2}{##1\comp,##2}
  \symdef{Int}{\comp{\mathbb Z}}
  \symdef{PosInt}{\comp{{\mathbb Z}^+}}
  \symdef{inttimes}[args=2]{#1 #2}
  \symdef{divides}[args=2]{#1\comp\|#2}

  \vardef{vara}{\comp a}
  \vardef{varb}{\comp b}
  \vardef{varc}{\comp c}

  \def\contradiction{}

\begin{latexcode}
  \begin{sassertion}[type=theorem,name=sqrt2irr]
    \conclusion{\irrational{$\arg{\realroot{2}}$ is \comp{irrational}}}.
\end{sassertion}

\begin{sproof}[for=sqrt2irr,method=contradiction]{By contradiction}
    \assumption{Assume \yield{\rational{$\arg{\realroot{2}}$ is 
      \comp{rational}}}}
    \begin{subproof}[method=straightforward]{Then 
        \yield{$\eq{\ratfrac{\intpow{\vara}{2}}{\intpow{\varb}2}}{2}$ 
        for some $\inset{\vara,\varb}\PosInt$ with 
        \coprime{$\arg{\vara},\arg{\varb}$ \comp{coprime}}}}
        \assumption{By assumption, \yield{there are 
        $\inset{\vara,\varb}\PosInt $ with 
        $\realroot{2}=\ratfrac{\vara}{\varb}$}}
        \spfstep{wlog, we can assume \coprime{$\arg{\vara},\arg{\varb}$ 
        to be \comp{coprime}}}
            % a comment:
            If not, reduce the fraction until numerator and denominator 
            are coprime, and let the resulting components be 
            $\vara $ and $\varb $
        \spfstep{Then \yield{$\eq{\intpow{\ratfrac{\vara}{\varb}}2}2$}}
        \eqstep{\ratfrac{\intpow{\vara}2}{\intpow{\varb}2}}
    \end{subproof}
    \begin{subproof}[term=\divides{2}{\vara},method=straightforward]{
        Then $\vara $ is even}
        \spfstep{Multiplying the equation by $\intpow{\varb}2$ yields 
        $\yield{\eq{\intpow{\vara}2}{\inttimes{2}{\intpow{\varb}2}}}$}
        \spfstep[term=\divides{2}{\intpow{\vara}2}]{Hence 
        $\intpow{\vara}2$ is even}
        \conclude[term=\divides{2}{\vara}]{Hence $\vara $ is even as well}
        % another comment:
        Hint: Think about the prime factorizations of $\vara $ and 
        $\intpow{\vara}2$
    \end{subproof}
    \begin{subproof}[term=\divides{2}{\varb},method=straightforward,]{
        Then $\varb $ is also even}
        \spfstep{Since $\vara $ is even, we have \yield{some $\varc $ 
          such that $\eq{\inttimes{2}{\varc}}{\vara}$}}
        \spfstep{Plugging into the above, we get 
          \yield{$\eq{\intpow{\inttimes{2}{\vara}}2}
            {\inttimes{2}{\intpow{\varb}2}}$}}
        \eqstep{\inttimes{4}{\intpow{\vara}2}}
        \spfstep{Dividing both sides by $2$ yields 
          \yield{$\eq{\intpow{\varb}2}{\inttimes{2}{\intpow{\vara}2}}$}}
        \spfstep[term=\divides{2}{\intpow{\varb}2}]{Hence 
          $\intpow{\varb}2$ is even}
        \conclude[term=\divides{2}{\varb}]{Hence $\varb $ is even}
        % one more comment:
        By the same argument as above
    \end{subproof}
    \conclude[term=\contradiction]{Contradiction to $\vara,\varb $ being 
    \symname{coprime}.}
\end{sproof}
\end{latexcode}

which will produce:

\begin{mdframed}
\begin{sassertion}[type=theorem,name=sqrt2irr]
  \conclusion{\irrational{$\arg{\realroot2}$ is \comp{irrational}}}.
\end{sassertion}

\begin{sproof}[for=sqrt2irr,method=contradiction]{By contradiction}
  \assumption{Assume \yield{\rational{$\arg{\realroot2}$ is \comp{rational}}}}
  \begin{subproof}[method=straightforward]%
      {Then \yield{$\eq{\ratfrac{\intpow \vara2}{\intpow \varb2}}{2}$ for some $\inset{\vara,\varb}\PosInt$ with \coprime{$\arg \vara,\arg \varb$ \comp{coprime}}}}
      \assumption{By assumption, \yield{there are $\inset{\vara,\varb}\PosInt$ with $\realroot2=\ratfrac\vara\varb$}}
      \spfstep{wlog, we can assume \coprime{$\arg{\vara},\arg{\varb}$ to be \comp{coprime}}}
          If not, reduce the fraction until numerator and denominator are 
          coprime, and let the resulting components be $\vara$ and $\varb$
      \spfstep{Then \yield{$\eq{\intpow{\ratfrac\vara\varb}2}2$}}
      \eqstep{\ratfrac{\intpow\vara2}{\intpow\varb2}}
  \end{subproof}
  \begin{subproof}[term=\divides{2}{\vara},method=straightforward]{Then $\vara$ is even}
      \spfstep{Multiplying the equation by $\intpow\varb2$ yields $\yield{\eq{\intpow\vara2}{\inttimes2{\intpow\varb2}}}$}
      \spfstep[term=\divides{2}{\intpow\vara2}]{Hence $\intpow\vara2$ is even}
      \conclude[term=\divides{2}{\vara}]{Hence $\vara$ is even as well}
      Hint: Think about the prime factorizations of $\vara$ and $\intpow\vara2$
  \end{subproof}
  \begin{subproof}[term=\divides{2}{\varb},method=straightforward]{Then $\varb$ is also even}
      \spfstep{Since $\vara$ is even, we have \yield{some $\varc$ such that $\eq{\inttimes2\varc}{\vara}$}}
      \spfstep{Plugging into the above, we get \yield{$\eq{\intpow{\inttimes2\vara}2}{\inttimes2{\intpow\varb2}}$}}
      \eqstep{\inttimes4{\intpow\vara2}}
      \spfstep{Dividing both sides by $2$ yields \yield{$\eq{\intpow\varb2}{\inttimes2{\intpow\vara2}}$}}
      \spfstep[term=\divides{2}{\intpow\varb2}]{Hence $\intpow\varb2$ is even}
      \conclude[term=\divides{2}{\varb}]{Hence $\varb$ is even}
      By the same argument as above
  \end{subproof}
  \conclude[term=\contradiction]{Contradiction to $\vara,\varb$ being \symname{coprime}.}
\end{sproof}
\end{mdframed}

If we mark all subproofs with |hide|, we will obtain the following
instead:

\begin{mdframed}
  \begin{sassertion}[type=theorem,name=sqrt2irr]
    \conclusion{\irrational{$\arg{\realroot2}$ is \comp{irrational}}}.
  \end{sassertion}
  
  \begin{sproof}[for=sqrt2irr,method=contradiction]{By contradiction}
    \assumption{Assume \yield{\rational{$\arg{\realroot2}$ is \comp{rational}}}}
    \begin{subproof}[hide,method=straightforward]%
        {Then \yield{$\eq{\ratfrac{\intpow \vara2}{\intpow \varb2}}{2}$ for some $\inset{\vara,\varb}\PosInt$ with \coprime{$\arg \vara,\arg \varb$ \comp{coprime}}}}
        \assumption{By assumption, \yield{there are $\inset{\vara,\varb}\PosInt$ with $\realroot2=\ratfrac\vara\varb$}}
        \spfstep{wlog, we can assume \coprime{$\arg{\vara},\arg{\varb}$ to be \comp{coprime}}}
            If not, reduce the fraction until numerator and denominator are 
            coprime, and let the resulting components be $\vara$ and $\varb$
        \spfstep{Then \yield{$\eq{\intpow{\ratfrac\vara\varb}2}2$}}
        \eqstep{\ratfrac{\intpow\vara2}{\intpow\varb2}}
    \end{subproof}
    \begin{subproof}[hide,term=\divides{2}{\vara},method=straightforward]{Then $\vara$ is even}
        \spfstep{Multiplying the equation by $\intpow\varb2$ yields $\yield{\eq{\intpow\vara2}{\inttimes2{\intpow\varb2}}}$}
        \spfstep[term=\divides{2}{\intpow\vara2}]{Hence $\intpow\vara2$ is even}
        \conclude[term=\divides{2}{\vara}]{Hence $\vara$ is even as well}
        Hint: Think about the prime factorizations of $\vara$ and $\intpow\vara2$
    \end{subproof}
    \begin{subproof}[hide,term=\divides{2}{\varb},method=straightforward,]{Then $\varb$ is also even}
        \spfstep{Since $\vara$ is even, we have \yield{some $\varc$ such that $\eq{\inttimes2\varc}{\vara}$}}
        \spfstep{Plugging into the above, we get \yield{$\eq{\intpow{\inttimes2\vara}2}{\inttimes2{\intpow\varb2}}$}}
        \eqstep{\inttimes4{\intpow\vara2}}
        \spfstep{Dividing both sides by $2$ yields \yield{$\eq{\intpow\varb2}{\inttimes2{\intpow\vara2}}$}}
        \spfstep[term=\divides{2}{\intpow\varb2}]{Hence $\intpow\varb2$ is even}
        \conclude[term=\divides{2}{\varb}]{Hence $\varb$ is even}
        By the same argument as above
    \end{subproof}
    \conclude[term=\contradiction]{Contradiction to $\vara,\varb$ being \symname{coprime}.}
  \end{sproof}
  \end{mdframed}

  However, the hidden subproofs will still be shown in the HTML,
  only in an expandable section which is collapsed by default.


The above style of writing proofs is usually called \emph{structured proofs}.
They have a huge advantage over the traditional purely prosaic style,
in that (as the name suggests) the actual \emph{structure} of the proof
is made explicit, which almost always makes it considerably more 
comprehensible. We, among many others, encourage the general use of 
structured proofs.

Alas, most proofs are not written in this style, and we would
do users a disservice by insisting on this style. For that reason,
the |spfblock| environment turns all subproofs and proof step
macros into presentationally neutral \emph{inline} annotations,
as in the induction step of the following example:

\begin{latexcode}
\begin{sproof}[id=simple-proof,method=induction]
   {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$}
  For the induction we have to consider three cases: % <- a comment
   \begin{subproof}{$n=1$}
    \spfstep*{then we compute $1=1^2$}
   \end{subproof}
   \begin{subproof}{$n=2$}
        This case is not really necessary, but we do it for the
        fun of it (and to get more intuition).
      \spfstep*{We compute $1+3=2^{2}=4$.}
   \end{subproof}
   \begin{subproof}{$n>1$}\begin{spfblock}
      \assumption[id=ind-hyp]{
        Now, we assume that the assertion is true for a certain $k\geq 1$,
        i.e. \yield{$\sum_{i=1}^k{(2i-1)}=k^{2}$}.
      }
      
        We have to show that we can derive the assertion for $n=k+1$ from
        this assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$.

      \spfstep{
        We obtain $\yield{\sum_{i=1}^{k+1}{2i-1}=
          \sum_{i=1}^k{2i-1}+2(k+1)-1}$
        \spfjust{by \splitsum{\comp{splitting the sum}
        \arg*{$\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$}}}.
      }
      \spfstep{
        Thus we have $\yield{\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1}$
        \spfjust{by \symname{induction-hypothesis}}.
      }
      \conclude{
        We can \spfjust{\simplification{\comp{simplify} the right-hand side
        \arg*{k^2+2k+1}}} to
        ${k+1}^2$, which proves the assertion.
      }
   \end{spfblock}\end{subproof}
    \conclude{
      We have considered all the cases, so we have proven the assertion.
    }
\end{sproof}
\end{latexcode}


\symdecl{splitsum}[args=1]
\symdecl{inducthypothesis}[name=induction-hypothesis]
\symdecl{simplification}[args=1]

This yields the following result: 

\begin{mdframed}
  \begin{sproof}[id=simple-proof,method=induction]
    {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$}
   For the induction we have to consider three cases: % <- a comment
    \begin{subproof}{$n=1$}
     \spfstep*{then we compute $1=1^2$}
    \end{subproof}
    \begin{subproof}{$n=2$}
         This case is not really necessary, but we do it for the
         fun of it (and to get more intuition).
       \spfstep*{We compute $1+3=2^{2}=4$.}
    \end{subproof}
    \begin{subproof}{$n>1$}\begin{spfblock}
       \assumption[id=ind-hyp]{
         Now, we assume that the assertion is true for a certain $k\geq 1$,
         i.e. \yield{$\sum_{i=1}^k{(2i-1)}=k^{2}$}.
       }
       
         We have to show that we can derive the assertion for $n=k+1$ from
         this assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$.
 
       \spfstep{
         We obtain $\yield{\sum_{i=1}^{k+1}{2i-1}=\sum_{i=1}^k{2i-1}+2(k+1)-1}$
         \spfjust{by \splitsum{\comp{splitting the sum}\arg*{$\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$}}}.
       }
       \spfstep{
         Thus we have $\yield{\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1}$
         \spfjust{by \symname{induction-hypothesis}}.
       }
       \conclude{
         We can \spfjust{\simplification{\comp{simplify} the right-hand side
         \arg*{k^2+2k+1}}} to
         ${k+1}^2$, which proves the assertion.
       }
    \end{spfblock}\end{subproof}
     \conclude{
       We have considered all the cases, so we have proven the assertion.
     }
 \end{sproof}
\end{mdframed}

\end{smodule}

\begin{environment}{sproof}
  The |sproof| environment is the main container for proofs. It takes an optional |KeyVal|
  argument that allows to specify the |id| (identifier) and |for| (for which assertion is
  this a proof) keys. The regular argument of the |proof| environment contains an
  introductory comment, that may be used to announce the proof style. The |proof|
  environment contains a sequence of |spfstep|, |spfcomment|, and |spfcases| environments
  that are used to markup the proof steps.
\end{environment}
  
\begin{function}{\spfidea}
  The |\spfidea| macro allows to give a one-paragraph description of the proof idea.
\end{function}

\begin{function}{\spfsketch}
  For one-line proof sketches, we use the |\spfsketch| macro, which takes the same
  optional argument as |sproof| and another one: a natural language text that sketches
  the proof.
\end{function}

\begin{function}{\spfstep}
  Regular proof steps are marked up with the |\spfstep| macro, which takes an optional
  |KeyVal| argument for annotations. A proof step usually contains a local assertion
  (the text of the step) together with some kind of evidence that this can be derived
  from already established assertions.
\end{function}

\begin{function}{\yield}
  See above
\end{function}

\begin{function}{\spfjust}
  This evidence is marked up with the |\spfjust| macro in the \pkg{stex-proofs}
  package. This environment totally invisible to the formatted result; it wraps the text
  in the proof step that corresponds to the evidence (ideally, a
  semantically marked-up term).
\end{function}

\begin{function}{\assumption}
  The |\assumption| macro allows to mark up a (justified) assumption.
\end{function}

\begin{function}{\justarg}
\end{function}

\begin{environment}{subproof}
  The |subproof| environment is used to mark up a subproof. This environment takes an
  optional |KeyVal| argument for semantic annotations and a second argument that allows
  to specify an introductory comment (just like in the |proof| environment). The
  |method| key can be used to give the name of the proof method
  executed to make this subproof.
\end{environment}

\begin{function}{\sproofend}
  Traditionally, the end of a mathematical proof is marked with a little box at the end of
  the last line of the proof (if there is space and on the end of the next line if there
  isn't), like so:\sproofend

  The \pkg{stex-proofs} package provides the |\sproofend| macro for this.
\end{function}
  
\begin{variable}{\sProofEndSymbol}
  If a different symbol for the proof end is to be used (e.g. {\sl{q.e.d}}), then this can
  be obtained by specifying it using the |\sProofEndSymbol| configuration macro (e.g. by
  specifying |\sProofEndSymbol{q.e.d}|).
\end{variable}
  
Some of the proof structuring macros above will insert proof end symbols for sub-proofs,
in most cases, this is desirable to make the proof structure explicit, but sometimes this
wastes space (especially, if a proof ends in a case analysis which will supply its own
proof end marker). To suppress it locally, just set |proofend={}| in them or use use
|\sProofEndSymbol{}|.
\end{sfragment}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "../stex-manual"
%%% End:

%  LocalWords:  hypothesis,id geq splitit arith:split-sum byindhyp rhs proofend eqstep
%  LocalWords:  sproofs coprime ratfrac 2,prec intpow ratpow inttimes varb varc sqrt2irr
%  LocalWords:  theorem,name sqrt2irr,method wlog hide,method hide,term spfblock splitsum
%  LocalWords:  simple-proof,method inducthypothesis