diff options
author | Norbert Preining <norbert@preining.info> | 2022-02-26 03:00:34 +0000 |
---|---|---|
committer | Norbert Preining <norbert@preining.info> | 2022-02-26 03:00:34 +0000 |
commit | 740a11f29a3551babe3d7edbb57ac3baa2280a3f (patch) | |
tree | 5d6d449e762f5ab95042e3517d03c5ac3ddaf7c3 /macros/latex/contrib/stex/source/stex/sproof.dtx | |
parent | 157cc9e776520d0b7d488317a69a10d4ae4d493b (diff) |
CTAN sync 202202260300
Diffstat (limited to 'macros/latex/contrib/stex/source/stex/sproof.dtx')
-rw-r--r-- | macros/latex/contrib/stex/source/stex/sproof.dtx | 1053 |
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 |