rework proof package into LaTeX3 style
This commit is contained in:
parent
31245c6a17
commit
4b695a6a06
1 changed files with 248 additions and 0 deletions
248
src/wip/refproofnew.pysty3
Normal file
248
src/wip/refproofnew.pysty3
Normal file
|
|
@ -0,0 +1,248 @@
|
||||||
|
__HEADER__(Automatic references to theorems in proofs. Claim counters within proofs)
|
||||||
|
\ExplSyntaxOn
|
||||||
|
\RequirePackage{xkeyval}
|
||||||
|
|
||||||
|
\RequirePackage{amssymb}
|
||||||
|
\RequirePackage{amsthm}
|
||||||
|
\RequirePackage{etoolbox}
|
||||||
|
\RequirePackage{xparse}
|
||||||
|
\RequirePackage{refcount}
|
||||||
|
\RequirePackage{translator}
|
||||||
|
|
||||||
|
\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}}}
|
||||||
|
|
||||||
|
\cs_new:Npn__PACKAGE_MACRO__(autoref)
|
||||||
|
{
|
||||||
|
\ref
|
||||||
|
}
|
||||||
|
|
||||||
|
\AddToHook{package/hyperref/after}
|
||||||
|
{
|
||||||
|
\cs_set:Npn__PACKAGE_MACRO__(autoref)
|
||||||
|
{
|
||||||
|
\autoref
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
\cs_new_eq:NN __PACKAGE_MACRO__(saved_proof) \proof
|
||||||
|
\cs_new_eq:NN __PACKAGE_MACRO__(saved_endproof) \endproof
|
||||||
|
|
||||||
|
\int_new:N __PACKAGE_MACRO__(proofdepth_int)
|
||||||
|
\seq_new:N __PACKAGE_MACRO__(nested_claim_counter_values_seq)
|
||||||
|
\prop_new:N __PACKAGE_MACRO__(refproof_claim_counters_prop)
|
||||||
|
|
||||||
|
\cs_generate_variant:Nn \seq_push:Nn { N x }
|
||||||
|
|
||||||
|
%%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}
|
||||||
|
{
|
||||||
|
\int_incr:N __PACKAGE_MACRO__(proofdepth_int)
|
||||||
|
%Save the current claim counter
|
||||||
|
\seq_push:Nx __PACKAGE_MACRO__(nested_claim_counter_values_seq)
|
||||||
|
{
|
||||||
|
\arabic{claim}
|
||||||
|
}
|
||||||
|
% 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 }
|
||||||
|
\IfBooleanTF { #1 }
|
||||||
|
{
|
||||||
|
\cs_set:Nn __PACKAGE_MACRO__(proof_prefix:)
|
||||||
|
{
|
||||||
|
\translate { Proof*~of }
|
||||||
|
}
|
||||||
|
}
|
||||||
|
{
|
||||||
|
\cs_set:Nn __PACKAGE_MACRO__(proof_prefix:)
|
||||||
|
{
|
||||||
|
\translate { Proof~of }
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
{
|
||||||
|
\setcounter{claim}
|
||||||
|
{
|
||||||
|
\tl_use:N \l_tmpa_tl
|
||||||
|
}
|
||||||
|
\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
|
||||||
|
\group_begin:
|
||||||
|
\renewcommand\theclaim{\getrefnumber{#2}.\arabic{claim}}
|
||||||
|
% Now, start the actual proof
|
||||||
|
__PACKAGE_MACRO__(saved_proof)
|
||||||
|
[
|
||||||
|
__PACKAGE_MACRO__(proof_prefix:)
|
||||||
|
~
|
||||||
|
__PACKAGE_MACRO__(autoref) { #2 }
|
||||||
|
\IfValueT{#3}
|
||||||
|
{
|
||||||
|
\space(#3)
|
||||||
|
}
|
||||||
|
]
|
||||||
|
}
|
||||||
|
{
|
||||||
|
__PACKAGE_MACRO__(saved_endproof) % End proof
|
||||||
|
\group_end:
|
||||||
|
% Save current claim counter for later restoration
|
||||||
|
\prop_put:Nnx __PACKAGE_MACRO__(refproof_claim_counters_prop)
|
||||||
|
{#2}
|
||||||
|
{
|
||||||
|
\value{claim}
|
||||||
|
}
|
||||||
|
%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)
|
||||||
|
}
|
||||||
|
|
||||||
|
%%% A 'smart' proof environment
|
||||||
|
\AtBeginDocument{
|
||||||
|
\RenewDocumentEnvironment{proof}{!s !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}
|
||||||
|
}
|
||||||
|
\setcounter{claim}{0}
|
||||||
|
|
||||||
|
\group_begin:
|
||||||
|
\renewcommand\theclaim{\arabic{claim}}
|
||||||
|
\int_compare:nNnTF __PACKAGE_MACRO__(proofdepth_int) > 1
|
||||||
|
{
|
||||||
|
__PACKAGE_MACRO__(saved_subproof)[%
|
||||||
|
\IfBooleanTF{#1}{%
|
||||||
|
\translate{Subproof*}%
|
||||||
|
}{%
|
||||||
|
\translate{Subproof}%
|
||||||
|
}%
|
||||||
|
\IfValueT{#2}{\space(#2)}%
|
||||||
|
]
|
||||||
|
}
|
||||||
|
{
|
||||||
|
__PACKAGE_MACRO__(saved_proof)[%
|
||||||
|
\IfBooleanTF{#1}{%
|
||||||
|
\translate{Proof*}%
|
||||||
|
}{%
|
||||||
|
\translate{Proof}%
|
||||||
|
}%
|
||||||
|
\IfValueT{#2}{\space(#2)}%
|
||||||
|
]
|
||||||
|
}
|
||||||
|
}
|
||||||
|
{
|
||||||
|
__PACKAGE_MACRO__(saved_endproof)
|
||||||
|
\group_end:
|
||||||
|
%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}
|
||||||
|
{
|
||||||
|
\int_incr:N __PACKAGE_MACRO__(proofdepth_int)
|
||||||
|
%Save the current claim counter
|
||||||
|
\seq_push:Nx __PACKAGE_MACRO__(nested_claim_counter_values_seq)
|
||||||
|
{
|
||||||
|
\arabic{claim}
|
||||||
|
}
|
||||||
|
\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)
|
||||||
|
\group_end:
|
||||||
|
%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 } { }
|
||||||
|
{
|
||||||
|
\int_to_arabic:n __PACKAGE_MACRO__(proofdepth_int)
|
||||||
|
}
|
||||||
Loading…
Reference in a new issue