allow to configure the proof labeling system in sproof

[kohlhase]

We should make the labeling system used for proof steps configurable. The current one is very intrusive.

[tpfeiffer]

In general, proofs follow a very strict structure (e.g. "Existence" and "Uniqueness" or "required" and "sufficient"), stricter than a complete human-understandable text in general. This is why semantically marking up parts of a proof might be even easier than marking up parts of a "normal" text.

However, it is, from my experience, very uncommon to have P.1, P.2, P.1.2 etc. within a proof. I would like these step numbers to disappear. Today, I can say \begin{spfstep}[title={Uniqueness}] and get "P.1 (Uniqueness)", where actually I would prefer a simple "Uniqueness:". Or, if I don't have a "title" to give, then just print nothing at all.

[kohlhase]

I have already some ideas on this but not the time to implement :-(. The idea is to add another level of indirection in labels. Currently the counters are set up to provide the proof label with the full proof tree path information. Instead of converting a path 3,4,7,1 into a label P3.P4.P7.P1 we should supply a macro named \prooflabel that we can customize. Then we would just call \prooflabel{3,4,7,1}.

Then what you want would just be achieved by

\def\prooflabel#1{}

And the old way of labeling would be achieved by defining

\def\prooflabel#1{\def\@path#1\@for\@I:={#1}\do{P\@I.}}

Moreover I think that I would also have a configuration key for subproofs that will allow to skip a whole level in the conters setup to get less chatty paths.

Finally, we would probably want to be able to change the labeling style with each proof hierarchy, e.g. with something like

\begin{proof}[labelstyle=classic]{this is really simple}
 \begin{cases}[labelstyle=alpha]{we have two cases}
    \begin{case}[labelstyle=empty]
  ....

The labelstyle=<stylespec> declaration would locally redefine the \prooflabel to \proof@<stylespec>@label, where we have defined above

\def\proof@empty@label#1{}
\def\proof@classic@label#1{\def\@path#1\@for\@I:={#1}\do{P\@I.}}
\def\proof@alpha@label#1{...}

and a couple of additional possibilities.

As I said, just first ideas that I want to document.

[kohlhase]

Actually, now that I look at things again, it seems that it is an even better idea to split the last level of the path off into a separate argument.

So we would have

\def\proof@empty@label#1#2{}
\def\proof@simple@label#1#2{#2}
\def\proof@full@label{\def\@path#1\@for\@I:=\@path\do{P\@I.}}

and so on.

[kohlhase]

I have added this and documented. I still want to be able to replace the description/item based markup for proofs.