Latex Proof Structuring Environment for the Course "Argumentation & Proof"

README.md

abproofs Proof Structuring Environment

Package containing a latex proof structuring environment according to the proof structuring rules of the course "Argumentation & Proof" / the proof tutorial of "Formal Methods of CS" at TU Vienna.

Installation

Place the file abproofs.sty inside of your latex working directory. Add the line \usepackage{abproofs} in your latex file.

Usage

Start a new proof

\begin{abproof}[NUM_INDENTS]

• NUM_INDENTS is optional, has to be a positive integer and specifies the number of needed indentations in your proof. The default is 6. The maximum I got it to work with is 11. The bigger this number is, the less indentation per indentation step is used.

State a new assumption

\ass{INDENT}{PROOF_STEP}

• INDENT is the level of indentation this proof step has
• PROOF_STEP is the content of the assumption itself

State a new proof step

\step{INDENT}{PROOF_STEP}{REF_STEPS}{TYPE}{OPERATOR}

• INDENT is again the level of indentation this proof step has
• PROOF_STEP is the content of the proof step itself
• REF_STEPS are the line numbers of the proof steps used to derive this step
• TYPE is the type of proof rule that was used (pr,us,def)
• OPERATOR is the operator of the used proof rule (\forall, \land, ...) - this part is always evaluated in math-mode, so there is no need to specify $$
• The last three parameters get formatted into (REF_STEPS; TYPE $OPERATOR$)

End the proof

\end{abproof}

Example

\begin{abproof}[4]

\ass{1}         {Let $x \in (A \setminus B)$ be arbitrary}
\step{1}        {$x \in A$ and $x \notin B$}                            {1}{def}{\setminus}
\step{1}        {$x \in A$}                                             {2}{us}{\land} 
\step{1}        {$x \notin B$}                                          {2}{us}{\land}
\step{1}        {$x \in \overline{B}$}                                  {4}{def}{\overline{\cdot}}
\step{1}        {$x \in (A \cap \overline{B})$}                         {3, 5}{def}{\cap}
\step{0}    {for all $x\in (A\setminus B):x\in (A\cap \overline{B})$}   {1-6}{pr}{\forall}
\step{0}    {$(A \setminus B) \subseteq (A \cap \overline{B})$}         {7}{def}{\subseteq}

\end{abproof}

abproofs.sty

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                 AB Proof Structuring Environment                                        %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Start a new proof using:
% \begin{abproof}[NUM_INDENTS]
%  - NUM_INDENTS is optional, has to be a positive integer and specifies the number 
%    of needed indentations in your proof. The default is 6. The maximum I got it
%    to work with is 11. The bigger this number is, the less indentation per
%    indentation step is used.

% State a new assumption using:
% \ass{INDENT}{PROOF_STEP}
%  - INDENT is the level of indentation this proof step has
%  - PROOF_STEP is the content of the assumption itself

% State a new proof step using:
% \step{INDENT}{PROOF_STEP}{REF_STEPS}{TYPE}{OPERATOR}
%  - INDENT is again the level of indentation this proof step has
%  - PROOF_STEP is the content of the proof step itself
%  - REF_STEPS are the line numbers of the proof steps used to derive this step
%  - TYPE is the type of proof rule that was used (pr,us,def)
%  - OPERATOR is the operator of the used proof rule (\forall, \land, ...) -
%      this part is always evaluated in math-mode, so there is no need to specify $$
% The last three parameters get formatted into (REF_STEPS; TYPE $OPERATOR$)

% End the proof using:
% \end{abproof}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% EXAMPLE:

%\begin{abproof}[4]
%
%\ass{1}         {Let $x \in (A \setminus B)$ be arbitrary}
%\step{1}        {$x \in A$ and $x \notin B$}                            {1}{def}{\setminus}
%\step{1}        {$x \in A$}                                             {2}{us}{\land} 
%\step{1}        {$x \notin B$}                                          {2}{us}{\land}
%\step{1}        {$x \in \overline{B}$}                                  {4}{def}{\overline{\cdot}}
%\step{1}        {$x \in (A \cap \overline{B})$}                         {3, 5}{def}{\cap}
%\step{0}    {for all $x\in (A\setminus B):x\in (A\cap \overline{B})$}   {1-6}{pr}{\forall}
%\step{0}    {$(A \setminus B) \subseteq (A \cap \overline{B})$}         {7}{def}{\subseteq}

%\end{abproof}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{abproofs}[]

\RequirePackage{calc}
\RequirePackage{expl3}
\RequirePackage{amssymb,amsfonts,amsmath,amsthm}

% New command for repeating other commands
\usepackage{calc}
\usepackage{expl3}
\usepackage{amssymb,amsfonts,amsmath,amsthm}

\ExplSyntaxOn
\cs_new_eq:NN \Repeat \prg_replicate:nn
\ExplSyntaxOff

% Custom Commands for proof structuring

\newcommand{\rl}[3]{(#1; #2 $#3$)}
\newcommand{\tabs}[1]{\Repeat{#1}{\>}}

\newcounter{abproofc}
\newcounter{abproofmaxindent}

\newcommand{\calculateNumberOfTabs}[2]{\number\numexpr#1-#2\relax}
\newcommand{\calculatedTabs}[2]{\tabs{\calculateNumberOfTabs{#1}{#2}}}

\newcommand{\step}[5]{\> \arabic{abproofc}. \> \tabs{#1} #2 \calculatedTabs{\arabic{abproofmaxindent}}{#1} \rl{#3}{#4}{#5} \stepcounter{abproofc}\\}
\newcommand{\ass}[2]{\> \arabic{abproofc}. \> \tabs{#1} #2 \calculatedTabs{\arabic{abproofmaxindent}}{#1} \stepcounter{abproofc}\\}

% Custom environment

\newenvironment{abproof}[1][6]{
% Set counters
\setcounter{abproofmaxindent}{#1}
\setcounter{abproofc}{1}
% Setup minipage and tabbing env
\begin{minipage}{0.7\textwidth}
\begin{tabbing}
\hspace*{1em} \= \hspace*{1.5em} \= \Repeat{\number\numexpr#1-1\relax}{\hspace*{\number\numexpr5/(#1-1)\relax em} \=} \hspace*{18em} \= \hspace*{5em} \kill
}{
\end{tabbing}
\end{minipage}
\setcounter{abproofc}{1}}

example-abproofs.tex

\documentclass[a4paper]{article}

\usepackage{amssymb,amsfonts,amsmath,amsthm}

\newtheorem{question}{Question}

\usepackage{abproofs}

\begin{document}

\begin{question}
  \noindent Prove $(A \setminus B) \subseteq (A \cap \overline{B})$
\end{question}

\begin{proof}
This proof is structured according to the structuring rules of the course \textit{Argumentation and Proof} / the proof tutorial of \textit{Formal Methods of CS} using the package \textit{abproofs}. \medskip

\begin{abproof}[4]
  \ass{1}         {Let $x \in (A \setminus B)$ be arbitrary}
  \step{1}        {$x \in A$ and $x \notin B$}                            {1}{def}{\setminus}
  \step{1}        {$x \in A$}                                             {2}{us}{\land} 
  \step{1}        {$x \notin B$}                                          {2}{us}{\land}
  \step{1}        {$x \in \overline{B}$}                                  {4}{def}{\overline{\cdot}}
  \step{1}        {$x \in (A \cap \overline{B})$}                         {3, 5}{def}{\cap}
  \step{0}    {for all $x\in (A\setminus B):x\in (A\cap \overline{B})$}   {1-6}{pr}{\forall}
  \step{0}    {$(A \setminus B) \subseteq (A \cap \overline{B})$}         {7}{def}{\subseteq}
\end{abproof}
\end{proof}

\end{document}

clean! thanks for your effort ❤️