diff options
Diffstat (limited to 'macros/latex/contrib/stex/doc/packages/stex-proofs.tex')
-rw-r--r-- | macros/latex/contrib/stex/doc/packages/stex-proofs.tex | 215 |
1 files changed, 214 insertions, 1 deletions
diff --git a/macros/latex/contrib/stex/doc/packages/stex-proofs.tex b/macros/latex/contrib/stex/doc/packages/stex-proofs.tex index 0523c65948..d06db1282f 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-proofs.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-proofs.tex @@ -1 +1,214 @@ -\textcolor{red}{TODO: sproofs documentation}
\ No newline at end of file +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. + +We will go over the general intuition by way of a running example: + +\begin{latexcode} +\begin{sproof}[id=simple-proof] + {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$} + \begin{spfcases}{For the induction we have to consider three cases:} + \begin{spfcase}{$n=1$} + \begin{spfstep}[type=inline] then we compute $1=1^2$\end{spfstep} + \end{spfcase} + \begin{spfcase}{$n=2$} + \begin{spfcomment}[type=inline] + This case is not really necessary, but we do it for the + fun of it (and to get more intuition). + \end{spfcomment} + \begin{spfstep}[type=inline] We compute $1+3=2^{2}=4$.\end{spfstep} + \end{spfcase} + \begin{spfcase}{$n>1$} + \begin{spfstep}[type=assumption,id=ind-hyp] + Now, we assume that the assertion is true for a certain $k\geq 1$, + i.e. $\sum_{i=1}^k{(2i-1)}=k^{2}$. + \end{spfstep} + \begin{spfcomment} + 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}$. + \end{spfcomment} + \begin{spfstep} + We obtain $\sum_{i=1}^{k+1}{2i-1}=\sum_{i=1}^k{2i-1}+2(k+1)-1$ + \spfjust[method=arith:split-sum]{by splitting the sum}. + \end{spfstep} + \begin{spfstep} + Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$ + \spfjust[method=fertilize]{by inductive hypothesis}. + \end{spfstep} + \begin{spfstep}[type=conclusion] + We can \spfjust[method=simplify]{simplify} the right-hand side to + ${k+1}^2$, which proves the assertion. + \end{spfstep} + \end{spfcase} + \begin{spfstep}[type=conclusion] + We have considered all the cases, so we have proven the assertion. + \end{spfstep} + \end{spfcases} +\end{sproof} +\end{latexcode} + +This yields the following result: + +\begin{mdframed} + \begin{sproof}[id=simple-proof] + {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$} + \begin{spfcases}{For the induction we have to consider the following cases:} + \begin{spfcase}{$n=1$} + \begin{spfstep}[type=inline] then we compute $1=1^2$\end{spfstep} + \end{spfcase} + \begin{spfcase}{$n=2$} + \begin{spfcomment}[type=inline] + This case is not really necessary, but we do it for the fun + of it (and to get more intuition). + \end{spfcomment} + \begin{spfstep}[type=inline] + We compute $1+3=2^{2}=4$ + \end{spfstep} + \end{spfcase} + \begin{spfcase}{$n>1$} + \begin{spfstep}[type=hypothesis,id=ind-hyp] + Now, we assume that the assertion is true for a certain $k\geq 1$, i.e. + $\sum_{i=1}^k{(2i-1)}=k^{2}$. + \end{spfstep} + \begin{spfcomment} + 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}$. + \end{spfcomment} + \begin{spfstep}[id=splitit] + We obtain $\sum_{i=1}^{k+1}{(2i-1)}=\sum_{i=1}^k{(2i-1)}+2(k+1)-1$ + \spfjust[method=arith:split-sum]{by splitting the sum}. + \end{spfstep} + \begin{spfstep}[id=byindhyp] + Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$ + \spfjust[method=fertilize]{by \premise[ind-hyp]{inductive hypothesis}}. + \end{spfstep} + \begin{spfstep}[type=conclusion] + We can \spfjust[method=simplify-eq]{simplify the \justarg[rhs]{right-hand side}} to + $(k+1)^2$, which proves the assertion. + \end{spfstep} + \end{spfcase} + \begin{spfstep}[type=conclusion] + We have considered all the cases, so we have proven the assertion. + \end{spfstep} + \end{spfcases} +\end{sproof} +\end{mdframed} + +\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{environment}{spfstep} + Regular proof steps are marked up with the |step| environment, 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{environment} + +\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. The environment takes an optional + |KeyVal| argument, which can have the |method| key, whose value is the name of a proof + method (this will only need to mean something to the application that consumes the + semantic annotations). Furthermore, the justification can contain ``premises'' + (specifications to assertions that were used justify the step) and ``arguments'' + (other information taken into account by the proof method). +\end{function} + +\begin{function}{\premise} + The |\premise| macro allows to mark up part of the text as reference to an assertion + that is used in the argumentation. In the running example we have used the |\premise| + macro to identify the inductive hypothesis. +\end{function} + +\begin{function}{\justarg} + The |\justarg| macro is very similar to |\premise| with the difference that it is used + to mark up arguments to the proof method. Therefore the content of the first argument + is interpreted as a mathematical object rather than as an identifier as in the case of + |\premise|. In our example, we specified that the simplification should take place on + the right hand side of the equation. Other examples include proof methods that + instantiate. Here we would indicate the substituted object in a |\justarg| macro. +\end{function} + +Note that both |\premise| and |\justarg| can be used with an empty second argument to +mark up premises and arguments that are not explicitly mentioned in the text. + +\begin{environment}{subproof} + The |spfcases| 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{environment}{spfcases} + The |spfcases| environment is used to mark up a proof by cases. Technically it is a + variant of the |subproof| where the |method| is |by-cases|. Its contents are |spfcase| + environments that mark up the cases one by one. +\end{environment} + +\begin{environment}{spfcase} + The content of a |spfcases| environment are a sequence of case proofs marked up in the + |spfcase| environment, which takes an optional |KeyVal| argument for semantic + annotations. The second argument is used to specify the the description of the case + under consideration. The content of a |spfcase| environment is the same as that of a + |sproof|, i.e. |spfstep|s, |spfcomment|s, and |spfcases| environments. +\end{environment} + +\begin{function}{\spfcasesketch} + |\spfcasesketch| is a variant of the |spfcase| environment that takes the same + arguments, but instead of the |spfstep|s in the body uses a third argument for a proof + sketch. +\end{function} + +\begin{environment}{spfcomment} + The |spfcomment| environment is much like a |step|, only that it does not have an + object-level assertion of its own. Rather than asserting some fact that is relevant + for the proof, it is used to explain where the proof is going, what we are attempting + to to, or what we have achieved so far. As such, it cannot be the target of a + |\premise|. +\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{}|. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: + +% LocalWords: hypothesis,id geq splitit arith:split-sum byindhyp rhs proofend |