Ghilbert expexp: structured calculational proof

Ghilbert expexp: structured calculational proof

$
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\calcop}[2]{\notag \\ #1 \;\;\; & \;\;\; \langle\mbox{#2}\rangle \notag \\ \quad & }
\newcommand{\endcalc}{\notag \end{align}}
\newcommand{\subcalc}{\quad \begin{aligned} \\ \bullet \quad &}
\newcommand{\subcalcop}[2]{\calcop{#1}{#2} \subcalc}
\newcommand{\endsubcalc}{\notag \end{aligned} \\ \\ \cdot \quad &}
\newcommand{\nextsubcalc}{\notag \end{aligned} \\ \\ & \subcalc}
$_(Referenced in [Ghilbert Google group thread 'Step theorem display and HTML typesetting'](https://groups.google.com/d/topic/ghilbert/44niyKKts_8/discussion).)_

The current Ghilbert proof for `expexp` (see http://ghilbert-test.appspot.com/showthm/expexp?style=step) looks like this:

    # Exponentiation over exponentiation yields multiplication.
    thm (expexp () () (= (exp (exp A B) C) (exp A (* B C)))
    x (0) A B expexp.1
    x y A B expexp.1
    x (S y) A B expexp.1
    x C A B expexp.1
    # base case
    (exp A B) exp0
      B pa_ax5 (* B (0)) (0) A expeq2 ax-mp
      A exp0 eqtr
    eqtr4
    # inductive step
    (exp (exp A B) y) (exp A (* B y)) (exp A B) muleq2
      (exp A B) y expsuc
        B y pa_ax6 (* B (S y)) (+ (* B y) B) A expeq2 ax-mp
        A (* B y) B expadd eqtr
        (exp A (* B y)) (exp A B) mulcom eqtr
      eqeq12i
    sylibr
    finds
    )

From this, it should be possible to automatically generate the following structured calculational proof (http://users.abo.fi/jwright/schoolmath/, which builds on the format explained in [EWD1300](http://www.cs.utexas.edu/users/EWD/transcriptions/EWD13xx/EWD1300.html)):

$$
\calc
\textit{TRUE}
\subcalcop{\vdash}{expexp.1; expexp.1; expexp.1; expexp.1; subproof; subproof; finds}
    (A^B)^0
    \calcop = {exp0}
    1
    \calcop = {exp0}
    A^0
    \calcop = {pa_ax5}
    A^{B \cdot 0}
    \nextsubcalc
    (A^B)^{y'} = A^{B \cdot y'}
    \subcalcop \leftrightarrow {LHS: expsuc; RHS: subproof}
        A^{B \cdot y'}
        \calcop = {pa_ax6}
        A^{B \cdot y + B}
        \calcop = {expadd}
        A^{B \cdot y} \cdot A^B
        \calcop = {mulcom}
        A^B \cdot A^{B \cdot y}
        \endsubcalc
    A^B \cdot (A^B)^y = A^B \cdot A^{B \cdot y}
    \calcop \leftarrow {Leibniz}
    (A^B)^y = A^{B \cdot y}
    \endsubcalc
(A^B)^C = A^{B \cdot C}
\endcalc
$$

Note how all transitivity rules (eqtr, eqtr4, eqeq12i, sylibr, and also ax-mp) and all Leibniz-like rules (expeq2, muleq2) are left implicit in the proof format.

I think this proof format helps in understanding the _essential_ structure of the proof, so that the reader can skip the _accidental_ complexity of the different transitivity and Leibniz/substitution rules.

What is needed to generate the above?  Apart from defining a rendering for each 'constant', like `exp`, we must manually describe which rules are transitivity/Leibniz rules.  Additionally, we could associate a short piece of text ("hint") with theorems, to make them more readable.  In the above example, I have done that for `eqeq12i`, for which I have used "LHS: ...; RHS: ...".

See http://wiki.planetmath.org/cgi-bin/wiki.pl/metamathCalculationalProofs for more examples and discussion.