\documentclass{article}
\usepackage{color}
\usepackage{alltt}
\usepackage{graphicx}
\usepackage{url}

\def\prover{proofweb}

\definecolor{mygreen}{rgb}{0,.75,0}
\definecolor{gray}{rgb}{.5,.5,.5}
\definecolor{orange}{rgb}{1,.5,0}
\def\green#1{\textcolor{mygreen}{#1}}
\def\red#1{\textcolor{red}{#1}}
\def\white#1{\textcolor{white}{#1}}
\def\black#1{\textcolor{black}{#1}}
\def\gray#1{\textcolor{gray}{#1}}
\def\orange#1{\textcolor{orange}{#1}}
\def\blue#1{\textcolor{blue}{#1}}
\def\redarrow{$\quad$\lower1.8pt\hbox{\LARGE\red{$\to$}}$\quad$}
\def\der#1#2#3{\setbox0=\hbox{$\strut #2$}%
\hbox to\wd0{$\hss\displaystyle{\strut{#1}\over\strut\box0}\rlap{$\,#3$}\hss$}}
\def\xder#1#2#3{\setbox0=\hbox{$\strut #2$}%
\hbox to\wd0{$\hss\displaystyle\white{{\strut{\black{#1}}\over\strut\black{\box0}}}\rlap{$\,#3$}\hss$}}
%\let\xder=\der
\def\leaf#1{\displaystyle{\strut\atop\strut #1}}
\def\lab#1{\green{\hspace{.5pt}\rlap{${\vrule height 7pt depth0pt width 0pt}^{\tt #1}$}}}
\def\third#1{\hbox{\vbox to 0pt{\vspace{.15em}\hbox{#1}\vss}}}
\def\lstrut{{\large\strut}}
\def\Lstrut{{\Large\strut}}
\def\skipforward{\noalign{\smallskip}}
\def\mbar{\multicolumn{1}{|l}{}}

\hyphenation{Proof-Web}

\raggedbottom

\begin{document}

\title{Deduction using the ProofWeb system}
\author{
Cezary Kaliszyk \\
Femke van Raamsdonk \\
Freek Wiedijk \\
Hanno Wupper \\
Maxim Hendriks \\
Roel de Vrijer
}
\date{}
\maketitle

\begin{abstract}
\noindent
This is the manual of the ProofWeb system that was
implemented at the Radboud University Nijmegen and the Free University Amsterdam
in the SURF education innovation project \emph{Web deduction for education in formal thinking}.
\end{abstract}

\newpage
\tableofcontents

\newpage
\section{Introduction}

This document is the manual of the ProofWeb system.
If you are just interested in using the system you can best skip
this introduction and directly go to Chapter~\ref{sec:session} on page~\pageref{sec:session}.

This document does \emph{not} explain mathematical logic in detail,
but is intended as a companion to a logic textbook
when using the ProofWeb system.
(For instance, one can read \cite{dal:04} for Gentzen style `tree' proofs, or
\cite{hut:rya:04} for Fitch style `box' proofs.)
However, the appendices of these notes can be used as a reference for natural deduction.

\bigskip
\noindent
ProofWeb is a system for practising natural deduction on a computer.
It is meant to be used in introductory courses in mathematical logic.
The logics that ProofWeb has been specifically designed for are the usual
basic ones:
\begin{quote}
-- first order propositional logic \\
-- first order predicate logic \\
-- first order predicate logic with equality
\end{quote}
\noindent
ProofWeb is designed for the classical variants of these logics, but
it is easy to work in ProofWeb in the constructive fragments of these
logics as well.

ProofWeb combines the following features:
\begin{itemize}
\item
ProofWeb has been designed to be as close as possible in look and feel to the 
way mathematical logic is taught in textbooks.
For Fitch style `box' proofs it specifically matches the conventions of
\emph{Logic in Computer Science: Modelling and Reasoning about
Systems} by Michael Huth and Mark Ryan \cite{hut:rya:04}, published by Cambridge University
Press.

\item
When using ProofWeb one is using the Coq proof assistant
(developed at the INRIA institute in France) without any
restrictions.
This means that with ProofWeb one is using a system that has the power to build computer proofs
like the one of the Four
Color Theorem \cite{gon:04}, or a proof of the correctness of an optimizing C compiler \cite{ler:06}.

\item
ProofWeb is used through the web.
One does not need to install any special software
to be able to use the system.
A web browser (without any ProofWeb specific plug-ins
and even without Java) is all that is needed.
Students will be able to work on their exercises from any
computer connected to the Internet (like for instance a computer in an Internet caf\'e),
without first having to copy their files or to install any special
software.

\item
With ProofWeb all files are on a central server.
Teachers will at all times be able to see the status of their students'
work, including their solutions to the exercises in full.
Also, the students' work can be easily backed up.

\item
ProofWeb comes with free course notes explaining the system.
(This is the text that you are currently reading.)

\item
ProofWeb comes with a database of around two hundred basic exercises.

\item
ProofWeb will automatically check whether solutions to exercises are
correct or not, and present this information both to the student and
the teacher in a clear tabular format.

\end{itemize}

\noindent
If you are a \emph{student} there are two ways to work with ProofWeb:
\begin{enumerate}
\item
Just go to the ProofWeb server provided by the Radboud University Nij\-me\-gen
\begin{center}
\texttt{http://\prover.cs.ru.nl/}
\end{center}
and use the free guest account.
There is no need to register or to provide a password.
(In this mode the full set of exercises is not available.
This way of working with ProofWeb is just for trying it out.)

\item
If you follow a course in mathematical logic that uses ProofWeb for the
practical work, then go to the ProofWeb server
of that course (which often also will be \texttt{\prover.cs.ru.nl}),
and use the account there that your teacher will have made for you.
Ask your teacher for the username and password of that account.

\end{enumerate}

\noindent
If you are a \emph{teacher} and want to use ProofWeb in your course,
then there also are two ways for this:
\begin{enumerate}
\item
Either you can host your course on the server of the Radboud University Nijmegen.
To do this send mail to
\begin{center}
\texttt{proofweb@cs.ru.nl}
\end{center}
and provide details about the course that you want to host.
This service is currently provided for free.

\item
Alternatively, you can host a ProofWeb server on a machine of your own.
To do this go to
\begin{center}
\texttt{http://\prover.cs.ru.nl/}
\end{center}
follow the link about installing the ProofWeb system,
and follow the installation instructions that will tell you what
files to download to install the ProofWeb system and
what to do with them.
(To follow these installation instructions on how to install ProofWeb,
you will need a machine running Linux.)

\end{enumerate}

\section{Using the system}\label{sec:session}

To use ProofWeb you need a web browser on a machine
connected to the Internet.
Unfortunately not all web browsers properly support the technologies
that ProofWeb uses.
For this reason Internet Explorer cannot be used.
Browsers that have been tested to work are recent versions of:
\begin{itemize}
\item
Gecko based browsers, like Mozilla, Firefox, Galeon,
Epiphany and Net\-scape.

\item
Webkit based browsers, like Safari and Konqueror.

\item
The Opera browser.

\end{itemize}
The ProofWeb system has been developed using Firefox.

\subsection{Logging in}

We will now explain the system by walking through a ProofWeb session.

We go to the URL of our ProofWeb server.
In the example that we are showing here this is
\begin{center}
\texttt{http://\prover.cs.ru.nl/}.
\end{center}
This shows us the main ProofWeb web page:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_00}
\end{center}

\noindent
We scroll down to the list of courses and click
on the link of our course:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_01}
\end{center}

\noindent
In this example we click the link `\texttt{Inleiding Logica 2007-2008}'
(which is Dutch for `Introduction to Logic'.)
This will get us to the login page for the course:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_02}
\end{center}

\noindent
We enter our username and password and click `{\small\texttt{GO TO USER PAGE}}'.
This logs us in to the system for the course that we are following.

\subsection{The list of exercises}

We now see the list of exercises for the course.
It gives for each exercise the name of file that holds the exercise,
an indication of the difficulty, the current status of the exercise, and
a button for resetting the exercise to its initial state.

\begin{center}
\includegraphics[scale=.47]{../shots/shot_03}
\end{center}

\noindent
The four possibilities for the status of an exercise are:
\begin{quote}
-- \gray{\textsf{Not touched}} \\
-- \red{\textsf{Incomplete}} \\
-- \orange{\textsf{Correct}} \\
-- \green{\textsf{Solved}}
\end{quote}
The colors are meant to resemble the colors of a traffic light.
(The challenge of ProofWeb is to have your list of
exercises be all green.)

We will explain the meaning of these statuses in detail below.
(The difference between `Correct' and `Solved' is that
according to the Coq system in both cases the solution to
the exercises has no errors, but that only in the latter
case is the solution restricted to deduction rules that are
allowed for the course.)

Now we scroll down in the list of exercises to the first exercise about
propositional logic called \textsf{prop\_001.v}:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_04}
\end{center}

\noindent
We click the button with the name of this file on the left.
This will open the exercise in the prover interface.

\subsection{The prover interface}

We are now looking at the prover interface of ProofWeb:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_05}
\end{center}

\noindent
It consists of a green menu bar at the top of our browser
window, and three \emph{panes}:
\begin{itemize}
\item 
On the left there is the pane in which we are editing a \emph{proof
script}.

\item
On the top right there is the pane that will show the \emph{proof state}
of our proof.
We will explain below what this means.
The proof state in this pane is shown in the style that is standard
when working with the Coq proof assistant.

Here also will be shown the messages of the Coq system that we are communicating
with on the ProofWeb server.

\item
On the bottom right there is the pane that shows the \emph{proof} that
we are working on.
The proof in this pane will be shown in the style that is customary
in mathematical logic teaching.

\end{itemize}

\noindent
ProofWeb can show the proof in the bottom right pane in three different
ways.
Depending on the course that you are following one of these proof display
styles already may be active.

To change the style of proof display one uses the \textsf{Display} menu.
Let us first put the system in the mode in which it displays proofs
in Gentzen `tree' style:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_06}
\end{center}

\noindent
Another setting that one might like to change when starting working
with ProofWeb is the `electric terminator'.
When this feature is active, typing a period (`\texttt{.}') automatically
executes the command that it terminates.
(Some people like this convenience, while others prefer to separate
typing their script from having the system execute their commands.)

To activate the electric terminator select \textsf{Toggle Electric Terminator}
from the \textsf{Debug} menu:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_07}
\end{center}

\noindent
We are now ready to start working on the exercise.
Currently the text on the left (the solution to the exercise that we
are editing)
has not yet been executed.
This text is a \emph{script}, consisting of commands that are
all terminated by a period character (`\texttt{.}').
One can execute those commands by clicking the downward arrow in the
green menu bar.
Alternatively one can execute the next command by holding down the control
key while simultaneously
typing the down-arrow key on the keyboard.

We now execute the commands (by clicking the down arrow) until we have executed the
\begin{quote}
\texttt{Proof.}
\end{quote}
command.
(At this point we are working on a proof, and
an incomplete proof will now
be displayed on the lower right.)
Then we remove the text
\begin{quote}
\texttt{(*!\ prop\char`\_proof *)}
\end{quote}
from the script.
It should be replaced by a series of commands that create a proof of
the statement.
We type the first command:
\begin{quote}
\texttt{imp\char`\_i H.}
\end{quote}
and execute it.
(The details of the commands that are available and what they mean will
be given below.)

We now have:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_08}
\end{center}

\noindent
On the bottom right the incomplete proof after this command now is:
\vspace{-\bigskipamount}
$$
\hspace{-2em}
\der{
\xder{
\leaf{\vdots}
}
{A}{}
}
{A \land B \to A}{{\to}\mbox{i}\,\green{\scriptstyle [{\tt H}]}}
$$
\noindent
The dots are the part of the proof that is not yet completed.
It has to be replaced by a valid proof of $A$ by issuing more commands in
the proof script.

On the top right we see the \emph{proof state} of the Coq
proof assistant that is checking our proof.
It looks like:
\begin{quote}
\def\\{\char`\\}
\def\up{\vspace{-\smallskipamount}}
\begin{alltt}
1 subgoal\medskip
  H : A /\\ B
  ============================
   A
\end{alltt}
\end{quote}
It means that our first \emph{subgoal} (out of only one) is
to prove the statement below the line, $A$, where
we are allowed to use the \emph{assumptions} above the line.
In this case there is only one assumption, $A \land B$.
The \emph{label} of this assumption is \texttt{H}, which is
how we should refer to the assumption in the script.
This `subgoal' corresponds to the triple dots in
the proof on the lower right.

We now look at what the proof looks like in the two
other display styles.
First here is what it looks like when instead of just
statements we ask the system to display \emph{sequents}:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_09}
\end{center}

\noindent
In this case the allowed assumptions are showed to the left of the
`turnstile' symbol (`$\vdash$').
Instead of just 
$$A$$
as the middle line of the proof we now have
$$A \land B \vdash A$$
Despite the change in presentation the proof has stayed exactly the same.

The third style is Fitch's `box style':

\begin{center}
\includegraphics[scale=.47]{../shots/shot_10}
\end{center}

\noindent
In this style the (incomplete) proof looks like:
\begin{center}
\begin{tabular}{llll}
\cline{2-4}
\Lstrut 1 & \multicolumn{1}{|l}{\green{\texttt{H:}}} & $A \land B$ & \multicolumn{1}{l|}{assumption} \\
\lstrut & \multicolumn{1}{|l}{} & \dots & \multicolumn{1}{l|}{} \\
\Lstrut 2 &\multicolumn{1}{|l}{} & $A$ & \multicolumn{1}{l|}{} \\
\cline{2-4}
\Lstrut 3 && $A \land B \to A$ & $\to$i 1---2
\end{tabular}
\end{center}
\noindent
Again the dots have to be filled in to complete the proof.

\bigskip
\noindent
We will now finish the exercise.
We add two more commands to the script:
\begin{quote}
\texttt{con\char`\_e1 (B).} \\
\texttt{exact H.}
\end{quote}
execute them, and then also execute the final
\begin{quote}
\texttt{Qed.}
\end{quote}
\noindent
This leads to the message 
\begin{quote}
\texttt{prop\char`\_001 is defined}
\end{quote}
at the top right where Coq shows its output:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_11}
\end{center}

\noindent
It means that the proof script is complete,
which means that it has generated a correct proof of the statement.

\subsection{Saving exercises}

We are now done with exercise (the script on the left is what it
should be).
We save the file on the server by selecting \textsf{Save} from the \textsf{File}
menu:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_12}
\end{center}

\noindent
This saves the script as the file \textsf{prop\_001.v} in the student's
directory on the ProofWeb server:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_13}
\end{center}

\noindent
Next, we select \textsf{Load / New} from the \textsf{File} menu to 
get back to the list with exercises:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_14}
\end{center}

\noindent
The system will warn us that we are leaving the page with
the script (it does not realize that it just has been saved):

\begin{center}
\includegraphics[scale=.47]{../shots/shot_15}
\end{center}

\noindent
Generally it is a good thing that ProofWeb will warn you about
this, but in this case we can of course ignore this message and click
\textsf{OK}.

\subsection{The status of the exercises}

We now again are looking at the list of exercises:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_16}
\end{center}

\noindent
The status of \textsf{prop\_001.v} has changed from a gray
\gray{\textsf{Not touched}}
to a green
\green{\textsf{Solved}}
because we saved a correct solution.

Instead of going for the next exercises, let us look what happens
when we save an incorrect solution.
We go back to the exercise by clicking the \textsf{prop\_001.v} button
once more, remove the lines
\begin{quote}
\texttt{con\char`\_e1 (B).} \\
\texttt{exact H.}
\end{quote}
from the proof script, save again, and go once more
to the list of exercises:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_17}
\end{center}

\noindent
The status now will be a red 
\red{\textsf{Incomplete}}.
This also will be the status when the file is not so much incomplete
as well just \emph{wrong}.

If you want to know why ProofWeb thinks there is an error in your
solution, you can click the
{\textsf{why?}}\ 
link next to the status.
You will get a new window that shows the error message of Coq:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_18}
\end{center}

\noindent
ProofWeb also has an orange status that is in between the green and the red ones
saying 
\orange{\textsf{Correct}}.
You get this when the file is correct Coq, but you modified it
in a way that is not allowed for the course.
For instance, you might ask Coq to do the proof for you, by
using the
\begin{center}
\texttt{tauto.}
\end{center}
command, which makes Coq run an automated propositional theorem
prover:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_19}
\end{center}

\noindent
This will prove the statement, but of course this is not an allowed
solution to the exercise.
Hence the status will become
\orange{\textsf{Correct}}
instead of
\green{\textsf{Solved}}:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_20}
\end{center}

\noindent
The
\orange{\textsf{Correct}}
status also will be given if you just delete all the text in the
file, as the empty file is a correct Coq file too.
Of course that is not an allowed solution to the 
exercise either.

Again, when the status is
\orange{\textsf{Correct}},
you can click on
{\textsf{why?}}\ 
to find out what you did that ProofWeb thinks is not
allowed in the course.
(The word
{\textsf{why?}}\ 
is a bit strange in this context,
as Coq will not so much explain why the thing is \emph{correct}, but
instead why it is \emph{not} `solved'.)
These error messages generally are a bit cryptic as well:

\begin{center}
\includegraphics[scale=.47]{../shots/shot_21}
\end{center}

\noindent
This ends our example of a ProofWeb session.
We will now discuss the system in detail.
First we will explain how to write formulas
in the ProofWeb system.

\section{Writing formulas}

The ASCII syntax for formulas of first order predicate logic is
given by the following table:
\begin{center}
\begin{tabular}{ccl}
$\bot$ && \texttt{False} \\
$\top$ && \texttt{True} \\
$\neg A$ && \texttt{\char`\~}$\;A$ \\
$A \land B$ && $A$\texttt{ /\char`\\\ }$B$ \\
$A \lor B$ && $A$\texttt{ \char`\\/ }$B$ \\
$A \to B$ && $A$\texttt{ -> }$B$ \\
$A \leftrightarrow B$ && $A$\texttt{ <-> }$B$ \\
$\forall x\, A$ && \texttt{all }$x$\texttt{, }$A$ \\
$\exists x\, A$ && \texttt{exi }$x$\texttt{, }$A$
\end{tabular}
\end{center}

\noindent
For example the formula
$$\exists x (P(x) \lor \neg Q(a)) \to Q(a) \to \exists x\,P(x)$$
is written in ASCII syntax as
\begin{center}
\texttt{exi x, (P(x) \char`\\/ \char`\~Q(a)) -> Q(a) -> exi x, P(x)}
\end{center}
Note that in ProofWeb one puts a comma after a quantifier.

Another slight deviation of the ProofWeb formula syntax from
standard syntax is that if a predicate has just a single variable
as the argument,
one is {allowed} to omit the brackets.
(It is not obligatory, though.)
Therefore the formula also might be written as:
\begin{center}
\texttt{exi x, (P x \char`\\/ \char`\~Q a) -> Q a -> exi x, P x}
\end{center}
In fact this is how Coq prints this formula back at the user.
(In the exercise files the formulas are always written with the
brackets present though.)

\bigskip
\noindent
\emph{A note for people who know the Coq system}:
In Coq a different notation for the quantifiers is customary:
\begin{center}
\begin{tabular}{ccl}
$\forall x\, A\enskip$ && \rlap{\texttt{forall }$x$ \texttt{:} $D$\texttt{, }$A$}\phantom{\texttt{all }$x$\texttt{, }$A$} \\
$\exists x\, A\enskip$ && \rlap{\texttt{exists }$x$ \texttt{:} $D$\texttt{, }$A$}
\end{tabular}
\end{center}
In this $D$ is the domain over which one quantifies.

There are two differences between the ProofWeb quantifiers and the
standard Coq quantifiers.
First, the ProofWeb quantifiers have a priority that is customary
in logic textbooks: they bind more strongly than the propositional
connectives.
The Coq quantifiers bind weakly, which is the standard in proof assistants.
For instance the formula
\begin{center}
\texttt{all x,\ A \char`\\/ B}
\end{center}
is read as
$$(\forall x\, A) \lor B$$
which is the reading of
$$\forall x\, A \lor B$$
in logic textbooks.
However
\begin{center}
\texttt{forall x :\ D,\ A \char`\\/ B}
\end{center}
is read as
$$\forall x\, (A \lor B)$$
Second, with the Coq quantifiers one indicates the domain.
The ProofWeb quantifiers do not need this, as they use a fixed domain \texttt{D}.
This domain is defined
in the file \texttt{ProofWeb.v} which is loaded at the start of the
ProofWeb exercises.

The Coq quantifiers can be useful for people who want to use ProofWeb for
complicated examples, in which different variables have different `types'.
In that case they can just use the Coq versions of the quantifiers.
The ProofWeb tactics, which are the subject of the next two chapters
have been programmed to work with either quantifier style.

%\noindent
%When formulas that are not single identifiers are used as arguments of tactics, they need to be put in brackets.
%
%The `\texttt{all}' and `\texttt{exi}' quantifiers bind more strongly
%than the built-in Coq quantifiers `\texttt{forall}' and `\texttt{exists}'.
%
%The `\texttt{all}' and `\texttt{exi}' internally use a function `\texttt{\char`\_K}'.
%If through a bug in one of the tactics this function ever appears in a goal, one should
%use the tactic `\texttt{remove\char`\_K}' to get rid of it (and report the bug).


\section{Gentzen style tree proofs}

This chapter explains how to build natural deduction proofs using
ProofWeb.
It treats a style of natural deduction introduced by Gerhard Gentzen
in 1935 in his dissertation at the University of G\"ottingen.
We will here call that style `tree proofs', to distinguish it
from the `box proofs' which will be the subject of the next chapter.

In this chapter we will not explain natural deduction proofs in detail.
You will need to read a textbook for that,
like Dirk van Dalen's \emph{Logic and Structure}
\cite{dal:04}.
Here we will just explain how to do this kind of proof in the ProofWeb system.

\subsection{Example on paper}

Here is an example of a natural deduction proof in predicate logic, in the
way that it is written on paper:
$$\label{proof:gentzen:large}
\def\green#1{\textcolor{white}{#1}}
\hspace{-12em}
\der{
\der{
\der{
\leaf{[\exists x (P(x) \lor \neg Q(a))]\lab{H1}}\qquad\qquad\qquad\qquad\qquad\enskip
\der{
\leaf{[P(b) \lor \neg Q(a)]\lab{H3}}\qquad\enskip
\der{
\leaf{[P(b)]\lab{H4}}
}
{\exists x\,P(x)}{{\exists}\mbox{i}}\qquad\qquad\enskip
\der{
\der{
\leaf{[\neg Q(a)]\lab{H5}}\quad\enskip
\leaf{[Q(a)]\lab{H2}}
}
{\bot}{{\neg}\mbox{e}}
}
{\exists x\,P(x)}{{\bot}\mbox{e}}
}
{\exists x\,P(x)}{{\lor}\mbox{e}\,\green{\scriptstyle [{\tt H4},{\tt H5}]}}
}
{\exists x\,P(x)}{{\exists}\mbox{e}\,\green{\scriptstyle [{\tt H3}]}}
}
{Q(a) \to \exists x\,P(x)}{{\to}\mbox{i}\,\green{\scriptstyle [{\tt H2}]}}
}
{\exists x (P(x) \lor \neg Q(a)) \to Q(a) \to \exists x\,P(x)}{{\to}\mbox{i}\,\green{\scriptstyle [{\tt H1}]}}
$$

\medskip
\noindent
In different textbooks the precise notation for this kind of proof will vary,
but whatever the details are, natural deduction proofs in the `tree' style
have a shape that is close to this.

Differences between textbooks might be that the order of the connective
and the `i' or `e' can be the other way around, in which case it is i$\to$ instead
of $\to$i,
or the `i' or `e' has to be capitalized, in which case it is $\to$I
instead of $\to$i.
Another difference is that often the assumptions at the `leaves' of
the proof tree are not put in square brackets, but instead are
crossed out with a diagonal slash.
(Crossing out an assumption in such a way while doing a proof
can give a very satisfactory feeling.
However, on a computer screen it is a bit hard to implement.
The convention of the square brackets we took from \cite{dal:04}.)

In natural deduction proofs the rules and assumptions generally are annotated
to indicate which assumption originates from which rule invocation.
In ProofWeb we do this in \green{green} in the following style:
$$
\hspace{-12em}
\der{
\der{
\der{
\leaf{[\exists x (P(x) \lor \neg Q(a))]\lab{H1}}\qquad\qquad\qquad\qquad\qquad\enskip
\der{
\leaf{[P(b) \lor \neg Q(a)]\lab{H3}}\qquad\enskip
\der{
\leaf{[P(b)]\lab{H4}}
}
{\exists x\,P(x)}{{\exists}\mbox{i}}\qquad\qquad\enskip
\der{
\der{
\leaf{[\neg Q(a)]\lab{H5}}\quad\enskip
\leaf{[Q(a)]\lab{H2}}
}
{\bot}{{\neg}\mbox{e}}
}
{\exists x\,P(x)}{{\bot}\mbox{e}}
}
{\exists x\,P(x)}{{\lor}\mbox{e}\,\green{\scriptstyle [{\tt H4},{\tt H5}]}}
}
{\exists x\,P(x)}{{\exists}\mbox{e}\,\green{\scriptstyle [{\tt H3}]}}
}
{Q(a) \to \exists x\,P(x)}{{\to}\mbox{i}\,\green{\scriptstyle [{\tt H2}]}}
}
{\exists x (P(x) \lor \neg Q(a)) \to Q(a) \to \exists x\,P(x)}{{\to}\mbox{i}\,\green{\scriptstyle [{\tt H1}]}}
$$

\medskip
\noindent
Again, the way this annotation is done differs between textbooks.
Often the annotations are subscripts or superscripts of the rules,
and often the annotations are numbers.
(Here we use the labels that one gets in the Coq system, which are not
numeric.)

Now here is the way this same proof is displayed in the ProofWeb window.
As you can see it is very similar to the mathematical style that we showed.
The main difference is that the lines are a bit longer.
\begin{center}\tt
\medskip
\strut\hspace{-4em}%
\begin{tabular}{ccclcl}
&&&& [$\neg$Q a]$^{\green{\tt H5}}\;$ [Q a]$^{\green{\tt H2}}$ & \third{$\neg$e} \\
\noalign{\vspace{.5\smallskipamount}}
\cline{5-5}
\noalign{\vspace{.5\smallskipamount}}
&& [P b]$^{\green{\tt H4}}$ & \third{$\exists$i} & $\bot$ & \third{$\bot$e} \\
\noalign{\vspace{.5\smallskipamount}}
\cline{3-3}\cline{5-5}
\noalign{\vspace{.5\smallskipamount}}
& [P b $\lor$ $\neg$Q a]$^{\green{\tt H3}}$ & $\exists$x, P x && $\exists$x, P x & \third{$\lor$e\green{[H4,H5]}} \\
\noalign{\vspace{.5\smallskipamount}}
\cline{2-5}
\noalign{\vspace{.5\smallskipamount}}
\strut[$\exists$x, (P x $\lor$ $\neg$Q a)]$^{\green{\tt H1}}$ && $\hspace{1.6em}${}$\exists$x, P x$\hspace{-1.6em}$ &&& \third{$\exists$e\green{[H3]}} \\
\noalign{\vspace{.5\smallskipamount}}
\cline{1-5}
\noalign{\vspace{.5\smallskipamount}}
& $\hspace{2.5em}${}$\exists$x, P x$\hspace{-2.5em}$ &&&& \third{$\to$i\green{[H2]}}\\
\noalign{\vspace{.5\smallskipamount}}
\cline{1-5}
\noalign{\vspace{.5\smallskipamount}}
& $\hspace{2.5em}$Q a $\to$ $\exists$x, P x$\hspace{-2.5em}$ &&&& \third{$\to$i\green{[H1]}} \\
\noalign{\vspace{.5\smallskipamount}}
\cline{1-5}
\noalign{\vspace{.5\smallskipamount}}
& $\hspace{-2.5em}${}$\exists$x, (P x $\lor$ $\neg$Q a) $\to$ Q a $\to$ $\exists$x, P x$\hspace{-8.5em}$ \\
\end{tabular}%
$\hspace{-8em}$
\end{center}

\medskip
\noindent
This example is quite involved.
For this reason we will use a simpler example in the next section
(which explains the commands that one uses to build a proof in ProofWeb):
\vspace{-\bigskipamount}
$$
\hspace{-2em}
\der{
\der{
\leaf{[A \land B]\lab{H}}
}
{A}{{\land}\mbox{e}_1}
}
{A \land B \to A}{{\to}\mbox{i}\,\green{\scriptstyle [{\tt H}]}}
$$

\smallskip
\noindent
This example is the same that was also used in Chapter~\ref{sec:session}.
In ProofWeb it is displayed like:
\begin{center}\tt
\medskip
\strut\hspace{2em}%
\begin{tabular}{cl}
\strut[A $\land$ B]$^{\green{\tt H}}$ & \third{$\land$e$_{\tt 1}$} \\
\noalign{\vspace{.5\smallskipamount}}
\cline{1-1}
\noalign{\vspace{.5\smallskipamount}}
A & \third{$\to$i\green{[H]}} \\
\noalign{\vspace{.5\smallskipamount}}
\cline{1-1}
\noalign{\vspace{.5\smallskipamount}}
A $\land$ B $\to$ A &
\end{tabular}
\end{center}

\medskip
\noindent
Next, we will explain how to write a ProofWeb script that generates this proof.

\subsection{Example in ProofWeb}

First let us show the exercise for this example,
which is generally the starting point when doing a proof in ProofWeb:
\begin{quote}
\def\\{\char`\\}
\begin{alltt}
\red{Require Import ProofWeb.\smallskip
Variable A B : Prop.\smallskip
Theorem prop_001 : {(A /\\\ B) -> A}.
Proof.
\green{(*! prop_proof *)}
Qed.}
\end{alltt}
\end{quote}
\noindent
It will be clear that the exercise here is to create a natural deduction
proof of the statement
$${A \land B \to A}$$

\noindent
The comment that tells where the proof has to be filled in is in
green.
(Note that Coq will not be able to process this file as it is.
It
will not want to process the `\texttt{Qed.}' line, as the
proof will not be finished at that point.)

Here is a solution to this exercise that Coq accepts, and that generates the proof
that we just showed:
\begin{quote}
\def\\{\char`\\}
\begin{alltt}
\red{Require Import ProofWeb.\smallskip
Variable A B : Prop.\smallskip
Theorem prop_001 : {(A /\\\ B) -> A}.
Proof.
\green{imp_i H.
con_e1 (B).
exact H.}
Qed.}
\end{alltt}
\end{quote}

\noindent
We will now explain this script line by line.
The two most interesting lines in the script are the \emph{tactics}
that actually build the proof.
They are shown in green.

The first line of the script
\begin{quote}
\red{\texttt{Require Import ProofWeb.}}
\end{quote}
tells Coq to load the definitions needed for ProofWeb.
(These are in a file \texttt{ProofWeb.v}, but the contents of that file is
not interesting for users of the system.)

The second line of the script
\begin{quote}
\red{\texttt{Variable A B : Prop.}}
\end{quote}
tells Coq that we want to use propositional variables $A$ and $B$.
In Coq everything needs to be \emph{declared} before it can be used.
For example to declare a unary predicate $P$ and a binary predicate $Q$
we need to write:
\begin{quote}
\begin{alltt}
Variable P : D -> Prop.
Variable Q : D * D -> Prop.
\end{alltt}
\end{quote}
Or if we want a unary function $f$ and a binary function $g$:
\begin{quote}
\begin{alltt}
Variable f : D -> D.
Variable g : D * D -> D.
\end{alltt}
\end{quote}
Even for variables of the predicate logic we need this kind of declaration.
Here is the declaration needed to have a proof use \emph{free} variables
$x$ and $y$:
\begin{quote}
\begin{alltt}
Variable x y : D.
\end{alltt}
\end{quote}
(Variables introduced by introduction or elimination
rules do not need a declaration like this.)

The domain of the logic called \texttt{D} is declared in the \texttt{ProofWeb.v} file.
In that file also a single constant in this domain is declared which is called \texttt{\char`\_d}.
(This constant is needed to make some of the proof commands work,
but one can use it in a proof too, if one likes.)

Now the third non-empty line of the script
\begin{quote}
\red{\texttt{Theorem prop\char`\_001 :\ {(A /\char`\\\ B) -> A}.}}
\end{quote}
tells the system that we will be going to prove a statement.
If we manage to finish this proof the name of the theorem will be \texttt{prop\char`\_001}.

The fourth non-empty line is
\begin{quote}
\red{\texttt{Proof.}}
\end{quote}
It does nothing.
It visually complements the `\texttt{Qed.}' at the end, that is all.
If it is left out everything works just as well.
(But if you remove it from the script you will not get a
\green{\textsf{Solved}}
status.
ProofWeb compares a solution to the original exercise
file, and if a line suddenly is missing it does not like it.)

Now we get to the lines that build the actual proof.
The command in these lines are called \emph{tactics}.
This proof just contains two tactics, but ProofWeb has many.
For the full list see Appendix~\ref{appendix:gentzen} on page~\pageref{appendix:gentzen}.

Before the first tactic is executed, the incomplete proof is just
the statement that has to be proved with dots where the proof should go:
\vspace{-\bigskipamount}
$$
\hspace{-2em}
\xder{
\leaf{\vdots}
}
{A \land B \to A}{}
$$
\noindent
We will `grow' the proof upward by executing tactics.
Clearly this statement should be proved by implication introduction.
So we execute the tactic for that which is called `\texttt{imp\char`\_i}':
\begin{quote}
\green{\texttt{imp\char`\_i H.}}
\end{quote}
Most of the ProofWeb tactic names consist of three letters that identify the
connective according to the following table:
\begin{center}
\begin{tabular}{ccl}
$\bot$ && \texttt{fls} \\
$\top$ && \texttt{tru} \\
$\neg$ && \texttt{neg} \\
$\land$ && \texttt{con} \\
$\lor$ && \texttt{dis} \\
$\to$ && \texttt{imp} \\
$\forall$ && \texttt{all} \\
$\exists$ && \texttt{exi} \\
$=$ && \texttt{equ}
\end{tabular}
\end{center}
then an underscore character, then an `\texttt{i}' or
`\texttt{e}' to distinguish between introduction and elimination
rules, and finally an optional `\texttt{1}' or `\texttt{2}' to
distinguish between left and right rules, or very occasionally a
prime character `\texttt{'}' for a special tactic variant.
These tactics also can be selected from the \textsf{Backward} menu
in the ProofWeb menu bar, in which case a template for the tactic
will be inserted in the text by the system.

After executing the \texttt{imp\char`\_i} tactic, the incomplete proof becomes:
\vspace{-\bigskipamount}
$$
\hspace{-2em}
\der{
\xder{
\leaf{\vdots}
}
{A}{}
}
{A \land B \to A}{{\to}\mbox{i}\,\green{\scriptstyle [{\tt H}]}}
$$
\noindent
As you can see, the \texttt{H} argument to the tactic gave the label
for the assumption that is introduced by this rule.
We will be able to use this assumption
in our proof as
$$
[A \land B]\lab{H}
$$
Tactics generally have \emph{arguments}, which are labels,
formulas and terms.
Important!
\begin{quote}
\emph{Formulas and terms that are tactic arguments
will need to be put in brackets.}
\end{quote}
Else the command will generally give a syntax error.
The templates inserted by the \textsf{Backward} menu already
has these brackets in them.

We now insert a left conjunction elimination rule in our incomplete
proof
by issuing the `\texttt{con\char`\_e1}' tactic:
\begin{quote}
\green{\texttt{con\char`\_e1 (B).}}
\end{quote}
\noindent
This turns the incomplete proof into:
\vspace{-\bigskipamount}
$$
\hspace{-2em}
\der{
\der{
\xder{
\leaf{\vdots}
}
{A \land B}{}
}
{A}{{\land}\mbox{e}_1}
}
{A \land B \to A}{{\to}\mbox{i}\,\green{\scriptstyle [{\tt H}]}}
$$
\noindent
Now to finish our proof, we will need to tell ProofWeb that the
$A \land B$ is one of the assumptions (the one labeled
\texttt{H}).
This is done by the command:
\begin{quote}
\green{\texttt{exact H.}}
\end{quote}
\noindent
After this tactic the proof that we built is finished, and looks like:
\vspace{-\bigskipamount}
$$
\hspace{-2em}
\der{
\der{
\leaf{[A \land B]\lab{H}}
}
{A}{{\land}\mbox{e}_1}
}
{A \land B \to A}{{\to}\mbox{i}\,\green{\scriptstyle [{\tt H}]}}
$$
We now issue the command
\begin{quote}
\red{\texttt{Qed.}}
\end{quote}
\noindent
to close the proof, and our script is done.

The larger proof on page~\pageref{proof:gentzen:large} can be generated
by a very similar script.
We will not walk through that script in detail, but we will just
present it here in its entirety.
Try to relate the tactics in this script
to the inference rules that are used in the proof:
\begin{quote}
\def\\{\char`\\}
\begin{alltt}
\red{Require Import ProofWeb.\smallskip
Variable P Q : D -> Prop.
Variable a : D.\smallskip
Theorem example :
  exi x, (P(x) \\/ ~Q(a)) -> Q(a) -> exi x, P(x).
Proof.
\green{imp_i H1.
imp_i H2.
exi_e (exi x, (P(x) \\/ ~Q(a))) b H3.
exact H1.
dis_e (P(b) \\/ ~Q(a)) H4 H5.
exact H3.
exi_i b.
exact H4.
fls_e.
neg_e (Q(a)).
exact H5.
exact H2.}
Qed.}
\end{alltt}
\end{quote}

\noindent
This finishes our description on how to build a natural deduction
proof in Gentzen's `tree' style using ProofWeb.
We have not discussed all natural deduction tactics in detail,
as they all behave in a very similar way.
See Appendix~\ref{appendix:gentzen} on page~\pageref{appendix:gentzen} for the full list,
with for each tactic a description of their behavior.

In the ProofWeb menus there also is a menu \textsf{Forward} next
to the \textsf{Backward} menu.
This tactics in this menu will behave reasonably when building a Gentzen style
`tree' proof, but they are primarily intended for making it easier to
build Fitch style `box' proofs,
which is the subject of the next chapter.

\section{Fitch style box proofs}

This chapter explains how to build natural deduction proofs using ProofWeb.
It treats a style of natural deduction introduced by Frederic Fitch.
We will call that style `box proofs', to distinguish it from the `tree proofs'
which were discussed in the previous chapter.
  We will not explain these natural deduction proofs in detail.
You will need to read a textbook for that first.
ProofWeb was designed to be used next to Michael Huth \& Mark Ryan's
\emph{Logic in Computer Science: Modelling and Reasoning about Systems} \cite{hut:rya:04},
so that is the book that we recommend to fully
understand Fitch style `box' proofs.

However, apart from minor notational differences ProofWeb can be used with
any textbook teaching natural deduction in Fitch's `box' style.

\subsection{Example on paper}

Here is an example of a natural deduction proof in predicate logic, in the way
that it is written on paper:
\begin{center}\label{proof:fitch:large}
\strut\hspace{-4em}%
\begin{tabular}{rlllllllllll}
\cline{2-10}
\Lstrut 1 & \mbar &&&& $\exists x (P(x) \lor \neg Q(a))$ & assumption &&&& \mbar \\
\cline{3-9}
\Lstrut 2 & \mbar & \mbar &&& $Q(a)$ & assumption &&& \mbar & \mbar \\
\cline{4-8}
\Lstrut 3 & \mbar & \mbar & \mbar & $b$ & $P(b) \lor \neg Q(a)$ & assumption && \mbar & \mbar & \mbar \\
\cline{5-7}
\Lstrut 4 & \mbar & \mbar & \mbar & \mbar & $P(b)$ & assumption & \mbar & \mbar & \mbar & \mbar \\
\Lstrut 5 & \mbar & \mbar & \mbar & \mbar & $\exists x\, P(x)$ & $\exists$i 4 & \mbar & \mbar & \mbar & \mbar \\
\cline{5-7}
& \mbar & \mbar & \mbar &&&&& \mbar & \mbar & \mbar \\
\noalign{\vspace{-\smallskipamount}}
\cline{5-7}
\Lstrut 6 & \mbar & \mbar & \mbar & \mbar & $\neg Q(a)$ & assumption & \mbar & \mbar & \mbar & \mbar \\
\lstrut 7 & \mbar & \mbar & \mbar & \mbar & $\bot$ & $\neg$e 6,2 & \mbar & \mbar & \mbar & \mbar \\
\Lstrut 8 & \mbar & \mbar & \mbar & \mbar & $\exists x\, P(x)$ & $\bot$e 7 & \mbar & \mbar & \mbar & \mbar \\
\cline{5-7}
\Lstrut 9 & \mbar & \mbar & \mbar && $\exists x\, P(x)$ & $\lor$e 3,4---5,6---8 && \mbar & \mbar & \mbar \\
\cline{4-8}
\Lstrut 10 & \mbar & \mbar &&& $\exists x\, P(x)$ & $\exists$e 1,3---9 &&& \mbar & \mbar \\
\cline{3-9}
\Lstrut 11 & \mbar &&&& $Q(a) \to \exists x\, P(x)$ & $\to$i 2---10 &&&& \mbar \\
\cline{2-10}
\Lstrut 12 &&&&& $\exists x (P(x) \lor \neg Q(a)) \to Q(a) \to \exists x\, P(x)$ & $\to$i 1---11
\end{tabular}%
\hspace{-4em}\strut
\end{center}
\medskip
\noindent
And here is the way this same proof is displayed in the ProofWeb system:
\begin{center}
\tt
\strut\hspace{-4em}%
\label{proof:fitch:proofweb}%
\begin{tabular}{rlllllll}
\cline{2-7}
1 & \mbar &&& \green{H1:} & $\exists$x, (P x $\lor$ $\neg$Q a) & assumption & \\
\cline{3-7}
2 & \mbar & \mbar && \green{H2:} & Q a & assumption \\
\cline{4-7}
& \mbar & \mbar & \mbar & b \\
3 & \mbar & \mbar & \mbar & \green{H3:} & P b $\lor$ $\neg$Q a & assumption \\
\cline{5-7}
4 & \mbar & \mbar & \mbar & \multicolumn{1}{|l}{\green{H4:}} & P b & assumption \\
5 & \mbar & \mbar & \mbar & \mbar & $\exists$x, P x & $\exists$i 4 \\
\cline{5-7}
6 & \mbar & \mbar & \mbar & \multicolumn{1}{|l}{\green{H5:}} & $\neg$Q a & assumption \\
7 & \mbar & \mbar & \mbar & \mbar & $\bot$ & $\neg$e 6,2 \\
8 & \mbar & \mbar & \mbar & \mbar & $\exists$x, P x & $\bot$e 7 \\
\cline{5-7}
9 & \mbar & \mbar & \mbar && $\exists$x, P x & $\lor$e 3,4-5,6-8 \\
\cline{4-7}
10 & \mbar & \mbar &&& $\exists$x, P x & $\exists$e 1,3-9 \\
\cline{3-7}
11 & \mbar &&&& Q a $\to$ $\exists$x, P x & $\to$i 2-10 \\
\cline{2-7}
12 &&&&& $\exists$x, (P x $\lor$ $\neg$Q a) $\to$ Q a $\to$ $\exists$x, P x & $\to$i 1-11
\end{tabular}%
\hspace{-4em}\strut
\end{center}
\medskip
\noindent
As you can see, some labels have been added in green, the boxes are not
closed on the right anymore (to save some space), and the two sub-boxes for the ${\lor}$e rule have
grown together.
Apart from that it is quite the same.

This example is quite involved.
For this reason we will now give a simpler example for the next
section
(which explains the commands that one uses to build a proof
in ProofWeb):
\begin{center}
\begin{tabular}{llll}
\cline{2-4}
\Lstrut 1 & \multicolumn{1}{|l}{} & $A \land B$ & \multicolumn{1}{l|}{assumption} \\
\Lstrut 2 &\multicolumn{1}{|l}{} & $A$ & \multicolumn{1}{l|}{$\land$e$_1$ 1} \\
\cline{2-4}
\Lstrut 3 && $A \land B \to A$ & $\to$i 1---2
\end{tabular}
\end{center}
\medskip
\noindent
In ProofWeb it is displayed like:
\medskip
\begin{center}
\tt
\begin{tabular}{llll}
\cline{2-4}
1 & \multicolumn{1}{|l}{\green{H:}} & A $\land$ B & assumption \\
2 &\multicolumn{1}{|l}{} & A & $\land$e$_1$ 1 \\
\cline{2-4}
3 && A $\land$ B $\to$ A & $\to$i 1-2
\end{tabular}
\end{center}
\medskip
\noindent
Now in different textbooks the notation for this kind of proof will vary, but
whatever the precise details are, natural deduction proofs in the `box' style
will have a structure that is very similar to this.

Differences between textbooks might be that the notation for the rules might
deviate in the details,
and in particular that the `subproofs' often will not be indicated by boxes
but by other shapes.
In \cite{hut:rya:04}, which we follow in ProofWeb, the subproofs are enclosed
in boxes:
\begin{center}
\begin{tabular}{llll}
\cline{2-4}
\Lstrut 1 & \multicolumn{1}{|l}{} & $A \land B$ & \multicolumn{1}{l|}{assumption} \\
\Lstrut 2 &\multicolumn{1}{|l}{} & $A$ & \multicolumn{1}{l|}{$\land$e$_1$ 1} \\
\cline{2-4}
\Lstrut 3 && $A \land B \to A$ & $\to$i 1---2
\end{tabular}
\end{center}
\noindent
However, in other books just a vertical line to left is used,
with a short horizontal
line indicating where the assumption is separated from the rest of the subproof:
\begin{center}
\begin{tabular}{llll}
\Lstrut 1 & \multicolumn{1}{|l}{} & $A \land B$ & assumption \\
\cline{2-2}
\Lstrut 2 &\multicolumn{1}{|l}{} & $A$ & $\land$e$_1$ 1 \\
\Lstrut 3 && $A \land B \to A$ & $\to$i 1---2
\end{tabular}
\end{center}
\noindent
Also occasionally a third variant is used, in which only the assumption is enclosed in a box.
This way of writing Fitch proofs is called `flag style', as there now is a shape
like a waving flag:
\begin{center}
\begin{tabular}{llll}
\cline{2-4}
\Lstrut 1 & \multicolumn{1}{|l}{} & $A \land B$ & \multicolumn{1}{l|}{assumption} \\
\cline{2-4}
\Lstrut 2 &\multicolumn{1}{|l}{} & $A$ & $\land$e$_1$ 1 \\
\Lstrut 3 && $A \land B \to A$ & $\to$i 1---2
\end{tabular}
\end{center}
\noindent
Currently ProofWeb only supports the first of these three variants
on the notation for Fitch-style proofs.

We will now explain how to write a ProofWeb script that generates this proof.

\subsection{Example in ProofWeb}

First let us show the exercise that corresponds to this example, which is
generally the starting point when doing a proof in ProofWeb:
\begin{quote}
\def\\{\char`\\}
\begin{alltt}
\red{Require Import ProofWeb.\smallskip
Variable A B : Prop.\smallskip
Theorem prop_001 : {(A /\\\ B) -> A}.
Proof.
\green{(*! prop_proof *)}
Qed.}
\end{alltt}
\end{quote}
\noindent
It will be clear that the exercise here is to create a natural deduction
proof of the statement
$${A \land B \to A}$$

\noindent
The comment that tells where the proof has to be filled in is colored
green.
(Note that Coq will not be able to process this file as it is.
It
will not want to process the `\texttt{Qed.}' line at the end, as the
proof will not be done at that point without having filled in the proof.)

Here is a solution that Coq accepts, and that generates the proof
that we just showed:
\begin{quote}
\def\\{\char`\\}
\begin{alltt}
\red{Require Import ProofWeb.\smallskip
Variable A B : Prop.\smallskip
Theorem prop_001 : {(A /\\\ B) -> A}.
Proof.
\green{imp_i H.
con_e1 (B).
exact H.}
Qed.}
\end{alltt}
\end{quote}

\noindent
We will now explain this script line by line.
The two most interesting lines in the script are the \emph{tactics}
that actually build the proof.
They are shown in green.

The first line of the script
\begin{quote}
\red{\texttt{Require Import ProofWeb.}}
\end{quote}
tells Coq to load the definitions needed for ProofWeb.
(These are in a file \texttt{ProofWeb.v}, but that file is
not interesting for users of the system.)

The second line of the script
\begin{quote}
\red{\texttt{Variable A B : Prop.}}
\end{quote}
tells Coq that we want to use propositional variables $A$ and $B$.
In Coq everything needs to be \emph{declared} before it can be used.
For example to declare a unary predicate $P$ and a binary predicate $Q$
we need to write:
\begin{quote}
\begin{alltt}
Variable P : D -> Prop.
Variable Q : D * D -> Prop.
\end{alltt}
\end{quote}
Or if we want a unary function $f$ and a binary function $g$:
\begin{quote}
\begin{alltt}
Variable f : D -> D.
Variable g : D * D -> D.
\end{alltt}
\end{quote}
Even for variables of the predicate logic we need this kind of declaration.
Here is the declaration for being able to use \emph{free} variables
$x$ and $y$ in a ProofWeb proof:
\begin{quote}
\begin{alltt}
Variable x y : D.
\end{alltt}
\end{quote}
(Please note that variables introduced by introduction or elimination
rules do not need a declaration like this.)

The domain of the logic called \texttt{D} is declared in the \texttt{ProofWeb.v} file.
In that file also a single constant in this domain is declared called \texttt{\char`\_d}.
(This constant is needed to make some of the proof commands work,
but you can also make use of it in your proof scripts if you like.)

Now the third non-empty line of the script
\begin{quote}
\red{\texttt{Theorem prop\char`\_001 :\ {(A /\char`\\\ B) -> A}.}}
\end{quote}
tells the system that we will be going to prove a statement.
The name of this statement will be \texttt{prop\char`\_001}.

The fourth non-empty line is
\begin{quote}
\red{\texttt{Proof.}}
\end{quote}
It does nothing.
It complements the `\texttt{Qed.}' at the end.
If it is left out everything works just as well.
(However, in that case you will not be able to get your exercise a
\green{\textsf{Solved}}
status.
ProofWeb compares your solution to the original exercise
file, and if a line is missing it does not like it.)

Now we get to the lines that build the actual proof.
The command in these lines are called \emph{tactics}.
This proof just consists of three tactics, but ProofWeb has many.
For the full list see Appendix~\ref{appendix:fitch} on page~\pageref{appendix:fitch}.

Before the first tactic is executed, the incomplete proof is just
the statement that has to be proved with dots where the proof should go:
\begin{center}
\begin{tabular}{llll}
\Lstrut && \dots & \\
\Lstrut 1 && $A \land B \to A$ &
\end{tabular}
\end{center}
\noindent
The number 1 to the left is the line number of the single line in this
(incomplete) proof.
When we work on the proof it will change.
(By the time the proof is finished it will have number 3.)
On the right there will be the rule that generated this line,
but this has not yet been fixed, so currently this space is empty.

Now this line will be proved by implication introduction.
So we execute the tactic for that called `\texttt{imp\char`\_i}':
\begin{quote}
\green{\texttt{imp\char`\_i H.}}
\end{quote}
Most of the ProofWeb tactic names consist of three letters that identify the
connective according to the following table:
\begin{center}
\begin{tabular}{ccl}
$\bot$ && \texttt{fls} \\
$\top$ && \texttt{tru} \\
$\neg$ && \texttt{neg} \\
$\land$ && \texttt{con} \\
$\lor$ && \texttt{dis} \\
$\to$ && \texttt{imp} \\
$\forall$ && \texttt{all} \\
$\exists$ && \texttt{exi} \\
$=$ && \texttt{equ}
\end{tabular}
\end{center}
then an underscore character, then an `\texttt{i}' or
`\texttt{e}' to distinguish between introduction and elimination
rules, and finally an optional `\texttt{1}' or `\texttt{2}' to
distinguish between left and right rules, or very occasionally a
prime character `\texttt{'}' for a special tactic variant.
These tactics also can be selected from the \textsf{Backward} menu
in the ProofWeb menu bar, in which case a template for the tactic
will be inserted in the text.

The \texttt{H} argument to the tactic gave the label
for the assumption that is introduced by this rule.
Tactics generally have \emph{arguments}, which can be labels,
formulas and terms.
Important!
\begin{quote}
\emph{Formulas and terms that are tactic arguments
will need to be put in brackets.}
\end{quote}
Else the command will give a syntax error.
The templates inserted by the \textsf{Backward} menu already
has these brackets in them.

After executing the \texttt{imp\char`\_i} tactic, the incomplete proof becomes:
\begin{center}
\begin{tabular}{llll}
\cline{2-4}
\Lstrut 1 & \multicolumn{1}{|l}{\green{\texttt{H:}}} & $A \land B$ & \multicolumn{1}{l|}{assumption} \\
\lstrut & \multicolumn{1}{|l}{} & \dots & \multicolumn{1}{l|}{} \\
\Lstrut 2 &\multicolumn{1}{|l}{} & $A$ & \multicolumn{1}{l|}{} \\
\cline{2-4}
\Lstrut 3 && $A \land B \to A$ & $\to$i 1---2
\end{tabular}
\end{center}
\noindent
As you can see the line number of the final line now has changed.
In ProofWeb we do not use the line numbers to refer to lines in
the tactics.
Instead we use \emph{labels}, which in the proofs are displayed in green.
In the tactic for implication introduction the label has to be
given as an argument.
In this case the label of the assumption is \texttt{H}.
In the ProofWeb script we will not use the number 1 to refer to this
line, but the label \texttt{H}.

The statement that we next will need to prove (the \emph{subgoal}) is
the line numbered 2, directly after the dots.
Of course we will use conjunction elimination to prove this.
In this section we use the \emph{backward} tactics, which means
that we will not be able to use the line that already has $A \land B$
on it.
Instead we work `backward' from the $A$ by giving the tactic:
\begin{quote}
\green{\texttt{con\char`\_e1 (B).}}
\end{quote}
\noindent
Look on page~\pageref{rule:fitch:con_e1}
to see how the \texttt{con\char`\_e1} tactic is documented in Appendix~\ref{appendix:fitch}.
It needs the argument $B$ because from the subgoal it cannot be deduced what
the other side of the conjunction was.
Also this argument is a formula, so it should be put in brackets.

After the \texttt{con\char`\_e1} tactic the (still incomplete) proof has become:
\begin{center}
\begin{tabular}{llll}
\cline{2-4}
\Lstrut 1 & \multicolumn{1}{|l}{\green{\texttt{H:}}} & $A \land B$ & \multicolumn{1}{l|}{assumption} \\
\lstrut & \multicolumn{1}{|l}{} & \dots & \multicolumn{1}{l|}{} \\
\lstrut 2 &\multicolumn{1}{|l}{} & $A \land B$ & \multicolumn{1}{l|}{} \\
\lstrut 3 &\multicolumn{1}{|l}{} & $A$ & \multicolumn{1}{l|}{$\land$e$_1$ 2} \\
\cline{2-4}
\Lstrut 4 && $A \land B \to A$ & $\to$i 1---3
\end{tabular}
\end{center}
\noindent
As you can see, the final line now has number 4, and the arguments
of the ${\to}$i rule on that line have been renumbered appropriately.

We can now finish the proof by noting that the subgoal that we are now
facing, $A \land B$, actually is the assumption labeled \texttt{H}.
For this execute the tactic:
\begin{quote}
\green{\texttt{exact H.}}
\end{quote}
You might expect this to change line 3 to a copy line (and in fact the tactic
called \texttt{exact}
has a synonym called \texttt{copy}):
\begin{center}
\begin{tabular}{llll}
\cline{2-4}
\Lstrut 1 & \multicolumn{1}{|l}{\green{\texttt{H:}}} & $A \land B$ & \multicolumn{1}{l|}{assumption} \\
\lstrut 2 &\multicolumn{1}{|l}{} & $A \land B$ & \multicolumn{1}{l|}{copy 1} \\
\lstrut 3 &\multicolumn{1}{|l}{} & $A$ & \multicolumn{1}{l|}{$\land$e$_1$ 2} \\
\cline{2-4}
\Lstrut 4 && $A \land B \to A$ & $\to$i 1---3
\end{tabular}
\end{center}
\noindent
but in fact it removes the duplication altogether and gives us as the final proof:
\begin{center}
\begin{tabular}{llll}
\cline{2-4}
\Lstrut 1 & \multicolumn{1}{|l}{\green{\texttt{H:}}} & $A \land B$ & \multicolumn{1}{l|}{assumption} \\
\Lstrut 2 &\multicolumn{1}{|l}{} & $A$ & \multicolumn{1}{l|}{$\land$e$_1$ 1} \\
\cline{2-4}
\Lstrut 3 && $A \land B \to A$ & $\to$i 1---2
\end{tabular}
\end{center}
\noindent
(Copy lines sometimes {are} retained, but only when necessary.)

We now issue the command
\begin{quote}
\red{\texttt{Qed.}}
\end{quote}
\noindent
to close the proof, and our script is done.

The larger proof on page~\pageref{proof:fitch:large} can be generated
by a very similar script.
We will not walk through that script in detail too.
We will just
present it here in its entirety.
Try to relate the tactics for the natural deduction rules in this script
to the inference rules that occur in the proof:
\begin{quote}
\def\\{\char`\\}
\begin{alltt}
\red{Require Import ProofWeb.\smallskip
Variable P Q : D -> Prop.
Variable a : D.\smallskip
Theorem example :
  exi x, (P(x) \\/ ~Q(a)) -> Q(a) -> exi x, P(x).
Proof.
\green{imp_i H1.
imp_i H2.
exi_e (exi x, (P(x) \\/ ~Q(a))) b H3.
exact H1.
dis_e (P(b) \\/ ~Q(a)) H4 H5.
exact H3.
exi_i b.
exact H4.
fls_e.
neg_e (Q(a)).
exact H5.
exact H2.}
Qed.}
\end{alltt}
\end{quote}

\noindent
This finishes our description on how to build a natural deduction
proof in Fitch's `box' style using only the backward tactics.
This method is conceptually easy, but often a bit laborious.
For this reason we will now look at the forward tactics.

\subsection{Forward tactics}

In the previous section we solved the exercise using a script
that only used backward tactics:
\begin{quote}
\begin{alltt}
\green{imp_i H.
con_e1 (B).
exact H.}
\end{alltt}
\end{quote}
\noindent
After the first line of that script the (incomplete) proof looked like:
\begin{center}
\begin{tabular}{llll}
\cline{2-4}
\Lstrut 1 & \multicolumn{1}{|l}{\green{\texttt{H:}}} & $A \land B$ & \multicolumn{1}{l|}{assumption} \\
\lstrut & \multicolumn{1}{|l}{} & \dots & \multicolumn{1}{l|}{} \\
\Lstrut 2 &\multicolumn{1}{|l}{} & $A$ & \multicolumn{1}{l|}{} \\
\cline{2-4}
\Lstrut 3 && $A \land B \to A$ & $\to$i 1---2
\end{tabular}
\end{center}
\noindent
If we had been doing the proof by hand we now just would put
$$\mbox{${\land}$e$_1$ 1}$$
on line 2 and be done with it.
This also can be done in ProofWeb with the appropriate {forward} tactic:
\begin{center}
\texttt{f\char`\_con\char`\_e1 H.}
\end{center}
Note that the reference to line 1 is given by the label \texttt{H}.
See for the documentation of the \texttt{f\char`\_con\char`\_e1} tactic page~\pageref{rule:fitch:f_con_e1} of Appendix~\ref{appendix:fitch}.

The prefix `\texttt{f\char`\_}' abbreviates `forward'.
In fact the backwards tactics also can be given with the
prefix `\texttt{b\char`\_}' added in front.
The forward tactics can be inserted in the script by using
the \textsf{Forward} menu in the ProofWeb menu bar.

After the \texttt{f\char`\_con\char`\_e1} tactic the proof will be
finished looking like:
\begin{center}
\begin{tabular}{llll}
\cline{2-4}
\Lstrut 1 & \multicolumn{1}{|l}{\green{\texttt{H:}}} & $A \land B$ & \multicolumn{1}{l|}{assumption} \\
\Lstrut 2 &\multicolumn{1}{|l}{} & $A$ & \multicolumn{1}{l|}{$\land$e$_1$ 1} \\
\cline{2-4}
\Lstrut 3 && $A \land B \to A$ & $\to$i 1---2
\end{tabular}
\end{center}
\noindent
This means that the following shorter script is also a solution to the problem:
\begin{quote}
\begin{alltt}
\green{imp_i H.
f_con_e1 H.}
\end{alltt}
\end{quote}
\noindent
In fact that is how any sensible ProofWeb user would solve it.

\subsection{The \texttt{insert} tactic}

There is one final tactic that we need to explain: the \texttt{insert} tactic.
When one builds a proof using backward tactics, one adds lines to the proof
\emph{after} the dots.
However, with the forward tactics the pattern generally is to add lines
\emph{before} the dots.
To be able to do that one needs the \texttt{insert} tactic.

Suppose that we have an incomplete proof starting like:
\begin{center}
\begin{tabular}{llll}
\cline{2-4}
\Lstrut 1 & \multicolumn{1}{|l}{\rlap{\green{\texttt{H:}}}\phantom{\texttt{H1:}}} & $A \land B$ & \multicolumn{1}{l|}{} \\
\lstrut & \multicolumn{1}{|l}{} & \rlap{\dots}\phantom{$A \land B \to A$} & \multicolumn{1}{l|}{\phantom{assumption}} \\
\end{tabular}
\end{center}
\noindent
(with more lines after the dots that we will not print here.)
Now suppose further that directly after line 1
we would like to insert another line
\begin{center}
\begin{tabular}{llll}
\Lstrut \phantom{2} & \multicolumn{1}{|l}{\green{\texttt{H1:}}} & \rlap{$A$}\phantom{$A \land B \to A$} & \multicolumn{1}{l|}{\rlap{$\land$e$_1$ 1}\phantom{assumption}} \\
\end{tabular}
\end{center}
\noindent
because we know that $A$ follows from $A \land B$.
The way to do this in ProofWeb is to execute \emph{two} tactics, the \texttt{insert} tactic
followed by a forward tactic:
\begin{quote}
\begin{alltt}
insert H1 (A).
f_con_e1 H.
\end{alltt}
\end{quote}
\noindent
What will happen if you execute these two tactics,
is that after the first tactic the proof looks like:
\begin{center}
\begin{tabular}{llll}
\cline{2-4}
\Lstrut 1 & \multicolumn{1}{|l}{\rlap{\green{\texttt{H:}}}\phantom{\texttt{H1:}}} & $A \land B$ & \multicolumn{1}{l|}{} \\
\lstrut & \multicolumn{1}{|l}{} & \dots & \multicolumn{1}{l|}{} \\
\lstrut {2} & \multicolumn{1}{|l}{\green{\texttt{H1:}}} & \rlap{$A$}\phantom{$A \land B \to A$} & \multicolumn{1}{l|}{} \\
\lstrut & \multicolumn{1}{|l}{} & \rlap{\dots}\phantom{$A \land B \to A$} & \multicolumn{1}{l|}{\phantom{assumption}} \\
\end{tabular}
\end{center}
\noindent
and after the second it is:
\begin{center}
\begin{tabular}{llll}
\cline{2-4}
\Lstrut 1 & \multicolumn{1}{|l}{\rlap{\green{\texttt{H:}}}\phantom{\texttt{H1:}}} & $A \land B$ & \multicolumn{1}{l|}{} \\
\lstrut {2} & \multicolumn{1}{|l}{\green{\texttt{H1:}}} & \rlap{$A$}\phantom{$A \land B \to A$} & \multicolumn{1}{l|}{\rlap{$\land$e$_1$ 1}\phantom{assumption}} \\
\lstrut & \multicolumn{1}{|l}{} & \dots & \multicolumn{1}{l|}{\phantom{assumption}} \\
\end{tabular}
\end{center}
\noindent
In other words: the \texttt{insert} tactic \emph{inserts} a new line in
the incomplete proof, and then the forward tactic proves it.

Note that the first tactic corresponds to the left part of the new line,
while the second tactic corresponds to the right part of the line:
\begin{center}
\hspace{1.4em}\texttt{insert {H1} (A).\ f\char`\_con\char`\_e1 H.}
\end{center}
\noindent
corresponds to the line
\begin{center}
\begin{tabular}{llll}
\Lstrut \phantom{2} & \multicolumn{1}{|l}{\green{\texttt{H1:}}} & \rlap{$A$}\phantom{$A \land B \to A$} & \multicolumn{1}{l|}{\rlap{$\land$e$_1$ 1}\phantom{assumption}} \\
\end{tabular}
\end{center}
\noindent
Of course it is not obligatory to directly prove an `inserted' line with just
a single forward tactic.
It is perfectly legal to prove it using a much more involved proof.
The \texttt{insert} tactic just means: `now first we will prove this,
and then we will go on with the rest of the proof.'
(A technical aside: in the logic this is called
a \emph{cut} or \emph{detour}.)

As a larger example, the bigger proof, on page~\pageref{proof:fitch:large}, can be more
efficiently generated by using forward tactics:
\begin{quote}
\def\\{\char`\\}
\begin{alltt}
\red{Require Import ProofWeb.\smallskip
Variable P Q : D -> Prop.
Variable a : D.\smallskip
Theorem example :
  exi x, (P(x) \\/ ~Q(a)) -> Q(a) -> exi x, P(x).
Proof.
\green{imp_i H1.
imp_i H2.
f_exi_e H1 b H3.
f_dis_e H3 H4 H5.
f_exi_i H4.
fls_e.
f_neg_e H5 H2.}
Qed.}
\end{alltt}
\end{quote}
\noindent
Note that in this script the proof is not generated in a fully forward way:
line 7 (the one with the contradiction) is generated in a backward
manner using the \texttt{fls\char`\_e} tactic.
(This saves one tactic in the script.)

This finishes our description on how to build a natural deduction proof
in Fitch's `box' style using ProofWeb.
We have not discussed all natural deduction tactics in detail here, as they
all behave in very similar ways.
See Appendix~\ref{appendix:fitch} on page~\pageref{appendix:fitch} for the full list,
with for each tactic a description of their behavior.

\subsection{The order of \texttt{insert} tactics}

ProofWeb has one unfortunate restriction, that is caused by the way it is implemented
on top of the Coq system.
Sometimes, when `\texttt{insert}'ing a line, later that line is not
visible in a place where according to the (incomplete) proof it \emph{should}
be visible.
This is caused by the fact that the line that was inserted {only} will
be visible in the part of the proof that corresponds to the dots where
it was inserted.

Here is a small example.
Suppose we have a proof:
\begin{center}
\begin{tabular}{llll}
\cline{2-4}
\Lstrut 1 & \multicolumn{1}{|l}{\phantom{\texttt{H1:}}} & $A$ & \multicolumn{1}{l|}{} \\
\lstrut & \multicolumn{1}{|l}{} & \rlap{\dots}\phantom{$A \land B \to A$} & \multicolumn{1}{l|}{\phantom{assumption}} \\
\Lstrut 2 & \multicolumn{1}{|l}{} & $D$ & \multicolumn{1}{l|}{} \\
\cline{2-4}
\end{tabular}
\end{center}
\noindent
and we want to insert lines $B$ and $C$ in between the $A$ and $D$.
Then we can do:
\begin{quote}
\begin{alltt}
insert H2 (C).
\end{alltt}
\end{quote}
\noindent
giving:
\begin{center}
\begin{tabular}{llll}
\cline{2-4}
\Lstrut 1 & \multicolumn{1}{|l}{} & $A$ & \multicolumn{1}{l|}{} \\
\lstrut & \multicolumn{1}{|l}{} & \rlap{\dots}\phantom{$A \land B \to A$} & \multicolumn{1}{l|}{\phantom{assumption}} \\
\Lstrut 2 & \multicolumn{1}{|l}{\green{\texttt{H2:}}} & $C$ & \multicolumn{1}{l|}{} \\
\lstrut & \multicolumn{1}{|l}{} & \dots & \multicolumn{1}{l|}{\phantom{assumption}} \\
\Lstrut 3 & \multicolumn{1}{|l}{} & $D$ & \multicolumn{1}{l|}{} \\
\cline{2-4}
\end{tabular}
\end{center}
\noindent
and subsequently:
\begin{quote}
\begin{alltt}
insert H1 (B).
\end{alltt}
\end{quote}
\noindent
giving:
\begin{center}
\begin{tabular}{llll}
\cline{2-4}
\Lstrut 1 & \multicolumn{1}{|l}{} & $A$ & \multicolumn{1}{l|}{} \\
\lstrut & \multicolumn{1}{|l}{} & \rlap{\dots}\phantom{$A \land B \to A$} & \multicolumn{1}{l|}{\phantom{assumption}} \\
\Lstrut 2 & \multicolumn{1}{|l}{\green{\texttt{H1:}}} & $B$ & \multicolumn{1}{l|}{} \\
\lstrut & \multicolumn{1}{|l}{} & \dots & \multicolumn{1}{l|}{\phantom{assumption}} \\
\Lstrut 3 & \multicolumn{1}{|l}{\green{\texttt{H2:}}} & $C$ & \multicolumn{1}{l|}{} \\
\lstrut & \multicolumn{1}{|l}{} & \dots & \multicolumn{1}{l|}{\phantom{assumption}} \\
\Lstrut 4 & \multicolumn{1}{|l}{} & $D$ & \multicolumn{1}{l|}{} \\
\cline{2-4}
\end{tabular}
\end{center}
\noindent
However, if we do this, in the proof the line labeled \texttt{H1} will not
be available after the $C$.
It will only be visible in the part of the proof that it
was inserted in, which is the part between $A$ and $C$.
So when working on the part of the proof that proves $D$ from $C$,
one will not be able to refer to the $B$ line.
This probably will be surprising by that time.

The solution to this problem is to have the \texttt{insert} lines in the
same order as their corresponding lines occur in the final proof.
If one reorders the `\texttt{insert}'s:
\begin{quote}
\begin{alltt}
insert H1 (B).
insert H2 (C).
\end{alltt}
\end{quote}
\noindent
there will not be a problem anymore.

Therefore, when using \texttt{insert} tactics in ProofWeb proofs, the rule of thumb should be:
\begin{quote}
\emph{%
Put the \emph{\texttt{insert}} lines in the script in the order in which the inserted lines
will appear in the proof.
}
\end{quote}
\noindent
This finishes the chapter on Fitch style `box' proofs in ProofWeb.

\section{ProofWeb versus Coq}\label{sec:coq}

In ProofWeb one really is using the Coq system.
One is processing a Coq script without any change to the Coq
syntax.
However, the ProofWeb tactics are not the ones that a Coq
user normally would use to prove something.
The Coq tactics are much more efficient, but less closely related
to the natural deduction rules of first order logic.
Also the ProofWeb formula syntax deviates a little bit from the way
that a Coq user normally would write formulas.
We will now briefly indicate what are the differences between using
Coq in the ProofWeb style and using it in the Coq style.

\subsection{Formula syntax}

In Coq one generally does not use \texttt{all} and \texttt{exi} for
the quantifiers, but instead one uses \texttt{forall} and \texttt{exists}.
The reason that ProofWeb defines its own quantifiers is to get the
binding strength the way it is in most logic textbooks.
Also in ProofWeb one is working in an \emph{unsorted} logic in which
all variables range over the same domain, while in Coq variables have
a \emph{type}.

So in ProofWeb one writes
\begin{center}
\texttt{all x, P(x)}
\end{center}
while a Coq user would write
\begin{center}
\texttt{forall x :\ D, P(x)}
\end{center}
(To make things subtle, in Coq the typing of the variable
can be omitted if the system can deduce the type from the way
it is being used.)
Similarly in ProofWeb one uses
\begin{center}
\texttt{exi x, P(x)}
\end{center}
while a Coq user would write
\begin{center}
\texttt{exists x :\ D, P(x)}
\end{center}
These are the only differences between ProofWeb formula syntax and
the customary Coq formula syntax.

The ProofWeb tactics have been designed to also work with
the `usual' Coq quantifiers.
If you prefer to have multiple sorts and
weakly binding quantifiers in your formula syntax, it still is perfectly
possible to use ProofWeb.

\subsection{Tactics}

In ProofWeb one uses many weak tactics.
There generally are two for every deduction rule, a backward and a forward one.
In Coq one uses fewer, but much more efficient tactics.
The most important Coq tactics are:
\begin{center}
\begin{tabular}{c}
\texttt{intros} \\
\texttt{apply} \\
\texttt{elim}
\end{tabular}
\end{center}
Also, there are a couple of Coq tactics that really are just
synonyms of the ProofWeb tactics (but without the systematic naming):
\begin{center}
\begin{tabular}{c}
\texttt{split} \\
\texttt{left} \\
\texttt{right} \\
\texttt{exists}
\end{tabular}
\end{center}
We will not explain the customary Coq tactics here.
Read the Coq manual \cite{coq:07} or the \emph{Coq'Art} book by Yves Bertot \cite{ber:cas:04} if you want to learn about this.
Here we will just present traditional Coq proofs for our two examples:
\begin{quote}
\def\\{\char`\\}
\begin{alltt}
\red{Variable A B : Prop.\smallskip
Theorem prop_001 : {A /\\\ B -> A}.
Proof.
\green{intros H.
elim H.
intros H1 H2.
apply H1.}
Qed.}
\end{alltt}
\end{quote}
\noindent
and:
\begin{quote}
\def\\{\char`\\}
\begin{alltt}
\red{Variable D : Set.
Variable P Q : D -> Prop.
Variable a : D.\smallskip
Theorem example :
  (exists x : D, P(x) \\/ ~Q(a)) -> Q(a) ->
  exists x : D, P(x).
Proof.
\green{intros H1 H2.
elim H1.
intros b H3.
elim H3.
intros H4.
exists b.
apply H4.
intros H5.
elim H5.
apply H2.}
Qed.}
\end{alltt}
\end{quote}
Of course an actual Coq user would probably not just solve these proofs
using these basic tactics, but instead would try to speed things up by using
automated tactics like \texttt{auto}, \texttt{tauto}
or \texttt{intuition}.
These are tactics that search for these small proofs themselves.
In fact these tactics will find the first proof, but not the second.
Of course if one uses real heavy tactics like \texttt{jprover} (which
can prove any formula of first order predicate logic, given enough
time and space), it
will solve the second one immediately as well.

\section{ProofWeb versus Huth \& Ryan}

ProofWeb was designed to follow as closely as possible
the conventions of Michael Huth \& Mark Ryan's
\emph{Logic in Computer Science: Modelling and Reasoning about
Systems} \cite{hut:rya:04}.
However, due to the use of the Coq system, and because of the design decision
to have the users work with undiluted Coq input (without preprocessing the
script in the ProofWeb system first), a few slight deviations crept
in.
We will now briefly discuss these.

\subsection{Formula syntax}

The ProofWeb quantifiers have a \emph{comma}.
This is not customary in logic textbooks.
There either they have nothing, or they have a period.

The formula
$$\forall x\, P(x)$$
is written in ProofWeb syntax as
\begin{center}
\texttt{all x, P(x)}
\end{center}
and the system will print the formula back at you as
\begin{center}
\texttt{all x, P x}
\end{center}
so without the brackets around the variable.
Also, in the proofs displayed in the window pane at the lower right the comma will be printed:
\begin{center}
\texttt{$\forall$x, P x}
\end{center}
We could have used a notation without commas, but we had two reasons
for retaining the comma.
First, we think that
\begin{center}
\texttt{all x P x}
\end{center}
looks confusing (to us it looks like the \texttt{P} is a relation symbol between the
two \texttt{x}'s).
Second, having the comma makes it easier for users to switch to the
customary Coq notation for quantifiers later, if they decide to go that way.

\subsection{Proof display}

The main difference between the proofs on paper and the proofs on the
screen is the presence of Coq labels.
We put them there to help writing the proof scripts.
To emphasize that they are `extra', they are in green.

Another slight difference between the proofs on paper and the proofs on
the screen is the placing of variables in the $\forall$i and $\exists$e
rules.
We push them one line up.
For instance, in the book the $\exists$e rule is written like:
\begin{center}
\begin{tabular}{rllll}
\Lstrut 1 && $\exists x\, P(x)$ \\
\cline{2-4}
\Lstrut 2 & \multicolumn{1}{|l}{$y$} & $P(y)$ && \multicolumn{1}{|l}{} \\
\lstrut & \multicolumn{1}{|l}{} & \dots && \multicolumn{1}{|l}{} \\
\Lstrut 3 & \multicolumn{1}{|l}{} & $A$ && \multicolumn{1}{|l}{} \\
\cline{2-4}
\Lstrut 4 && $A$ & $\exists$e 1,2---3 \\
\end{tabular}
\end{center}
while in ProofWeb it is:
\begin{center}
\begin{tabular}{rllll}
\Lstrut 1 && $\exists x\, P(x)$ \\
\cline{2-4}
\Lstrut & \multicolumn{1}{|l}{$y$} &&& \multicolumn{1}{|l}{} \\
\lstrut 2 & \multicolumn{1}{|l}{} & $P(y)$ && \multicolumn{1}{|l}{} \\
\lstrut & \multicolumn{1}{|l}{} & \dots && \multicolumn{1}{|l}{} \\
\Lstrut 3 & \multicolumn{1}{|l}{} & $A$ && \multicolumn{1}{|l}{} \\
\cline{2-4}
\Lstrut 4 && $A$ & $\exists$e 1,2---3 \\
\end{tabular}
\end{center}
\noindent
A third deviation from the book is that we write the rules for the quantifiers
in the style
$$\mbox{$\forall$i}$$
while the book writes
$$\mbox{$\forall$ x i}$$
A final difference between the book and the system is that in the
disjunction elimination rule we run the sub-boxes together.
(See the example on page~\pageref{proof:fitch:proofweb}.)

\section{Outlook}

With ProofWeb we have created a system for teaching and practicing
natural deduction in first order logic, both for propositional and
for predicate logic.
We hope that it will be a useful tool for people trying to study these
logics, and that it will find widespread use all over the world.

\subsection*{Acknowledgements}
Thanks to (nobody yet) for helpful comments on these notes.

\bibliographystyle{plain}
\bibliography{proofweb-manual}

\newpage
\appendix

\section{Tactics in Gentzen style}\label{appendix:gentzen}

Rules that are not intuitionistically valid are marked with a star.
Rules that according to \cite{hut:rya:04} are derived rules are marked with a dagger.

\begin{center}
\begin{tabular}{lccc}
\hline
\Lstrut \rlap{\red{\texttt{exact H}}} \\
\noalign{\vspace{-\bigskipamount}} &
$\displaystyle
\xder{\leaf{\vdots}}{A}{}
$
& $\redarrow$ &
$\displaystyle
\leaf{[A]\rlap{$^{\green{\tt H}}$}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{conjunction introduction}} \\
\strut \rlap{\red{\texttt{con\char`\_i}}} \\
\noalign{\vspace{-\bigskipamount}} &
$\displaystyle
\xder{\leaf{\vdots}}{A \land B}{}
$
& $\redarrow$ &
$\displaystyle
\strut\hspace{2em}
\der{
\xder{\leaf{\vdots}}{A}{}
\qquad
\xder{\leaf{\vdots}}{B}{}
}{A \land B}{\mbox{$\land$i}}
\hspace{2em}\strut
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{conjunction elimination left}} \\
\strut \rlap{\red{\texttt{con\char`\_e1 $B$}}} \\
\noalign{\vspace{-\bigskipamount}} &
$\displaystyle
\xder{\leaf{\vdots}}{A}{}
$
& $\redarrow$ &
$\displaystyle
\der{
\xder{\leaf{\vdots}}{A \land B}{}
}{A}{\mbox{$\land$e$_1$}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{conjunction elimination right}} \\
\strut \rlap{\red{\texttt{con\char`\_e2 $A$}}} \\
\noalign{\vspace{-\bigskipamount}} &
$\displaystyle
\xder{\leaf{\vdots}}{B}{}
$
& $\redarrow$ &
$\displaystyle
\der{
\xder{\leaf{\vdots}}{A \land B}{}
}{B}{\mbox{$\land$e$_2$}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{disjunction introduction left}} \\
\strut \rlap{\red{\texttt{dis\char`\_i1}}} \\
\noalign{\vspace{-\bigskipamount}} &
$\displaystyle
\xder{\leaf{\vdots}}{A \lor B}{}
$
& $\redarrow$ &
$\displaystyle
\der{
\xder{\leaf{\vdots}}{A}{}
}{A \lor B}{\mbox{$\lor$i$_1$}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{disjunction introduction right}} \\
\strut \rlap{\red{\texttt{dis\char`\_i2}}} \\
\noalign{\vspace{-\bigskipamount}} &
$\displaystyle
\xder{\leaf{\vdots}}{A \lor B}{}
$
& $\redarrow$ &
$\displaystyle
\der{
\xder{\leaf{\vdots}}{B}{}
}{A \lor B}{\mbox{$\lor$i$_2$}}
$ \\
\skipforward
\hline
\end{tabular}
\end{center}
\newpage
\begin{center}
\begin{tabular}{lccc}
\hline
\Lstrut \rlap{\emph{disjunction elimination}} \\
\strut \rlap{\red{\texttt{dis\char`\_e ($A$ \char`\\/ $B$) H1 H2}}} \\
&
$\displaystyle
\xder{\leaf{\vdots}}{C}{}
$
& $\redarrow$ &
$\displaystyle
\strut\hspace{8em}
\der{
\xder{\leaf{\vdots}}{A \lor B}{}
\qquad
\xder{
\hspace{-1em}
\begin{array}{c}
[A]\rlap{$^{\green{\tt H1}}$} \\
\noalign{\vspace{-\smallskipamount}}
\vdots
\end{array}
\hspace{-1em}
}
{C}{}
\qquad
\xder{
\hspace{-1em}
\begin{array}{c}
[B]\rlap{$^{\green{\tt H2}}$} \\
\noalign{\vspace{-\smallskipamount}}
\vdots
\end{array}
\hspace{-1em}
}
{C}{}
}{C}{\mbox{$\lor$e$\,\green{\scriptstyle [{\tt H1},{\tt H2}]}$}}
\hspace{8em}\strut
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{implication introduction}} \\
\strut \rlap{\red{\texttt{imp\char`\_i H}}} \\
&
$\displaystyle
\xder{\leaf{\vdots}}{A \to B}{}
$
& $\redarrow$ &
$\displaystyle
\der{
\xder{
\hspace{-1em}
\begin{array}{c}
[A]\rlap{$^{\green{\tt H}}$} \\
\noalign{\vspace{-\smallskipamount}}
\vdots
\end{array}
\hspace{-1em}
}{B}{}
}
{A \to B}{\mbox{${\to}$i$\,\green{\scriptstyle [{\tt H}]}$}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{implication elimination}} \\
\strut \rlap{\red{\texttt{imp\char`\_e $A$}}} \\
\noalign{\vspace{-\bigskipamount}} &
$\displaystyle
\xder{\leaf{\vdots}}{B}{}
$
& $\redarrow$ &
$\displaystyle
\der{
\xder{\leaf{\vdots}}{A \to B}{}
\qquad
\xder{\leaf{\vdots}}{A}{}
}{B}{\mbox{$\to$e}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{negation introduction}} \\
\strut \rlap{\red{\texttt{neg\char`\_i H}}} \\
&
$\displaystyle
\xder{\leaf{\vdots}}{\neg A}{}
$
& $\redarrow$ &
$\displaystyle
\der{
\xder{
\hspace{-1em}
\begin{array}{c}
[A]\rlap{$^{\green{\tt H}}$} \\
\noalign{\vspace{-\smallskipamount}}
\vdots
\end{array}
\hspace{-1em}
}{\bot}{}
}
{\neg A}{\mbox{${\neg}$i$\,\green{\scriptstyle [{\tt H}]}$}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{negation elimination}} \\
\strut \rlap{\red{\texttt{neg\char`\_e $A$}}} \\
\noalign{\vspace{-\bigskipamount}} &
$\displaystyle
\xder{\leaf{\vdots}}{\bot}{}
$
& $\redarrow$ &
$\displaystyle
\der{
\xder{\leaf{\vdots}}{\neg A}{}
\qquad
\xder{\leaf{\vdots}}{A}{}
}{B}{\mbox{$\neg$e}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{falsum elimination}} \\
\strut \rlap{\red{\texttt{fls\char`\_e}}} \\
\noalign{\vspace{-\bigskipamount}} &
$\displaystyle
\xder{\leaf{\vdots}}{A}{}
$
& $\redarrow$ &
$\displaystyle
\der{
\xder{\leaf{\vdots}}{\bot}{}
}{A}{\mbox{$\bot$e}}
$ \\
\skipforward
\hline
\end{tabular}
\end{center}
\newpage
\begin{center}
\begin{tabular}{lccc}
\hline
\Lstrut \rlap{\emph{truth introduction}} \\
\strut \rlap{\red{\texttt{tru\char`\_i}}} \\
\noalign{\vspace{-\bigskipamount}} &
$\displaystyle
\xder{\leaf{\vdots}}{\top}{}
$
& $\redarrow$ &
$\displaystyle
\der{
}{\top}{\mbox{$\top$i}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{double negation introduction}$^\dagger$} \\
\strut \rlap{\red{\texttt{negneg\char`\_i}}} \\
\noalign{\vspace{-\bigskipamount}} &
$\displaystyle
\xder{\leaf{\vdots}}{\neg\neg A}{}
$
& $\redarrow$ &
$\displaystyle
\der{
\xder{\leaf{\vdots}}{A}{}
}{\neg\neg A}{\mbox{$\neg\neg$i}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{double negation elimination}*} \\
\strut \rlap{\red{\texttt{negneg\char`\_e}}} \\
\noalign{\vspace{-\bigskipamount}} &
$\displaystyle
\xder{\leaf{\vdots}}{A}{}
$
& $\redarrow$ &
$\displaystyle
\der{
\xder{\leaf{\vdots}}{\neg\neg A}{}
}{A}{\mbox{$\neg\neg$e}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{law of excluded middle}*$^\dagger$} \\
\strut \rlap{\red{\texttt{LEM}}} \\
\noalign{\vspace{-\bigskipamount}} &
$\displaystyle
\xder{\leaf{\vdots}}{A \lor \neg A}{}
$
& $\redarrow$ &
$\displaystyle
\der{
}{A \lor \neg A}{\mbox{LEM}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{proof by contradiction}*$^\dagger$} \\
\strut \rlap{\red{\texttt{PBC H}}} \\
&
$\displaystyle
\xder{\leaf{\vdots}}{A}{}
$
& $\redarrow$ &
$\displaystyle
\der{
\xder{
\hspace{-1em}
\begin{array}{c}
[\neg A]\rlap{$^{\green{\tt H}}$} \\
\noalign{\vspace{-\smallskipamount}}
\vdots
\end{array}
\hspace{-1em}
}{\bot}{}
}
{A}{\mbox{PBC$\,\green{\scriptstyle [{\tt H}]}$}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{modus tollens}$^\dagger$} \\
\strut \rlap{\red{\texttt{MT $B$}}} \\
\noalign{\vspace{-\bigskipamount}} &
$\displaystyle
\xder{\leaf{\vdots}}{\neg A}{}
$
& $\redarrow$ &
$\displaystyle
\hspace{5em}
\der{
\xder{\leaf{\vdots}}{A \to B}{}
\qquad
\xder{\leaf{\vdots}}{\neg B}{}
}{\neg A}{\mbox{MT}}
\hspace{5em}
$ \\
\skipforward
\hline
\end{tabular}
\end{center}
\newpage
\begin{center}
\begin{tabular}{lccc}
\hline
\Lstrut \rlap{\emph{universal introduction}} \\
\strut \rlap{\red{\texttt{all\char`\_i $y$}}} \\
&
$\displaystyle
\xder{\leaf{\vdots}}{\forall x\, A}{}
$
& $\redarrow$ &
$\displaystyle
\der{
\xder{
\vdots
}{A[y/x]}{}
}
{\forall x\, A}{\mbox{${\forall}$i}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{universal elimination}} \\
\strut \rlap{\red{\texttt{all\char`\_e (all x, $A$)}}} \\
&
$\displaystyle
\xder{\leaf{\vdots}}{A[t/x]}{}
$
& $\redarrow$ &
$\displaystyle
\der{
\xder{
\vdots
}{\forall x\, A}{}
}
{A[t/x]}{\mbox{${\forall}$e}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{existential introduction}} \\
\strut \rlap{\red{\texttt{exi\char`\_i $t$}}} \\
&
$\displaystyle
\xder{\leaf{\vdots}}{\exists x\, A}{}
$
& $\redarrow$ &
$\displaystyle
\der{
\xder{
\vdots
}{A[t/x]}{}
}
{\exists x\, A}{\mbox{${\exists}$i}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{existential elimination}} \\
\strut \rlap{\red{\texttt{exi\char`\_e (exi x, $A$) $y$ H}}} \\
&
$\displaystyle
\xder{\leaf{\vdots}}{B}{}
$
& $\redarrow$ &
$\displaystyle
\der{
\xder{\leaf{\vdots}}{\exists x\, A}{}
\qquad
\xder{
\hspace{-1em}
\begin{array}{c}
\big[A[y/x]\big]\rlap{$^{\green{\tt H}}$} \\
\noalign{\vspace{-\smallskipamount}}
\vdots
\end{array}
\hspace{-1em}
}
{B}{}
}{B}{\mbox{$\exists$e$\,\green{\scriptstyle [{\tt H}]}$}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{equality introduction}} \\
\strut \rlap{\red{\texttt{equ\char`\_i}}} \\
\noalign{\vspace{-\bigskipamount}} &
$\displaystyle
\xder{\leaf{\vdots}}{t = t}{}
$
& $\redarrow$ &
$\displaystyle
\der{
}{t = t}{\mbox{${=}$i}}
$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{equality elimination, simple version}} \\
\strut \rlap{\red{\texttt{equ\char`\_e ($t_1$ = $t_2$)}}} \\
\noalign{\vspace{-\bigskipamount}} &
$\displaystyle
\xder{\leaf{\vdots}}{A[t_2/x]}{}
$
& $\redarrow$ &
$\displaystyle
\strut\hspace{4.5em}
\der{
\xder{\leaf{\vdots}}{t_1 = t_2}{}
\qquad
\xder{\leaf{\vdots}}{A[t_1/x]}{}
}{A[t_2/x]}{\mbox{${=}$e}}
\strut\hspace{4.5em}
$ \\
\skipforward
\hline
\end{tabular}
\end{center}
\newpage
\begin{center}
\begin{tabular}{lccc}
\hline
\Lstrut \rlap{\emph{equality elimination, general version} (\emph{$t_2$ may occur in $A$})} \\
\strut \rlap{\red{\texttt{equ\char`\_e' ($t_1$ = $t_2$) (fun x => $A$)}}} \\
\noalign{\vspace{-\bigskipamount}} &
$\displaystyle
\xder{\leaf{\vdots}}{A[t_2/x]}{}
$
& $\redarrow$ &
$\displaystyle
\strut\hspace{4.5em}
\der{
\xder{\leaf{\vdots}}{t_1 = t_2}{}
\qquad
\xder{\leaf{\vdots}}{A[t_1/x]}{}
}{A[t_2/x]}{\mbox{${=}$e}}
\hspace{4.5em}\strut
$ \\
\skipforward
\hline
\end{tabular}
\end{center}

\newpage
\section{Tactics in Fitch style}\label{appendix:fitch}

\def\leftlabel#1{\phantom{$m$}\llap{#1}}
\def\rightlabel#1{\green{\texttt{#1}$\,:$}}

The green `\rightlabel{H}' labels that occur in these descriptions are not part of the way proofs are written in Huth \& Ryan,
but are necessary for working in ProofWeb.
They are the symbolic equivalents (which stay the same throughout the proof process) of the line numbers (which change all the time).

\subsection{Structural tactics}
\ 

\begin{center}
\begin{tabular}{lrlcrrlll}
\hline
\Lstrut \rlap{\red{\texttt{exact H}}} \\
\noalign{\medskip}
\lstrut \leftlabel{$m$} & $\;$\rightlabel{H} & $A$ && $m$ & $\;$\rightlabel{H} & $A$ \\
\noalign{\medskip}
\lstrut && \dots &&& \\
\lstrut \leftlabel{$n$} && $A$ & \redarrow & $n$ && $A$ & copy $m$ \\
\skipforward
\hline
\Lstrut \rlap{\red{\texttt{insert H $B$}}} \\
\noalign{\medskip}
\lstrut &&&&&& \dots \\
\lstrut &&&& $n$ & $\;$\rightlabel{H} & $B$ & \\
\lstrut && \dots &&&& \dots \\
\lstrut \leftlabel{$n$} && $A$ & \redarrow & $n + 1$ && $A$ & \\
\skipforward
\hline
\end{tabular}
\end{center}

\subsection{Backward tactics}

The tactic names may be prefixed with\red{\texttt{ b\char`\_}\dots} to contrast them to the corresponding forward tactics.

Rules that are not intuitionistically valid are marked with a star.
Rules that according to Huth \& Ryan are derived rules are marked with a dagger.

\begin{center}
\begin{tabular}{lrlcrrlll}
\hline
\Lstrut \rlap{\emph{conjunction introduction}} \\
\strut \rlap{\red{\texttt{con\char`\_i}}} \\
\lstrut &&&& && \dots \\
\lstrut &&&& $n$ && $A$ \\
\lstrut &&&& && \dots \\
\lstrut && \dots && $n + 1$ && $B$ \\
\lstrut \leftlabel{$n$} && $A \land B$ & \redarrow & $n + 2$ && $A \land B$ & $\land$i $n,(n + 1)$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{conjunction elimination left}}\label{rule:fitch:con_e1} \\
\strut \rlap{\red{\texttt{con\char`\_e1 $B$}}} \\
\lstrut &&&& && \dots \\
\lstrut && \dots && $n$ && $A \land B$ \\
\lstrut \leftlabel{$n$} && $A$ & \redarrow & $n + 1$ && $A$ & $\land$e$_1$ $n$ \\
\skipforward
\hline
\end{tabular}
\end{center}
\newpage
\begin{center}
\begin{tabular}{lrlcrrlll}
\hline
\Lstrut \rlap{\emph{conjunction elimination right}} \\
\strut \rlap{\red{\texttt{con\char`\_e2 $A$}}} \\
\lstrut &&&& && \dots \\
\lstrut && \dots && $n$ && $A \land B$ \\
\lstrut \leftlabel{$n$} && $B$ & \redarrow & $n + 1$ && $B$ & $\land$e$_2$ $n$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{disjunction introduction left}} \\
\strut \rlap{\red{\texttt{dis\char`\_i1}}} \\
\lstrut &&&& && \dots \\
\lstrut && \dots && $n$ && $A$ \\
\lstrut \leftlabel{$n$} && $A \lor B$ & \redarrow & $n + 1$ && $A \lor B$ & $\lor$i$_1$ $n$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{disjunction introduction right}} \\
\strut \rlap{\red{\texttt{dis\char`\_i2}}} \\
\lstrut &&&& && \dots \\
\lstrut && \dots && $n$ && $B$ \\
\lstrut \leftlabel{$n$} && $A \lor B$ & \redarrow & $n + 1$ && $A \lor B$ & $\lor$i$_1$ $n$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{disjunction elimination}} \\
\strut \rlap{\red{\texttt{dis\char`\_e ($A$ \char`\\/ $B$) H1 H2}}} \\
\lstrut &&&& && \dots \\
\Lstrut &&&& $n$ && $A \lor B$ && \\
\cline{6-8}
\Lstrut &&&& $n + 1$ & \multicolumn{1}{|l}{\rightlabel{H1}} & $A$ & assumption & \multicolumn{1}{|l}{} \\
\lstrut &&&&& \multicolumn{1}{|l}{} & \dots && \multicolumn{1}{|l}{}  \\
\Lstrut &&&& $n + 2$ & \multicolumn{1}{|l}{} & $C$ && \multicolumn{1}{|l}{} \\
\cline{6-8} \\
\cline{6-8}
\Lstrut &&&& $n + 3$ & \multicolumn{1}{|l}{\rightlabel{H2}} & $B$ & assumption & \multicolumn{1}{|l}{} \\
\lstrut &&&&& \multicolumn{1}{|l}{} & \dots && \multicolumn{1}{|l}{}  \\
\Lstrut && \dots && $n + 4$ & \multicolumn{1}{|l}{} & $C$ && \multicolumn{1}{|l}{} \\
\cline{6-8}
\Lstrut \leftlabel{$n$} && $C$ & \redarrow & $n + 5$ && $C$ & \rlap{$\lor$e $n$,$(n + 1)$---$(n + 2)$,$(n + 3)$---$(n + 4)$} \\
\skipforward
\hline
\Lstrut \rlap{\emph{implication introduction}} \\
\strut \rlap{\red{\texttt{imp\char`\_i H}}} \\
\cline{6-8}
\Lstrut &&&& $n$ & \multicolumn{1}{|l}{\rightlabel{H}} & $A$ & assumption & \multicolumn{1}{|l}{} \\
\lstrut &&&&& \multicolumn{1}{|l}{} & \dots && \multicolumn{1}{|l}{}  \\
\Lstrut && \dots && $n + 1$ & \multicolumn{1}{|l}{} & $B$ && \multicolumn{1}{|l}{} \\
\cline{6-8}
\Lstrut \leftlabel{$n$} && $A \to B$ & \redarrow & $n + 2$ && $A \to B$ & $\to$i $n$---$(n + 1)$ & \\
\skipforward
\hline
\end{tabular}
\end{center}
\newpage
\begin{center}
\begin{tabular}{lrlcrrlll}
\hline
\Lstrut \rlap{\emph{implication elimination}} \\
\strut \rlap{\red{\texttt{imp\char`\_e $A$}}} \\
\lstrut &&&& && \dots \\
\lstrut &&&& $n$ && $A \to B$ \\
\lstrut &&&& && \dots \\
\lstrut && \dots && $n + 1$ && $A$ \\
\lstrut \leftlabel{$n$} && $B$ & \redarrow & $n + 2$ && $B$ & $\to$e $n,(n + 1)$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{negation introduction}} \\
\strut \rlap{\red{\texttt{neg\char`\_i H}}} \\
\cline{6-8}
\Lstrut &&&& $n$ & \multicolumn{1}{|l}{\rightlabel{H}} & $A$ & assumption & \multicolumn{1}{|l}{} \\
\lstrut &&&&& \multicolumn{1}{|l}{} & \dots && \multicolumn{1}{|l}{}  \\
\Lstrut && \dots && $n + 1$ & \multicolumn{1}{|l}{} & $\bot$ && \multicolumn{1}{|l}{} \\
\cline{6-8}
\Lstrut \leftlabel{$n$} && $\neg A$ & \redarrow & $n + 2$ && $\neg A$ & $\neg$i $n$---$(n + 1)$ & \\
\skipforward
\hline
\Lstrut \rlap{\emph{negation elimination}} \\
\strut \rlap{\red{\texttt{neg\char`\_e $A$}}} \\
\lstrut &&&& && \dots \\
\lstrut &&&& $n$ && $\neg A$ \\
\lstrut &&&& && \dots \\
\lstrut && \dots && $n + 1$ && $A$ \\
\lstrut \leftlabel{$n$} && $\bot$ & \redarrow & $n + 2$ && $\bot$ & $\neg$e $n,(n + 1)$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{falsum elimination}} \\
\strut \rlap{\red{\texttt{fls\char`\_e}}} \\
\lstrut &&&& && \dots \\
\lstrut && \dots && $n$ && $\bot$ \\
\lstrut \leftlabel{$n$} && $A$ & \redarrow & $n + 1$ && $A$ & $\bot$e $n$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{truth introduction}} \\
\strut \rlap{\red{\texttt{tru\char`\_i}}} \\
\lstrut && \dots \\
\lstrut \leftlabel{$n$} && $\top$ & \redarrow & $n$ && $\top$ & $\top$i $n$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{double negation introduction}$^\dagger$} \\
\strut \rlap{\red{\texttt{negneg\char`\_i}}} \\
\lstrut &&&& && \dots \\
\lstrut && \dots && $n$ && $A$ \\
\lstrut \leftlabel{$n$} && $\neg\neg A$ & \redarrow & $n + 1$ && $\neg\neg A$ & $\neg\neg$i $n$ \\
\skipforward
\hline
\end{tabular}
\end{center}
\newpage
\begin{center}
\begin{tabular}{lrlcrrlll}
\hline
\Lstrut \rlap{\emph{double negation elimination}*} \\
\strut \rlap{\red{\texttt{negneg\char`\_e}}} \\
\lstrut &&&& && \dots \\
\lstrut && \dots && $n$ && $\neg\neg A$ \\
\lstrut \leftlabel{$n$} && $A$ & \redarrow & $n + 1$ && $A$ & $\neg\neg$e $n$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{law of excluded middle}*$^\dagger$} \\
\strut \rlap{\red{\texttt{LEM}}} \\
\lstrut && \dots \\
\lstrut \leftlabel{$n$} && $A \lor \neg A$ & \redarrow & $n$ && $A \lor \neg A$ & LEM \\
\skipforward
\hline
\Lstrut \rlap{\emph{proof by contradiction}*$^\dagger$} \\
\strut \rlap{\red{\texttt{PBC H}}} \\
\cline{6-8}
\Lstrut &&&& $n$ & \multicolumn{1}{|l}{\rightlabel{H}} & $\neg A$ & assumption & \multicolumn{1}{|l}{} \\
\lstrut &&&&& \multicolumn{1}{|l}{} & \dots && \multicolumn{1}{|l}{}  \\
\Lstrut && \dots && $n + 1$ & \multicolumn{1}{|l}{} & $\bot$ && \multicolumn{1}{|l}{} \\
\cline{6-8}
\Lstrut \leftlabel{$n$} && $A$ & \redarrow & $n + 2$ && $A$ & PBC $n$---$(n + 1)$ & \\
\skipforward
\hline
\Lstrut \rlap{\emph{modus tollens}$^\dagger$} \\
\strut \rlap{\red{\texttt{MT $B$}}} \\
\lstrut &&&& && \dots \\
\lstrut &&&& $n$ && $A \to B$ \\
\lstrut &&&& && \dots \\
\lstrut && \dots && $n + 1$ && $\neg B$ \\
\lstrut \leftlabel{$n$} && $\neg A$ & \redarrow & $n + 2$ && $\neg A$ & MT $n,(n + 1)$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{universal introduction}} \\
\strut \rlap{\red{\texttt{all\char`\_i $y$}}} \\
\cline{6-8}
\Lstrut &&&&& \multicolumn{1}{|l}{$y$} &&& \multicolumn{1}{|l}{} \\
\lstrut &&&&& \multicolumn{1}{|l}{} & \dots && \multicolumn{1}{|l}{} \\
\Lstrut && \dots && $n$ & \multicolumn{1}{|l}{} & $A[y/x]$ && \multicolumn{1}{|l}{} \\
\cline{6-8}
\Lstrut \leftlabel{$n$} && $\forall x\, A$ & \redarrow & $n + 1$ && $\forall x\, A$ & $\forall$i $n$---$n$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{universal elimination}} \\
\strut \rlap{\red{\texttt{all\char`\_e (all x, $A$)}}} \\
\lstrut &&&&&& \dots \\
\lstrut && \dots && $n$ && $\forall x\, A$ \\
\lstrut \leftlabel{$n$} && $A[t/x]$ & \redarrow & $n + 1$ && $A[t/x]$ & $\forall$e $n$ & \\
\skipforward
\hline
\end{tabular}
\end{center}
\newpage
\begin{center}
\begin{tabular}{lrlcrrlll}
\hline
\Lstrut \rlap{\emph{existential introduction}} \\
\strut \rlap{\red{\texttt{exi\char`\_i $t$}}} \\
\lstrut &&&&&& \dots \\
\lstrut && \dots && $n$ && $A[t/x]$ \\
\lstrut \leftlabel{$n$} && $\exists x\, A$ & \redarrow & $n + 1$ && $\exists x\, A$ & $\exists$i $n$ & \\
\skipforward
\hline
\Lstrut \rlap{\emph{existential elimination}} \\
\strut \rlap{\red{\texttt{exi\char`\_e (exi x, $A$) $y$ H}}} \\
\lstrut &&&& && \dots \\
\Lstrut &&&& $n$ && $\exists x\, A$ && \\
\cline{6-8}
\Lstrut &&&&& \multicolumn{1}{|l}{$y$} &&& \multicolumn{1}{|l}{} \\
\lstrut &&&& $n + 1$ & \multicolumn{1}{|l}{\rightlabel{H}} & $A[y/x]$ && \multicolumn{1}{|l}{} \\
\lstrut &&&&& \multicolumn{1}{|l}{} & \dots && \multicolumn{1}{|l}{} \\
\Lstrut && \dots && $n + 2$ & \multicolumn{1}{|l}{} & $B$ && \multicolumn{1}{|l}{} \\
\cline{6-8}
\Lstrut \leftlabel{$n$} && $B$ & \redarrow & $n + 3$ && $B$ & \rlap{$\exists$e $n$,$(n + 1)$---$(n + 2)$} \\
\skipforward
\hline
\Lstrut \rlap{\emph{equality introduction}} \\
\strut \rlap{\red{\texttt{equ\char`\_i}}} \\
\lstrut && \dots \\
\lstrut \leftlabel{$n$} && $t = t$ & \redarrow & $n$ && $t = t$ & $=$i \\
\skipforward
\hline
\Lstrut \rlap{\emph{equality elimination, simple version}} \\
\strut \rlap{\red{\texttt{equ\char`\_e ($t_1$ = $t_2$)}}} \\
\lstrut &&&& && \dots \\
\lstrut &&&& $n$ && $t_1 = t_2$ \\
\lstrut &&&& && \dots \\
\lstrut && \dots && $n + 1$ && $A[t_1/x]$ \\
\lstrut \leftlabel{$n$} && $A[t_2/x]$ & \redarrow & $n + 2$ && $A[t_2/x]$ & $=$e $n,(n + 1)$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{equality elimination, general version} (\emph{$t_2$ may occur in $A$})} \\
\strut \rlap{\red{\texttt{equ\char`\_e' ($t_1$ = $t_2$) (fun x => $A$)}}} \\
\lstrut &&&& && \dots \\
\lstrut && \dots && $n$ && $t_1 = t_2$ \\
\lstrut &&&& && \dots \\
\lstrut && \dots && $n + 1$ && $A[t_1/x]$ \\
\lstrut \leftlabel{$n$} && $A[t_2/x]$ & \redarrow & $n + 2$ && $A[t_2/x]$ & $=$e $n,(n + 1)$ \\
\skipforward
\hline
\end{tabular}
\end{center}

\def\leftlabel#1{\phantom{$m_1$}\llap{#1}}

\newpage
\subsection{Forward versus backward tactics}
\ 
\begin{center}
\begin{tabular}{lrlcrrlll}
\hline
\Lstrut \rlap{\emph{conjunction introduction}} \\
\strut \rlap{\red{\texttt{f\char`\_con\char`\_i H1 H2}}} \\
\noalign{\medskip}
\lstrut \leftlabel{$m_1$} & $\;$\rightlabel{H1} & $A$ && $m_1$ & $\;$\rightlabel{H1} & $A$ \\
\noalign{\medskip}
\lstrut \leftlabel{$m_2$} & $\;$\rightlabel{H2} & $B$ && $m_2$ & $\;$\rightlabel{H2} & $B$ \\
\noalign{\medskip}
\lstrut && \dots &&& \\
\lstrut \leftlabel{$n$} && $A \land B$ & \redarrow & $n$ && $A \land B$ & $\land$i $m_1,m_2$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{conjunction elimination left}}\label{rule:fitch:f_con_e1} \\
\strut \rlap{\red{\texttt{f\char`\_con\char`\_e1 H}}} \\
\noalign{\medskip}
\lstrut \leftlabel{$m$} & $\;$\rightlabel{H} & $A \land B$ && $m$ & $\;$\rightlabel{H} & $A \land B$ \\
\noalign{\medskip}
\lstrut && \dots &&& \\
\lstrut \leftlabel{$n$} && $A$ & \redarrow & $n$ && $A$ & $\land$e$_1$ $m$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{conjunction elimination right}} \\
\strut \rlap{\red{\texttt{f\char`\_con\char`\_e2 H}}} \\
\noalign{\medskip}
\lstrut \leftlabel{$m$} & $\;$\rightlabel{H} & $A \land B$ && $m$ & $\;$\rightlabel{H} & $A \land B$ \\
\noalign{\medskip}
\lstrut && \dots &&& \\
\lstrut \leftlabel{$n$} && $B$ & \redarrow & $n$ && $B$ & $\land$e$_2$ $m$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{disjunction introduction left}} \\
\strut \rlap{\red{\texttt{f\char`\_dis\char`\_i1 H}}} \\
\noalign{\medskip}
\lstrut \leftlabel{$m$} & $\;$\rightlabel{H} & $A$ && $m$ & $\;$\rightlabel{H}& $A$ \\
\noalign{\medskip}
\lstrut && \dots &&& \\
\lstrut \leftlabel{$n$} && $A \lor B$ & \redarrow & $n$ && $A \lor B$ & $\lor$i$_1$ $m$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{disjunction introduction right}} \\
\strut \rlap{\red{\texttt{f\char`\_dis\char`\_i2 H}}} \\
\noalign{\medskip}
\lstrut \leftlabel{$m$} & $\;$\rightlabel{H} & $B$ && $m$ & $\;$\rightlabel{H}& $B$ \\
\noalign{\medskip}
\lstrut && \dots &&& \\
\lstrut \leftlabel{$n$} && $A \lor B$ & \redarrow & $n$ && $A \lor B$ & $\lor$i$_2$ $m$ \\
\skipforward
\hline
\end{tabular}
\end{center}
\newpage
\begin{center}
\begin{tabular}{lrlcrrlll}
\hline
\Lstrut \rlap{\emph{disjunction elimination}} \\
\strut \rlap{\red{\texttt{f\char`\_dis\char`\_e H H1 H2}}} \\
\noalign{\medskip}
\Lstrut $m$ & \rightlabel{H} & $A \lor B$ && $m$ & \rightlabel{H} & $A \lor B$ && \\
\noalign{\bigskip}
\cline{6-8}
\Lstrut &&&& $n$ & \multicolumn{1}{|r}{\rightlabel{H1}} & $A$ & assumption & \multicolumn{1}{|l}{} \\
\lstrut &&&&& \multicolumn{1}{|r}{} & \dots && \multicolumn{1}{|l}{}  \\
\Lstrut &&&& $n + 1$ & \multicolumn{1}{|r}{} & $C$ && \multicolumn{1}{|l}{} \\
\cline{6-8} \\
\cline{6-8}
\Lstrut &&&& $n + 2$ & \multicolumn{1}{|r}{\rightlabel{H2}} & $B$ & assumption & \multicolumn{1}{|l}{} \\
\lstrut &&&&& \multicolumn{1}{|r}{} & \dots && \multicolumn{1}{|l}{}  \\
\Lstrut && \dots && $n + 3$ & \multicolumn{1}{|r}{} & $C$ && \multicolumn{1}{|l}{} \\
\cline{6-8}
\Lstrut \leftlabel{$n$} && $C$ & \redarrow & $n + 4$ && $C$ & \rlap{$\lor$e $m$,$n$---$(n + 1)$,$(n + 2)$---$(n + 3)$} \\
\skipforward
\hline
\Lstrut \rlap{\emph{implication elimination}} \\
\strut \rlap{\red{\texttt{f\char`\_imp\char`\_e H1 H2}}} \\
\noalign{\medskip}
\lstrut \leftlabel{$m_1$} & $\;$\rightlabel{H1} & $A \to B$ && $m_1$ & $\;$\rightlabel{H1}& $A \to B$ \\
\noalign{\medskip}
\lstrut \leftlabel{$m_2$} & $\;$\rightlabel{H2} & $A$ && $m_2$ & $\;$\rightlabel{H2}& $A$ \\
\noalign{\medskip}
\lstrut && \dots &&& \\
\lstrut \leftlabel{$n$} && $B$ & \redarrow & $n$ && $B$ & $\to$e $m_1,m_2$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{negation elimination}} \\
\strut \rlap{\red{\texttt{f\char`\_neg\char`\_e H1 H2}}} \\
\noalign{\medskip}
\lstrut \leftlabel{$m_1$} & $\;$\rightlabel{H1} & $\neg A$ && $m_1$ & $\;$\rightlabel{H1}& $\neg A$ \\
\noalign{\medskip}
\lstrut \leftlabel{$m_2$} & $\;$\rightlabel{H2} & $A$ && $m_2$ & $\;$\rightlabel{H2} & $A$ \\
\noalign{\medskip}
\lstrut && \dots &&& \\
\lstrut \leftlabel{$n$} && $\bot$ & \redarrow & $n$ && $\bot$ & $\neg$e $m_1,m_2$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{falsum elimination}} \\
\strut \rlap{\red{\texttt{f\char`\_fls\char`\_e H}}} \\
\noalign{\medskip}
\lstrut \leftlabel{$m$} & $\;$\rightlabel{H} & $\bot$ && $m$ & $\;$\rightlabel{H} & $\bot$ \\
\noalign{\medskip}
\lstrut && \dots &&& \\
\lstrut \leftlabel{$n$} && $A$ & \redarrow & $n$ && $A$ & $\bot$e $m$ \\
\skipforward
\hline
\end{tabular}
\end{center}
\newpage
\begin{center}
\begin{tabular}{lrlcrrlll}
\hline
\Lstrut \rlap{\emph{truth introduction}} \\
\strut \rlap{\red{\texttt{f\char`\_tru\char`\_i}}} \\
\lstrut && \dots \\
\lstrut \leftlabel{$n$} && $\top$ & \redarrow & $n$ && $\top$ & $\top$i $n$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{double negation introduction}$^\dagger$} \\
\strut \rlap{\red{\texttt{f\char`\_negneg\char`\_i H}}} \\
\noalign{\medskip}
\lstrut \leftlabel{$m$} & $\;$\rightlabel{H} & $A$ && $m$ & $\;$\rightlabel{H} & $A$ \\
\noalign{\medskip}
\lstrut && \dots &&& \\
\lstrut \leftlabel{$n$} && $\neg\neg A$ & \redarrow & $n$ && $\neg\neg A$ & $\neg\neg$i $m$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{double negation elimination}*} \\
\strut \rlap{\red{\texttt{f\char`\_negneg\char`\_e H}}} \\
\noalign{\medskip}
\lstrut \leftlabel{$m$} & $\;$\rightlabel{H} & $\neg\neg A$ && $m$ & $\;$\rightlabel{H} & $\neg\neg A$ \\
\noalign{\medskip}
\lstrut && \dots &&& \\
\lstrut \leftlabel{$n$} && $A$ & \redarrow & $n$ && $A$ & $\neg\neg$e $m$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{law of excluded middle}*$^\dagger$} \\
\strut \rlap{\red{\texttt{f\char`\_LEM}}} \\
\lstrut && \dots \\
\lstrut \leftlabel{$n$} && $A \lor \neg A$ & \redarrow & $n$ && $A \lor \neg A$ & LEM \\
\skipforward
\hline
\Lstrut \rlap{\emph{modus tollens}$^\dagger$} \\
\strut \rlap{\red{\texttt{f\char`\_MT H1 H2}}} \\
\noalign{\medskip}
\lstrut \leftlabel{$m_1$} & $\;$\rightlabel{H1} & $A \to B$ && $m_1$ & $\;$\rightlabel{H1}& $A \to B$ \\
\noalign{\medskip}
\lstrut \leftlabel{$m_2$} & $\;$\rightlabel{H2} & $\neg B$ && $m_2$ & $\;$\rightlabel{H2}& $\neg B$ \\
\noalign{\medskip}
\lstrut && \dots &&&& \\
\lstrut \leftlabel{$n$} && $\neg A$ & \redarrow & $n$ && $\neg A$ & MT $m_1,m_2$ \\
\skipforward
\hline
\Lstrut \rlap{\emph{universal elimination}} \\
\strut \rlap{\red{\texttt{f\char`\_all\char`\_e H}}} \\
\noalign{\medskip}
\lstrut \leftlabel{$m$} & $\;$\rightlabel{H} & $\forall x\, A$ && $m$ & $\;$\rightlabel{H} & $\forall x\, A$ \\
\noalign{\medskip}
\lstrut && \dots &&& \\
\lstrut \leftlabel{$n$} && $A[t/x]$ & \redarrow & $n$ && $A[t/x]$ & $\forall$e $m$ & \\
\skipforward
\hline
\end{tabular}
\end{center}
\newpage
\begin{center}
\begin{tabular}{lrlcrrlll}
\hline
\Lstrut \rlap{\emph{existential introduction}} \\
\strut \rlap{\red{\texttt{f\char`\_exi\char`\_i H}}} \\
\noalign{\medskip}
\lstrut \leftlabel{$m$} & $\;$\rightlabel{H} & $A[t/x]$ && $m$ & $\;$\rightlabel{H}& $A[t/x]$ \\
\noalign{\medskip}
\lstrut && \dots &&& \\
\lstrut \leftlabel{$n$} && $\exists x\, A$ & \redarrow & $n$ && $\exists x\, A$ & $\exists$i $m$ & \\
\skipforward
\hline
\Lstrut \rlap{\emph{existential elimination}} \\
\strut \rlap{\red{\texttt{f\char`\_exi\char`\_e H $y$ H1}}} \\
\noalign{\medskip}
\Lstrut $m$ & \rightlabel{H} & $\exists x\, A$ && $m$ & \rightlabel{H} & $\exists x\, A$ && \\
\noalign{\bigskip}
\cline{6-8}
\Lstrut &&&&& \multicolumn{1}{|l}{$y$} &&& \multicolumn{1}{|l}{} \\
\lstrut &&&& $n$ & \multicolumn{1}{|r}{\rightlabel{H1}} & $A[y/x]$ && \multicolumn{1}{|l}{} \\
\lstrut &&&&& \multicolumn{1}{|r}{} & \dots && \multicolumn{1}{|l}{} \\
\Lstrut && \dots && $n + 1$ & \multicolumn{1}{|r}{} & $B$ && \multicolumn{1}{|l}{} \\
\cline{6-8}
\Lstrut \leftlabel{$n$} && $B$ & \redarrow & $n + 2$ && $B$ & \rlap{$\exists$e $m$,$n$---$(n + 1)$} \\
\skipforward
\hline
\Lstrut \rlap{\emph{equality introduction}} \\
\strut \rlap{\red{\texttt{f\char`\_equ\char`\_i}}} \\
\lstrut && \dots \\
\lstrut \leftlabel{$n$} && $t = t$ & \redarrow & $n$ && $t = t$ & $=$i \\
\skipforward
\hline
\Lstrut \rlap{\emph{equality elimination}} \\
\strut \rlap{\red{\texttt{f\char`\_equ\char`\_e H1 H2}}} \\
\noalign{\medskip}
\lstrut \leftlabel{$m_1$} & $\;$\rightlabel{H1} & $t_1 = t_2$ && $m_1$ & $\;$\rightlabel{H1}& $t_1 = t_2$ \\
\noalign{\medskip}
\lstrut \leftlabel{$m_2$} & $\;$\rightlabel{H2} & $A[t_1/x]$ && $m_2$ & $\;$\rightlabel{H2} & $A[t_1/x]$ \\
\noalign{\medskip}
\lstrut && \dots &&& \\
\lstrut \leftlabel{$n$} && $A[t_2/x]$ & \redarrow & $n$ && $A[t_2/x]$ & $=$e $m_1,m_2$ \\
\skipforward
\hline
\end{tabular}
\end{center}

\end{document}