diff options
Diffstat (limited to 'macros/latex/contrib/stex/doc/packages')
-rw-r--r-- | macros/latex/contrib/stex/doc/packages/stex-document-structure.tex | 26 | ||||
-rw-r--r-- | macros/latex/contrib/stex/doc/packages/stex-features.tex | 12 | ||||
-rw-r--r-- | macros/latex/contrib/stex/doc/packages/stex-hwexam.tex | 60 | ||||
-rw-r--r-- | macros/latex/contrib/stex/doc/packages/stex-idesetup.tex | 61 | ||||
-rw-r--r-- | macros/latex/contrib/stex/doc/packages/stex-mathhub.tex | 2 | ||||
-rw-r--r-- | macros/latex/contrib/stex/doc/packages/stex-mathhubsetup.tex | 25 | ||||
-rw-r--r-- | macros/latex/contrib/stex/doc/packages/stex-notesslides.tex (renamed from macros/latex/contrib/stex/doc/packages/stex-slides.tex) | 81 | ||||
-rw-r--r-- | macros/latex/contrib/stex/doc/packages/stex-problem.tex | 97 | ||||
-rw-r--r-- | macros/latex/contrib/stex/doc/packages/stex-proofs.tex | 425 | ||||
-rw-r--r-- | macros/latex/contrib/stex/doc/packages/stex-references.tex | 90 | ||||
-rw-r--r-- | macros/latex/contrib/stex/doc/packages/stex-setup.tex | 34 | ||||
-rw-r--r-- | macros/latex/contrib/stex/doc/packages/stex-symbols.tex | 8 |
12 files changed, 719 insertions, 202 deletions
diff --git a/macros/latex/contrib/stex/doc/packages/stex-document-structure.tex b/macros/latex/contrib/stex/doc/packages/stex-document-structure.tex index f8d570ea5e..f2cabec6c0 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-document-structure.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-document-structure.tex @@ -1,3 +1,4 @@ +\begin{sfragment}[id=sec:ds:intro]{Introduction} The \pkg{document-structure} package supplies an infrastructure for writing {\omdoc} documents in {\LaTeX}. This includes a simple structure sharing mechanism for \sTeX that allows to to move from a copy-and-paste document development model to a copy-and-reference model, which @@ -17,7 +18,9 @@ after translation. DAG models of documents allow to replace the ``Copy and Paste'' in the source document with a label-and-reference model where document are shared in the document source and the formatter does the copying during document formatting/presentation. +\end{sfragment} +\begin{sfragment}{Package Options} The \pkg{document-structure} package accepts the following options: \begin{center} \begin{tabular}{|l|p{10cm}|}\hline @@ -26,7 +29,9 @@ The \pkg{document-structure} package accepts the following options: \meta{sect} is \texttt{section}\\\hline \end{tabular} \end{center} +\end{sfragment} +\begin{sfragment}{Document Fragments} \begin{environment}{sfragment} The structure of the document is given by nested |sfragment| environments. In the {\LaTeX} route, the |sfragment| environment is flexibly mapped to sectioning commands, @@ -36,8 +41,8 @@ The \pkg{document-structure} package accepts the following options: sfragment. The optional metadata argument has the keys |id| for an identifier, |creators| and |contributors| for the Dublin Core metadata~\cite{DCMI:dmt03}. The option |short| allows to give a short title for the generated section. If the title contains - semantic macros, they need to be protected by |\protect|\ednote{MK: still?}, and we need - to give the |loadmodules| key it needs no value. For instance we would have + semantic macros, we need to give the |loadmodules| key (it needs no value). For instance + we would have \begin{latexcode} \begin{smodule}{foo} \symdef{bar}{B^a_r} @@ -90,9 +95,8 @@ Here we use two levels of |blindfragment|: the introductory remarks become a ``chapter'' instead of a ``part''. \item The inner one groups the frontmatter\footnote{We shied away from redefining the |frontmatter| to induce a blindfragment, but this may be the ``right'' way to go in - the future.} and makes the preface of the book a section-level construct.\ednote{MK: - We need a substitute for the ``Note that here the |display=flow| on the |sfragment| - environment prevents numbering as is traditional for prefaces.''} + the future.} and makes the preface of the book a section-level construct. The + |frontmatter| environment also suppresses numbering as is traditional for prefaces. \end{itemize} \end{environment} @@ -110,11 +114,13 @@ Here we use two levels of |blindfragment|: will\ldots'' in an |sfragment| environment, where we do not know which sectioning level we will end up. \end{function} +\end{sfragment} +\begin{sfragment}{Ending Documents Prematurely} \begin{function}{\prematurestop,\afterprematurestop} For prematurely stopping the formatting of a document, \sTeX provides the |\prematurestop| macro. It can be used everywhere in a document and ignores all input - after that -- backing out of the |sfragment| environment as needed. After that -- and + after that -- backing out of the |sfragment| environments as needed. After that -- and before the implicit |\end{document}| it calls the internal |\afterprematurestop|, which can be customized to do additional cleanup or e.g. print the bibliography. @@ -132,7 +138,12 @@ instance, the admin section of a course can be made course-independent (and ther re-usable) by using variables (actually token registers) |courseAcronym| and |courseTitle| instead of the text itself. The variables can then be set in the \sTeX preamble of the course notes file. - +\end{sfragment} + +\begin{sfragment}{Global Document Variables} + To make document fragments more reusable, we sometimes want to make the content depend + on the context. We use \defemph{document variables} for that. + \begin{function}{\setSGvar,\useSGvar} |\setSGvar{|\meta{vname}|}{|\meta{text}|}| to set the global variable \meta{vname} to \meta{text} and |\useSGvar{|\meta{vname}|}| to reference it. @@ -144,6 +155,7 @@ course notes file. variable \meta{vname}, only if (after expansion) it is equal to \meta{val}, the conditional text \meta{ctext} is formatted. \end{function} +\end{sfragment} %%% Local Variables: %%% mode: latex diff --git a/macros/latex/contrib/stex/doc/packages/stex-features.tex b/macros/latex/contrib/stex/doc/packages/stex-features.tex index b5ce5906d1..4e0cd21457 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-features.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-features.tex @@ -144,8 +144,16 @@ and be a \symname{monoid} on $\Int$ ... } - We will return to these two example later, when we also know - how to handle the \emph{axioms} of a monoid. + +We will return to these two example later, when we also know how to handle the +\emph{axioms} of a monoid. + +\begin{environment}{usestructure} + The |usestructure{<struct>}| environment is used in multilingual settings as a parallel + to the |mathstructure|. It opens a group and then issues a + |\usemodule{.../<struct>-structure}| that gives the body access to all the semantic + macros in the referenced structure. +\end{environment} \end{smodule} \end{sfragment} diff --git a/macros/latex/contrib/stex/doc/packages/stex-hwexam.tex b/macros/latex/contrib/stex/doc/packages/stex-hwexam.tex index 5aced96e66..a3679d0d94 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-hwexam.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-hwexam.tex @@ -1,15 +1,29 @@ - +\begin{sfragment}{Introduction} The \pkg{hwexam} package and class supplies an infrastructure that allows to format nice-looking assignment sheets by simply including problems from problem files marked up -with the \pkg{roblem} package. It is designed to be compatible with |problems.sty|, and +with the \pkg{problem} package. It is designed to be compatible with |problems.sty|, and inherits some of the functionality. +\end{sfragment} +\begin{sfragment}{Package Options} \begin{variable}{solutions,notes,hints,gnotes,pts,min} - The \pkg{wexam} package and class take the options |solutions|, |notes|, |hints|, + The \pkg{hwexam} package and class take the options |solutions|, |notes|, |hints|, |gnotes|, |pts|, |min|, and |boxed| that are just passed on to the \pkg{problems} package (cf. its documentation for a description of the intended behavior). \end{variable} +Furthermore, the \pkg{hwexam} package takes the option +\DescribeMacro{multiple}|multiple| that allows to combine multiple assignment sheets +into a compound document (the assignment sheets are treated as section, there is a table +of contents, etc.). + +Finally, there is the option \DescribeMacro{test}|test| that modifies the behavior to +facilitate formatting tests. Only in |test| mode, the macros |\testspace|, +|\testnewpage|, and |\testemptypage| have an effect: they generate space for the +students to solve the given problems. Thus they can be left in the {\LaTeX} source. +\end{sfragment} + +\begin{sfragment}{Assignments} This package supplies the \DescribeEnv{assignment}|assignment| environment that groups problems into assignment sheets. It takes an optional KeyVal argument with the keys \DescribeMacro{number}|number| (for the assignment number; if none is given, 1 is @@ -19,23 +33,22 @@ is referenced in the title of the assignment sheet), \DescribeMacro{type}|type| assignment type; e.g. ``quiz'', or ``homework''), \DescribeMacro{given}|given| (for the date the assignment was given), and \DescribeMacro{due}|due| (for the date the assignment is due). +\end{sfragment} -Furthermore, the \pkg{hwexam} package takes the option -\DescribeMacro{multiple}|multiple| that allows to combine multiple assignment sheets -into a compound document (the assignment sheets are treated as section, there is a table -of contents, etc.). - -Finally, there is the option \DescribeMacro{test}|test| that modifies the behavior to -facilitate formatting tests. Only in |test| mode, the macros |\testspace|, -|\testnewpage|, and |\testemptypage| have an effect: they generate space for the -students to solve the given problems. Thus they can be left in the {\LaTeX} source. +\begin{sfragment}{Including Assignments} +\begin{function}{\inputassignment} + The |\inputassignment| macro can be used to input an assignment from another file. It + takes an optional KeyVal argument and a second argument which is a path to the file + containing the problem (the macro assumes that there is only one |assignment| + environment in the included file). The keys |number|, |title|, |type|, |given|, and + |due| are just as for the |assignment| environment and (if given) overwrite the ones + specified in the |assignment| environment in the included file. +\end{function} +\end{sfragment} -\DescribeMacro{\testspace}|\testspace| takes an argument that expands to a dimension, -and leaves vertical space accordingly. \DescribeMacro{\testnewpage}|\testnewpage| makes -a new page in |test| mode, and \DescribeMacro{\testemptypage}|\testemptypage| generates -an empty page with the cautionary message that this page was intentionally left empty. +\begin{sfragment}{Typesetting Exams} -Finally, the \DescribeEnv{testheading}|\testheading| takes an optional keyword argument +The \DescribeEnv{testheading}|\testheading| takes an optional keyword argument where the keys \DescribeMacro{duration}|duration| specifies a string that specifies the duration of the test, \DescribeMacro{min}|min| specifies the equivalent in number of minutes, and \DescribeMacro{reqpts}|reqpts| the points that are required for a perfect @@ -68,17 +81,12 @@ Will result in \end{center} \ednote{MK: The first three ``problems'' come from the stex examples above, how do we get rid of this?} - -\begin{function}{\inputassignment} - The |\inputassignment| macro can be used to input an assignment from another file. It - takes an optional KeyVal argument and a second argument which is a path to the file - containing the problem (the macro assumes that there is only one |assignment| - environment in the included file). The keys |number|, |title|, |type|, |given|, and - |due| are just as for the |assignment| environment and (if given) overwrite the ones - specified in the |assignment| environment in the included file. -\end{function} +\end{sfragment} %%% Local Variables: %%% mode: latex %%% TeX-master: "../stex-manual" %%% End: + +% LocalWords: hwexam solutions,notes,hints,gnotes,pts,min gnotes testemptypage reqpts +% LocalWords: inputassignment reqpts hour,min 60,reqpts diff --git a/macros/latex/contrib/stex/doc/packages/stex-idesetup.tex b/macros/latex/contrib/stex/doc/packages/stex-idesetup.tex new file mode 100644 index 0000000000..b4d495b628 --- /dev/null +++ b/macros/latex/contrib/stex/doc/packages/stex-idesetup.tex @@ -0,0 +1,61 @@ +\begin{sfragment}{Setting up the \sTeX IDE} + + The \sTeX IDE consists of two components using the + \emph{Language Server Protocol (LSP)}: A \emph{client} + in the form of a VSCode extension, and a \emph{server} + included in the \mmt system. Installing the extension will + open up a setup routine that will guide you through the rest. + + \begin{sfragment}{The \sTeX VSCode Extension} + + If you have not already, you should first install the VSCode editor + available at \url{https://code.visualstudio.com/}. + + Next, open VSCode and install the \sTeX extension by clicking on + the \emph{extensions} menu on the very left of the VSCode window + and searching for ``sTeX'' in the + \emph{``Search Extensions in Marketplace''} field, as in + \autoref{fig:install}, and clicking the \emph{Install}-button + of the \sTeX extension by KWARC. + + \begin{figure} + \begin{center} + \includegraphics[width=0.6\textwidth]{img/vsc1.png} + \end{center} + \caption{Installing the \sTeX extension for VSCode}\label{fig:install} + \end{figure} + + \end{sfragment} + + \begin{sfragment}{Setting up \mmt} + + Next, open any directory (\texttt{File $\to$ Open Folder...}) that contains + a \verb|.tex|-file, and a setup window as in \autoref{fig:setup} + will pop up. Clik on the highlighted link `\emph{here}' and download + the latest version of the \texttt{MMT.jar} file (at least version 23.0.0) + anywhere you like. Then click the \emph{``Browse...''}-button + and select your freshly downloaded \texttt{MMT.jar}. + + If you have already set a system variable for your MathHub-directory, + you are now done and can click \emph{``Finish''}. If you have not, + you can now also enter a directory path in the lower text field, + and the VSCode extension will attempt to globally set one up + for you, depending on your operating system. + + \begin{figure} + \begin{center} + \includegraphics[width=\textwidth]{img/vsc2.png} + \end{center} + \caption{\sTeX Setup Routine}\label{fig:setup} + \end{figure} + + Once you click \emph{``Finish''}, the client will connect + to \url{https://stexmmt.mathhub.info/:sTeX}, query for + available archives, download the core libraries required + for all (or most) semantic services (\texttt{MMT/urtheories} + and \texttt{sTeX/meta-inf}) and set up \RusTeX for you + automatically. + + \end{sfragment} + + \end{sfragment}
\ No newline at end of file diff --git a/macros/latex/contrib/stex/doc/packages/stex-mathhub.tex b/macros/latex/contrib/stex/doc/packages/stex-mathhub.tex index fb872acfba..eb09414ac7 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-mathhub.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-mathhub.tex @@ -1,4 +1,4 @@ -\begin{sfragment}{The Local MathHub-Directory} +\begin{sfragment}[id=sec:localmh]{The Local MathHub-Directory} \stexcode"\usemodule", \stexcode"\importmodule", \stexcode"\inputref" etc. allow for including content modularly without having to specify absolute diff --git a/macros/latex/contrib/stex/doc/packages/stex-mathhubsetup.tex b/macros/latex/contrib/stex/doc/packages/stex-mathhubsetup.tex new file mode 100644 index 0000000000..7a653186b3 --- /dev/null +++ b/macros/latex/contrib/stex/doc/packages/stex-mathhubsetup.tex @@ -0,0 +1,25 @@ + \begin{sfragment}{Setting your MathHub Directory} + One of \sTeX's features is a proper \emph{module system} + of interconnected document snippets for mathematical + content. Analogously to \emph{object-oriented programming}, + it allows for ``object-oriented mathematics'' via individual + combinable and, importantly, \emph{reusable} modules, developed + collaboratively. + + To make use of such modules, the \sTeX system needs to be told + where to find them. There are several ways to do so (see + \sref[file=stex-mathhub]{sec:localmh}[in=../stex-manual, + title={\href{\basedocurl/stex-manual.pdf}{the \sTeX{}3 Manual}}]), + but the most convenient way to do so is via a system variable. + + To do so, create a directory \texttt{MathHub} somewhere on + your local file system and set the environment + variable \texttt{MATHHUB} to the file path to that directory. + + In linux, you can do so by writing + \begin{lstlisting}[language=bash] + export MATHHUB="/path/to/your/MathHub" + \end{lstlisting} + in your \verb|~/.profile| (for all shells) or \verb|~/.bashrc| + (for the bash terminal only) file. + \end{sfragment}
\ No newline at end of file diff --git a/macros/latex/contrib/stex/doc/packages/stex-slides.tex b/macros/latex/contrib/stex/doc/packages/stex-notesslides.tex index a900c1fcbb..75fd9ee9e8 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-slides.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-notesslides.tex @@ -1,4 +1,5 @@ -The \pkg{notesslides} document class is derived from |beamer.cls|~\cite{beamerclass:on}, +\begin{sfragment}{Introduction} + The \pkg{notesslides} document class is derived from |beamer.cls|~\cite{beamerclass:on}, it adds a ``notes version'' for course notes that is more suited to printing than the one supplied by |beamer.cls|. @@ -14,27 +15,36 @@ In practice we want to generate two documents from the same source: the slides f presentation in the lecture and the course notes as a narrative document for home study. To achieve this, the \pkg{notesslides} class has two modes: \emph{slides mode} and \emph{notes mode} which are determined by the package option. +\end{sfragment} + +\begin{sfragment}{Package Options} + The \pkg{notesslides} class takes a variety of class options: + + \begin{variable}{slides,notes} The options |slides| and |notes| switch between slides + mode and notes mode (see \sref{sec:user:notesslides}). + \end{variable} + + \begin{variable}{sectocframes} If the option |sectocframes| is given, then for the + |sfragment|s, special frames with the |sfragment| title (and number) are generated. + \end{variable} + \begin{variable}{frameimages,fiboxed} + If the option |frameimages| is set, then slide mode also shows the + |\frameimage|-generated frames (see \sref{sec:user:frameimage}). If also the |fiboxed| + option is given, the slides are surrounded by a box. + \end{variable} +\end{sfragment} + +\begin{sfragment}[id=sec:user:notesslides]{Notes and Slides} -\begin{variable}{slides,notes,sectocframes,frameimages,fiboxed} - The \pkg{notesslides} class takes a variety of class options: - \begin{itemize} - \item The options |slides| and |notes| switch between slides mode and notes mode (see - Section~\ref{sec:user:notesslides}). - \item If the option |sectocframes| is given, then for the |sfragment|s, special frames - with the |sfragment| title (and number) are generated. - \item If the option |frameimages| is set, then slide mode also shows the - |\frameimage|-generated frames (see section~\ref{sec:user:frameimage}). If also the - |fiboxed| option is given, the slides are surrounded by a box. - \end{itemize} -\end{variable} - -\begin{environment}{frame,note} +\begin{environment}{frame} Slides are represented with the |frame| environment just like in the \pkg{beamer} class, - see~\cite{Tantau:ugbc} for details. The \pkg{notesslides} class adds the |note| - environment for encapsulating the course note fragments.\footnote{MK: it would be very - nice, if we did not need this environment, and this should be possible in principle, - but not without intensive LaTeX trickery. Hints to the author are welcome.} + see~\cite{Tantau:ugbc} for details. +\end{environment} + +\begin{environment}{note} + The \pkg{notesslides} class adds the |note| environment for encapsulating the course + note fragments. \end{environment} \begin{dangerbox} @@ -86,6 +96,7 @@ here: least in conjunction with |\newpage|, frame numbering behaves funnily (we have tried to fix this, but who knows). \end{dangerbox} +\end{sfragment} \begin{function}{\inputref*} If we want to transclude a the contents of a file as a note, we can use a new variant @@ -101,6 +112,17 @@ here: |ndefinition|, |nexample|, |nsproof|, and |nassertion| environments. \end{environment} +\begin{sfragment}{Customizing Header and Footer Lines} + The \pkg{notesslides} package and class comes with a simple default theme named + \pkg{sTeX} that provided by the \pkg{beamterthemesTeX}. It is assumed as the default + theme for \sTeX-based notes and slides. + The result in |notes| mode (which is like the |slides| version except that the slide + hight is variable) is + + \includegraphics[width=.95\textwidth]{\libfolder{img/notes-frame}} + +The footer line can be customized. In particular the logos. + \begin{function} {\setslidelogo} The default logo provided by the \pkg{notesslides} package is the {\sTeX} logo it can be customized using |\setslidelogo{|\meta{logo name}|}|. @@ -108,10 +130,9 @@ here: \begin{function}{\setsource} The default footer line of the \pkg{notesslides} package mentions copyright and - licensing. In the \pkg{beamer} class, |\source| stores the author's name as the - copyright holder . By default it is \emph{Michael Kohlhase} in the \pkg{notesslides} - package since he is the main user and designer of this - package. |\setsource{|\meta{name}|}| can change the writer's name. + licensing. In \pkg{notesslides} |\source| stores the author's name as the copyright + holder. By default it is the author's name as defined in the |\author| macro in the + preamble. |\setsource{|\meta{name}|}| can change the writer's name. \end{function} \begin{function}{\setlicensing} @@ -120,8 +141,10 @@ here: hyperlink to the license logo. |\setlicensing[|\meta{url}|]{|\meta{logo name}|}| is used for customization, where \meta{url} is optional. \end{function} +\end{sfragment} -Sometimes, we want to integrate slides as images after all -- e.g. because we already +\begin{sfragment}[id=sec:user:frameimages]{Frame Images} + Sometimes, we want to integrate slides as images after all -- e.g. because we already have a PowerPoint presentation, to which we want to add \sTeX notes. \begin{function}{\frameimage,\mhframeimage} @@ -150,21 +173,28 @@ argument is redundant, so we can just use \begin{latexcode} \mhframeimage{baz/foobar} \end{latexcode} +\end{sfragment} \begin{function}{\textwarning} The |\textwarning| macro generates a warning sign: \textwarning \end{function} +\begin{sfragment}[id=sec:user:excursions]{Excursions} In course notes, we sometimes want to point to an ``excursion'' -- material that is either presupposed or tangential to the course at the moment -- e.g. in an appendix. The typical setup is the following: \begin{latexcode} -\excursion{founif}{../ex/founif}{We will cover first-order unification in} +\excursion{founif}{../fragments/founif.en} + {We will cover first-order unification in} ... \begin{appendix}\printexcursions\end{appendix} \end{latexcode} +It generates a paragraph that references the excursion whose source is in the file +|../fragments/founif.en.tex| and automatically books the file for the |\printexcursions| +command that is used here to put it into the appendix. We will look at the mechanics now. + \begin{function}{\excursion} The |\excursion{|\meta{ref}|}{|\meta{path}|}{|\meta{text}|}| is syntactic sugar for @@ -198,6 +228,7 @@ setup is the following: \end{note} \end{latexcode} \end{function} +\end{sfragment} \begin{dangerbox} When option |book| which uses |\pagestyle{headings}| is given and semantic macros are diff --git a/macros/latex/contrib/stex/doc/packages/stex-problem.tex b/macros/latex/contrib/stex/doc/packages/stex-problem.tex index a90c36412d..53316b28bc 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-problem.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-problem.tex @@ -1,4 +1,5 @@ -The \pkg{problem} package supplies an infrastructure that allows specify problem. Problems +\begin{sfragment}{Introduction} + The \pkg{problem} package supplies an infrastructure that allows specify problem. Problems are text fragments that come with auxiliary functions: hints, notes, and solutions\footnote{for the moment multiple choice problems are not supported, but may well be in a future version}. Furthermore, we can specify how long the solution to a @@ -7,7 +8,11 @@ solution. Finally, the \pkg{problem} package facilitates the management of problems in small files, so that problems can be re-used in multiple environment. +\end{sfragment} + +\begin{sfragment}{Problems and Solutions} + \begin{function}{solutions,notes,hints,gnotes,pts,min,boxed,test} The \pkg{problem} package takes the options |solutions| (should solutions be output?), |notes| (should the problem notes be presented?), |hints| (do we give the hints?), @@ -43,7 +48,7 @@ so that problems can be re-used in multiple environment. \begin{exnote} Justify your answer \end{exnote} -\begin{solution}[for=elefants,height=3cm] +\begin{solution}[for=elefants] Four, two in the front seats, and two in the back. \begin{gnote} if they do not give the justification deduct 5 pts @@ -66,7 +71,7 @@ so that problems can be re-used in multiple environment. \begin{environment}{hint,exnote,gnote} The |hint| and |exnote| environments can be used in a |problem| environment to give hints and to make notes that elaborate certain aspects of the problem. The |gnote| - (grading notes) environment can be used to document situtations that may arise in + (grading notes) environment can be used to document situations that may arise in grading. \end{environment} @@ -80,7 +85,22 @@ so that problems can be re-used in multiple environment. Also, sometimes, we want content (e.g. in an exam with master solutions) conditional on whether solutions are shown. This can be done with the |\ifsolutions| conditional. \end{function} +\end{sfragment} + +\begin{sfragment}{Markup for Added-Value Services} + +\begin{sparagraph} + The |problem| package is all about specifying the meaning of the various moving parts of + practice/exam problems. The motivation for the additional markup is that we can base + added-value services from these, for instance auto-grading and immediate feedback. + The simplest example of this are multiple-choice problems, where the |problem| package + allows to annotate answer options with the intended values and possibly feedback that + can be delivered to the users in an interactive setting. In this section we will give + some infrastructure for these, we expect that this will grow over time. +\end{sparagraph} + +\begin{sfragment}{Multiple Choice Blocks} \begin{environment}{mcb} Multiple choice blocks can be formatted using the |mcb| environment, in which single choices are marked up with |\mcc| macro. @@ -96,8 +116,8 @@ so that problems can be re-used in multiple environment. \item |feedback| for a short feedback text given to the student. \end{itemize} \end{function} - -If we start the solutions, then we get +What we see when this is formatted to PDF depends on the context. In solutions mode (we +start the solutions in the code fragment below) we get \stexexample{% \startsolutions @@ -111,8 +131,8 @@ If we start the solutions, then we get \end{mcb} \end{sproblem} } -without solutions (that is what the students see during the exam/quiz)\ednote{MK: that did -not work!} + +In ``exam mode'' where disable solutions (here via |\stopsolutions|) \stexexample{% \stopsolutions \begin{sproblem}[title=Functions,name=functions1] @@ -125,7 +145,44 @@ not work!} \end{mcb} \end{sproblem} } - +we get the questions without solutions (that is what the students see during the +exam/quiz). +\end{sfragment} + +\begin{sfragment}{Filling-In Concrete Solutions} +The next simplest situation, where we can implement auto-grading is the case where we +have fill-in-the-blanks + +\begin{function}{\fillinsol} + The |\fillinsol| macro takes\Ednote{for now; more to come} an a single argument, which + contains a concrete solution (i.e. a number, a string, \ldots), which generates a + fill-in-box in test mode: +\stexexample{% + \stopsolutions + \begin{sproblem}[id=elefants.fillin,title=Fitting Elefants] + How many Elefants can you fit into a Volkswagen beetle? \fillinsol{4} +\end{sproblem}} + and the actual solution in solutions mode: +\end{function} +\stexexample{% + \begin{sproblem}[id=elefants.fillin,title=Fitting Elefants] + How many Elefants can you fit into a Volkswagen beetle? \fillinsol{4} + \end{sproblem}} +If we do not want to leak information about the solution by the size of the blank we can +also give |\fillinsol| an optional argument with a size: |\fillinsol[3cm]{12}| makes a box + three cm wide. + + Obviously, the required argument of |\fillinsol| can be used for auto-grading. For + concrete data like numbers, this is immediate, for more complex data like strings ``soft + comparisons'' might be in order. \ednote{For the moment we only assume a single concrete + value as correct. In the future we will almost certainly want to extend the + functionality to multiple answer classes that allow different feedback like im + MCQ. This still needs a bit of design. Also we want to make the formatting of the + answer in solutions/test mode configurable.} +\end{sfragment} +\end{sfragment} + +\begin{sfragment}{Including Problems} \begin{function}{\includeproblem} The |\includeproblem| macro can be used to include a problem from another file. It takes an optional KeyVal argument and a second argument which is a path to the file containing @@ -144,8 +201,32 @@ The |\min| and |\pts| macros allow to specify (i.e. to print to the margin) the distribution of time and reward to parts of a problem, if the |pts| and |pts| options are set. This allows to give students hints about the estimated time and the points to be awarded. +\end{sfragment} + +\begin{sfragment}{Testing and Spacing} +The |problem| package is often used by the |hwexam| package, which is used to create +homework assignments and exams. Both of these have a ``test mode'' (invoked by the +package option |test|), where certain information --master solutions or feedback -- is +not shown in the presentation. + +\DescribeMacro{\testspace}|\testspace| takes an argument that expands to a dimension, and +leaves vertical space accordingly. Specific instances exist: +\DescribeMacro{\testsmallspace}|\testsmallspace|, +\DescribeMacro{\testsmallspace}|\testsmallspace|, +\DescribeMacro{\testsmallspace}|\testsmallspace| give small (1cm), medium (2cm), and big (3cm) +vertical space. + +\DescribeMacro{\testnewpage}|\testnewpage| makes a new page in |test| mode, and +\DescribeMacro{\testemptypage}|\testemptypage| generates an empty page with the cautionary +message that this page was intentionally left empty. +\end{sfragment} %%% Local Variables: %%% mode: latex %%% TeX-master: "../stex-manual" %%% End: + +% LocalWords: solutions,notes,hints,gnotes,pts,min,boxed,test gnotes elefants,pts gnote +% LocalWords: 2,title exnote hint,exnote,gnote ifsolutions mcb keyvals Ttext Ftext +% LocalWords: Functions,name F,feedback Nooooooooo,feedback 2,title includeproblem +% LocalWords: elefants.fillin,title diff --git a/macros/latex/contrib/stex/doc/packages/stex-proofs.tex b/macros/latex/contrib/stex/doc/packages/stex-proofs.tex index d06db1282f..9e6e44f5ca 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-proofs.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-proofs.tex @@ -1,100 +1,308 @@ +\begin{sfragment}{Proofs} + The \pkg{stex-proof} package supplies macros and environment that allow to annotate the structure of mathematical proofs in \sTeX document. This structure can be used by MKM systems for added-value services, either directly from the \sTeX sources, or after translation. -We will go over the general intuition by way of a running example: +Its central component is the |sproof|-environment, whose body consists +of: +\begin{itemize} + \item \emph{subproofs} via the |subproof|-environment, + \item \emph{proof steps} via the |\spfstep|, |\eqstep| + |\assumption|, and |\conclude| macros, and + \item \emph{comments}, via normal text without special markup. +\end{itemize} + +|sproof|, |subproof| and the various proof step macros take the following +optional arguments: +\begin{itemize} + \item[|id|] (\meta{string}) for referencing, + \item[|method|] (\meta{string}) the proof method (e.g. contradiction, induction,...) + \item[|term|] (\meta{token list}) the (ideally semantically-marked up) + proposition that is derived/proven by this proof/subproof/proof step. +\end{itemize} +Additionally, they take one mandatory argument for the document text +to be annotated, or (in the case of the environments) +as an introductory description of the proof itself. Since +the latter often contains the |term| to be derived +as text, alternatively to providing it as +an optional argument, the mandatory argument can use the +|\yield|-macro to mark it up in the text. + +The |sproof| and |subproof| environments additionally take +two optional arguments: +\begin{itemize} + \item[|for|] the symbol identifier/name corresponding to the |sassertion| + to be proven. This too subsumes |\yield| and the |term|-argument. + \item[|hide|] In the pdf, this only shows the mandatory argument text + and hides the body of the environment. In the HTML (as served by \mmt), + the bodies of all |proof| and |subproof| environments are \emph{collapsible}, + and |hide| collapses the body by default. +\end{itemize} + +\begin{smodule}{sproofs} + \symdef{coprime}[args=2]{#1 \comp\bot #2} + \symdef{realroot}[args=1]{\sqrt{#1}} + \symdecl{irrational}[args=1] + \symdecl{rational}[args=1] + \symdef{eq}[args=2]{#1 \comp= #2} + \symdef{ratfrac}[args=2,prec=1]{\frac{#1}{#2}} + \symdef{intpow}[args=2,prec=-1]{{#1}^{#2}} + \symdef{ratpow}[args=2]{{#1}^{#2}} + \symdef{inset}[args=ai]{#1\comp\in#2}{##1\comp,##2} + \symdef{Int}{\comp{\mathbb Z}} + \symdef{PosInt}{\comp{{\mathbb Z}^+}} + \symdef{inttimes}[args=2]{#1 #2} + \symdef{divides}[args=2]{#1\comp\|#2} + + \vardef{vara}{\comp a} + \vardef{varb}{\comp b} + \vardef{varc}{\comp c} + + \def\contradiction{} \begin{latexcode} -\begin{sproof}[id=simple-proof] + \begin{sassertion}[type=theorem,name=sqrt2irr] + \conclusion{\irrational{$\arg{\realroot{2}}$ is \comp{irrational}}}. +\end{sassertion} + +\begin{sproof}[for=sqrt2irr,method=contradiction]{By contradiction} + \assumption{Assume \yield{\rational{$\arg{\realroot{2}}$ is + \comp{rational}}}} + \begin{subproof}[method=straightforward]{Then + \yield{$\eq{\ratfrac{\intpow{\vara}{2}}{\intpow{\varb}2}}{2}$ + for some $\inset{\vara,\varb}\PosInt$ with + \coprime{$\arg{\vara},\arg{\varb}$ \comp{coprime}}}} + \assumption{By assumption, \yield{there are + $\inset{\vara,\varb}\PosInt $ with + $\realroot{2}=\ratfrac{\vara}{\varb}$}} + \spfstep{wlog, we can assume \coprime{$\arg{\vara},\arg{\varb}$ + to be \comp{coprime}}} + % a comment: + If not, reduce the fraction until numerator and denominator + are coprime, and let the resulting components be + $\vara $ and $\varb $ + \spfstep{Then \yield{$\eq{\intpow{\ratfrac{\vara}{\varb}}2}2$}} + \eqstep{\ratfrac{\intpow{\vara}2}{\intpow{\varb}2}} + \end{subproof} + \begin{subproof}[term=\divides{2}{\vara},method=straightforward]{ + Then $\vara $ is even} + \spfstep{Multiplying the equation by $\intpow{\varb}2$ yields + $\yield{\eq{\intpow{\vara}2}{\inttimes{2}{\intpow{\varb}2}}}$} + \spfstep[term=\divides{2}{\intpow{\vara}2}]{Hence + $\intpow{\vara}2$ is even} + \conclude[term=\divides{2}{\vara}]{Hence $\vara $ is even as well} + % another comment: + Hint: Think about the prime factorizations of $\vara $ and + $\intpow{\vara}2$ + \end{subproof} + \begin{subproof}[term=\divides{2}{\varb},method=straightforward,]{ + Then $\varb $ is also even} + \spfstep{Since $\vara $ is even, we have \yield{some $\varc $ + such that $\eq{\inttimes{2}{\varc}}{\vara}$}} + \spfstep{Plugging into the above, we get + \yield{$\eq{\intpow{\inttimes{2}{\vara}}2} + {\inttimes{2}{\intpow{\varb}2}}$}} + \eqstep{\inttimes{4}{\intpow{\vara}2}} + \spfstep{Dividing both sides by $2$ yields + \yield{$\eq{\intpow{\varb}2}{\inttimes{2}{\intpow{\vara}2}}$}} + \spfstep[term=\divides{2}{\intpow{\varb}2}]{Hence + $\intpow{\varb}2$ is even} + \conclude[term=\divides{2}{\varb}]{Hence $\varb $ is even} + % one more comment: + By the same argument as above + \end{subproof} + \conclude[term=\contradiction]{Contradiction to $\vara,\varb $ being + \symname{coprime}.} +\end{sproof} +\end{latexcode} + +which will produce: + +\begin{mdframed} +\begin{sassertion}[type=theorem,name=sqrt2irr] + \conclusion{\irrational{$\arg{\realroot2}$ is \comp{irrational}}}. +\end{sassertion} + +\begin{sproof}[for=sqrt2irr,method=contradiction]{By contradiction} + \assumption{Assume \yield{\rational{$\arg{\realroot2}$ is \comp{rational}}}} + \begin{subproof}[method=straightforward]% + {Then \yield{$\eq{\ratfrac{\intpow \vara2}{\intpow \varb2}}{2}$ for some $\inset{\vara,\varb}\PosInt$ with \coprime{$\arg \vara,\arg \varb$ \comp{coprime}}}} + \assumption{By assumption, \yield{there are $\inset{\vara,\varb}\PosInt$ with $\realroot2=\ratfrac\vara\varb$}} + \spfstep{wlog, we can assume \coprime{$\arg{\vara},\arg{\varb}$ to be \comp{coprime}}} + If not, reduce the fraction until numerator and denominator are + coprime, and let the resulting components be $\vara$ and $\varb$ + \spfstep{Then \yield{$\eq{\intpow{\ratfrac\vara\varb}2}2$}} + \eqstep{\ratfrac{\intpow\vara2}{\intpow\varb2}} + \end{subproof} + \begin{subproof}[term=\divides{2}{\vara},method=straightforward]{Then $\vara$ is even} + \spfstep{Multiplying the equation by $\intpow\varb2$ yields $\yield{\eq{\intpow\vara2}{\inttimes2{\intpow\varb2}}}$} + \spfstep[term=\divides{2}{\intpow\vara2}]{Hence $\intpow\vara2$ is even} + \conclude[term=\divides{2}{\vara}]{Hence $\vara$ is even as well} + Hint: Think about the prime factorizations of $\vara$ and $\intpow\vara2$ + \end{subproof} + \begin{subproof}[term=\divides{2}{\varb},method=straightforward]{Then $\varb$ is also even} + \spfstep{Since $\vara$ is even, we have \yield{some $\varc$ such that $\eq{\inttimes2\varc}{\vara}$}} + \spfstep{Plugging into the above, we get \yield{$\eq{\intpow{\inttimes2\vara}2}{\inttimes2{\intpow\varb2}}$}} + \eqstep{\inttimes4{\intpow\vara2}} + \spfstep{Dividing both sides by $2$ yields \yield{$\eq{\intpow\varb2}{\inttimes2{\intpow\vara2}}$}} + \spfstep[term=\divides{2}{\intpow\varb2}]{Hence $\intpow\varb2$ is even} + \conclude[term=\divides{2}{\varb}]{Hence $\varb$ is even} + By the same argument as above + \end{subproof} + \conclude[term=\contradiction]{Contradiction to $\vara,\varb$ being \symname{coprime}.} +\end{sproof} +\end{mdframed} + +If we mark all subproofs with |hide|, we will obtain the following +instead: + +\begin{mdframed} + \begin{sassertion}[type=theorem,name=sqrt2irr] + \conclusion{\irrational{$\arg{\realroot2}$ is \comp{irrational}}}. + \end{sassertion} + + \begin{sproof}[for=sqrt2irr,method=contradiction]{By contradiction} + \assumption{Assume \yield{\rational{$\arg{\realroot2}$ is \comp{rational}}}} + \begin{subproof}[hide,method=straightforward]% + {Then \yield{$\eq{\ratfrac{\intpow \vara2}{\intpow \varb2}}{2}$ for some $\inset{\vara,\varb}\PosInt$ with \coprime{$\arg \vara,\arg \varb$ \comp{coprime}}}} + \assumption{By assumption, \yield{there are $\inset{\vara,\varb}\PosInt$ with $\realroot2=\ratfrac\vara\varb$}} + \spfstep{wlog, we can assume \coprime{$\arg{\vara},\arg{\varb}$ to be \comp{coprime}}} + If not, reduce the fraction until numerator and denominator are + coprime, and let the resulting components be $\vara$ and $\varb$ + \spfstep{Then \yield{$\eq{\intpow{\ratfrac\vara\varb}2}2$}} + \eqstep{\ratfrac{\intpow\vara2}{\intpow\varb2}} + \end{subproof} + \begin{subproof}[hide,term=\divides{2}{\vara},method=straightforward]{Then $\vara$ is even} + \spfstep{Multiplying the equation by $\intpow\varb2$ yields $\yield{\eq{\intpow\vara2}{\inttimes2{\intpow\varb2}}}$} + \spfstep[term=\divides{2}{\intpow\vara2}]{Hence $\intpow\vara2$ is even} + \conclude[term=\divides{2}{\vara}]{Hence $\vara$ is even as well} + Hint: Think about the prime factorizations of $\vara$ and $\intpow\vara2$ + \end{subproof} + \begin{subproof}[hide,term=\divides{2}{\varb},method=straightforward,]{Then $\varb$ is also even} + \spfstep{Since $\vara$ is even, we have \yield{some $\varc$ such that $\eq{\inttimes2\varc}{\vara}$}} + \spfstep{Plugging into the above, we get \yield{$\eq{\intpow{\inttimes2\vara}2}{\inttimes2{\intpow\varb2}}$}} + \eqstep{\inttimes4{\intpow\vara2}} + \spfstep{Dividing both sides by $2$ yields \yield{$\eq{\intpow\varb2}{\inttimes2{\intpow\vara2}}$}} + \spfstep[term=\divides{2}{\intpow\varb2}]{Hence $\intpow\varb2$ is even} + \conclude[term=\divides{2}{\varb}]{Hence $\varb$ is even} + By the same argument as above + \end{subproof} + \conclude[term=\contradiction]{Contradiction to $\vara,\varb$ being \symname{coprime}.} + \end{sproof} + \end{mdframed} + + However, the hidden subproofs will still be shown in the HTML, + only in an expandable section which is collapsed by default. + + +The above style of writing proofs is usually called \emph{structured proofs}. +They have a huge advantage over the traditional purely prosaic style, +in that (as the name suggests) the actual \emph{structure} of the proof +is made explicit, which almost always makes it considerably more +comprehensible. We, among many others, encourage the general use of +structured proofs. + +Alas, most proofs are not written in this style, and we would +do users a disservice by insisting on this style. For that reason, +the |spfblock| environment turns all subproofs and proof step +macros into presentationally neutral \emph{inline} annotations, +as in the induction step of the following example: + +\begin{latexcode} +\begin{sproof}[id=simple-proof,method=induction] {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$} - \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] + For the induction we have to consider three cases: % <- a comment + \begin{subproof}{$n=1$} + \spfstep*{then we compute $1=1^2$} + \end{subproof} + \begin{subproof}{$n=2$} This case is not really necessary, but we do it for the fun of it (and to get more intuition). - \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] + \spfstep*{We compute $1+3=2^{2}=4$.} + \end{subproof} + \begin{subproof}{$n>1$}\begin{spfblock} + \assumption[id=ind-hyp]{ Now, we assume that the assertion is true for a certain $k\geq 1$, - i.e. $\sum_{i=1}^k{(2i-1)}=k^{2}$. - \end{spfstep} - \begin{spfcomment} + i.e. \yield{$\sum_{i=1}^k{(2i-1)}=k^{2}$}. + } + We have to show that we can derive the assertion for $n=k+1$ from this assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$. - \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 + + \spfstep{ + We obtain $\yield{\sum_{i=1}^{k+1}{2i-1}= + \sum_{i=1}^k{2i-1}+2(k+1)-1}$ + \spfjust{by \splitsum{\comp{splitting the sum} + \arg*{$\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$}}}. + } + \spfstep{ + Thus we have $\yield{\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1}$ + \spfjust{by \symname{induction-hypothesis}}. + } + \conclude{ + We can \spfjust{\simplification{\comp{simplify} the right-hand side + \arg*{k^2+2k+1}}} to ${k+1}^2$, which proves the assertion. - \end{spfstep} - \end{spfcase} - \begin{spfstep}[type=conclusion] + } + \end{spfblock}\end{subproof} + \conclude{ We have considered all the cases, so we have proven the assertion. - \end{spfstep} - \end{spfcases} + } \end{sproof} \end{latexcode} + +\symdecl{splitsum}[args=1] +\symdecl{inducthypothesis}[name=induction-hypothesis] +\symdecl{simplification}[args=1] + This yields the following result: \begin{mdframed} - \begin{sproof}[id=simple-proof] - {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} + \begin{sproof}[id=simple-proof,method=induction] + {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$} + For the induction we have to consider three cases: % <- a comment + \begin{subproof}{$n=1$} + \spfstep*{then we compute $1=1^2$} + \end{subproof} + \begin{subproof}{$n=2$} + This case is not really necessary, but we do it for the + fun of it (and to get more intuition). + \spfstep*{We compute $1+3=2^{2}=4$.} + \end{subproof} + \begin{subproof}{$n>1$}\begin{spfblock} + \assumption[id=ind-hyp]{ + Now, we assume that the assertion is true for a certain $k\geq 1$, + i.e. \yield{$\sum_{i=1}^k{(2i-1)}=k^{2}$}. + } + + We have to show that we can derive the assertion for $n=k+1$ from + this assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$. + + \spfstep{ + We obtain $\yield{\sum_{i=1}^{k+1}{2i-1}=\sum_{i=1}^k{2i-1}+2(k+1)-1}$ + \spfjust{by \splitsum{\comp{splitting the sum}\arg*{$\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$}}}. + } + \spfstep{ + Thus we have $\yield{\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1}$ + \spfjust{by \symname{induction-hypothesis}}. + } + \conclude{ + We can \spfjust{\simplification{\comp{simplify} the right-hand side + \arg*{k^2+2k+1}}} to + ${k+1}^2$, which proves the assertion. + } + \end{spfblock}\end{subproof} + \conclude{ + We have considered all the cases, so we have proven the assertion. + } + \end{sproof} \end{mdframed} +\end{smodule} + \begin{environment}{sproof} The |sproof| environment is the main container for proofs. It takes an optional |KeyVal| argument that allows to specify the |id| (identifier) and |for| (for which assertion is @@ -114,78 +322,39 @@ This yields the following result: the proof. \end{function} -\begin{environment}{spfstep} - Regular proof steps are marked up with the |step| environment, which takes an optional +\begin{function}{\spfstep} + Regular proof steps are marked up with the |\spfstep| macro, which takes an optional |KeyVal| argument for annotations. A proof step usually contains a local assertion (the text of the step) together with some kind of evidence that this can be derived from already established assertions. -\end{environment} +\end{function} + +\begin{function}{\yield} + See above +\end{function} \begin{function}{\spfjust} This evidence is marked up with the |\spfjust| macro in the \pkg{stex-proofs} package. This environment totally invisible to the formatted result; it wraps the text - in the proof step that corresponds to the evidence. 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). + in the proof step that corresponds to the evidence (ideally, a + semantically marked-up term). \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. +\begin{function}{\assumption} + The |\assumption| macro allows to mark up a (justified) assumption. \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 + The |subproof| environment is used to mark up a subproof. This environment takes an optional |KeyVal| argument for semantic annotations and a second argument that allows to specify an introductory comment (just like in the |proof| environment). The |method| key can be used to give the name of the proof method executed to make this subproof. \end{environment} -\begin{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 @@ -205,10 +374,14 @@ in most cases, this is desirable to make the proof structure explicit, but somet wastes space (especially, if a proof ends in a case analysis which will supply its own proof end marker). To suppress it locally, just set |proofend={}| in them or use use |\sProofEndSymbol{}|. +\end{sfragment} %%% Local Variables: %%% mode: latex %%% TeX-master: "../stex-manual" %%% End: -% LocalWords: hypothesis,id geq splitit arith:split-sum byindhyp rhs proofend +% LocalWords: hypothesis,id geq splitit arith:split-sum byindhyp rhs proofend eqstep +% LocalWords: sproofs coprime ratfrac 2,prec intpow ratpow inttimes varb varc sqrt2irr +% LocalWords: theorem,name sqrt2irr,method wlog hide,method hide,term spfblock splitsum +% LocalWords: simple-proof,method inducthypothesis diff --git a/macros/latex/contrib/stex/doc/packages/stex-references.tex b/macros/latex/contrib/stex/doc/packages/stex-references.tex index 11de003e9b..3850d644ee 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-references.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-references.tex @@ -1,6 +1,90 @@ -\begin{sfragment}[id=sec.references]{Referencing Symbols and Statements} -\textcolor{red}{TODO: references documentation} -\end{sfragment} +If we take features like \stexcode"\inputref" and \stexcode"\mhinput" +(and the \stexcode"sfragment"-environment, see +\sref[file=stex-document-structure]{sec:ds:intro}[in=../stex-manual,title={the \sTeX{}3 manual}]) seriously, +and build large documents modularly from individually compiling documents for sections, chapters +and so on, cross-referencing becomes an interesting problem. + +Say, we have a document |main.tex|, which \stexcode"\inputref"s a section +|section1.tex|, which references a definition with label |some_definition| in +|section2.tex| (subsequently also inputted in |main.tex|). +Then the numbering of the definition will depend on the \emph{document context} +in which the document fragment |section2.tex| occurs - in |section2.tex| itself +(as a standalone document), it might be \emph{Definition 1}, in |main.tex| it might +be \emph{Definition 3.1}, and in |section1.tex|, the definition \emph{does not even occur}, so +it needs to be referenced by some other text. + +What we would want in that instance is an equivalent of \stexcode"\autoref", that takes +the document context into account to yield something like \emph{Definition 1}, \emph{Definition 3.1} +or ``\emph{Definition 1 in the section on Foo}'' respectively. + +The \stexcode"\sref" command attempts to do precisely that. Unlike plain \stexcode"\ref", \stexcode"\autoref" +etc., \stexcode"\sref" refers to not just a \emph{label}, but instead a pair consisting of a \emph{label} +and the \emph{document} in whose context we want to refer to it. Conversely, every \emph{document} +(i.e. standalone compilable |.tex|-file) keeps track of the ``names'' (\emph{Definition 3.1} etc.) for every +label as determined in the context of the document, and stores them in a dedicated file |\jobname.sref|. +Additionally, every document has a ``\emph{reference name}'' (e.g. ``\emph{the section on Foo}''). +This allows us to refer to ``label $x$ in document $D$'' to yield ``\emph{Definition 1 in the section on Foo}''. +And of course, \sTeX can decide based on the current document to either refer to the label by its +``full name'' or directly as e.g. \emph{Definition 3.1} depending on whether the label occurs in +the current document anyway (and link to it accordingly). + +\paragraph{} For that to work, we need to supply (up to) three pieces +of information: +\begin{itemize} + \item The \emph{label} of the reference target (e.g. |some_definition|), + \item (optionally) the \emph{file}/document containing the reference target + (e.g. |section2|). + This is not strictly necessary, but allows for additional disambiguation + between possibly duplicate labels across files, and + \item (optionally) the document context, in which we want to + refer to the reference target (e.g. |main|). +\end{itemize} +Additionally, the document in which we want to reference a label needs +a title for external references. + + +\begin{function}{\sref} + \begin{syntax} \cs{sref}|[archive=|\meta{archive1}|,file=|\meta{file}|]|% + \Arg{label}|[archive=|\meta{archive2}|,in=|\meta{document-context}|,title=|\meta{title}|]| \end{syntax} + This command references \meta{label} (declared in \meta{file} in \meta{archive1}). + If the object (section, figure, etc.) with that label occurs ultimately + in the same document, \cs{sref} will ignore the second set of optional arguments + and simply defer to \cs{autoref} if that command exists, or \cs{ref} if the \pkg{hyperref} + package is not included. + + If the referenced object does \emph{not} occur in the current document however, + \cs{sref} will refer to it by the object's name as it occurs in + the file \meta{document-context} in \meta{archive2}. + +For example, the reference to the \stexcode"sfragment"-environment above +will appear as ``subsection 7.2.1 (Introduction) in the \sTeX{}3 manual'' +if you are reading this in the package documentation for |stex-references| +directly, but as a linked ``subsection 7.2.1'' in the full documentation +or manual. This is achieved using + +\stexcode"\sref[file=stex-document-structure]{sec:ds:intro}[in=../stex-manual,title={the \sTeX{}3 manual}]". + +\end{function} + +For a further example, the following: +\begin{center} + \sref[file=../stex-doc]{part:extends}[in=../stex-doc,title={the full \sTeX{}3 documentation}] +\end{center} +will say ``Part III'' (and link accordingly) in the full documentation, +and ``Part III (Extensions) in the full \sTeX{}3 documentation'' +everywhere else. This is achieved using + +\stexcode"\sref[file=../stex-doc]{part:extends}[in=../stex-doc,title={the full \sTeX{}3 documentation}]". + +\begin{function}{\extref} + \begin{syntax} \cs{sref}|[archive=|\meta{archive1}|,file=|\meta{file}|]|% + \Arg{label}|{archive=|\meta{archive2}|,in=|\meta{document-context}|,title=|\meta{title}|}| \end{syntax} + The \cs{extref}-command behaves exactly like \cs{sref}, but takes + \emph{required} the document context argument and will always use it + for generating the document text, regardless of whether the label + occurs in the current document. +\end{function} + %%% Local Variables: %%% mode: latex diff --git a/macros/latex/contrib/stex/doc/packages/stex-setup.tex b/macros/latex/contrib/stex/doc/packages/stex-setup.tex new file mode 100644 index 0000000000..7e0e1fe4a4 --- /dev/null +++ b/macros/latex/contrib/stex/doc/packages/stex-setup.tex @@ -0,0 +1,34 @@ +\begin{sfragment}{Setting up the \sTeX Package} + + \begin{sfragment}[id=sec.minimal-setup]{Minimal Setup for the \sTeX Package} + In the best of all worlds, there is no setup, as you already have a new version of + {\TeX}Live on your system as a {\LaTeX} enthusiast. If not now is the time to + install it; see \cite{TeXLive:on}. You can usually update {\TeX}Live via a package + manager or the {\TeX}Live manager \textbf{tlmgr}. + \sTeX requires a \TeX{} kernel newer than February 2022. + + Alternatively, you can install \sTeX from CTAN, the Comprehensive {\TeX} Archive + Network; see \cite{stexCTAN:on} for details. We + assume you have the \sTeX package in at least version 3.2 (September 2022). + \end{sfragment} + + \begin{sfragment}[id=sec.git-setup]{GIT-based Setup for the \sTeX Development Version} + If you want use the latest and greatest \sTeX packages + that have not even been released to CTAN, + then you can directly clone them from the \sTeX development + repository \cite{sTeX:github:on} by the following command-line instructions: + \begin{lstlisting}[language=bash] + cd <stexdir> + git clone https://github.com/slatex/sTeX.git + \end{lstlisting} + and keep it updated by pulling updates via \lstinline|git pull| in the cloned \sTeX + directory. + Make sure to either clone the \sTeX repository into a local texmf-tree or to update your \lstinline|TEXINPUTS| environment variable, e.g. by placing the following line in your \lstinline|.bashrc|: + \begin{lstlisting}[language=bash] + export TEXINPUTS="$(TEXINPUTS):<sTeXDIR>//:" + \end{lstlisting} + \end{sfragment} + + \input{packages/stex-mathhubsetup} + +\end{sfragment}
\ No newline at end of file diff --git a/macros/latex/contrib/stex/doc/packages/stex-symbols.tex b/macros/latex/contrib/stex/doc/packages/stex-symbols.tex index e7bafeda6b..67e9a32e70 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-symbols.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-symbols.tex @@ -413,9 +413,9 @@ Note that the precise numbers used for precedences are pretty arbitrary - what m which precedences are higher than which other precedences when used in conjunction. \begin{variable}{\infprec,\neginfprec} It is occasionally useful to have ``infinitely'' high or low precedences to enforce or - forbid automated bracketing entirely -- for those purposes, \stexcode"\infprec" and - \stexcode"\neginfprec" exist (which are implemented as the maximal and minimal integer - values accordingly). + forbid automated bracketing entirely, e.g. for bracket-like notations such as intervals + -- for those purposes, \stexcode"\infprec" and \stexcode"\neginfprec" exist (which are + implemented as the maximal and minimal integer values accordingly).g \end{variable} \begin{dangerbox} @@ -499,7 +499,7 @@ which precedences are higher than which other precedences when used in conjuncti \vardef{varx}[name=x,type=\Nat]{\comp{x}} Given a function $\varf!:\funtype{\Nat}{\Nat}$, -by $\addition{\varf!,\varn}$ we mean the function +by $\addition{\varf!,\varn}$ we mean the function\rustexBREAK $\fun{\varx}{\varf{\addition{\varx,\varn}}}$ } |