latex/latex-packages
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

rework of refproof as latex3 package complete. outsorced subproof properly

Browse source
This commit is contained in:
Maximilian Keßler 2022-01-15 14:56:53 +01:00
parent 754278a807
commit 4eb5d7cd9c
3 changed files with 183 additions and 170 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

316
src/wip/refproofnew.pysty3
View file

@ -1,38 +1,38 @@
__HEADER__(Automatic references to theorems in proofs. Claim counters within proofs) __HEADER__(Automatic references to theorems in proofs. Claim counters within proofs)
\ExplSyntaxOn \ExplSyntaxOn
\RequirePackage{xkeyval}
\RequirePackage{amssymb} \RequirePackage{amssymb}
\RequirePackage{amsthm} \RequirePackage{amsthm}
\RequirePackage{etoolbox}
\RequirePackage{xparse} \RequirePackage{xparse}
\RequirePackage{refcount} \RequirePackage{refcount}
\RequirePackage{translator} \RequirePackage{translator}
\RequirePackage{mkessler-subproof} % TODO: let PyTeX format the mkessler- prefix
\usedictionary{translator-proof-dictionary}
%%Give claim an own counter and let it reset at each proof %%%% Hook management
%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}}}
\cs_new:Npn__PACKAGE_MACRO__(autoref) \cs_new:Npn__PACKAGE_MACRO__(autoref:n)
{ {
\ref \ref
} }
\AddToHook{package/hyperref/after} \AddToHook{package/hyperref/after}
{ {
\cs_set:Npn__PACKAGE_MACRO__(autoref) \cs_set:Npn__PACKAGE_MACRO__(autoref:n)
{ {
\autoref \autoref
} }
} }
\cs_new_eq:NN __PACKAGE_MACRO__(saved_proof) \proof %%% Saving old definitions
\cs_new_eq:NN __PACKAGE_MACRO__(saved_endproof) \endproof
\cs_new_eq:NN __PACKAGE_MACRO__(saved_proof:w) \proof
\cs_new_eq:NN __PACKAGE_MACRO__(saved_endproof:) \endproof
\cs_new_eq:NN __PACKAGE_MACRO__(saved_subproof:n) \rawsubproof
\cs_new_eq:NN __PACKAGE_MACRO__(saved_endsubproof:) \rawendsubproof
%%% Internal variables
\int_new:N __PACKAGE_MACRO__(proofdepth_int) \int_new:N __PACKAGE_MACRO__(proofdepth_int)
\seq_new:N __PACKAGE_MACRO__(nested_claim_counter_values_seq) \seq_new:N __PACKAGE_MACRO__(nested_claim_counter_values_seq)
@ -40,206 +40,204 @@ __HEADER__(Automatic references to theorems in proofs. Claim counters within pro
\cs_generate_variant:Nn \seq_push:Nn { N x } \cs_generate_variant:Nn \seq_push:Nn { N x }
%%subproof environment - essentially copied proof environment from amsthm and modified its name + symbol %%% Language translations
\DeclareRobustCommand{\blackqed}{%
\ifmmode \mathqed
\else
\leavevmode\unskip\penalty9999 \hbox{}\nobreak\hfill
\quad\hbox{$\blacksquare$}%
\fi
}
\newenvironment{__PACKAGE_PREFIX__saved_subproof}[1][\translate{Subproof}]{\par \usedictionary{translator-proof-dictionary}
\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 %%%Now, we internally got a proof and a subproof environment
%%%Make them available as 'old' variants, with their defautl behaviour %%%Make them available as 'old' variants, with their defautl behaviour
\NewDocumentEnvironment{oldproof}{} \NewDocumentEnvironment{oldproof}{ o }
{ {
__PACKAGE_MACRO__(saved_proof) \IfValueTF { #1 }
}
{
__PACKAGE_MACRO__(saved_endproof)
}
\NewDocumentEnvironment{oldsubproof}{}
{
\__PACKAGE_PREFIX__saved_subproof
}
\end__PACKAGE_PREFIX__saved_subproof
{
\NewDocumentEnvironment{refproof}{s m !o}
{
\int_incr:N __PACKAGE_MACRO__(proofdepth_int)
%Save the current claim counter
\seq_push:Nx __PACKAGE_MACRO__(nested_claim_counter_values_seq)
{ {
\arabic{claim} __PACKAGE_MACRO__(saved_proof:w) { #1 }
} }
% Restore correct counter for claims in this refproof
\prop_get:NnN
__PACKAGE_MACRO__(refproof_claim_counters_prop)
{ #2 }
\l_tmpa_tl
% \tl_show:N \l_tmpa_tl
% \error
\quark_if_no_value:NTF \l_tmpa_tl
{ {
\setcounter { claim } { 0 } __PACKAGE_MACRO__(saved_proof:w)
}
}
{
__PACKAGE_MACRO__(saved_endproof:)
}
\NewDocumentEnvironment{oldsubproof}{ o }
{
\IfValueTF { #1 }
{
__PACKAGE_MACRO__(saved_subproof:n) { #1 }
}
{
__PACKAGE_MACRO__(saved_subproof:n) { \translate { Subproof } }
}
}
{
__PACKAGE_MACRO__(saved_endsubproof:)
}
%%% Main implementation
%Introduce claim environment
\newtheorem{claim}{\translate{Claim}}
\newtheorem*{claim*}{\translate{Claim}}
\AtBeginDocument{\def\claimautorefname{\translate{Claim}}}
\cs_new:Nn __PACKAGE_MACRO__(enter_proof:)
{
\int_gincr:N __PACKAGE_MACRO__(proofdepth_int)
\seq_gpush:Nx __PACKAGE_MACRO__(nested_claim_counter_values_seq)
{
\arabic { claim }
}
\group_begin:
}
\cs_new:Nn __PACKAGE_MACRO__(leave_proof:)
{
\group_end:
\seq_gpop:NN __PACKAGE_MACRO__(nested_claim_counter_values_seq) \l_tmpa_tl
\setcounter { claim } { \tl_use:N \l_tmpa_tl }
\int_gdecr:N __PACKAGE_MACRO__(proofdepth_int)
}
% Usage:
% #1 = \BooleanTrue or \BooleanFalse indicating presence of star
% #2 = star version of translation
% #3 = nonstar version of translation
\cs_new:Nn __PACKAGE_MACRO__(set_proof_prefix:nnn)
{
\IfBooleanTF { #1 } \IfBooleanTF { #1 }
{ {
\cs_set:Nn __PACKAGE_MACRO__(proof_prefix:) \cs_set:Nn __PACKAGE_MACRO__(proof_prefix:)
{ {
\translate { Proof*~of } \translate { #2 }
} }
} }
{ {
\cs_set:Nn __PACKAGE_MACRO__(proof_prefix:) \cs_set:Nn __PACKAGE_MACRO__(proof_prefix:)
{ {
\translate { Proof~of } \translate { #3 }
} }
} }
} }
\cs_new:Nn __PACKAGE_MACRO__(proof_comment:n)
{
\IfValueT { #1 }
{
\c_space_tl ( #1 )
}
}
\NewDocumentEnvironment{refproof}{s m !o}
{
__PACKAGE_MACRO__(enter_proof:)
\prop_get:NnN
__PACKAGE_MACRO__(refproof_claim_counters_prop)
{ #2 }
\l_tmpa_tl
\quark_if_no_value:NTF \l_tmpa_tl
{
\setcounter { claim } { 0 }
__PACKAGE_MACRO__(set_proof_prefix:nnn) { #1 }
{ Proof* ~ of }
{ Proof ~ of }
}
{ {
\setcounter{claim} \setcounter { claim } { \tl_use:N \l_tmpa_tl }
{ __PACKAGE_MACRO__(set_proof_prefix:nnn) { #1 }
\tl_use:N \l_tmpa_tl { Continuation ~ of ~ proof* ~ of }
} { Continuation ~ of ~ proof ~ of }
\IfBooleanTF{#1}
{
\cs_set:Nn __PACKAGE_MACRO__(proof_prefix:)
{
\translate { Continuation~of~proof*~of }
}
}
{
\cs_set:Nn __PACKAGE_MACRO__(proof_prefix:)
{
\translate { Continuation~of~proof~of }
}
}
} }
% Set up counter number printing as subindexed by numbering of the reference % Set up counter number printing as subindexed by numbering of the reference
\group_begin: \renewcommand \theclaim
\renewcommand\theclaim{\getrefnumber{#2}.\arabic{claim}} {
% Now, start the actual proof \getrefnumber { #2 } . \arabic { claim }
__PACKAGE_MACRO__(saved_proof) }
__PACKAGE_MACRO__(saved_proof:w)
[ [
__PACKAGE_MACRO__(proof_prefix:) __PACKAGE_MACRO__(proof_prefix:)
~ \c_space_tl
__PACKAGE_MACRO__(autoref) { #2 } __PACKAGE_MACRO__(autoref:n) { #2 }
\IfValueT{#3} __PACKAGE_MACRO__(proof_comment:n) { #3 }
{
\space(#3)
}
] ]
} }
{ {
__PACKAGE_MACRO__(saved_endproof) % End proof __PACKAGE_MACRO__(saved_endproof:)
\group_end: \prop_gput:Nnx __PACKAGE_MACRO__(refproof_claim_counters_prop)
% Save current claim counter for later restoration { #2 }
\prop_put:Nnx __PACKAGE_MACRO__(refproof_claim_counters_prop)
{#2}
{ {
\value{claim} \value{claim}
} }
%Restore previous claim counter __PACKAGE_MACRO__(leave_proof:)
\seq_pop:NN __PACKAGE_MACRO__(nested_claim_counter_values_seq)
\l_tmpa_tl
\setcounter{claim}
{
\tl_use:N \l_tmpa_tl
}
\int_decr:N __PACKAGE_MACRO__(proofdepth_int)
} }
%%% A 'smart' proof environment %%% A 'smart' proof environment
\AtBeginDocument{ \AtBeginDocument{
\RenewDocumentEnvironment{proof}{!s !o} \RenewDocumentEnvironment{proof}{!s !o}
{ {
\int_incr:N __PACKAGE_MACRO__(proofdepth_int) __PACKAGE_MACRO__(enter_proof:)
%Save the current claim counter
\seq_push:Nx __PACKAGE_MACRO__(nested_claim_counter_values_seq)
{
\arabic{claim}
}
\setcounter{claim}{0} \setcounter{claim}{0}
\group_begin: \renewcommand \theclaim
\renewcommand\theclaim{\arabic{claim}} {
\arabic { claim }
}
\int_compare:nNnTF __PACKAGE_MACRO__(proofdepth_int) > 1 \int_compare:nNnTF __PACKAGE_MACRO__(proofdepth_int) > 1
{ {
__PACKAGE_MACRO__(saved_subproof)[% __PACKAGE_MACRO__(set_proof_prefix:nnn) { #1 }
\IfBooleanTF{#1}{% { Subproof* }
\translate{Subproof*}% { Subproof }
}{% __PACKAGE_MACRO__(saved_subproof:n)
\translate{Subproof}% {
}% __PACKAGE_MACRO__(proof_prefix:)
\IfValueT{#2}{\space(#2)}% __PACKAGE_MACRO__(proof_comment:n) { #2 }
] }
} }
{ {
__PACKAGE_MACRO__(saved_proof)[% __PACKAGE_MACRO__(set_proof_prefix:nnn) { #1 }
\IfBooleanTF{#1}{% { Proof* }
\translate{Proof*}% { Proof }
}{% __PACKAGE_MACRO__(saved_proof:w)
\translate{Proof}% [
}% __PACKAGE_MACRO__(proof_prefix:)
\IfValueT{#2}{\space(#2)}% __PACKAGE_MACRO__(proof_comment:n) { #2 }
] ]
} }
} }
{ {
__PACKAGE_MACRO__(saved_endproof) __PACKAGE_MACRO__(saved_endproof:)
\group_end: __PACKAGE_MACRO__(leave_proof:)
%Restore previous claim counter
\seq_pop:NN __PACKAGE_MACRO__(nested_claim_counter_values_seq) \l_tmpa_tl
\setcounter{claim}{\tl_use:N \l_tmpa_tl}
\int_decr:N __PACKAGE_MACRO__(proofdepth_int)
} }
} }
\NewDocumentEnvironment{subproof}{!s !o} \RenewDocumentEnvironment{subproof}{!s !o}
{ {
\int_incr:N __PACKAGE_MACRO__(proofdepth_int) __PACKAGE_MACRO__(enter_proof:)
%Save the current claim counter
\seq_push:Nx __PACKAGE_MACRO__(nested_claim_counter_values_seq) \setcounter { claim } { 0 }
\renewcommand \theclaim
{ {
\arabic{claim} \arabic { claim }
}
__PACKAGE_MACRO__(set_proof_prefix:nnn) { #1 }
{ Subproof* }
{ Subproof }
__PACKAGE_MACRO__(saved_subproof:n)
{
__PACKAGE_MACRO__(proof_prefix:)
__PACKAGE_MACRO__(proof_comment:n) { #2 }
} }
\setcounter{claim}{0}
\group_begin:
\renewcommand\theclaim{\arabic{claim}}
__PACKAGE_MACRO__(saved_subproof)[%
\IfBooleanTF{#1}{%
\translate{Subproof*}%
}{%
\translate{Subproof}%
}%
\IfValueT{#2}{\space(#2)}%
]
} }
{ {
__PACKAGE_MACRO__(saved_endproof) __PACKAGE_MACRO__(saved_endsubproof:)
\group_end: __PACKAGE_MACRO__(leave_proof:)
%Restore previous claim counter
\seq_pop:NN __PACKAGE_MACRO__(nested_claim_counter_values_seq) \l_tmpa_tl
\setcounter{claim}{\tl_use:N \l_tmpa_tl}
\int_decr:N __PACKAGE_MACRO__(proofdepth_int)
} }
\DeclareDocumentCommand { \proofdepth } { } \DeclareDocumentCommand { \proofdepth } { }

29
src/wip/subproof.pysty
View file

@ -16,15 +16,8 @@ __HEADER__(Subproof environment with black square at end of proof.)
\fi \fi
} }
\DeclareDocumentEnvironment{subproof}{ o } \newcommand\rawsubproof[1]
{ {
\IfValueTF{#1}
{
\def__PACKAGE_MACRO__(subproof@prefix){#1}
}
{
\def__PACKAGE_MACRO__(subproof@prefix){\translate{Subproof}}
}
\pushQED \pushQED
{ {
\blackqed \blackqed
@ -33,8 +26,26 @@ __HEADER__(Subproof environment with black square at end of proof.)
\trivlist \trivlist
\item[\hskip\labelsep \item[\hskip\labelsep
\itshape \itshape
__PACKAGE_MACRO__(subproof@prefix)\@addpunct{.}]\ignorespaces #1\@addpunct{.}]\ignorespaces
} }
\newcommand\rawendsubproof
{ {
\popQED\endtrivlist\@endpefalse \popQED\endtrivlist\@endpefalse
} }
%%subproof environment - essentially copied proof environment from amsthm and modified its name + symbol
\DeclareDocumentEnvironment{subproof}{ o }
{
\IfValueTF{#1}
{
\rawsubproof{#1}
}
{
\rawsubproof{\translate{Subproof}}
}
}
{
\rawendsubproof
}

10
tests/wip/refproof/test.tex
View file

@ -3,13 +3,17 @@
\usepackage{babel} \usepackage{babel}
\usepackage{mkessler-refproofnew} \usepackage{mkessler-refproofnew}
\usepackage{mkessler-fancythm} \usepackage{mkessler-fancythm}
\usepackage{mkessler-hypersetup} %\usepackage{mkessler-hypersetup}
\usepackage{parskip} \usepackage{parskip}
\begin{document} \begin{document}
\section{test} \section{test}
\begin{oldsubproof}[hi]
test
\end{oldsubproof}
\begin{subproof} \begin{subproof}
test test
\end{subproof} \end{subproof}
@ -53,7 +57,7 @@
\begin{claim}\label{cl:qed} \begin{claim}\label{cl:qed}
Der QED ist toll. Der QED ist toll.
\end{claim} \end{claim}
Um \autoref{cl:qed} zu beweisen, brauchen wir zunächst ein Lemma. Um \ref{cl:qed} zu beweisen, brauchen wir zunächst ein Lemma.
\begin{proof} \begin{proof}
\begin{claim} \begin{claim}
test test
@ -93,7 +97,7 @@ Nun kommen wir wieder zurück zum eigentlichen Beweis:
\begin{oldsubproof} \begin{oldsubproof}
Zu prüfen in der DB. Fakt! Zu prüfen in der DB. Fakt!
\end{oldsubproof} \end{oldsubproof}
Aus \autoref{cl:qed} und \autoref{cl:würzburg} folgt nun die Aussage. Aus \ref{cl:qed} und \ref{cl:würzburg} folgt nun die Aussage.
\end{refproof} \end{refproof}
\begin{proof}[anm] \begin{proof}[anm]