latex-packages/src/wip/refproof.pysty

__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}}