1

I'd like to define a custom environment for natural deduction proofs which prints tables that look like this:

enter image description here

At the moment, I use the tabular environment to write these proofs:

    \documentclass{article}
    \begin{document}
    Some random text.
    \begin{center}
    \begin{tabular}{|c|c|c|c|c|c|}
    \hline
    \multicolumn{2}{|c|}{Stars} & Line & Formula & Reference & Rule \\ \hline
    $\star$ && 1 & $p \to q$ & -- & Hyp \\ \hline
    &$\star$& 2 & $p$ & -- & Hyp \\ \hline
    $\star$~~&$\star$ & 3 & $q$ & 1, 2 & E$\to$\\ \hline
    \end{tabular}
    \end{center}
    \noindent
    Yet again some random text.
    \end{document}

As you can imagine, writing proofs this way is cumbersome, so I'd like to have my own environment for that. Here are some features I'd like to have implemented:

  • you specify the number of star columns with an argument
  • Whenever you write "*", LaTeX prints \star
  • Horizontal lines are added automatically so you don't need to use \hline every time
  • The Line column is numbered automatically so you can ignore it
  • If you specify less star cells than required, the remaining star cells are added as empty cells
  • The environment is centered by default
  • The paragraph after the table is not indented.

For example, the proof above could look like this in the new environment:

  \begin{ndproof}{2} % two star columns
   *& $p \to  q$ & -- & Hyp \\ % just one star cell specified, so second star cell empty
   &*& $p$ & -- & Hyp \\ 
   *&*&$p$ & 1, 2 & E$\to$ 
   \end{ndproof}

I'm new to LaTeX and this is a project that is simply too big for me. Can anyone of you help me out? Maybe you even have ideas to make the environment even better!

1 Answer 1

1

This is a possible approach:

\documentclass{article}
\usepackage{array}

\ExplSyntaxOn

\newcounter{LN}
\newcommand{\LN}{\stepcounter{LN}\theLN}

\NewDocumentEnvironment{ndproof}{m}
 {
  \[
  \setcounter{LN}{0}
  \begin{tabular}
   {
    *{#1}{|c} | % stars
    >{\LN}c   | % line
    >{$}c<{$} | % formula
    c         | % reference
    c         | % rule
   }
  \hline
  \multicolumn{#1}{|c|}{Stars} &
  \multicolumn{1}{c|}{Line} &
  \multicolumn{1}{c|}{Formula} &
  Reference &
  Rule \\
  \hline
 }
 {
  \end{tabular}
  \]
  \ignorespacesafterend
 }

\NewDocumentCommand{\ndline}{mmmm}
 {
  \vitus_addstars:n { #1 } & & #2 & #3 & #4 \\ \hline
 }

\cs_new_protected:Nn \vitus_addstars:n
 {
  \seq_set_split:Nnn \l_tmpa_seq { } { #1 }
  \seq_set_map:NNn \l_tmpb_seq \l_tmpa_seq { \__vitus_star:n { ##1 } }
  \seq_use:Nn \l_tmpb_seq { & }
 }
\cs_new_protected:Nn \__vitus_star:n
 {
  \str_case:nn { #1 } { {-}{} {*}{$\star$} }
 }

\ExplSyntaxOff

\begin{document}

Some words preceding the proof, let's make it long enough so that
it splits across lines in order to well present the job.
\begin{ndproof}{2}
\ndline{*-}{p\to q}{--}{Hyp}
\ndline{-*}{p}{--}{Hyp}
\ndline{**}{q}{1, 2}{E$\to$}
\end{ndproof}
Some words following the proof, let's make it long enough so that
it splits across lines in order to well present the job.

\end{document}

enter image description here

For the stars, I think it's necessary to specify - if you don't want it in a line. That also makes the input more consistent.

A fix for the case when the “Stars” header is a bit long for just two columns.

\documentclass{article}
\usepackage{array}

\ExplSyntaxOn

\newcounter{LN}
\NewDocumentCommand{\LN}{}{\stepcounter{LN}\theLN}

\NewDocumentEnvironment{ndproof}{m}
 {
  \[
  \setcounter{LN}{0}
  \settowidth{\dimen0}{Sterne}
  \setlength{\dimen0}{\dim_eval:n { \dimen0/2-\tabcolsep }}
  \use:x
   {
    \noexpand\begin{tabular}
     {
      *{#1}{|\int_compare:nTF{ #1=2 }{w{c}{\dimen0}}{c}} | % stars
      >{\LN}c   | % line
      >{$}c<{$} | % formula
      c         | % reference
      c         | % rule
     }
   }
  \hline
  \multicolumn{#1}{|c|}{Sterne} &
  \multicolumn{1}{c|}{Linie} &
  \multicolumn{1}{c|}{Formel} &
  Referenz &
  Regel \\
  \hline
 }
 {
  \end{tabular}
  \]
  \ignorespacesafterend
 }

\NewDocumentCommand{\ndline}{mmmm}
 {
  \vitus_addstars:n { #1 } & & #2 & #3 & #4 \\ \hline
 }

\cs_new_protected:Nn \vitus_addstars:n
 {
  \seq_set_split:Nnn \l_tmpa_seq { } { #1 }
  \seq_set_map:NNn \l_tmpb_seq \l_tmpa_seq { \__vitus_star:n { ##1 } }
  \seq_use:Nn \l_tmpb_seq { & }
 }
\cs_new_protected:Nn \__vitus_star:n
 {
  \str_case:nn { #1 } { {-}{} {*}{$\star$} }
 }

\ExplSyntaxOff

\begin{document}

Some words preceding the proof, let's make it long enough so that
it splits across lines in order to well present the job.
\begin{ndproof}{1}
\ndline{-}{p\to q}{--}{Hyp}
\ndline{-}{p}{--}{Hyp}
\ndline{*}{q}{1, 2}{E$\to$}
\end{ndproof}
Some words following the proof, let's make it long enough so that
it splits across lines in order to well present the job.
\begin{ndproof}{2}
\ndline{*-}{p\to q}{--}{Hyp}
\ndline{-*}{p}{--}{Hyp}
\ndline{**}{q}{1, 2}{E$\to$}
\end{ndproof}
Some words following the proof, let's make it long enough so that
it splits across lines in order to well present the job.
\begin{ndproof}{3}
\ndline{*--}{p\to q}{--}{Hyp}
\ndline{-*-}{p}{--}{Hyp}
\ndline{***}{q}{1, 2}{E$\to$}
\end{ndproof}
Some words following the proof, let's make it long enough so that
it splits across lines in order to well present the job.

\end{document}

enter image description here

3
  • This is awesome, thank you so much! There is just one little problem I don't understand: Since I'm writing these proofs in german, I changed the name of the first column to "Sterne". Now, the two columns below the star cell don't have the same width; the second is much wider. If I use three star proofs, on the other hand, this is not the case. I'm pretty sure it has something to do with the number of characters of "Sterne", but I'm not too sure. Is there an easy way to fix this? Commented Jun 24, 2021 at 16:52
  • @VitusSchäfftlein Added.
    – egreg
    Commented Jun 24, 2021 at 17:25
  • Awesome, thank you! Commented Jun 24, 2021 at 17:29

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .