From e0c6872cf40896c7be36b11dcc744620f10adf1d Mon Sep 17 00:00:00 2001 From: Norbert Preining Date: Mon, 2 Sep 2019 13:46:59 +0900 Subject: Initial commit --- macros/latex/contrib/bussproofs-extra/LICENSE.txt | 416 +++++++++++++ macros/latex/contrib/bussproofs-extra/README.md | 16 + macros/latex/contrib/bussproofs-extra/bpextra.sty | 5 + .../contrib/bussproofs-extra/bussproofs-extra.dtx | 685 +++++++++++++++++++++ .../contrib/bussproofs-extra/bussproofs-extra.ins | 57 ++ .../contrib/bussproofs-extra/bussproofs-extra.pdf | Bin 0 -> 225363 bytes 6 files changed, 1179 insertions(+) create mode 100644 macros/latex/contrib/bussproofs-extra/LICENSE.txt create mode 100644 macros/latex/contrib/bussproofs-extra/README.md create mode 100644 macros/latex/contrib/bussproofs-extra/bpextra.sty create mode 100644 macros/latex/contrib/bussproofs-extra/bussproofs-extra.dtx create mode 100644 macros/latex/contrib/bussproofs-extra/bussproofs-extra.ins create mode 100644 macros/latex/contrib/bussproofs-extra/bussproofs-extra.pdf (limited to 'macros/latex/contrib/bussproofs-extra') diff --git a/macros/latex/contrib/bussproofs-extra/LICENSE.txt b/macros/latex/contrib/bussproofs-extra/LICENSE.txt new file mode 100644 index 0000000000..2244313901 --- /dev/null +++ b/macros/latex/contrib/bussproofs-extra/LICENSE.txt @@ -0,0 +1,416 @@ +The LaTeX Project Public License +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- + +LPPL Version 1.3c 2008-05-04 + +Copyright 1999 2002-2008 LaTeX3 Project + Everyone is allowed to distribute verbatim copies of this + license document, but modification of it is not allowed. + + +PREAMBLE +======== + +The LaTeX Project Public License (LPPL) is the primary license under +which the LaTeX kernel and the base LaTeX packages are distributed. + +You may use this license for any work of which you hold the copyright +and which you wish to distribute. This license may be particularly +suitable if your work is TeX-related (such as a LaTeX package), but +it is written in such a way that you can use it even if your work is +unrelated to TeX. + +The section `WHETHER AND HOW TO DISTRIBUTE WORKS UNDER THIS LICENSE', +below, gives instructions, examples, and recommendations for authors +who are considering distributing their works under this license. + +This license gives conditions under which a work may be distributed +and modified, as well as conditions under which modified versions of +that work may be distributed. + +We, the LaTeX3 Project, believe that the conditions below give you +the freedom to make and distribute modified versions of your work +that conform with whatever technical specifications you wish while +maintaining the availability, integrity, and reliability of +that work. If you do not see how to achieve your goal while +meeting these conditions, then read the document `cfgguide.tex' +and `modguide.tex' in the base LaTeX distribution for suggestions. + + +DEFINITIONS +=========== + +In this license document the following terms are used: + + `Work' + Any work being distributed under this License. + + `Derived Work' + Any work that under any applicable law is derived from the Work. + + `Modification' + Any procedure that produces a Derived Work under any applicable + law -- for example, the production of a file containing an + original file associated with the Work or a significant portion of + such a file, either verbatim or with modifications and/or + translated into another language. + + `Modify' + To apply any procedure that produces a Derived Work under any + applicable law. + + `Distribution' + Making copies of the Work available from one person to another, in + whole or in part. Distribution includes (but is not limited to) + making any electronic components of the Work accessible by + file transfer protocols such as FTP or HTTP or by shared file + systems such as Sun's Network File System (NFS). + + `Compiled Work' + A version of the Work that has been processed into a form where it + is directly usable on a computer system. This processing may + include using installation facilities provided by the Work, + transformations of the Work, copying of components of the Work, or + other activities. Note that modification of any installation + facilities provided by the Work constitutes modification of the Work. + + `Current Maintainer' + A person or persons nominated as such within the Work. If there is + no such explicit nomination then it is the `Copyright Holder' under + any applicable law. + + `Base Interpreter' + A program or process that is normally needed for running or + interpreting a part or the whole of the Work. + + A Base Interpreter may depend on external components but these + are not considered part of the Base Interpreter provided that each + external component clearly identifies itself whenever it is used + interactively. Unless explicitly specified when applying the + license to the Work, the only applicable Base Interpreter is a + `LaTeX-Format' or in the case of files belonging to the + `LaTeX-format' a program implementing the `TeX language'. + + + +CONDITIONS ON DISTRIBUTION AND MODIFICATION +=========================================== + +1. Activities other than distribution and/or modification of the Work +are not covered by this license; they are outside its scope. In +particular, the act of running the Work is not restricted and no +requirements are made concerning any offers of support for the Work. + +2. You may distribute a complete, unmodified copy of the Work as you +received it. Distribution of only part of the Work is considered +modification of the Work, and no right to distribute such a Derived +Work may be assumed under the terms of this clause. + +3. You may distribute a Compiled Work that has been generated from a +complete, unmodified copy of the Work as distributed under Clause 2 +above, as long as that Compiled Work is distributed in such a way that +the recipients may install the Compiled Work on their system exactly +as it would have been installed if they generated a Compiled Work +directly from the Work. + +4. If you are the Current Maintainer of the Work, you may, without +restriction, modify the Work, thus creating a Derived Work. You may +also distribute the Derived Work without restriction, including +Compiled Works generated from the Derived Work. Derived Works +distributed in this manner by the Current Maintainer are considered to +be updated versions of the Work. + +5. If you are not the Current Maintainer of the Work, you may modify +your copy of the Work, thus creating a Derived Work based on the Work, +and compile this Derived Work, thus creating a Compiled Work based on +the Derived Work. + +6. If you are not the Current Maintainer of the Work, you may +distribute a Derived Work provided the following conditions are met +for every component of the Work unless that component clearly states +in the copyright notice that it is exempt from that condition. Only +the Current Maintainer is allowed to add such statements of exemption +to a component of the Work. + + a. If a component of this Derived Work can be a direct replacement + for a component of the Work when that component is used with the + Base Interpreter, then, wherever this component of the Work + identifies itself to the user when used interactively with that + Base Interpreter, the replacement component of this Derived Work + clearly and unambiguously identifies itself as a modified version + of this component to the user when used interactively with that + Base Interpreter. + + b. Every component of the Derived Work contains prominent notices + detailing the nature of the changes to that component, or a + prominent reference to another file that is distributed as part + of the Derived Work and that contains a complete and accurate log + of the changes. + + c. No information in the Derived Work implies that any persons, + including (but not limited to) the authors of the original version + of the Work, provide any support, including (but not limited to) + the reporting and handling of errors, to recipients of the + Derived Work unless those persons have stated explicitly that + they do provide such support for the Derived Work. + + d. You distribute at least one of the following with the Derived Work: + + 1. A complete, unmodified copy of the Work; + if your distribution of a modified component is made by + offering access to copy the modified component from a + designated place, then offering equivalent access to copy + the Work from the same or some similar place meets this + condition, even though third parties are not compelled to + copy the Work along with the modified component; + + 2. Information that is sufficient to obtain a complete, + unmodified copy of the Work. + +7. If you are not the Current Maintainer of the Work, you may +distribute a Compiled Work generated from a Derived Work, as long as +the Derived Work is distributed to all recipients of the Compiled +Work, and as long as the conditions of Clause 6, above, are met with +regard to the Derived Work. + +8. The conditions above are not intended to prohibit, and hence do not +apply to, the modification, by any method, of any component so that it +becomes identical to an updated version of that component of the Work as +it is distributed by the Current Maintainer under Clause 4, above. + +9. Distribution of the Work or any Derived Work in an alternative +format, where the Work or that Derived Work (in whole or in part) is +then produced by applying some process to that format, does not relax or +nullify any sections of this license as they pertain to the results of +applying that process. + +10. a. A Derived Work may be distributed under a different license + provided that license itself honors the conditions listed in + Clause 6 above, in regard to the Work, though it does not have + to honor the rest of the conditions in this license. + + b. If a Derived Work is distributed under a different license, that + Derived Work must provide sufficient documentation as part of + itself to allow each recipient of that Derived Work to honor the + restrictions in Clause 6 above, concerning changes from the Work. + +11. This license places no restrictions on works that are unrelated to +the Work, nor does this license place any restrictions on aggregating +such works with the Work by any means. + +12. Nothing in this license is intended to, or may be used to, prevent +complete compliance by all parties with all applicable laws. + + +NO WARRANTY +=========== + +There is no warranty for the Work. Except when otherwise stated in +writing, the Copyright Holder provides the Work `as is', without +warranty of any kind, either expressed or implied, including, but not +limited to, the implied warranties of merchantability and fitness for a +particular purpose. The entire risk as to the quality and performance +of the Work is with you. Should the Work prove defective, you assume +the cost of all necessary servicing, repair, or correction. + +In no event unless required by applicable law or agreed to in writing +will The Copyright Holder, or any author named in the components of the +Work, or any other party who may distribute and/or modify the Work as +permitted above, be liable to you for damages, including any general, +special, incidental or consequential damages arising out of any use of +the Work or out of inability to use the Work (including, but not limited +to, loss of data, data being rendered inaccurate, or losses sustained by +anyone as a result of any failure of the Work to operate with any other +programs), even if the Copyright Holder or said author or said other +party has been advised of the possibility of such damages. + + +MAINTENANCE OF THE WORK +======================= + +The Work has the status `author-maintained' if the Copyright Holder +explicitly and prominently states near the primary copyright notice in +the Work that the Work can only be maintained by the Copyright Holder +or simply that it is `author-maintained'. + +The Work has the status `maintained' if there is a Current Maintainer +who has indicated in the Work that they are willing to receive error +reports for the Work (for example, by supplying a valid e-mail +address). It is not required for the Current Maintainer to acknowledge +or act upon these error reports. + +The Work changes from status `maintained' to `unmaintained' if there +is no Current Maintainer, or the person stated to be Current +Maintainer of the work cannot be reached through the indicated means +of communication for a period of six months, and there are no other +significant signs of active maintenance. + +You can become the Current Maintainer of the Work by agreement with +any existing Current Maintainer to take over this role. + +If the Work is unmaintained, you can become the Current Maintainer of +the Work through the following steps: + + 1. Make a reasonable attempt to trace the Current Maintainer (and + the Copyright Holder, if the two differ) through the means of + an Internet or similar search. + + 2. If this search is successful, then enquire whether the Work + is still maintained. + + a. If it is being maintained, then ask the Current Maintainer + to update their communication data within one month. + + b. If the search is unsuccessful or no action to resume active + maintenance is taken by the Current Maintainer, then announce + within the pertinent community your intention to take over + maintenance. (If the Work is a LaTeX work, this could be + done, for example, by posting to comp.text.tex.) + + 3a. If the Current Maintainer is reachable and agrees to pass + maintenance of the Work to you, then this takes effect + immediately upon announcement. + + b. If the Current Maintainer is not reachable and the Copyright + Holder agrees that maintenance of the Work be passed to you, + then this takes effect immediately upon announcement. + + 4. If you make an `intention announcement' as described in 2b. above + and after three months your intention is challenged neither by + the Current Maintainer nor by the Copyright Holder nor by other + people, then you may arrange for the Work to be changed so as + to name you as the (new) Current Maintainer. + + 5. If the previously unreachable Current Maintainer becomes + reachable once more within three months of a change completed + under the terms of 3b) or 4), then that Current Maintainer must + become or remain the Current Maintainer upon request provided + they then update their communication data within one month. + +A change in the Current Maintainer does not, of itself, alter the fact +that the Work is distributed under the LPPL license. + +If you become the Current Maintainer of the Work, you should +immediately provide, within the Work, a prominent and unambiguous +statement of your status as Current Maintainer. You should also +announce your new status to the same pertinent community as +in 2b) above. + + +WHETHER AND HOW TO DISTRIBUTE WORKS UNDER THIS LICENSE +====================================================== + +This section contains important instructions, examples, and +recommendations for authors who are considering distributing their +works under this license. These authors are addressed as `you' in +this section. + +Choosing This License or Another License +---------------------------------------- + +If for any part of your work you want or need to use *distribution* +conditions that differ significantly from those in this license, then +do not refer to this license anywhere in your work but, instead, +distribute your work under a different license. You may use the text +of this license as a model for your own license, but your license +should not refer to the LPPL or otherwise give the impression that +your work is distributed under the LPPL. + +The document `modguide.tex' in the base LaTeX distribution explains +the motivation behind the conditions of this license. It explains, +for example, why distributing LaTeX under the GNU General Public +License (GPL) was considered inappropriate. Even if your work is +unrelated to LaTeX, the discussion in `modguide.tex' may still be +relevant, and authors intending to distribute their works under any +license are encouraged to read it. + +A Recommendation on Modification Without Distribution +----------------------------------------------------- + +It is wise never to modify a component of the Work, even for your own +personal use, without also meeting the above conditions for +distributing the modified component. While you might intend that such +modifications will never be distributed, often this will happen by +accident -- you may forget that you have modified that component; or +it may not occur to you when allowing others to access the modified +version that you are thus distributing it and violating the conditions +of this license in ways that could have legal implications and, worse, +cause problems for the community. It is therefore usually in your +best interest to keep your copy of the Work identical with the public +one. Many works provide ways to control the behavior of that work +without altering any of its licensed components. + +How to Use This License +----------------------- + +To use this license, place in each of the components of your work both +an explicit copyright notice including your name and the year the work +was authored and/or last substantially modified. Include also a +statement that the distribution and/or modification of that +component is constrained by the conditions in this license. + +Here is an example of such a notice and statement: + + %% pig.dtx + %% Copyright 2005 M. Y. Name + % + % This work may be distributed and/or modified under the + % conditions of the LaTeX Project Public License, either version 1.3 + % of this license or (at your option) any later version. + % The latest version of this license is in + % http://www.latex-project.org/lppl.txt + % and version 1.3 or later is part of all distributions of LaTeX + % version 2005/12/01 or later. + % + % This work has the LPPL maintenance status `maintained'. + % + % The Current Maintainer of this work is M. Y. Name. + % + % This work consists of the files pig.dtx and pig.ins + % and the derived file pig.sty. + +Given such a notice and statement in a file, the conditions +given in this license document would apply, with the `Work' referring +to the three files `pig.dtx', `pig.ins', and `pig.sty' (the last being +generated from `pig.dtx' using `pig.ins'), the `Base Interpreter' +referring to any `LaTeX-Format', and both `Copyright Holder' and +`Current Maintainer' referring to the person `M. Y. Name'. + +If you do not want the Maintenance section of LPPL to apply to your +Work, change `maintained' above into `author-maintained'. +However, we recommend that you use `maintained', as the Maintenance +section was added in order to ensure that your Work remains useful to +the community even when you can no longer maintain and support it +yourself. + +Derived Works That Are Not Replacements +--------------------------------------- + +Several clauses of the LPPL specify means to provide reliability and +stability for the user community. They therefore concern themselves +with the case that a Derived Work is intended to be used as a +(compatible or incompatible) replacement of the original Work. If +this is not the case (e.g., if a few lines of code are reused for a +completely different task), then clauses 6b and 6d shall not apply. + + +Important Recommendations +------------------------- + + Defining What Constitutes the Work + + The LPPL requires that distributions of the Work contain all the + files of the Work. It is therefore important that you provide a + way for the licensee to determine which files constitute the Work. + This could, for example, be achieved by explicitly listing all the + files of the Work near the copyright notice of each file or by + using a line such as: + + % This work consists of all files listed in manifest.txt. + + in that place. In the absence of an unequivocal list it might be + impossible for the licensee to determine what is considered by you + to comprise the Work and, in such a case, the licensee would be + entitled to make reasonable conjectures as to which files comprise + the Work. + diff --git a/macros/latex/contrib/bussproofs-extra/README.md b/macros/latex/contrib/bussproofs-extra/README.md new file mode 100644 index 0000000000..a9a6d58b2f --- /dev/null +++ b/macros/latex/contrib/bussproofs-extra/README.md @@ -0,0 +1,16 @@ +bussproofs-extra +================ + +Additional functionality for bussproofs.sty. Specifically, it allows +for typesetting of entire (sub)deductions. + +To install, download the files, and run +``` +latex bussproofs-extra.ins +``` +To generate the documentation, run +``` +pdflatex bussproofs-extra.dtx +``` + +This package is distributed under the terms of the LPPL 1.3c diff --git a/macros/latex/contrib/bussproofs-extra/bpextra.sty b/macros/latex/contrib/bussproofs-extra/bpextra.sty new file mode 100644 index 0000000000..e83935d50d --- /dev/null +++ b/macros/latex/contrib/bussproofs-extra/bpextra.sty @@ -0,0 +1,5 @@ +% Wrapper for backwards compatibility + +\RequirePackage{bussproofs-extra} +\PackageWarning{bussproofs-extra}{You've loaded bussproofs with + bpextra, but you should use bussproofs-extra instead} diff --git a/macros/latex/contrib/bussproofs-extra/bussproofs-extra.dtx b/macros/latex/contrib/bussproofs-extra/bussproofs-extra.dtx new file mode 100644 index 0000000000..a371cff408 --- /dev/null +++ b/macros/latex/contrib/bussproofs-extra/bussproofs-extra.dtx @@ -0,0 +1,685 @@ +% \iffalse meta-comment +% +% +% Copyright (C) 2019 by Richard Zach +% ------------------------------------------------------ +% +% This work may be distributed and/or modified under the +% conditions of the LaTeX Project Public License, either version 1.3 +% of this license or (at your option) any later version. +% The latest version of this license is in +% http://www.latex-project.org/lppl.txt +% and version 1.3 or later is part of all distributions of LaTeX +% version 2005/12/01 or later. +% +% This work has the LPPL maintenance status `maintained'. +% +% The Current Maintainer of this work is Richard Zach. +% +% This work consists of the files bussproofs-pextra.dtx, +% bussproofs-extra.ins, bussproofs-extra.sty +% +% \fi +% +% \iffalse +%<*driver> +\ProvidesFile{bussproofs-extra.dtx} +% +%\NeedsTeXFormat{LaTeX2e} +%\ProvidesPackage{bussproofs-extra} +% [2019/05/31 0.4 Extra commands for bussproofs.sty] +%<*driver> +\documentclass{ltxdoc} + +\usepackage{bussproofs-extra} +\usepackage[colorlinks,allcolors=blue]{hyperref} +\usepackage{calc} + +\renewcommand{\fCenter}{\ensuremath{\,{\to}\,}} + +\EnableCrossrefs +\RecordChanges +\begin{document} + \DocInput{bussproofs-extra.dtx} + \PrintChanges +\end{document} +% +% \fi +% +% \CheckSum{0} +% +% \CharacterTable +% {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z +% Lower-case \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z +% Digits \0\1\2\3\4\5\6\7\8\9 +% Exclamation \! Double quote \" Hash (number) \# +% Dollar \$ Percent \% Ampersand \& +% Acute accent \' Left paren \( Right paren \) +% Asterisk \* Plus \+ Comma \, +% Minus \- Point \. Solidus \/ +% Colon \: Semicolon \; Less than \< +% Equals \= Greater than \> Question mark \? +% Commercial at \@ Left bracket \[ Backslash \\ +% Right bracket \] Circumflex \^ Underscore \_ +% Grave accent \` Left brace \{ Vertical bar \| +% Right brace \} Tilde \~} +% +% +% \changes{v0.4}{2019/05/31}{Better implementation of line labels; add +% shortDeduce; style deduce lines} +% \changes{v0.3}{2019/04/04}{Rename to bussproofs-extra.sty} +% \changes{v0.2}{2014/10/16}{Fixed bug in dotsdDeduce, added examples} +% \changes{v0.1}{2014/04/26}{Initial version with deduce, linelabel functionality} +% +% \GetFileInfo{bussproofs-extra.sty} +% +% \DoNotIndex{\newcommand,\newenvironment} +% +% +% \title{The \textsf{bussproofs-extra} package\thanks{This document +% corresponds to \textsf{bussproofs-extra}~\fileversion, dated \filedate.}} +% \author{\href{http://richardzach.org/}{Richard Zach}} +% \date{} +% +% \maketitle +% +% \section{Introduction} +% +% The \textsf{bussproofs-extra} package provides additional functionality for +% the proof tree typesetting package +% \href{http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/}{\textsf{bussproofs}} +% by Sam Buss. It is experimental and tested only with v.1.1, and +% only in \LaTeX{} mode with upward-growing trees. +% Functionality provided includes: +% +% \begin{enumerate} +% \item |\Deduce$| and |\DeduceC| commands, which work much +% like |\Infer| commands but indicate missing parts of a proof. +% \item Multiple styles for typesetting the result of |\Deduce|, +% including +% \begin{enumerate} +% \item |\straightDeduce|, which produces vertical dots +% \item |\branchDeduce|, which produces diagonal plus vertical dots +% \item |\ddotsDeduce|, which produces diagonal dots from top left +% to bottom right +% \item |\dotsdDeduce|, which produces diagonal dots from top right +% to bottom left +% \item |\shortDeduce|, which is like |\straightDeduce| but half the length +% \end{enumerate} +% |\straightDeduce| is the default. It can be changed by redefining +% |\alwaysDeduce|. +% \item |\LeftLineLabel| and |\RightLineLabel| commands which +% work like |\LeftLabel| and |\RightLabel| but place a label +% next to the conclusion of an inference/deduction instead of the score +% line. +% \item |\LeftSubproofLabel| and |\RightSubproofLabel| commands which +% work like |\LeftLabel| and |\RightLabel| but place a label +% next to the entire preceding subproof with a curly brace. +% \end{enumerate} +% +% Here's what these deductions look like: +% +% \begin{center} +% \begin{tabular}{@{}cccc@{}} +% \fbox{\AxiomC{$A$} +% \straightDeduce +% \DeduceC{$B$} +% \DisplayProof} & +% \fbox{\AxiomC{$A$} +% \branchDeduce +% \DeduceC{$B$} +% \DisplayProof} & +% \fbox{\AxiomC{$A$} +% \ddotsDeduce +% \DeduceC{$B$} +% \DisplayProof} & +% \fbox{\AxiomC{$A$} +% \dotsdDeduce +% \DeduceC{$B$} +% \DisplayProof} \\ \\ +% \fbox{\Axiom$A \fCenter B$ +% \straightDeduce +% \Deduce$A \lor C \fCenter B$ +% \DisplayProof} & +% \fbox{\Axiom$A \fCenter B$ +% \branchDeduce +% \Deduce$A \lor C \fCenter B$ +% \DisplayProof} & +% \fbox{\Axiom$A \fCenter B$ +% \ddotsDeduce +% \Deduce$A \lor C \fCenter B$ +% \DisplayProof} & +% \fbox{\Axiom$A \fCenter B$ +% \dotsdDeduce +% \Deduce$A \lor C \fCenter B$ +% \DisplayProof} +% \\ \\ +% \texttt{straightDeduce} & +% \texttt{branchDeduce} & +% \texttt{ddotsDeduce} & +% \texttt{dotsdDeduce} +% \end{tabular} +% \end{center} +% +% +% The most up-to-date version of this package is available at the +% \href{https://github.com/OpenLogicProject/bussproofs-extra}{Open Logic +% Project github site}, where you can file bug reports as well. +% +% \subsection{Example} +% +% \begin{verbatim} +% \begin{prooftree} +% \AxiomC{} +% \RightLabel{$\pi_1(a)$} +% \Deduce$\Gamma_1 \fCenter \Theta_1, F(a)$ +% \RightLabel{$\forall$R} +% \UnaryInf$\Gamma_1 \fCenter \Theta_1, \forall x\,F(x)$ +% \ddotsDeduce +% \RightLabel{$\pi_1'$} +% \Deduce$\Gamma \fCenter \Theta, \forall x\,F(x)$ +% \AxiomC{} +% \RightLabel{$\pi_2$} +% \Deduce$F(n), \Delta_1 \fCenter \Lambda_1$ +% \RightLabel{$\forall$L} +% \UnaryInf$\forall x\,F(x), \Delta_1 \fCenter \Lambda_1$ +% \dotsdDeduce +% \RightLabel{$\pi_2'$} +% \Deduce$\forall x\,F(x), \Delta \fCenter \Lambda$ +% \RightLabel{cut} +% \BinaryInf$\Gamma, \Delta \fCenter \Theta, \Lambda$ +% \RightLabel{$\pi_4$} +% \branchDeduce +% \Deduce$\Pi \fCenter \Xi$ +% \end{prooftree} +% \end{verbatim} +% produces this: +% \begin{prooftree} +% \AxiomC{} +% \RightLabel{$\pi_1(a)$} +% \Deduce$\Gamma_1 \fCenter \Theta_1, F(a)$ +% \RightLabel{$\forall$R} +% \UnaryInf$\Gamma_1 \fCenter \Theta_1, \forall x\,F(x)$ +% \ddotsDeduce +% \RightLabel{$\pi_1'$} +% \Deduce$\Gamma \fCenter \Theta, \forall x\,F(x)$ +% \AxiomC{} +% \RightLabel{$\pi_2$} +% \Deduce$F(n), \Delta_1 \fCenter \Lambda_1$ +% \RightLabel{$\forall$L} +% \UnaryInf$\forall x\,F(x), \Delta_1 \fCenter \Lambda_1$ +% \dotsdDeduce +% \RightLabel{$\pi_2'$} +% \Deduce$\forall x\,F(x), \Delta \fCenter \Lambda$ +% \RightLabel{cut} +% \BinaryInf$\Gamma, \Delta \fCenter \Theta, \Lambda$ +% \RightLabel{$\pi_4$} +% \branchDeduce +% \Deduce$\Pi \fCenter \Xi$ +% \end{prooftree} + +% It is also possible to label entire subproofs on the left and on the right. +% \begin{verbatim} +% \begin{prooftree} +% \AxiomC{} +% \Deduce$\Gamma \fCenter \Delta$ +% \LeftLineLabel{$S_1$} +% \Deduce$\Gamma \fCenter \Delta, A$ +% \LeftSubproofLabel{$\pi$} +% \AxiomC{} +% \Deduce$\Gamma' \fCenter \Delta'$ +% \LeftLineLabel{$S_2$} +% \Deduce$A, \Gamma' \fCenter \Delta'$ +% \RightSubproofLabel{$\pi'$} +% \RightLabel{cut} +% \LeftLineLabel{$S_3$} +% \BinaryInf$\Gamma, \Gamma' \fCenter \Delta, \Delta'$ +% \Deduce$\Pi \fCenter \Lambda$ +% \end{prooftree} +% \end{verbatim} +% \begin{prooftree} +% \AxiomC{} +% \Deduce$\Gamma \fCenter \Delta$ +% \Deduce$\Gamma \fCenter \Delta, A$ +% \LeftSubproofLabel{$\pi$} +% \AxiomC{} +% \Deduce$\Gamma' \fCenter \Delta'$ +% \Deduce$A, \Gamma' \fCenter \Delta'$ +% \RightSubproofLabel{$\pi'$} +% \RightLabel{cut} +% \BinaryInf$\Gamma, \Gamma' \fCenter \Delta, \Delta'$ +% \Deduce$\Pi \fCenter \Lambda$ +% \end{prooftree} +% +% The |\LeftLineLabel| and |\RightLineLabel| commands add labels to +% the sequent or formula produced by the following |\Axiom|, |\XxxxInf|, +% and |\Deduce| command. +% \begin{prooftree} +% \LeftLineLabel{$S_1$} +% \RightLineLabel{$S_1$} +% \Axiom$\phantom{A, {}}\Gamma \fCenter \Delta$ +% \LeftLineLabel{$S_2$} +% \RightLineLabel{$S_2$} +% \UnaryInf$A, \Gamma \fCenter \Delta, B$ +% \LeftLineLabel{$S_3$} +% \Deduce$\Pi \fCenter \Lambda$ +% \LeftLineLabel{$S_1'$} +% \AxiomC{\makebox[\widthof{$A \lor B$}][c]{$A$}} +% \LeftLineLabel{$S_2'$} +% \UnaryInfC{$A \lor B$} +% \LeftLineLabel{$S_3'$} +% \DeduceC{$C$} +% \LeftLineLabel{$S_4$} +% \BinaryInf$\Pi \fCenter \Lambda$ +% \RightLineLabel{$S_5$} +% \UnaryInf$\Pi \fCenter \Lambda$ +% \end{prooftree} +% If the sequent or formula is itself a premise of an |\XxxInf| +% command and the conclusion is longer, this may produce a less +% than optimal result, as the label is produced before the score +% line below (compare the left and right labels of the top left +% sequent above). In that case you may want to insert extra space +% using |\phantom|, or use |\makebox| and the |\widthof| command +% of the |calc| package for the |XxxC| variants of the commands +% (see the top right formula below) as in the |\Axiom| commands +% below. +% \begin{verbatim} +% \begin{prooftree} +% \LeftLineLabel{$S_1$} +% \RightLineLabel{$S_1$} +% \Axiom$\phantom{A, {}}\Gamma \fCenter \Delta$ +% \LeftLineLabel{$S_2$} +% \RightLineLabel{$S_2$} +% \UnaryInf$A, \Gamma \fCenter \Delta, B$ +% \LeftLineLabel{$S_3$} +% \Deduce$\Pi \fCenter \Lambda$ +% \LeftLineLabel{$S_1'$} +% \AxiomC{\makebox[\widthof{$A \lor B$}][c]{$A$}} +% \LeftLineLabel{$S_2'$} +% \UnaryInfC{$A \lor B$} +% \LeftLineLabel{$S_3'$} +% \DeduceC{$C$} +% \LeftLineLabel{$S_4$} +% \BinaryInf$\Pi \fCenter \Lambda$ +% \RightLineLabel{$S_5$} +% \UnaryInf$\Pi \fCenter \Lambda$ +% \end{prooftree} +% \end{verbatim} +% +% \StopEventually{} +% +% \section{Implementation} +% +% \subsection{Setup} +% +% We require \textsf{bussproofs} (obviously) and and \textsf{tikz} for +% drawing things. +% +% \begin{macrocode} +\RequirePackage{bussproofs} +\RequirePackage{tikz} +% \end{macrocode} +% \subsection{Dimensions and boxes} +% +% \textsf{bussproofs} aligns sequents at the right end of the sequent +% arrow, so we need to remember by how much to correct to get +% deductions to the middle of sequents. For |\ddotsDeduce| and +% |\dotsdDeduce| (diagonal) styles, the upper and lower sequents will be +% displaced. +% \begin{macrocode} +\newdimen\CenterCorrection +\newdimen\DiagCorrection +% \end{macrocode} +% We need two boxes to hold the left and right line labels. +% \begin{macrocode} +\newbox\myBoxLLL +\newbox\myBoxRLL +% \end{macrocode} +% \subsection{Deduce Styles} +% +% The following commands set the style for the next |\Deduce| +% command. |\straightDeduce| produces a simple vertical line of dots, +% and |\shortDeduce| a line of half that length. +% |\branchDeduce| produces centered branching (Takeuti/Gentzen-style) +% dots, |\ddotsDeduce| left-to-right diagonal dots, and |\dotsdDeduce| +% right-to-left diagonal dots. They do this by redefining the +% |\fDeduce| command which produces the dots and sets up the +% dimensions. The TikZ style |deduceLine| is used as argument to the +% |\draw| command and can be redefined for other line styles as well +% (e.g., smaller dots or closer spacing). +% \begin{macrocode} +\tikzset{ + deduceLine/.style = {line width=1.1pt, loosely dotted}} + +\def\straightDeduce{% + \gdef\fDeduce{\tikz\draw[deduceLine] (0,0) -- (0,1);} + \global\DiagCorrection=0pt + \ignorespaces +} + +\def\shortDeduce{% + \gdef\fDeduce{\tikz\draw[deduceLine] (0,0) -- (0,.5);} + \global\DiagCorrection=0pt + \ignorespaces +} + +\def\branchDeduce{% + \gdef\fDeduce{\begin{tikzpicture} + \draw[deduceLine] (0,0) -- (0,1); + \draw[deduceLine] (-.5,.5) -- (0,0); + \draw[deduceLine] (.5,.5) -- (0,0); + \end{tikzpicture}} + \global\DiagCorrection=0pt + \ignorespaces +} + +\def\ddotsDeduce{% + \gdef\fDeduce{\begin{tikzpicture} + \draw[deduceLine] (0,1) -- (1,0); + \end{tikzpicture}} + \setbox\myBoxA=\hbox{\fDeduce} + \global\DiagCorrection=-\wd\myBoxA + \ignorespaces +} + +\def\dotsdDeduce{% + \gdef\fDeduce{\begin{tikzpicture} + \draw[deduceLine] (1,1) -- (0,0); + \end{tikzpicture}} + \setbox\myBoxA=\hbox{\fDeduce} + \global\DiagCorrection=\wd\myBoxA + \ignorespaces +} +% \end{macrocode} +% The |\alwaysDeduce| command is used to (re)set the +% deduce style to a default and is executed every time a deduction is +% typeset. It can be redefined to change the default deduce style. +% \begin{macrocode} +\def\alwaysDeduce{\straightDeduce} +\straightDeduce +% \end{macrocode} +% \subsection{\texttt{\textbackslash Deduce\$} and +% \texttt{\textbackslash DeduceC}} +% +% |\Deduce$| and |\DeduceC| are the commands to actually produce the +% deductions. They are used and work just like |\UnaryInf$| and +% |\UnaryInfC|. +% \begin{macrocode} +\def\Deduce$#1\fCenter#2${% + \prepUnary% + \buildConclusion{#1}{#2}% + \setbox\myBoxA=\hbox{\fCenter}% + \global\CenterCorrection=-.5\wd\myBoxA + \joinDeduce% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\DeduceC#1{ + \prepUnary% + \buildConclusionC{#1}% + \global\CenterCorrection=0pt + \joinDeduce% + \resetInferenceDefaults% + \ignorespaces% +} +% \end{macrocode} +% \section{Typesetting the Deduction} +% +% |\joinDeduce| aligns and joins |\curBox| and |\myBoxC| into a single +% |vbox|. |\curBox| holds the upper proof, |\curScoreStart| is +% distance to where the line below the premise would start, +% |\curScoreCenter| is distance from left edge of score to the +% alignment point, and |\curScoreEnd| is width of the score line. +% \begin{macrocode} + +\def\joinDeduce{% + \global\advance\curCenter by -\hypKernAmt% +% \end{macrocode} +% If center of premise is left of center of conclusion move upper box +% to right by difference, else move lower box right by difference +% \begin{macrocode} + \ifnum\curCenter<\newCenter% + \displace=\newCenter% + \advance \displace by -\curCenter% + \kernUpperBox% + \else% + \displace=\curCenter% + \advance \displace by -\newCenter% + \kernLowerBox% + \fi% +% \end{macrocode} +% For |\ddotsDeduce|, move lower box right; for |\dotsdDeduce|, move +% upper box right; then set |\curCenter| to align with horizontal center +% of dots. +% \begin{macrocode} + \ifnum\DiagCorrection<0% + \displace=-\DiagCorrection + \kernLowerBox% + \else + \displace=\DiagCorrection + \kernUpperBox% + \fi% + \advance\curCenter by-.5\DiagCorrection +% \end{macrocode} +% Now we draw the deduction. +% \begin{macrocode} + \buildDeduce% +% \end{macrocode} +% Put the deduction and labels into a box. +% \begin{macrocode} + \buildScoreLabels% +% \end{macrocode} +% Put everything into a new box and compute the dimensions for the +% next |\Deduce| or |\XxxxInf|. +% \begin{macrocode} + \ifx\rootAtBottomFlag\myTrue% + \buildRootBottom% + \else% + \buildRootTop% + \fi% + \global \curScoreStart=\newScoreStart% + \global \curScoreEnd=\newScoreEnd% + \global \curCenter=\newCenter% +} +% \end{macrocode} +% |\buildDeduce| does for |\DeduceX| what |\buildInf| does for +% |\XxxInf|: put the deduction bit (dots) into a box and set the +% dimensions properly. +% \begin{macrocode} + +\def\buildDeduce{% + \global\setbox \myBoxD =% + \hbox{\fDeduce}% + \displace = \wd\myBoxD % find width of vdots +% \end{macrocode} +% set start and end of current score to left and right of the box +% holding the deduction. +% \begin{macrocode} + \global\curScoreStart = \curCenter% + \global\advance\curScoreStart by -.5\displace% + \global\curScoreEnd = \curCenter% + \global\advance\curScoreEnd by .5\displace% + \global\advance\curScoreStart by\CenterCorrection + \global\advance\curScoreEnd by\CenterCorrection +} +% \end{macrocode} +% \subsection{Line Labels} +% +% |\LeftLineLabel| and |\RightLineLabel| set the label to place to the +% left or right, respectively, of the conclusion of the next |\Axiom|, +% |\XxxInf| or |\Deduce| command. They are aligned with the text +% produced by |\LeftLabel| and |\RightLabel| (i.e., the distance to +% the line is $|\ScoreOverhang| + |\labelSpacing|$. +% \begin{macrocode} + +\def\LeftLineLabel#1{% + \global\def\displayLeftLineLabel{% + {#1\hskip\labelSpacing}} + \ignorespaces} + +\def\RightLineLabel#1{% + \global\def\displayRightLineLabel{% + {\hskip\labelSpacing #1}} + \ignorespaces} + +\global\let\displayLeftLineLabel\relax +\global\let\displayRightLineLabel\relax +% \end{macrocode} +% +% \subsection{Subproof Labels} +% Sometimes you'd like to lable entire subproofs. This is done with +% commands |\LeftSubproofLabel| and |\RightSubproofLabel|. +% \begin{macrocode} + +\def\LeftSubproofLabel#1{% + \global\setbox\curBox = + \hbox{\vbox to \ht\curBox{% + \vfil + \llap{#1$\left\{\vrule height .5\ht\curBox width 0pt\right.$}% + \vfil}\box\curBox}% +} + +\def\RightSubproofLabel#1{% + \displace=\ht\curBox + \global\setbox\curBox = + \hbox{\box\curBox\vbox to \displace{% + \vfil + \rlap{$\left.\vrule height .5\displace width 0pt\right\}$#1}% + \vfil}}% +} +% \end{macrocode} +% \subsection{Patched commands from \textsf{bussproofs}} +% +% Some commands from \textsf{bussproofs.sty} have to be redefined to include +% |bussproofs-extra| functionality. Added/changed lines are indicated by a +% |%bpextra| comment +% \begin{macrocode} +\def\resetInferenceDefaults{% + \global\def\theHypSeparation{\defaultHypSeparation}% + \global\setbox\myBoxLL=\hbox{\defaultLeftLabel}% + \global\setbox\myBoxRL=\hbox{\defaultRightLabel}% + \global\def\buildScore{\alwaysBuildScore}% + \global\def\theScoreFiller{\alwaysScoreFiller}% + % reset line labels to nothing %bpextra + \global\let\displayLeftLineLabel\relax %bpextra + \global\let\displayRightLineLabel\relax %bpextra + % reset to defaul deduce style %bpextra + \alwaysDeduce %bpextra + \gdef\hypKernAmt{0pt}% Restore to zero kerning. +} + +\def\Axiom$#1\fCenter#2${% + % Get level and correct names set. + \prepAxiom% + % Define the boxes + % bpextra -- add line labels + \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}% + \setbox\myBoxB=\hbox{$#2$}% %bpextra + \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra + \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra + \global\setbox\curBox=% + \hbox{\unhcopy\myBoxLLL%bpextra + \hskip\ScoreOverhangLeft\relax + \unhcopy\myBoxA + \unhcopy\myBoxB + \hskip\ScoreOverhangRight + \unhcopy\myBoxRLL}%bpextra + % Set the relevant dimensions for the boxes + \global\curScoreStart=0pt \relax + \global\curScoreEnd=\wd\curBox \relax + \global\curCenter=\wd\myBoxA \relax %bpextra + \global\advance \curCenter by \ScoreOverhangLeft% + % bpextra adjust by dimensions of labels + \global\advance \curCenter by \wd\myBoxLLL%bpextra + \global\advance\curScoreStart by \wd\myBoxLLL%bpextra + \global\advance\curScoreEnd by -\wd\myBoxRLL%bpextra + % reset line labels to nothing %bpextra + \global\let\displayLeftLineLabel\relax %bpextra + \global\let\displayRightLineLabel\relax %bpextra + \ignorespaces +} + +\def\AxiomC#1{ % Note argument not in math mode + % Get level and correct names set. + \prepAxiom% + % Define the box. + \setbox\myBoxA=\hbox{#1}% + \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra + \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra + \global\setbox\curBox =% + \hbox{\unhcopy\myBoxLLL%bpextra + \hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA + \hskip\ScoreOverhangRight\relax + \unhcopy\myBoxRLL}% %bpextra + % Set the relevant dimensions for the boxes + \global\curScoreStart=0pt \relax + \global\curScoreEnd=\wd\curBox \relax + \global\curCenter=.5\wd\myBoxA \relax %bpextra + \global\advance \curCenter by \ScoreOverhangLeft% + % bpextra adjust by dimensions of labels + \global\advance \curCenter by \wd\myBoxLLL%bpextra + \global\advance\curScoreStart by \wd\myBoxLLL%bpextra + \global\advance\curScoreEnd by -\wd\myBoxRLL%bpextra + % reset line labels to nothing %bpextra + \global\let\displayLeftLineLabel\relax %bpextra + \global\let\displayRightLineLabel\relax %bpextra + \ignorespaces +} + +\def\buildConclusion#1#2{% Build lower sequent w/ center at \fCenter position. + % Define the boxes + \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}% + \setbox\myBoxB=\hbox{$#2$}% + \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra + \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra + % Put them together in \myBoxC + \setbox\myBoxC =% + \hbox{\unhcopy\myBoxLLL%bpextra + \hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\unhcopy\myBoxB + \hskip\ScoreOverhangRight + \unhcopy\myBoxRLL}% %bpextra + % Calculate the center of the \myBoxC string. + \newScoreStart=0pt \relax% + \newCenter=\wd\myBoxA \relax% + \advance \newCenter by \ScoreOverhangLeft% + \newScoreEnd=\wd\myBoxC% + % bpextra adjust by dimensions of labels + \global\advance\newCenter by \wd\myBoxLLL%bpextra + \global\advance\newScoreStart by \wd\myBoxLLL%bpextra + \global\advance\newScoreEnd by -\wd\myBoxRLL%bpextra + % reset line labels to nothing %bpextra + \global\let\displayLeftLineLabel\relax %bpextra + \global\let\displayRightLineLabel\relax %bpextra +} + +\def\buildConclusionC#1{% Build lower sequent w/o \fCenter present. + % Define the box. + \setbox\myBoxA=\hbox{#1}% + \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra + \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra +\setbox\myBoxC =% + \hbox{\unhcopy\myBoxLLL%bpextra + \hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA + \hskip\ScoreOverhangRight + \unhcopy\myBoxRLL}%bpextra + % Calculate kerning to line up centers + \newScoreStart=0pt \relax% + \newCenter=.5\wd\myBoxA \relax% bpextra + \newScoreEnd=\wd\myBoxC% + \advance \newCenter by \ScoreOverhangLeft% + % bpextra adjust by dimensions of labels + \global\advance\newCenter by \wd\myBoxLLL%bpextra + \global\advance\newScoreStart by \wd\myBoxLLL%bpextra + \global\advance\newScoreEnd by -\wd\myBoxRLL%bpextra + % reset line labels to nothing %bpextra + \global\let\displayLeftLineLabel\relax %bpextra + \global\let\displayRightLineLabel\relax %bpextra +} +% \end{macrocode} +% \Finale +% \PrintChanges +\endinput diff --git a/macros/latex/contrib/bussproofs-extra/bussproofs-extra.ins b/macros/latex/contrib/bussproofs-extra/bussproofs-extra.ins new file mode 100644 index 0000000000..e511feff73 --- /dev/null +++ b/macros/latex/contrib/bussproofs-extra/bussproofs-extra.ins @@ -0,0 +1,57 @@ +%% +%% Copyright (C) 2019 by Richard Zach +%% +%% This file may be distributed and/or modified under the conditions of +%% the LaTeX Project Public License, either version 1.2 of this license +%% or (at your option) any later version. The latest version of this +%% license is in: +%% +%% http://www.latex-project.org/lppl.txt +%% +%% and version 1.2 or later is part of all distributions of LaTeX version +%% 1999/12/01 or later. +%% + +\input docstrip.tex +\keepsilent + +\usedir{tex/latex/bussproofs-extra} + +\preamble + +This is a generated file. + +Copyright (C) 2019 by Richard Zach + +This file may be distributed and/or modified under the conditions of +the LaTeX Project Public License, either version 1.3 of this license +or (at your option) any later version. The latest version of this +license is in: + + http://www.latex-project.org/lppl.txt + +and version 1.3 or later is part of all distributions of LaTeX version +1999/12/01 or later. + +\endpreamble + +\generate{\file{bussproofs-extra.sty}{\from{bussproofs-extra.dtx}{package}}} + +\obeyspaces +\Msg{*************************************************************} +\Msg{* *} +\Msg{* To finish the installation you have to move the following *} +\Msg{* file into a directory searched by TeX: *} +\Msg{* *} +\Msg{* bussproofs-extra.sty *} +\Msg{* *} +\Msg{* To produce the documentation run the file bpextra.dtx *} +\Msg{* through LaTeX, and then *} +\Msg{* makeindex -s gglo.ist -o bussproofs-extra.gls bussproofs-extra.glo *} +\Msg{* Then run LaTeX on bussproofs-extra.dtx again *} +\Msg{* *} +\Msg{* Happy TeXing! *} +\Msg{* *} +\Msg{*************************************************************} + +\endbatchfile diff --git a/macros/latex/contrib/bussproofs-extra/bussproofs-extra.pdf b/macros/latex/contrib/bussproofs-extra/bussproofs-extra.pdf new file mode 100644 index 0000000000..d20f69d4fa Binary files /dev/null and b/macros/latex/contrib/bussproofs-extra/bussproofs-extra.pdf differ -- cgit v1.2.3