summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/stex/doc/packages/stex-proofs.tex
diff options
context:
space:
mode:
Diffstat (limited to 'macros/latex/contrib/stex/doc/packages/stex-proofs.tex')
-rw-r--r--macros/latex/contrib/stex/doc/packages/stex-proofs.tex215
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