2022-01-30 21:47:14 +01:00
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
% Copyright © 2022 Maximilian Keßler
|
|
|
|
%
|
|
|
|
% This work may be distributed and/or modified
|
|
|
|
%
|
|
|
|
% 1. under the LaTeX Project Public License and/or
|
|
|
|
% 2. under the GNU General Public License
|
|
|
|
%
|
|
|
|
% Distribution under conditions of the LaTeX Project Public License,
|
|
|
|
% requires 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 Maximilian Keßler.
|
|
|
|
%
|
|
|
|
%
|
|
|
|
% Distribution under the GNU General Public License requires either
|
|
|
|
% version 3 or (at your opinion) any later version.
|
|
|
|
%
|
|
|
|
% This package has been generated by PyTeX, available at
|
|
|
|
% https://github.com/kesslermaximilian/PyTeX
|
|
|
|
% and built from source file 'refproof.pysty3'.
|
|
|
|
% It is STRONGLY DISCOURAGED to edit this source file directly, since local
|
|
|
|
% changes will not be versioned by Git and overwritten by the next build. Always
|
|
|
|
% edit the source file and build the package again.
|
|
|
|
%
|
|
|
|
% Build details:
|
2022-01-31 00:49:04 +01:00
|
|
|
% PyTeX version: v1.2.0-31-gc9bb0e8 (commit c9bb0e8)
|
|
|
|
% Source code version: v2.8.1-9-g4bda829 (commit 4bda829)
|
2022-01-30 21:47:14 +01:00
|
|
|
%
|
|
|
|
% This LaTeX package is free software and is dual-licensed
|
|
|
|
% under the LPPLv1.3c and the GPLv3 licenses.
|
|
|
|
% You may use it freely for your purposes.
|
|
|
|
% The latest version of the package sources can be obtained
|
|
|
|
% via GitLab under
|
|
|
|
% https://gitlab.com/latexci/packages/LatexPackages
|
|
|
|
% The latest version of the built packages can be obtained via GitLab under
|
|
|
|
% https://gitlab.com/latexci/packages/LatexPackagesBuild
|
|
|
|
% For further information see the urls above.
|
|
|
|
% Reportings of bugs, suggestions and improvements are welcome, see the README
|
|
|
|
% at the Git repository for further information.
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
|
2022-01-31 00:49:04 +01:00
|
|
|
\ProvidesExplPackage{mkessler-refproof}{2022/01/30}{2.8.1-9-g4bda829}{Automatic references to theorems in proofs. Claim counters within proofs}
|
2022-01-30 21:47:14 +01:00
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\ExplSyntaxOn
|
|
|
|
|
|
|
|
\RequirePackage{amssymb}
|
|
|
|
\RequirePackage{amsthm}
|
|
|
|
\RequirePackage{xparse}
|
|
|
|
\RequirePackage{refcount}
|
|
|
|
\RequirePackage{translator}
|
|
|
|
\RequirePackage{mkessler-subproof} % TODO: let PyTeX format the mkessler- prefix
|
|
|
|
|
|
|
|
|
|
|
|
%%%% Hook management
|
|
|
|
|
|
|
|
\cs_new:Npn\__mkessler_refproof_autoref:n
|
|
|
|
{
|
|
|
|
\ref
|
|
|
|
}
|
|
|
|
|
|
|
|
\AddToHook{package/hyperref/after}
|
|
|
|
{
|
|
|
|
\cs_set:Npn\__mkessler_refproof_autoref:n
|
|
|
|
{
|
|
|
|
\autoref
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
%%% Saving old definitions
|
|
|
|
|
|
|
|
\cs_new_eq:NN \__mkessler_refproof_saved_proof:w \proof
|
|
|
|
\cs_new_eq:NN \__mkessler_refproof_saved_endproof: \endproof
|
|
|
|
\cs_new_eq:NN \__mkessler_refproof_saved_subproof:n \rawsubproof
|
|
|
|
\cs_new_eq:NN \__mkessler_refproof_saved_endsubproof: \rawendsubproof
|
|
|
|
|
|
|
|
%%% Internal variables
|
|
|
|
|
|
|
|
\int_new:N \__mkessler_refproof_proofdepth_int
|
|
|
|
\seq_new:N \__mkessler_refproof_nested_claim_counter_values_seq
|
|
|
|
\prop_new:N \__mkessler_refproof_refproof_claim_counters_prop
|
|
|
|
|
|
|
|
\cs_generate_variant:Nn \seq_push:Nn { N x }
|
|
|
|
|
|
|
|
%%% Language translations
|
|
|
|
|
|
|
|
\usedictionary{translator-proof-dictionary}
|
|
|
|
|
|
|
|
%%%Now, we internally got a proof and a subproof environment
|
|
|
|
%%%Make them available as 'old' variants, with their defautl behaviour
|
|
|
|
\NewDocumentEnvironment{oldproof}{ o }
|
|
|
|
{
|
|
|
|
\IfValueTF { #1 }
|
|
|
|
{
|
|
|
|
\__mkessler_refproof_saved_proof:w { #1 }
|
|
|
|
}
|
|
|
|
{
|
|
|
|
\__mkessler_refproof_saved_proof:w
|
|
|
|
}
|
|
|
|
}
|
|
|
|
{
|
|
|
|
\__mkessler_refproof_saved_endproof:
|
|
|
|
}
|
|
|
|
|
|
|
|
\NewDocumentEnvironment{oldsubproof}{ o }
|
|
|
|
{
|
|
|
|
\IfValueTF { #1 }
|
|
|
|
{
|
|
|
|
\__mkessler_refproof_saved_subproof:n { #1 }
|
|
|
|
}
|
|
|
|
{
|
|
|
|
\__mkessler_refproof_saved_subproof:n { \translate { Subproof } }
|
|
|
|
}
|
|
|
|
}
|
|
|
|
{
|
|
|
|
\__mkessler_refproof_saved_endsubproof:
|
|
|
|
}
|
|
|
|
|
|
|
|
%%% Main implementation
|
|
|
|
|
|
|
|
%Introduce claim environment
|
|
|
|
\newtheorem{claim}{\translate{Claim}}
|
|
|
|
\newtheorem*{claim*}{\translate{Claim}}
|
|
|
|
\AtBeginDocument{\def\claimautorefname{\translate{Claim}}}
|
|
|
|
|
|
|
|
|
|
|
|
\cs_new:Nn \__mkessler_refproof_enter_proof:
|
|
|
|
{
|
|
|
|
\int_gincr:N \__mkessler_refproof_proofdepth_int
|
|
|
|
\seq_gpush:Nx \__mkessler_refproof_nested_claim_counter_values_seq
|
|
|
|
{
|
|
|
|
\arabic { claim }
|
|
|
|
}
|
|
|
|
\group_begin:
|
|
|
|
}
|
|
|
|
|
|
|
|
\cs_new:Nn \__mkessler_refproof_leave_proof:
|
|
|
|
{
|
|
|
|
\group_end:
|
|
|
|
\seq_gpop:NN \__mkessler_refproof_nested_claim_counter_values_seq \l_tmpa_tl
|
|
|
|
\setcounter { claim } { \tl_use:N \l_tmpa_tl }
|
|
|
|
\int_gdecr:N \__mkessler_refproof_proofdepth_int
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
% Usage:
|
|
|
|
% #1 = \BooleanTrue or \BooleanFalse indicating presence of star
|
|
|
|
% #2 = star version of translation
|
|
|
|
% #3 = nonstar version of translation
|
|
|
|
\cs_new:Nn \__mkessler_refproof_set_proof_prefix:nnn
|
|
|
|
{
|
|
|
|
\IfBooleanTF { #1 }
|
|
|
|
{
|
|
|
|
\cs_set:Nn \__mkessler_refproof_proof_prefix:
|
|
|
|
{
|
|
|
|
\translate { #2 }
|
|
|
|
}
|
|
|
|
}
|
|
|
|
{
|
|
|
|
\cs_set:Nn \__mkessler_refproof_proof_prefix:
|
|
|
|
{
|
|
|
|
\translate { #3 }
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
\cs_new:Nn \__mkessler_refproof_proof_comment:n
|
|
|
|
{
|
|
|
|
\IfValueT { #1 }
|
|
|
|
{
|
|
|
|
\c_space_tl ( #1 )
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
\NewDocumentEnvironment{refproof}{s m !o}
|
|
|
|
{
|
|
|
|
\__mkessler_refproof_enter_proof:
|
|
|
|
|
|
|
|
\prop_get:NnN
|
|
|
|
\__mkessler_refproof_refproof_claim_counters_prop
|
|
|
|
{ #2 }
|
|
|
|
\l_tmpa_tl
|
|
|
|
|
|
|
|
\quark_if_no_value:NTF \l_tmpa_tl
|
|
|
|
{
|
|
|
|
\setcounter { claim } { 0 }
|
|
|
|
\__mkessler_refproof_set_proof_prefix:nnn { #1 }
|
|
|
|
{ Proof* ~ of }
|
|
|
|
{ Proof ~ of }
|
|
|
|
}
|
|
|
|
{
|
|
|
|
\setcounter { claim } { \tl_use:N \l_tmpa_tl }
|
|
|
|
\__mkessler_refproof_set_proof_prefix:nnn { #1 }
|
|
|
|
{ Continuation ~ of ~ proof* ~ of }
|
|
|
|
{ Continuation ~ of ~ proof ~ of }
|
|
|
|
}
|
|
|
|
% Set up counter number printing as subindexed by numbering of the reference
|
|
|
|
\renewcommand \theclaim
|
|
|
|
{
|
|
|
|
\getrefnumber { #2 } . \arabic { claim }
|
|
|
|
}
|
|
|
|
\__mkessler_refproof_saved_proof:w
|
|
|
|
[
|
|
|
|
\__mkessler_refproof_proof_prefix:
|
|
|
|
\c_space_tl
|
|
|
|
\__mkessler_refproof_autoref:n { #2 }
|
|
|
|
\__mkessler_refproof_proof_comment:n { #3 }
|
|
|
|
]
|
|
|
|
}
|
|
|
|
{
|
|
|
|
\__mkessler_refproof_saved_endproof:
|
|
|
|
\prop_gput:Nnx \__mkessler_refproof_refproof_claim_counters_prop
|
|
|
|
{ #2 }
|
|
|
|
{
|
|
|
|
\value{claim}
|
|
|
|
}
|
|
|
|
\__mkessler_refproof_leave_proof:
|
|
|
|
}
|
|
|
|
|
|
|
|
%%% A 'smart' proof environment
|
|
|
|
\AtBeginDocument{
|
|
|
|
\RenewDocumentEnvironment{proof}{!s !o}
|
|
|
|
{
|
|
|
|
\__mkessler_refproof_enter_proof:
|
|
|
|
|
|
|
|
\setcounter{claim}{0}
|
|
|
|
|
|
|
|
\renewcommand \theclaim
|
|
|
|
{
|
|
|
|
\arabic { claim }
|
|
|
|
}
|
|
|
|
\int_compare:nNnTF \__mkessler_refproof_proofdepth_int > 1
|
|
|
|
{
|
|
|
|
\__mkessler_refproof_set_proof_prefix:nnn { #1 }
|
|
|
|
{ Subproof* }
|
|
|
|
{ Subproof }
|
|
|
|
\__mkessler_refproof_saved_subproof:n
|
|
|
|
{
|
|
|
|
\__mkessler_refproof_proof_prefix:
|
|
|
|
\__mkessler_refproof_proof_comment:n { #2 }
|
|
|
|
}
|
|
|
|
}
|
|
|
|
{
|
|
|
|
\__mkessler_refproof_set_proof_prefix:nnn { #1 }
|
|
|
|
{ Proof* }
|
|
|
|
{ Proof }
|
|
|
|
\__mkessler_refproof_saved_proof:w
|
|
|
|
[
|
|
|
|
\__mkessler_refproof_proof_prefix:
|
|
|
|
\__mkessler_refproof_proof_comment:n { #2 }
|
|
|
|
]
|
|
|
|
}
|
|
|
|
}
|
|
|
|
{
|
|
|
|
\__mkessler_refproof_saved_endproof:
|
|
|
|
\__mkessler_refproof_leave_proof:
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
\RenewDocumentEnvironment{subproof}{!s !o}
|
|
|
|
{
|
|
|
|
\__mkessler_refproof_enter_proof:
|
|
|
|
|
|
|
|
\setcounter { claim } { 0 }
|
|
|
|
\renewcommand \theclaim
|
|
|
|
{
|
|
|
|
\arabic { claim }
|
|
|
|
}
|
|
|
|
|
|
|
|
\__mkessler_refproof_set_proof_prefix:nnn { #1 }
|
|
|
|
{ Subproof* }
|
|
|
|
{ Subproof }
|
|
|
|
\__mkessler_refproof_saved_subproof:n
|
|
|
|
{
|
|
|
|
\__mkessler_refproof_proof_prefix:
|
|
|
|
\__mkessler_refproof_proof_comment:n { #2 }
|
|
|
|
}
|
|
|
|
}
|
|
|
|
{
|
|
|
|
\__mkessler_refproof_saved_endsubproof:
|
|
|
|
\__mkessler_refproof_leave_proof:
|
|
|
|
}
|
|
|
|
|
|
|
|
\DeclareDocumentCommand { \proofdepth } { }
|
|
|
|
{
|
|
|
|
\int_to_arabic:n \__mkessler_refproof_proofdepth_int
|
|
|
|
}
|