5

I am trying to expand a macro as part of a style within a forest tree.

Here's an MWE:

\documentclass[tikz,border=5pt]{standalone}
\usepackage{forest,ifthen}
\begin{document}
\bracketset{action character=@}
\newcount\linesleptcount
\newcounter{lineleaps}
\setcounter{lineleaps}{0}
\newcommand\prooftreeleaping[2]{%
  @@\linesleptcount=1
  \edef\xtemp{[#2]}%
  \whiledo{#1 > \the\linesleptcount}{%
    \advance\linesleptcount1
    \let\oldxtemp\xtemp
    \edef\xtemp{@+[, shape=coordinate, \oldxtemp]}%
  }%
  \expandafter\bracketResume\xtemp
}
\forestset{
  declare count={leaps}{0},
  to line/.style n args=2{
      replace by={
        @+\prooftreeleaping{#1}{#2}
    },
  },
}
\begin{forest}
  [first line
    [second line]
    [staying put,
      @+\prooftreeleaping{3}{moving down}
    ]
    [staying put,
%     to line={3}{getting stuck}
    ]
  ]
\end{forest}
\end{document}

This works fine:

moving downwards

However, if I uncomment

%     to line={3}{getting stuck}

it does not work. Specifically, it tells me that it is inserting \csname and then it complains that control sequences from the macro should not be used within \csname... \endcsname:

! Missing \endcsname inserted.
<to be read again> 
                   \linesleptcount 
l.41 \end{forest}

? h
The control sequence marked <to be read again> should
not appear between \csname and \endcsname.

The intended output is:

not getting stuck

How can I resolve this?

Note that if this seems a bizarre thing to want to do, it is part of a larger thing I'm attempting and, for various reasons which would exceed the site's character limit on posts, this currently seems the least unpromising approach. (Basically, I want to line not to require single branches in prooftrees.]

  • If I try \prooftreeleaping{3}{moving down} I see that the input stream should receive @+[, shape=coordinate, @+[, shape=coordinate, [moving down]]]. Is this really what's expected? – egreg May 10 '15 at 9:13
  • @egreg Thanks! Not really what's expected, but how did you 'see' that the input stream expected that exactly? – cfr May 10 '15 at 13:34
  • 1
    I tried \prooftreeleaping{3}{moving down} with \show\xtemp instead of \expandafter\bracketResume\xtemp – egreg May 10 '15 at 13:38
6

replace by and other dynamic tree keys check if their argument is a node specification simply by checking if the argument starts with a [ (see the definition of \forest@nodehandleby@nnb@checkfirst). In your case, it does not, so forest tries to interpret @+\prooftreeleaping{#1}{#2} as a node walk.

I guess this should be mentioned in the documentation. Will do. (I don't think that implementing some other check is worth the effort.)

A workaround might be to redefine \prooftreeleaping to yield only the content of the node, i.e. no outer [], as I do below. Note that the desired effect is achieved not by replace by, but rather by append. (Also node that @+ in the definition of \xtemp is unnecessary.)

\newcommand\prooftreeleaping[2]{%
  @@\linesleptcount=1
  \edef\xtemp{#2}%
  \whiledo{#1 > \the\linesleptcount}{%
    \advance\linesleptcount1
    \let\oldxtemp\xtemp
    \edef\xtemp{, shape=coordinate, [\oldxtemp]}%
  }%
  \expandafter\bracketResume\xtemp
}
\forestset{
  declare count={leaps}{0},
  to line/.style n args=2{
      append={
        [@+\prooftreeleaping{#1}{#2}]
    },
  },
}
  • Thanks! This is really helpful - especially the information about what forest is looking for. I actually need replace by which is why it was there - I overlooked it when minimising the example. Now I just need a way of keeping the node's options other than to line with the node... ;) as this solution unfortunately breaks other bits. – cfr May 10 '15 at 13:33
  • Is there any way to align a node to a particular tier after xy is computed for the tree? The only reason I'm trying to do this this way is because I couldn't get the tier alignment to work in this case. – cfr May 10 '15 at 14:47
  • I guess I should just stick to 'to line requires single branches'... nothing is perfect :( but I currently have no clue how to actually make this work. – cfr May 10 '15 at 14:57
  • Never mind - thanks. I think I figured out an alternative... ;). – cfr May 10 '15 at 16:09
  • See tex.stackexchange.com/a/242261 in case you are curious ;). Your answer is really useful even though I didn't end up needing to do this in this particular case. [I know the code is messy and probably has lots of other bugs.] – cfr May 10 '15 at 16:34
2

This is not a direct answer to the question. Rather it illustrates the outcome of the process which involved this question.

EDIT: v0.06 does away with the need to specify phantom for the root, although it is still necessary to leave an empty node if not using a theorem statement. More significantly, it provides an environment as an alternative to the forest style. The environment does not require an empty root. Rather, you just start the tree. The syntax is

\begin{prooftree}{<options>}
  <proof using bracket notation>
\end{prooftree}

It should not even be necessary for the proof to have a single root if using the prooftree environment. (Of course, usually there will be a single root.)

To specify a theorem statement, you can use the option to prove={<theorem statement>} in the options passed to prooftree.

The mandatory argument consists of the preamble of the tree. It may be empty but it must be given. It may include the options provided by prooftree and anything you would otherwise put in the preamble of a forest tree. Usually, the options will be the ones provided by prooftree, of course, because the style is quite specific. But, in theory, you could override everything prooftree does via the <options> just as you could after specifying proof tree style in the preamble to a forest.

For example, the following creates two pairs of identical trees. The first uses the prooftree environment. The second uses the proof tree forest style. The first pair include no theorem statement so the second must begin with an empty node, as it uses proof tree as a forest style. The first, however, begins with the first assumption as it uses the new prooftree environment.

\documentclass[tikz,border=5pt,multi]{standalone}
\usepackage{etex,prooftrees}
\usepackage{amssymb}
\usepackage{mathtools,turnstile}
\newcommand*{\tnot}{\ensuremath{\mathord{\sim}}}
\begin{document}
  \begin{prooftree}{single branches}
        [$P \vee (Q \vee \lnot R)$, grouped,  just=Ass
        [$P \supset \lnot R$, grouped,  just=Ass
        [$Q \supset \lnot R$, grouped,  just=Ass
        [$\lnot\lnot R$, grouped, just={Negated conclusion}
          [$P$,  just={1 $\vee$ Elim}
            [$\lnot R$,  close, just={2,5 $\supset$ Elim; 5 $\vee$ Elim}
            ]
          ]
          [$Q \vee \lnot R$
            [$Q$
              [$\lnot R$,  close, just={3,6 $\supset$ Elim}
              ]
            ]
            [$\lnot R$, close
            ]
          ]
        ]
        ]
        ]
        ]
  \end{prooftree}
 \begin{forest}
    proof tree,
    single branches,
    [
        [$P \vee (Q \vee \lnot R)$, grouped,  just=Ass
        [$P \supset \lnot R$, grouped,  just=Ass
        [$Q \supset \lnot R$, grouped,  just=Ass
        [$\lnot\lnot R$, grouped, just={Negated conclusion}
          [$P$,  just={1 $\vee$ Elim}
            [$\lnot R$,  close, just={2,5 $\supset$ Elim; 5 $\vee$ Elim}
            ]
          ]
          [$Q \vee \lnot R$
            [$Q$
              [$\lnot R$,  close, just={3,6 $\supset$ Elim}
              ]
            ]
            [$\lnot R$, close
            ]
          ]
        ]
        ]
        ]
        ]
    ]
  \end{forest}

  \begin{prooftree}
    {
      to prove={$(\exists x)(\forall y)(Py \equiv x = y) \vdash (\exists x)((\forall y)(Py \supset x = y) \,\&\, Px)$}
    }
    [{$(\exists x)(\forall y)(Py \equiv x = y)\ \checkmark a$}, just={Premise}
      [{$\tnot (\exists x)((\forall y)(Py \supset x = y) \,\&\, Px)\ \backslash a$}, just={Conclusion negated}
        [{$(\forall y)(Py \equiv a = y)\ \backslash a,b$}, just={From 1}
          [{$\tnot ((\forall y)(Py \supset a = y) \,\&\, Pa)\ \checkmark$}, just={From 2}
            [{$Pa \equiv a = a\ \checkmark$}, just={From 3}
              [{$Pa$}, just={From 5}
                [{$a = a$}, just={From 5}
                  [{$\tnot (\forall y)(Py \supset a = y)\ \checkmark b$}, just={From 4}
                    [{$\tnot (Pb \supset a = b)\ \checkmark$}, just={From 8}
                      [{$Pb$}, just={From 9}
                        [{$a \neq b$}, just={From 9}
                          [{$Pb \equiv a = b\ \checkmark$}, just={From 3}
                            [{$Pb$}, just={From 12}
                              [{$a = b$}, just={From 12}
                                [{$a \neq a$}, just={From 11,14}, close
                                ]
                              ]
                            ]
                            [{$\tnot Pb$}
                              [{$a \neq b$}, close
                              ]
                            ]
                          ]
                        ]
                      ]
                    ]
                  ]
                  [{$\tnot Pa$}, close
                  ]
                ]
              ]
              [{$\tnot Pa$}
                [{$a \neq a$}, close
                ]
              ]
            ]
          ]
        ]
      ]
    ]
  \end{prooftree}
  \begin{forest}
    proof tree,
    [{$(\exists x)(\forall y)(Py \equiv x = y) \vdash (\exists x)((\forall y)(Py \supset x = y) \,\&\, Px)$}
      [{$(\exists x)(\forall y)(Py \equiv x = y)\ \checkmark a$}, just={Premise}
        [{$\tnot (\exists x)((\forall y)(Py \supset x = y) \,\&\, Px)\ \backslash a$}, just={Conclusion negated}
          [{$(\forall y)(Py \equiv a = y)\ \backslash a,b$}, just={From 1}
            [{$\tnot ((\forall y)(Py \supset a = y) \,\&\, Pa)\ \checkmark$}, just={From 2}
              [{$Pa \equiv a = a\ \checkmark$}, just={From 3}
                [{$Pa$}, just={From 5}
                  [{$a = a$}, just={From 5}
                    [{$\tnot (\forall y)(Py \supset a = y)\ \checkmark b$}, just={From 4}
                      [{$\tnot (Pb \supset a = b)\ \checkmark$}, just={From 8}
                        [{$Pb$}, just={From 9}
                          [{$a \neq b$}, just={From 9}
                            [{$Pb \equiv a = b\ \checkmark$}, just={From 3}
                              [{$Pb$}, just={From 12}
                                [{$a = b$}, just={From 12}
                                  [{$a \neq a$}, just={From 11,14}, close
                                  ]
                                ]
                              ]
                              [{$\tnot Pb$}
                                [{$a \neq b$}, close
                                ]
                              ]
                            ]
                          ]
                        ]
                      ]
                    ]
                    [{$\tnot Pa$}, close
                    ]
                  ]
                ]
                [{$\tnot Pa$}
                  [{$a \neq a$}, close
                  ]
                ]
              ]
            ]
          ]
        ]
      ]
    ]
  \end{forest}
\end{document}

First tree from first pair of trees (the second is identical):

<code>prooftree</code> tree proof

First tree from second pair of trees (the second is identical):

<code>prooftree</code> tree proof

Package code (v0.06):

%% Copyright 2015 Clea F. Rees
\NeedsTeXFormat{LaTeX2e}
\RequirePackage{svn-prov}
\ProvidesPackageSVN{$Id: prooftrees.sty 3594 2015-06-22 02:12:59Z cfrees $}[v0.06 \filebase \revinfo]
\RequirePackage{forest}
\newcounter{prooftree@countlevels}% count the levels in the proof tree
\setcounter{prooftree@countlevels}{0}
\newcount\prooftree@lcount% count the line numbers (on the left)
\newcount\prooftree@jcount% count the justifications (on the right)
\forestset{
  declare boolean={numbers}{0},% line numbering
  declare boolean={justifiers}{0},% line justifications
  declare boolean={verticals}{0},% single branches
  grouped/.style={% this adjusts the alignment of line numbers and justifications when some levels of the tree are grouped together either whenever the number of children is only 1 or by applying the grouped style to particular nodes when specifying the tree
    before computing xy={
      l=\baselineskip,
      if={\forestove{numbers}==1}{
        if={\forestove{justifiers}==1}{
          node walk={
            every step/.style={l=\baselineskip},
            after walk/.style={l=\baselineskip},
            name/.wrap pgfmath arg={just ##1}{level()},
            name/.wrap pgfmath arg={line no ##1}{level()},
          },
        }{
          node walk={
            after walk/.style={l=\baselineskip},
            name/.wrap pgfmath arg={line no ##1}{level()},
          },
        },
      }{
        if={\forestove{justifiers}==1}{
          node walk={
            after walk/.style={l=\baselineskip},
            name/.wrap pgfmath arg={just ##1}{level()}
          },
        }{},
      },
    },
    no edge,
  },
  close/.style={
    label={[yshift=2.5pt]below:$\otimes$},
  },
  line no/.style={% creates the line numbers on the left
    no edge,
    before typesetting nodes={% page 51
      TeX={\advance\prooftree@lcount1},
      content/.expanded={\the\prooftree@lcount.},% content i.e. the line number
      name/.expanded={line no \the\prooftree@lcount},% name them so they can be moved later
      if={\the\prooftree@lcount>2}{% the initial location of most line numbers is incorrect and they must be moved
        for previous={% move the line number below the previous line number
          append/.expanded={line no \the\prooftree@lcount}
        },
      }{},
    },
  },
  line justification/.style={% creates the justifications on the right but does not yet specify any content
    anchor=base west,
    no edge,
    before typesetting nodes={% page 51
      TeX={\advance\prooftree@jcount1},
      name/.expanded={just \the\prooftree@jcount},% name them so they can be moved
      if={\the\prooftree@jcount>2}{% correct the location as for the line numbers (cf. line no style)
        for previous={
          append/.expanded={just \the\prooftree@jcount}
        },
      }{},
    },
  },
  line numbering/.style={
    for tree={numbers},
  },
  no line numbering/.style={
    for tree={not numbers},
  },
  line justifications/.style={
    for tree={justifiers},
  },
  no line justifications/.style={
    for tree={not justifiers},
  },
  single branches/.style={
    for tree={verticals},
  },
  no single branches/.style={
    for tree={not verticals},
  },
  to prove/.style={
    before typesetting nodes={
      if level=0{
        content={#1},
        phantom=false,
      }{}
    }
  },
  proof tree/.style={
    for tree={
      parent anchor=south,
      line numbering,
      delay={
        where content={}{
          shape=coordinate,
        }{}
      },
    },
    where level=0{
      for children={
        no edge,
      },
      delay={
        if content={}{phantom}{},
        if={(\forestove{numbers}==1) || (\forestove{justifiers}==1)}{% count the levels if necessary
          for descendants={
            if={level()>\value{prooftree@countlevels}}{
              TeX={
                \stepcounter{prooftree@countlevels}
              },
            }{},
          },
        }{},
        if={(\forestove{numbers}==1)}{% create the line numbers if appropriate
          prepend={
            [,
              line no,
              repeat={\value{prooftree@countlevels}-1}{% most are created in the wrong place but line no moves them later
                delay n={\the\prooftree@lcount}{
                    append={[, line no]}
                },
              }
            ]
          },
        }{},
        if={(\forestove{justifiers}==1}{% create the nodes which will hold the justifications, if required
          append={
            [,
              fit=rectangle,
              line justification,
              repeat={\value{prooftree@countlevels}-1}{% most are created in the wrong place but line justification moves them later
                delay n={\the\prooftree@jcount}{
                  append={[, line justification]}
                },
              }
            ]
          }
        }{},
      },
    }{
      delay={
        if={(\forestove{verticals}==0}{% automatically group lines if not using single branches
          if n children=1{
            for children={
              if ={(\forestove{verticals}==0}{
                grouped
              }{},
            }
          }{},
        }{},
      }
    },
    before packing={
      for tree={
        tier/.wrap pgfmath arg={tier ##1}{level()},
      },
    },
  },
  just/.style={
    if={\forestove{justifiers}==0}{
      for root={
        line justifications,
      },
    }{},
      before packing={% puts the content of the justifications into the empty justification nodes on the right; because this is done late, the nodes need to be typeset again
        for={name/.wrap pgfmath arg={just ##1}{level()}}{
          content={#1},
          typeset node
        },
      }
  },
  toing/.style={% this is here so I can easily override no edge when to line={} is used
    edge path={
      \noexpand\path [draw, \forestoption{edge}] (!u.parent anchor) -- (.child anchor)\forestoption{edge label};
    },
  },
  to line/.style={% this option is intended for use with justifications and, although it should not give an error, it will have no effect in other cases (There is simply no reason to typeset a proof with this if not giving justifications, that I can think of)
    if={#1>\value{prooftree@countlevels}}{% ensure that we get enough lines in the tree since #1 may well specify a line which would not otherwise exist
      TeX={
        \setcounter{prooftree@countlevels}{#1}
      },
    }{},
    if={#1>level()}{% only try to move the node if the target line number exceeds the current level
      if={\forestove{justifiers}==0}{% don't do anything if there are no justifications - there is no point in moving things in such a case
      }{
        if={\forestove{verticals}==0}{% if no single branches, get the vertical alignment from the correctly aligned line justification
          before drawing tree={
            y/.wrap pgfmath arg={##1}{y("!name={just #1}")},
            toing
          },
        }{
          before packing={% if single branches, a simple tier alignment suffices
            tier=tier #1,
          },
        },
      },
    }{},
  },
  just to line/.style n args=2{
    if={\forestove{justifiers}==0}{
      for root={
        line justifications,
      },
    }{},
    if={#1>\value{prooftree@countlevels}}{% make sure the tree contains enough lines since #1 may exceed the total line count otherwise
      TeX={
        \setcounter{prooftree@countlevels}{#1}
      },
    }{},
    if={#1>level()}{% only if the target line number exceeds the current level
      before packing={
        for={name={just #1}}{% specify the content of the target line justification and, because this is done late, typeset the node again
          content={#2},
          typeset node
        },
      }
    }{% do nothing if the target line number is less than the current level
      if={#1==level()}{% only if the target line number equals the current level
        just=#2,
      }{},
    },
  },
}
\environbodyname\prooftreebody
\bracketset{action character=@}
\NewEnviron{prooftree}[1]{% \forest/\endforest from egreg's answer at http://tex.stackexchange.com/a/229608/
  \forest
    proof tree,
    #1,
    [@\prooftreebody]
  \endforest}
\endinput
%% end prooftrees.sty
  • Note that a later version of this package is now on CTAN. Please do not use the version above, which I leave because otherwise the explanation of the question doesn't make much sense. – cfr Mar 22 '16 at 3:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.