From b36220f82a7bf6cac618afb8ce23d52e98bff584 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maximilian=20Ke=C3=9Fler?= Date: Fri, 14 Jan 2022 18:48:21 +0100 Subject: [PATCH] start latex3 implementation of refproof --- src/wip/refproof3.pysty3 | 191 ++++++++++++++++++++++++++++++++++++ tests/wip/refproof/Makefile | 1 + tests/wip/refproof/test.tex | 128 ++++++++++++++++++++++++ 3 files changed, 320 insertions(+) create mode 100644 src/wip/refproof3.pysty3 create mode 120000 tests/wip/refproof/Makefile create mode 100644 tests/wip/refproof/test.tex diff --git a/src/wip/refproof3.pysty3 b/src/wip/refproof3.pysty3 new file mode 100644 index 0000000..633ad34 --- /dev/null +++ b/src/wip/refproof3.pysty3 @@ -0,0 +1,191 @@ +__HEADER__(Automatic references to theorems in proofs. Claim counters within proofs) + +\RequirePackage{xkeyval} + +__LANGUAGE_OPTIONS_X__ + +__END_OPTIONS_X__ + +\RequirePackage{amssymb} +\RequirePackage{amsthm} +\RequirePackage{etoolbox} +\RequirePackage{xparse} +\RequirePackage{refcount} +\RequirePackage{translator} +\RequirePackage{fifo-stack} + +\usedictionary{translator-proof-dictionary} + +%%Give claim an own counter and let it reset at each proof +%See also at: +%https://tex.stackexchange.com/questions/283502/reset-counter-at-beginning-of-proof +\newtheorem{claim}{\translate{Claim}} +\newtheorem*{claim*}{\translate{Claim}} +\AtBeginDocument{\def\claimautorefname{\translate{Claim}}} + +\AtBeginDocument{ + \@ifpackageloaded{hyperref}{ + \let__PACKAGE_MACRO__(autoref)\autoref + }{ + \let__PACKAGE_MACRO__(autoref)\ref + } +} + +\newcounter{__PACKAGE_PREFIX__proofdepth} +\setcounter{__PACKAGE_PREFIX__proofdepth}{0} + +\let__PACKAGE_MACRO__(saved@proof)\proof +\let__PACKAGE_MACRO__(saved@endproof)\endproof + +\FSCreate{__PACKAGE_PREFIX__save@claim}{-1} + +%%subproof environment - essentially copied proof environment from amsthm and modified its name + symbol +\DeclareRobustCommand{\blackqed}{% + \ifmmode \mathqed + \else + \leavevmode\unskip\penalty9999 \hbox{}\nobreak\hfill + \quad\hbox{$\blacksquare$}% + \fi +} + +\newenvironment{__PACKAGE_PREFIX__saved@subproof}[1][\translate{Subproof}]{\par + \pushQED{\blackqed}% + \normalfont \topsep6\p@\@plus6\p@\relax + \trivlist + \item[\hskip\labelsep + \itshape + #1\@addpunct{.}]\ignorespaces +}{% + \popQED\endtrivlist\@endpefalse +} + +%%%Now, we internally got a proof and a subproof environment +%%%Make them available as 'old' variants, with their defautl behaviour +\NewDocumentEnvironment{oldproof}{} +{ + __PACKAGE_MACRO__(saved@proof) +} +{ + __PACKAGE_MACRO__(saved@endproof) +} +\NewDocumentEnvironment{oldsubproof}{} +{ + \__PACKAGE_PREFIX__saved@subproof +} + \end__PACKAGE_PREFIX__saved@subproof +{ + +\NewDocumentEnvironment{refproof}{s m !o} +{ + \stepcounter{__PACKAGE_PREFIX__proofdepth} + %Save the current claim counter + \protected@edef__PACKAGE_MACRO__(dummy@expand){\arabic{claim}} + \FSPush{__PACKAGE_PREFIX__save@claim}{__PACKAGE_MACRO__(dummy@expand)} + % Restore correct counter for claims in this refproof + \ifcsdef{the__PACKAGE_PREFIX__#2@save@claim}{ + \setcounter{claim}{\value{__PACKAGE_PREFIX__#2@save@claim}} + \def__PACKAGE_MACRO__(proofprefix){ + \IfBooleanTF{#1}{% + \translate{Continuation of proof* of}% + }{% + \translate{Continuation of proof of}% + } + } + }{ + \newcounter{__PACKAGE_PREFIX__#2@save@claim} + \setcounter{claim}{0} + \def__PACKAGE_MACRO__(proofprefix){% + \IfBooleanTF{#1}{% + \translate{Proof* of}% + }{% + \translate{Proof of}% + } + } + } + % Set up counter number printing as subindexed by numbering of the reference + \let__PACKAGE_MACRO__(saved@theclaim)\theclaim + \def\theclaim{\getrefnumber{#2}.\arabic{claim}} + % Now, start the actual proof + __PACKAGE_MACRO__(saved@proof)[% + __PACKAGE_MACRO__(proofprefix)\space__PACKAGE_MACRO__(autoref){#2}% + \IfValueT{#3}{\space(#3)}% + ] +} +{ + __PACKAGE_MACRO__(saved@endproof) % End proof + % Save current claim counter for later restoration + \setcounter{__PACKAGE_PREFIX__#2@save@claim}{\value{claim}} + %Restore previous claim counter + \setcounter{claim}{\FSTop{__PACKAGE_PREFIX__save@claim}} + \FSPop{__PACKAGE_PREFIX__save@claim} + \addtocounter{__PACKAGE_PREFIX__proofdepth}{-1} + \let\theclaim__PACKAGE_MACRO__(saved@theclaim) +} + +%%% A 'smart' proof environment +\AtBeginDocument{ + \RenewDocumentEnvironment{proof}{!s !o} + { + \stepcounter{__PACKAGE_PREFIX__proofdepth} + %Save the current claim counter + \protected@edef__PACKAGE_MACRO__(dummy@expand){\arabic{claim}} + \FSPush{__PACKAGE_PREFIX__save@claim}{__PACKAGE_MACRO__(dummy@expand)} + \setcounter{claim}{0} + \let__PACKAGE_MACRO__(saved@theclaim)\theclaim + \def\theclaim{\arabic{claim}} + \ifnum\value{__PACKAGE_PREFIX__proofdepth}>1% + __PACKAGE_MACRO__(saved@subproof)[% + \IfBooleanTF{#1}{% + \translate{Subproof*}% + }{% + \translate{Subproof}% + }% + \IfValueT{#2}{\space(#2)}% + ] + \else% + __PACKAGE_MACRO__(saved@proof)[% + \IfBooleanTF{#1}{% + \translate{Proof*}% + }{% + \translate{Proof}% + }% + \IfValueT{#2}{\space(#2)}% + ] + \fi + } + { + __PACKAGE_MACRO__(saved@endproof) + %Restore previous claim counter + \setcounter{claim}{\FSTop{__PACKAGE_PREFIX__save@claim}} + \FSPop{__PACKAGE_PREFIX__save@claim} + \addtocounter{__PACKAGE_PREFIX__proofdepth}{-1} + \let\theclaim__PACKAGE_MACRO__(saved@theclaim) + } +} + +\NewDocumentEnvironment{subproof}{!s !o} +{ + \stepcounter{__PACKAGE_PREFIX__proofdepth} + %Save the current claim counter + \protected@edef__PACKAGE_MACRO__(dummy@expand){\arabic{claim}} + \FSPush{__PACKAGE_PREFIX__save@claim}{__PACKAGE_MACRO__(dummy@expand)} + \setcounter{claim}{0} + \def\theclaim{\arabic{claim}} + __PACKAGE_MACRO__(saved@subproof)[% + \IfBooleanTF{#1}{% + \translate{Subproof*}% + }{% + \translate{Subproof}% + }% + \IfValueT{#2}{\space(#2)}% + ] +} +{ + __PACKAGE_MACRO__(saved@endproof) + %Restore previous claim counter + \setcounter{claim}{\FSTop{__PACKAGE_PREFIX__save@claim}} + \FSPop{__PACKAGE_PREFIX__save@claim} + \addtocounter{__PACKAGE_PREFIX__proofdepth}{-1} +} + +\newcommand\proofdepth{\arabic{__PACKAGE_PREFIX__proofdepth}} diff --git a/tests/wip/refproof/Makefile b/tests/wip/refproof/Makefile new file mode 120000 index 0000000..0fde22c --- /dev/null +++ b/tests/wip/refproof/Makefile @@ -0,0 +1 @@ +../../COMPILE_MAKEFILE \ No newline at end of file diff --git a/tests/wip/refproof/test.tex b/tests/wip/refproof/test.tex new file mode 100644 index 0000000..e686702 --- /dev/null +++ b/tests/wip/refproof/test.tex @@ -0,0 +1,128 @@ +\documentclass[ngerman]{article} + +\usepackage{babel} +\usepackage{mkessler-refproof3} +\usepackage{mkessler-fancythm} +\usepackage{mkessler-hypersetup} +\usepackage{parskip} + +\begin{document} +\section{test} + + +\begin{subproof} + test +\end{subproof} + +\begin{subproof}*[hi] + test +\end{subproof} + +\begin{proof} + Beginn des Beweises: + \begin{proof}* + Ein unterbeweis + \end{proof} + Jetzt sind wir fertig. +\end{proof} + +\begin{theorem}\label{thm:krass} + Man sollte nach Würzburg fahren. +\end{theorem} + +\begin{claim} + test +\end{claim} + +\begin{proof} + \begin{claim} + hi + \end{claim} + \begin{proof} + \end{proof} + \begin{claim} + + \end{claim} +\end{proof} + +\begin{claim} + test +\end{claim} + +\begin{refproof}*{thm:krass}[hi] + \begin{claim}\label{cl:qed} + Der QED ist toll. + \end{claim} + Um \autoref{cl:qed} zu beweisen, brauchen wir zunächst ein Lemma. + \begin{proof} + \begin{claim} + test + \end{claim} + hi + \proofdepth + \end{proof} + \begin{claim} + hi + \end{claim} +\end{refproof} + +\begin{claim} + next +\end{claim} + +\begin{lemma}\label{lm:krass} + Mathevereine sind krass. +\end{lemma} + +\begin{refproof}{lm:krass}[quasi ein Fakt] + \begin{claim} + Mathe ist cool. + \end{claim} + \begin{oldsubproof} + trivial. + \end{oldsubproof} + Damit folgt nun das Lemma. +\end{refproof} + +Nun kommen wir wieder zurück zum eigentlichen Beweis: + +\begin{refproof}{thm:krass}[hi] + \begin{claim}\label{cl:würzburg} + Der QED macht ein Seminar in Würzburg + \end{claim} + \begin{oldsubproof} + Zu prüfen in der DB. Fakt! + \end{oldsubproof} +Aus \autoref{cl:qed} und \autoref{cl:würzburg} folgt nun die Aussage. +\end{refproof} + +\begin{proof}[anm] + second +\end{proof} +\begin{proof} + first +\end{proof} +\begin{proof}* + third +\end{proof} +\begin{proof}*[anm] + fourth +\end{proof} + +\begin{oldproof} + test +\end{oldproof} + +\def\four{4} + +\def\foo{1} +{\def\foo{2}\foo} +{\let\foo\four\foo} +\foo + +\begin{proof} + \def\foo{5}\foo +\end{proof} +\foo + +\end{document}