summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/stex/source/stex/sproof.dtx
diff options
context:
space:
mode:
Diffstat (limited to 'macros/latex/contrib/stex/source/stex/sproof.dtx')
-rw-r--r--macros/latex/contrib/stex/source/stex/sproof.dtx1053
1 files changed, 1053 insertions, 0 deletions
diff --git a/macros/latex/contrib/stex/source/stex/sproof.dtx b/macros/latex/contrib/stex/source/stex/sproof.dtx
new file mode 100644
index 0000000000..f3cbdb869a
--- /dev/null
+++ b/macros/latex/contrib/stex/source/stex/sproof.dtx
@@ -0,0 +1,1053 @@
+% \iffalse meta-comment
+% An Infrastructure for Structural Markup for Proofs
+% Copyright (c) 2019 Michael Kohlhase, all rights reserved
+% this file is released under the
+% LaTeX Project Public License (LPPL)
+%
+% The original of this file is in the public repository at
+% http://github.com/sLaTeX/sTeX/
+% \fi
+%
+% \iffalse
+%<*driver>
+\def\bibfolder{../../lib/bib}
+\input{../../doc/docheader}
+
+\begin{document}
+ \DocInput{\jobname.dtx}
+\end{document}
+%</driver>
+% \fi
+%
+% \iffalse\CheckSum{341}\fi
+%
+% ^^A \changes{v0.9}{2005/06/14}{First Version with Documentation}
+%
+% \GetFileInfo{sproof.sty}
+%
+% \title{\sTeX-Proofs: Structural Markup for Proofs\thanks{Version {\fileversion} (last revised
+% {\filedate})}}
+% \author{Michael Kohlhase, Dennis Müller\\
+% FAU Erlangen-N\"urnberg\\
+% \url{http://kwarc.info/kohlhase}}
+% \maketitle
+%
+%\ifinfulldoc\else
+% This is the documentation for the \pkg{stex-proofs} package.
+% For a more high-level introduction,
+% see \href{\basedocurl/manual.pdf}{the \sTeX Manual} or the
+% \href{\basedocurl/stex.pdf}{full \sTeX documentation}.
+%
+% \input{../../doc/packages/sproofs}
+% \fi
+%
+% \begin{documentation}
+%
+% The |sproof| package is part of the {\stex} collection, a version of {\TeX/\LaTeX} that
+% allows to markup {\TeX/\LaTeX} documents semantically without leaving the document
+% format, essentially turning {\TeX/\LaTeX} into a document format for mathematical
+% knowledge management (MKM).
+%
+% This package supplies macros and environment that allow to annotate the structure of
+% mathematical proofs in {\stex} files. This structure can be used by MKM systems for
+% added-value services, either directly from the \sTeX sources, or after translation.
+%
+% \newpage\tableofcontents\newpage
+%
+%\section{Introduction}\label{sec:sproof}
+%
+% The |sproof| ({\twintoo{semantic}{proofs}}) package supplies macros and environment that
+% allow to annotate the structure of mathematical proofs in {\stex} files. This structure
+% can be used by MKM systems for added-value services, either directly from the \sTeX
+% sources, or after translation. Even though it is part of the {\stex} collection, it can
+% be used independently, like it's sister package |statements|.
+%
+% {\stex} is a version of {\TeX/\LaTeX} that allows to markup {\TeX/\LaTeX} documents
+% semantically without leaving the document format, essentially turning {\TeX/\LaTeX} into
+% a document format for mathematical knowledge management (MKM).
+%
+% \begin{exfig}\scriptsize
+% \begin{verbatim}
+% \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{sproofcomment}[type=inline]
+% This case is not really necessary, but we do it for the
+% fun of it (and to get more intuition).
+% \end{sproofcomment}
+% \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{sproofcomment}
+% 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{sproofcomment}
+% \begin{spfstep}
+% We obtain $\sum_{i=1}^{k+1}{2i-1}=\sum_{i=1}^k{2i-1}+2(k+1)-1$
+% \begin{justification}[method=arith:split-sum]
+% by splitting the sum.
+% \end{justification}
+% \end{spfstep}
+% \begin{spfstep}
+% Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$
+% \begin{justification}[method=fertilize]
+% by inductive hypothesis.
+% \end{justification}
+% \end{spfstep}
+% \begin{spfstep}[type=conclusion]
+% We can \begin{justification}[method=simplify]simplify\end{justification}
+% 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{verbatim}
+% \vspace*{-.5cm}
+% \caption{A very explicit proof, marked up semantically}\label{fig:proof:src}
+% \end{exfig}
+%
+% We will go over the general intuition by way of our running example (see
+% Figure~\ref{fig:proof:src} for the source and Figure~\ref{fig:proof:result} for the
+% formatted result).\ednote{talk a bit more about proofs and their structure,... maybe
+% copy from OMDoc spec. }
+%
+% \section{The User Interface}
+%
+% \subsection{Package Options}\label{sec:user:options}
+%
+% The |sproof| package takes a single option: \DescribeMacro{showmeta}|showmeta|. If
+% this is set, then the metadata keys are shown (see~\cite{Kohlhase:metakeys} for details
+% and customization options).
+%
+% \subsection{Proofs and Proof steps}
+%
+% \DescribeEnv{sproof} The |proof| 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 |\step|, |proofcomment|, and
+% |pfcases| environments that are used to markup the proof steps. The |proof| environment
+% has a variant |Proof|, which does not use the proof end marker. This is convenient, if a
+% proof ends in a case distinction, which brings it's own proof end marker with it.
+% \DescribeEnv{sProof} The |Proof| environment is a variant of |proof| that does not mark
+% the end of a proof with a little box; presumably, since one of the subproofs already has
+% one and then a box supplied by the outer proof would generate an otherwise empty line.
+% \DescribeMacro{\spfidea} The |\spfidea| macro allows to give a one-paragraph
+% description of the proof idea.
+%
+% For one-line proof sketches, we use the \DescribeMacro{spfsketch}|\spfsketch| macro,
+% which takes the |KeyVal| argument as |sproof| and another one: a natural language text
+% that sketches the proof.
+%
+% \DescribeEnv{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.
+%
+% 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{exfig}
+% \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{sproofcomment}[type=inline]
+% This case is not really necessary, but we do it for the fun
+% of it (and to get more intuition).
+% \end{sproofcomment}
+% \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{sproofcomment}
+% 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{sproofcomment}
+% \begin{spfstep}[id=splitit]
+% We obtain $\sum_{i=1}^{k+1}{(2i-1)}=\sum_{i=1}^k{(2i-1)}+2(k+1)-1$
+% \begin{justification}[method=arith:split-sum]
+% by splitting the sum
+% \end{justification}
+% \end{spfstep}
+% \begin{spfstep}[id=byindhyp]
+% Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$
+% \begin{justification}[method=fertilize]
+% by \premise[ind-hyp]{inductive hypothesis}.
+% \end{justification}
+% \end{spfstep}
+% \begin{spfstep}[type=conclusion]
+% We can \begin{justification}[method=simplify-eq]
+% simplify the {\justarg[rhs]{right-hand side}}
+% \end{justification} 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}
+% \caption{The formatted result of the proof in Figure~\ref{fig:proof:src}}\label{fig:proof:result}
+% \end{exfig}
+%
+% \subsection{Justifications}
+%
+% \DescribeEnv{justification} This evidence is marked up with the |justification|
+% environment in the |sproof| 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).
+%
+% \DescribeMacro{\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 example in
+% Figure~\ref{fig:proof:src} we have used the |\premise| macro to identify the inductive
+% hypothesis.
+%
+% \DescribeMacro{\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.
+%
+% \subsection{Proof Structure}
+%
+% \DescribeEnv{subproof} The |pfcases| 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 \DescribeMacro{method}|method| key can be used to give the name of the
+% proof method executed to make this subproof.
+%
+% \DescribeEnv{spfcases} The |pfcases| 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.
+%
+% \DescribeEnv{spfcase} The content of a |pfcases| environment are a sequence of case
+% proofs marked up in the |pfcase| 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 |pfcase| environment is the same as that
+% of a |proof|, i.e. |step|s, |proofcomment|s, and |pfcases|
+% environments. \DescribeMacro{\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.
+%
+% \DescribeEnv{sproofcomment} The |proofcomment| 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|.
+%
+% \subsection{Proof End Markers}
+%
+% 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 |sproof| package provides the \DescribeMacro{\sproofend}|\sproofend| macro for
+% this. 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
+% \DescribeMacro{\sProofEndSymbol}|\sProofEndSymbol| configuration macro (e.g. by specifying
+% |\sProofEndSymbol{q.e.d}|).
+%
+% 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{}|.
+%
+% \subsection{Configuration of the Presentation}\label{sec:user:conf}
+%
+% Finally, we provide configuration hooks in Figure~\ref{fig:hooks} for the keywords in
+% proofs. These are mainly intended for package authors building on |statements|, e.g. for
+% multi-language support.\ednote{we might want to develop an extension
+% \texttt{sproof-babel} in the future.}.
+%\begin{figure}[ht]\centering
+% \begin{tabular}{|lll|}\hline
+% Environment & configuration macro & value\\\hline\hline
+% \texttt{sproof} & \texttt{\textbackslash spf@proof@kw} & \makeatletter\spf@proof@kw\\\hline
+% \texttt{sketchproof} & \texttt{\textbackslash spf@sketchproof@kw} & \makeatletter\spf@proofsketch@kw\\\hline
+% \end{tabular}
+% \caption{Configuration Hooks for Semantic Proof Markup}\label{fig:hooks}
+% \end{figure}
+% The proof step labels can be customized via the
+% \DescribeMacro{\pstlabelstyle}|\pstlabelstyle| macro: |\pstlabelstyle{|\meta{style}|}|
+% sets the style; see Figure~\ref{fig:pstlabel} for an overview of styles. Package writers
+% can add additional styles by adding a macro |\pst@make@label@|\meta{style} that takes
+% two arguments: a comma-separated list of ordinals that make up the prefix and the current
+% ordinal. Note that comma-separated lists can be conveniently iterated over by the
+% {\LaTeX} |\@for|\ldots|:=|\ldots|\do{|\ldots|}| macro; see Figure~\ref{fig:pstlabel} for
+% examples.
+%
+% \section{Limitations}\label{sec:limitations}
+%
+% In this section we document known limitations. If you want to help alleviate them,
+% please feel free to contact the package author. Some of them are currently discussed in
+% the \sTeX issue tracker at \cite{sTeX:github:on}.
+% \begin{enumerate}
+% \item The numbering scheme of proofs cannot be changed. It is more geared for teaching
+% proof structures (the author's main use case) and not for writing papers.\lec{reported
+% by Tobias Pfeiffer (fixed)}
+% \item currently proof steps are formatted by the {\LaTeX} |description| environment. We
+% would like to configure this, e.g. to use the |inparaenum| environment for more
+% condensed proofs. I am just not sure what the best user interface would be I can
+% imagine redefining an internal environment |spf@proofstep@list| or adding a key
+% |prooflistenv| to the |proof| environment that allows to specify the environment
+% directly. Maybe we should do both.
+% \end{enumerate}
+%
+% \end{documentation}
+%
+% \begin{implementation}
+%
+% \section{The Implementation}
+%
+% \subsection{Package Options}\label{sec:impl:options}
+%
+% We declare some switches which will modify the behavior according to the package
+% options. Generally, an option |xxx| will just set the appropriate switches to true
+% (otherwise they stay false).\ednote{need an implementation for {\latexml}}
+%
+% \begin{macrocode}
+%<*package>
+%<@@=stex_sproof>
+
+%%%%%%%%%%%%% sproof.dtx %%%%%%%%%%%%%
+
+% \end{macrocode}
+%
+%
+% \subsection{Proofs}\label{sec:impl:proofs}
+%
+% We first define some keys for the |proof| environment.
+% \begin{macrocode}
+\keys_define:nn { stex / spf } {
+ id .str_set_x:N = \spfid,
+ for .clist_set:N = \l_@@_spf_for_clist ,
+ from .tl_set:N = \l_@@_spf_from_tl ,
+ proofend .tl_set:N = \l_@@_spf_proofend_tl,
+ type .str_set_x:N = \spftype,
+ title .tl_set:N = \spftitle,
+ continues .tl_set:N = \l_@@_spf_continues_tl,
+ functions .tl_set:N = \l_@@_spf_functions_tl,
+ method .tl_set:N = \l_@@_spf_method_tl
+}
+\cs_new_protected:Nn \_@@_spf_args:n {
+ \str_clear:N \spfid
+ \tl_clear:N \l_@@_spf_for_tl
+ \tl_clear:N \l_@@_spf_from_tl
+ \tl_set:Nn \l_@@_spf_proofend_tl {\sproof@box}
+ \str_clear:N \spftype
+ \tl_clear:N \spftitle
+ \tl_clear:N \l_@@_spf_continues_tl
+ \tl_clear:N \l_@@_spf_functions_tl
+ \tl_clear:N \l_@@_spf_method_tl
+ \bool_set_false:N \l_@@_inc_counter_bool
+ \keys_set:nn { stex / spf }{ #1 }
+}
+% \end{macrocode}
+%
+% \begin{macro}{\c_@@_flow_str}
+% We define this macro, so that we can test whether the |display| key has the value |flow|
+% \begin{macrocode}
+\str_set:Nn\c_@@_flow_str{inline}
+% \end{macrocode}
+% \end{macro}
+%
+% For proofs, we will have to have deeply nested structures of enumerated list-like
+% environments. However, {\LaTeX} only allows |enumerate| environments up to nesting depth
+% 4 and general list environments up to listing depth 6. This is not enough for us.
+% Therefore we have decided to go along the route proposed by Leslie Lamport to use a
+% single top-level list with dotted sequences of numbers to identify the position in the
+% proof tree. Unfortunately, we could not use his |pf.sty| package directly, since it does
+% not do automatic numbering, and we have to add keyword arguments all over the place, to
+% accomodate semantic information.
+%
+% \begin{environment}{pst@with@label}
+% This environment manages\footnote{This gets the labeling right but only works 8 levels
+% deep} the path labeling of the proof steps in the description environment of the
+% outermost |proof| environment. The argument is the label prefix up to now; which we
+% cache in |\pst@label| (we need evaluate it first, since are in the right place
+% now!). Then we increment the proof depth which is stored in |\count10| (lower counters
+% are used by {\TeX} for page numbering) and initialize the next level counter
+% |\count\count10| with 1. In the end call for this environment, we just decrease the
+% proof depth counter by 1 again.
+% \begin{macrocode}
+\intarray_new:Nn\l_@@_counter_intarray{50}
+\cs_new_protected:Npn \sproofnumber {
+ \int_set:Nn \l_tmpa_int {1}
+ \bool_while_do:nn {
+ \int_compare_p:nNn {
+ \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int
+ } > 0
+ }{
+ \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int .
+ \int_incr:N \l_tmpa_int
+ }
+}
+\cs_new_protected:Npn \_@@_inc_counter: {
+ \int_set:Nn \l_tmpa_int {1}
+ \bool_while_do:nn {
+ \int_compare_p:nNn {
+ \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int
+ } > 0
+ }{
+ \int_incr:N \l_tmpa_int
+ }
+ \int_compare:nNnF \l_tmpa_int = 1 {
+ \int_decr:N \l_tmpa_int
+ }
+ \intarray_gset:Nnn \l_@@_counter_intarray \l_tmpa_int {
+ \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int + 1
+ }
+}
+
+\cs_new_protected:Npn \_@@_add_counter: {
+ \int_set:Nn \l_tmpa_int {1}
+ \bool_while_do:nn {
+ \int_compare_p:nNn {
+ \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int
+ } > 0
+ }{
+ \int_incr:N \l_tmpa_int
+ }
+ \intarray_gset:Nnn \l_@@_counter_intarray \l_tmpa_int { 1 }
+}
+
+\cs_new_protected:Npn \_@@_remove_counter: {
+ \int_set:Nn \l_tmpa_int {1}
+ \bool_while_do:nn {
+ \int_compare_p:nNn {
+ \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int
+ } > 0
+ }{
+ \int_incr:N \l_tmpa_int
+ }
+ \int_decr:N \l_tmpa_int
+ \intarray_gset:Nnn \l_@@_counter_intarray \l_tmpa_int { 0 }
+}
+% \end{macrocode}
+% \end{environment}
+%
+%
+%\begin{macro}{\sproofend}
+% This macro places a little box at the end of the line if there is space, or at the
+% end of the next line if there isn't
+% \begin{macrocode}
+\def\sproof@box{
+ \hbox{\vrule\vbox{\hrule width 6 pt\vskip 6pt\hrule}\vrule}
+}
+\def\sproofend{
+ \tl_if_empty:NF \l_@@_spf_proofend_tl {
+ \hfil\null\nobreak\hfill\l_@@_spf_proofend_tl\par\smallskip
+ }
+}
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{spf@*@kw}
+% \begin{macrocode}
+\def\spf@proofsketch@kw{Proof~Sketch}
+\def\spf@proof@kw{Proof}
+\def\spf@step@kw{Step}
+% \end{macrocode}
+% \end{macro}
+%
+% For the other languages, we set up triggers
+% \begin{macrocode}
+\AddToHook{begindocument}{
+ \ltx@ifpackageloaded{babel}{
+ \makeatletter
+ \clist_set:Nx \l_tmpa_clist {\bbl@loaded}
+ \clist_if_in:NnT \l_tmpa_clist {ngerman}{
+ \input{sproof-ngerman.ldf}
+ }
+ \clist_if_in:NnT \l_tmpa_clist {finnish}{
+ \input{sproof-finnish.ldf}
+ }
+ \clist_if_in:NnT \l_tmpa_clist {french}{
+ \input{sproof-french.ldf}
+ }
+ \clist_if_in:NnT \l_tmpa_clist {russian}{
+ \input{sproof-russian.ldf}
+ }
+ \makeatother
+ }{}
+}
+% \end{macrocode}
+%
+% \begin{macro}{spfsketch}
+% \begin{macrocode}
+\newcommand\spfsketch[2][]{
+ \begingroup
+ \let \premise \stex_proof_premise:
+ \_@@_spf_args:n{#1}
+ \stex_if_smsmode:TF {
+ \str_if_empty:NF \spfid {
+ \stex_ref_new_doc_target:n \spfid
+ }
+ }{
+ \seq_clear:N \l_tmpa_seq
+ \clist_map_inline:Nn \l_@@_spf_for_clist {
+ \tl_if_empty:nF{ ##1 }{
+ \stex_get_symbol:n { ##1 }
+ \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq {
+ \l_stex_get_symbol_uri_str
+ }
+ }
+ }
+ \exp_args:Nnx
+ \stex_annotate:nnn{proofsketch}{\seq_use:Nn \l_tmpa_seq {,}}{
+ \str_if_empty:NF \spftype {
+ \stex_annotate_invisible:nnn{type}{\spftype}{}
+ }
+ \clist_set:No \l_tmpa_clist \spftype
+ \tl_set:Nn \l_tmpa_tl {
+ \titleemph{
+ \tl_if_empty:NTF \spftitle {
+ \spf@proofsketch@kw
+ }{
+ \spftitle
+ }
+ }:~
+ }
+ \clist_map_inline:Nn \l_tmpa_clist {
+ \exp_args:No \str_if_eq:nnT \c_@@_flow_str {##1} {
+ \tl_clear:N \l_tmpa_tl
+ }
+ }
+ \str_if_empty:NF \spfid {
+ \stex_ref_new_doc_target:n \spfid
+ }
+ \l_tmpa_tl #2 \sproofend
+ }
+ }
+ \endgroup
+ \stex_smsmode_do:
+}
+
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{spfeq}
+% This is very similar to |\spfsketch|, but uses a computation array\ednote{This should
+% really be more like a tabular with an ensuremath in it. or invoke text on the last
+% column}\ednote{document above}
+% \begin{macrocode}
+\newenvironment{spfeq}[2][]{
+ \_@@_spf_args:n{#1}
+ \let \premise \stex_proof_premise:
+ \stex_if_smsmode:TF {
+ \str_if_empty:NF \spfid {
+ \stex_ref_new_doc_target:n \spfid
+ }
+ }{
+ \seq_clear:N \l_tmpa_seq
+ \clist_map_inline:Nn \l_@@_spf_for_clist {
+ \tl_if_empty:nF{ ##1 }{
+ \stex_get_symbol:n { ##1 }
+ \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq {
+ \l_stex_get_symbol_uri_str
+ }
+ }
+ }
+ \exp_args:Nnnx
+ \begin{stex_annotate_env}{spfeq}{\seq_use:Nn \l_tmpa_seq {,}}
+ \str_if_empty:NF \spftype {
+ \stex_annotate_invisible:nnn{type}{\spftype}{}
+ }
+
+ \clist_set:No \l_tmpa_clist \spftype
+ \tl_clear:N \l_tmpa_tl
+ \clist_map_inline:Nn \l_tmpa_clist {
+ \tl_if_exist:cT {_@@_spfeq_##1_start:}{
+ \tl_set:Nn \l_tmpa_tl {\use:c{_@@_spfeq_##1_start:}}
+ }
+ \exp_args:No \str_if_eq:nnT \c_@@_flow_str {##1} {
+ \tl_set:Nn \l_tmpa_tl {\use:n{}}
+ }
+ }
+ \tl_if_empty:NTF \l_tmpa_tl {
+ \_@@_spfeq_start:
+ }{
+ \l_tmpa_tl
+ }{~#2}
+ \str_if_empty:NF \spfid {
+ \stex_ref_new_doc_target:n \spfid
+ }
+ \begin{displaymath}\begin{array}{rcll}
+ }
+ \stex_smsmode_do:
+}{
+ \stex_if_smsmode:F {
+ \end{array}\end{displaymath}
+ \clist_set:No \l_tmpa_clist \spftype
+ \tl_clear:N \l_tmpa_tl
+ \clist_map_inline:Nn \l_tmpa_clist {
+ \tl_if_exist:cT {_@@_spfeq_##1_end:}{
+ \tl_set:Nn \l_tmpa_tl {\use:c{_@@_spfeq_##1_end:}}
+ }
+ }
+ \tl_if_empty:NTF \l_tmpa_tl {
+ \_@@_spfeq_end:
+ }{
+ \l_tmpa_tl
+ }
+ \end{stex_annotate_env}
+ }
+}
+
+\cs_new_protected:Nn \_@@_spfeq_start: {
+ \titleemph{
+ \tl_if_empty:NTF \spftitle {
+ \spf@proof@kw
+ }{
+ \spftitle
+ }
+ }:
+}
+\cs_new_protected:Nn \_@@_spfeq_end: {\sproofend}
+
+\newcommand\stexpatchspfeq[3][] {
+ \str_set:Nx \l_tmpa_str{ #1 }
+ \str_if_empty:NTF \l_tmpa_str {
+ \tl_set:Nn \_@@_spfeq_start: { #2 }
+ \tl_set:Nn \_@@_spfeq_end: { #3 }
+ }{
+ \exp_after:wN \tl_set:Nn \csname _@@_spfeq_#1_start:\endcsname{ #2 }
+ \exp_after:wN \tl_set:Nn \csname _@@_spfeq_#1_end:\endcsname{ #3 }
+ }
+}
+
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{environment}{sproof}
+% In this environment, we initialize the proof depth counter |\count10| to 10, and set
+% up the description environment that will take the proof steps. At the end of the
+% proof, we position the proof end into the last line.
+% \begin{macrocode}
+\newenvironment{sproof}[2][]{
+ \let \premise \stex_proof_premise:
+ \intarray_gzero:N \l_@@_counter_intarray
+ \intarray_gset:Nnn \l_@@_counter_intarray 1 1
+ \_@@_spf_args:n{#1}
+ \stex_if_smsmode:TF {
+ \str_if_empty:NF \spfid {
+ \stex_ref_new_doc_target:n \spfid
+ }
+ }{
+ \seq_clear:N \l_tmpa_seq
+ \clist_map_inline:Nn \l_@@_spf_for_clist {
+ \tl_if_empty:nF{ ##1 }{
+ \stex_get_symbol:n { ##1 }
+ \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq {
+ \l_stex_get_symbol_uri_str
+ }
+ }
+ }
+ \exp_args:Nnnx
+ \begin{stex_annotate_env}{sproof}{\seq_use:Nn \l_tmpa_seq {,}}
+ \str_if_empty:NF \spftype {
+ \stex_annotate_invisible:nnn{type}{\spftype}{}
+ }
+
+ \clist_set:No \l_tmpa_clist \spftype
+ \tl_clear:N \l_tmpa_tl
+ \clist_map_inline:Nn \l_tmpa_clist {
+ \tl_if_exist:cT {_@@_sproof_##1_start:}{
+ \tl_set:Nn \l_tmpa_tl {\use:c{_@@_sproof_##1_start:}}
+ }
+ \exp_args:No \str_if_eq:nnT \c_@@_flow_str {##1} {
+ \tl_set:Nn \l_tmpa_tl {\use:n{}}
+ }
+ }
+ \tl_if_empty:NTF \l_tmpa_tl {
+ \_@@_sproof_start:
+ }{
+ \l_tmpa_tl
+ }{~#2}
+ \str_if_empty:NF \spfid {
+ \stex_ref_new_doc_target:n \spfid
+ }
+ \begin{description}
+ }
+ \stex_smsmode_do:
+}{
+ \stex_if_smsmode:F{
+ \end{description}
+ \clist_set:No \l_tmpa_clist \spftype
+ \tl_clear:N \l_tmpa_tl
+ \clist_map_inline:Nn \l_tmpa_clist {
+ \tl_if_exist:cT {_@@_sproof_##1_end:}{
+ \tl_set:Nn \l_tmpa_tl {\use:c{_@@_sproof_##1_end:}}
+ }
+ }
+ \tl_if_empty:NTF \l_tmpa_tl {
+ \_@@_sproof_end:
+ }{
+ \l_tmpa_tl
+ }
+ \end{stex_annotate_env}
+ }
+}
+
+\cs_new_protected:Nn \_@@_sproof_start: {
+ \par\noindent\titleemph{
+ \tl_if_empty:NTF \spftype {
+ \spf@proof@kw
+ }{
+ \spftype
+ }
+ }:
+}
+\cs_new_protected:Nn \_@@_sproof_end: {\sproofend}
+
+\newcommand\stexpatchsproof[3][] {
+ \str_set:Nx \l_tmpa_str{ #1 }
+ \str_if_empty:NTF \l_tmpa_str {
+ \tl_set:Nn \_@@_sproof_start: { #2 }
+ \tl_set:Nn \_@@_sproof_end: { #3 }
+ }{
+ \exp_after:wN \tl_set:Nn \csname _@@_sproof_#1_start:\endcsname{ #2 }
+ \exp_after:wN \tl_set:Nn \csname _@@_sproof_#1_end:\endcsname{ #3 }
+ }
+}
+% \end{macrocode}
+% \end{environment}
+%
+% \begin{macro}{\spfidea}
+% \begin{macrocode}
+\newcommand\spfidea[2][]{
+ \_@@_spf_args:n{#1}
+ \titleemph{
+ \tl_if_empty:NTF \spftype {Proof~Idea}{
+ \spftype
+ }:
+ }~#2
+ \sproofend
+}
+% \end{macrocode}
+% \end{macro}
+%
+% The next two environments (proof steps) and comments, are mostly semantical, they take
+% |KeyVal| arguments that specify their semantic role. In draft mode, they read these
+% values and show them. If the surrounding proof had |display=flow|, then no new |\item| is
+% generated, otherwise it is. In any case, the proof step number (at the current level) is
+% incremented.
+% \begin{environment}{spfstep}
+% \begin{macrocode}
+\newenvironment{spfstep}[1][]{
+ \_@@_spf_args:n{#1}
+ \stex_if_smsmode:TF {
+ \str_if_empty:NF \spfid {
+ \stex_ref_new_doc_target:n \spfid
+ }
+ }{
+ \@in@omtexttrue
+ \seq_clear:N \l_tmpa_seq
+ \clist_map_inline:Nn \l_@@_spf_for_clist {
+ \tl_if_empty:nF{ ##1 }{
+ \stex_get_symbol:n { ##1 }
+ \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq {
+ \l_stex_get_symbol_uri_str
+ }
+ }
+ }
+ \exp_args:Nnnx
+ \begin{stex_annotate_env}{spfstep}{\seq_use:Nn \l_tmpa_seq {,}}
+ \str_if_empty:NF \spftype {
+ \stex_annotate_invisible:nnn{type}{\spftype}{}
+ }
+ \clist_set:No \l_tmpa_clist \spftype
+ \tl_set:Nn \l_tmpa_tl {
+ \item[\sproofnumber]
+ \bool_set_true:N \l_@@_inc_counter_bool
+ }
+ \clist_map_inline:Nn \l_tmpa_clist {
+ \exp_args:No \str_if_eq:nnT \c_@@_flow_str {##1} {
+ \tl_clear:N \l_tmpa_tl
+ }
+ }
+ \l_tmpa_tl
+ \tl_if_empty:NF \spftitle {
+ {(\titleemph{\spftitle})\enspace}
+ }
+ \str_if_empty:NF \spfid {
+ \stex_ref_new_doc_target:n \spfid
+ }
+ }
+ \stex_smsmode_do:
+ \ignorespacesandpars
+}{
+ \bool_if:NT \l_@@_inc_counter_bool {
+ \_@@_inc_counter:
+ }
+ \stex_if_smsmode:F {
+ \end{stex_annotate_env}
+ }
+}
+% \end{macrocode}
+% \end{environment}
+%
+% \begin{environment}{sproofcomment}
+% \begin{macrocode}
+\newenvironment{sproofcomment}[1][]{
+ \_@@_spf_args:n{#1}
+ \clist_set:No \l_tmpa_clist \spftype
+ \tl_set:Nn \l_tmpa_tl {
+ \item[\sproofnumber]
+ \bool_set_true:N \l_@@_inc_counter_bool
+ }
+ \clist_map_inline:Nn \l_tmpa_clist {
+ \exp_args:No \str_if_eq:nnT \c_@@_flow_str {##1} {
+ \tl_clear:N \l_tmpa_tl
+ }
+ }
+ \l_tmpa_tl
+}{
+ \bool_if:NT \l_@@_inc_counter_bool {
+ \_@@_inc_counter:
+ }
+}
+% \end{macrocode}
+% \end{environment}
+%
+% The next two environments also take a |KeyVal| argument, but also a regular one, which
+% contains a start text. Both environments start a new numbered proof level.
+%
+% \begin{environment}{subproof}
+% In the |subproof| environment, a new (lower-level) proproofof environment is started.
+% \begin{macrocode}
+\newenvironment{subproof}[2][]{
+ \_@@_spf_args:n{#1}
+ \stex_if_smsmode:TF{
+ \str_if_empty:NF \spfid {
+ \stex_ref_new_doc_target:n \spfid
+ }
+ }{
+ \seq_clear:N \l_tmpa_seq
+ \clist_map_inline:Nn \l_@@_spf_for_clist {
+ \tl_if_empty:nF{ ##1 }{
+ \stex_get_symbol:n { ##1 }
+ \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq {
+ \l_stex_get_symbol_uri_str
+ }
+ }
+ }
+ \exp_args:Nnnx
+ \begin{stex_annotate_env}{subproof}{\seq_use:Nn \l_tmpa_seq {,}}
+ \str_if_empty:NF \spftype {
+ \stex_annotate_invisible:nnn{type}{\spftype}{}
+ }
+
+ \clist_set:No \l_tmpa_clist \spftype
+ \tl_set:Nn \l_tmpa_tl {
+ \item[\sproofnumber]
+ \bool_set_true:N \l_@@_inc_counter_bool
+ }
+ \clist_map_inline:Nn \l_tmpa_clist {
+ \exp_args:No \str_if_eq:nnT \c_@@_flow_str {##1} {
+ \tl_clear:N \l_tmpa_tl
+ }
+ }
+ \l_tmpa_tl
+ \tl_if_empty:NF \spftitle {
+ {(\titleemph{\spftitle})\enspace}
+ }
+ {~#2}
+ \str_if_empty:NF \spfid {
+ \stex_ref_new_doc_target:n \spfid
+ }
+ }
+ \_@@_add_counter:
+ \stex_smsmode_do:
+}{
+ \_@@_remove_counter:
+ \bool_if:NT \l_@@_inc_counter_bool {
+ \_@@_inc_counter:
+ }
+ \stex_if_smsmode:F{
+ \end{stex_annotate_env}
+ }
+}
+% \end{macrocode}
+% \end{environment}
+%
+% \begin{environment}{spfcases}
+% In the |pfcases| environment, the start text is displayed as the first comment of the
+% proof.
+% \begin{macrocode}
+\newenvironment{spfcases}[2][]{
+ \tl_if_empty:nTF{#1}{
+ \begin{subproof}[method=by-cases]{#2}
+ }{
+ \begin{subproof}[#1,method=by-cases]{#2}
+ }
+}{
+ \end{subproof}
+}
+% \end{macrocode}
+% \end{environment}
+%
+% \begin{environment}{spfcase}
+% In the |pfcase| environment, the start text is displayed specification of the case
+% after the |\item|
+% \begin{macrocode}
+\newenvironment{spfcase}[2][]{
+ \_@@_spf_args:n{#1}
+ \stex_if_smsmode:TF {
+ \str_if_empty:NF \spfid {
+ \stex_ref_new_doc_target:n \spfid
+ }
+ }{
+ \seq_clear:N \l_tmpa_seq
+ \clist_map_inline:Nn \l_@@_spf_for_clist {
+ \tl_if_empty:nF{ ##1 }{
+ \stex_get_symbol:n { ##1 }
+ \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq {
+ \l_stex_get_symbol_uri_str
+ }
+ }
+ }
+ \exp_args:Nnnx
+ \begin{stex_annotate_env}{spfcase}{\seq_use:Nn \l_tmpa_seq {,}}
+ \str_if_empty:NF \spftype {
+ \stex_annotate_invisible:nnn{type}{\spftype}{}
+ }
+ \clist_set:No \l_tmpa_clist \spftype
+ \tl_set:Nn \l_tmpa_tl {
+ \item[\sproofnumber]
+ \bool_set_true:N \l_@@_inc_counter_bool
+ }
+ \clist_map_inline:Nn \l_tmpa_clist {
+ \exp_args:No \str_if_eq:nnT \c_@@_flow_str {##1} {
+ \tl_clear:N \l_tmpa_tl
+ }
+ }
+ \l_tmpa_tl
+ \tl_if_empty:nF{#2}{
+ \titleemph{#2}:~
+ }
+ }
+ \_@@_add_counter:
+ \stex_smsmode_do:
+}{
+ \_@@_remove_counter:
+ \bool_if:NT \l_@@_inc_counter_bool {
+ \_@@_inc_counter:
+ }
+ \stex_if_smsmode:F{
+ \clist_set:No \l_tmpa_clist \spftype
+ \tl_set:Nn \l_tmpa_tl{\sproofend}
+ \clist_map_inline:Nn \l_tmpa_clist {
+ \exp_args:No \str_if_eq:nnT \c_@@_flow_str {##1} {
+ \tl_clear:N \l_tmpa_tl
+ }
+ }
+ \l_tmpa_tl
+ \end{stex_annotate_env}
+ }
+}
+% \end{macrocode}
+% \end{environment}
+%
+% \begin{environment}{spfcase}
+% similar to |spfcase|, takes a third argument.
+% \begin{macrocode}
+\newcommand\spfcasesketch[3][]{
+ \begin{spfcase}[#1]{#2}#3\end{spfcase}
+}
+% \end{macrocode}
+% \end{environment}
+%
+% \subsection{Justifications}
+%
+% We define the actions that are undertaken, when the keys for justifications are
+% encountered. Here this is very simple, we just define an internal macro with the value,
+% so that we can use it later.
+% \begin{macrocode}
+\keys_define:nn { stex / just }{
+ id .str_set_x:N = \l_@@_just_id_str,
+ method .tl_set:N = \l_@@_just_method_tl,
+ premises .tl_set:N = \l_@@_just_premises_tl,
+ args .tl_set:N = \l_@@_just_args_tl
+}
+% \end{macrocode}
+%
+% The next three environments and macros are purely semantic, so we ignore the keyval
+% arguments for now and only display the content.\ednote{need to do something about the
+% premise in draft mode.}
+%
+% \begin{environment}{justification}
+% \begin{macrocode}
+\newenvironment{justification}[1][]{}{}
+% \end{macrocode}
+% \end{environment}
+%
+% \begin{macro}{\premise}
+% \begin{macrocode}
+\newcommand\stex_proof_premise:[2][]{#2}
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\justarg}
+% the |\justarg| macro is purely semantic, so we ignore the keyval arguments for now and
+% only display the content.
+% \begin{macrocode}
+\newcommand\justarg[2][]{#2}
+%</package>
+% \end{macrocode}
+% \end{macro}
+% \end{implementation}
+% \Finale
+\endinput
+%%% Local Variables:
+%%% mode: doctex
+%%% TeX-master: t
+%%% End:
+% LocalWords: GPL structuresharing STR sproof dtx CPERL keyval methodfalse env
+% LocalWords: methodtrue envtrue medhodtrue DefKeyVal Semiverbatim omdoc args
+% LocalWords: DefEnvironment OptionalKeyVals KeyVal omtext DefConstructor str
+% LocalWords: proofidea KeyVal pfstep DefCMPEnvironment KeyVal proofcomment eq
+% LocalWords: KeyVal pfcases KeyVal pfcase KeyVal extractBodyText unlist elsif
+% LocalWords: foreach getBody toString str str str LookupValue LastSeenCMP Thu
+% LocalWords: appendText getValue undef openElement closeElement DefMacro omd
+% LocalWords: afterClose nodeType childNodes firstCMP localname hasChildNodes
+% LocalWords: firstChild textContent removeChild iffalse kohlhase sref scsys
+% LocalWords: sproofs.sty sc sc mathml openmath latexml cmathml activemath geq
+% LocalWords: twintoo atwin atwintoo texttt fileversion maketitle stex newpage
+% LocalWords: tableofcontents newpage exfig scriptsize vspace ednote spfidea
+% LocalWords: spfidea spfsketch spfsketch spfstep justarg spfcases spfcase rhs
+% LocalWords: sproofcomment ind-hyp splitit arith byindhyp sproofend proofend
+% LocalWords: printbibliography textsf langle textsf langle ltxml ctancite spf
+% LocalWords: srefaddidkey pf.sty newenvironment hbox vrule vbox ifx showmeta
+% LocalWords: hrule vskip hrule vrule hfil nobreak hfill smallskip newcommand
+% LocalWords: stDMemph newcount endsproof xref doctex showmeta hline lec ldots
+% LocalWords: textbackslash makeatletter sketchproof compactenum tracissue
+% LocalWords: metakeys addmetakey metasetkeys stylable pstlabelstyle pstlabel
+% LocalWords: pstlabelstyle pstlabelstyle ldots ldots ensuremath inparaenum
+% LocalWords: nameuse prooflistenv spfcasesketch spfcasesketch spfeq rcll
+% LocalWords: displaymath noindent ignorespaces