% !TeX root = easycrypt.tex

%% TODO (Francois): For index, rather than \texttt, use \rawec and make a class of keywords for tactics and tacticals

\chapter{Writing Proofs\label{chap:tactics}}

\EasyCrypt comes with a proof engine that allows to state and prove properties
about programs written in the various languages described in
Chapter~\ref{chap:theories}.
%
Proofs are built interactively by applying \define[tactic]{tactics}, that transform a
current \define[goal]{proof goal} into a (possibly empty) set of
\define[subgoal]{subgoals} such that the conjunction of the subgoals implies the
original goal.
%
This process is repeated, starting from the theorem statement, up to the point
where all the subgoals correspond to general axioms or premises of the theorem.

In this chapter, we describe this proof engine in general before listing and
describing the existing tactics for various fragments of \EasyCrypt's
underlying logic.

\section{The proof engine}

The proof engine deals with \define[judgment]{judgments} or goals of the form
$\Env; \Gamma \vdash \phi$ where $\Env$ is the (global) \define{environment},
$\Gamma$ is the \define{context} (a set of local facts) and $\phi$ is the
formula we want to prove. Here is an example of such a judgment:

\begin{center}
$\Int; x, y , z: \tint, x \le y \vdash x + z \le y + z$.
\end{center}

It states that in the environment ($\Env$) solely composed of the
theory $\Int$, having three local variables $x, y, z$ of type $\tint$ along
with the fact $x \le y$ (the context $\Gamma$), we are interested
in proving $x + z \le y + z$.

\medskip

On top on this, a set of \define[deduction rule]{deduction rules} is given. They
describe how one can derive a judgment $\Env; \Gamma \vdash \phi$ given
that a set of prerequisites (or \define[premise]{premises}) are fulfilled. The
general form of such a rule is given as follow:

\begin{displaymath}
 \infrule{A_1 \cdots A_n}{\Env; \Gamma \vdash \phi}
\end{displaymath}

It has to be read as: \emph{given that $A_1 \cdots A_n$ are derivable, then
so is $\Env, \Gamma \vdash \phi$}. We give three examples of such deduction
rules:

\begin{displaymath}
 \infrule
         {\Env; \Gamma \vdash \phi_1 \quad
          \Env; \Gamma \vdash \phi_1 \Rightarrow \phi_2}
         {\Env; \Gamma \vdash \phi_2}
         {\rname{MP}}
 \quad\quad
 \infrule
         {\Env; \Gamma, \phi_1 \vdash \phi_2}
         {\Env; \Gamma \vdash \phi_1 \Rightarrow \phi_2}
         {\rname{$\Rightarrow$-I}}
 \quad\quad
 \infrule{ }{\Env; \Gamma, \phi, \Delta \vdash \phi}{\rname{Ax}}
\end{displaymath}

The first, the \emph{modus ponens}, states that one can derive
$\Env; \Gamma \vdash \phi_2$ given that $\Env; \Gamma \vdash \phi_1
\Rightarrow \phi_2$ and $\Env; \Gamma \vdash \phi_1$ are derivable.
%
The next provides a way for deriving $\phi_1 \Rightarrow \phi_2$ from
a derivation of $\phi_2$, but with a context augmented by $\phi_1$.
%
The last states that $\Env; \Gamma, \phi, \Delta \vdash \phi$ is derivable as-is.

Combining these deduction rules, it is possible to build a tree rooted by
a judgment $\Env; \Gamma \vdash \phi$ and with leaves composed of deduction
rules with no premises (as the third one in the previous example). Such a
tree forms a \define{proof} of $\Env; \Gamma \vdash \phi$.
%
For instance, Figure~\ref{fig:LJproof} gives a proof of
%
\[\Env; b_1, b_2 : \tbool \vdash (b_1 \Rightarrow b_2) \Rightarrow b_1 \Rightarrow b_2\]

\begin{figure}
  \begin{displaymath}
    \infrule
      {\infrule{ }{\Env; b_1, b_2 : \tbool, b_1 \Rightarrow b_2, b_1 \vdash b_1 \Rightarrow b_2} \quad
       \infrule{ }{\Env; b_1, b_2 : \tbool, b_1 \Rightarrow b_2, b_1 \vdash b_1}}
      {\infrule
        {\Env; b_1, b_2 : \tbool, b_1 \Rightarrow b_2, b_1 \vdash b_2}
        {\infrule
           {\Env; b_1, b_2 : \tbool, b_1 \Rightarrow b_2 \vdash b_1 \Rightarrow b_2}
           {\Env; b_1, b_2 : \tbool \vdash (b_1 \Rightarrow b_2) \Rightarrow b_1 \Rightarrow b_2}}}
  \end{displaymath}

  \caption{\label{fig:LJproof} Proof tree of
    $\Env; b_1, b_2 : \tbool \vdash
        (b_1 \Rightarrow b_2) \Rightarrow b_1 \Rightarrow b_2$}
\end{figure}

The \EasyCrypt proof engine helps the user build such proofs. At each step
of the proof building, the system presents to the user the set of goals
that have to be proved. The user can then \emph{apply} a tactic to one of
them, each tactic corresponding to a deduction rule. If the conclusion
of the rule corresponding to the applied tactic matches the goal to which
it is applied, the proof engine replaces it with the set of the
premises of the applied rule - the subgoals. This application may generate
no, one or several subgoals depending on the rule. This process is repeated
iteratively, up to the point where no goals remain.

\section{Tacticals}

\input{tacticals}

\section{Ambient Logic}
\input{ambient}

TODO: restructure the program tactics between "tactics that eat the program up", "tactics that transform the program" (swap, rcond, kill...) and "tactics that operate on the overall judgment" (conseq, exfalso).

\section{Common Hoare tactics}
The tactics mentioned so far permit to build proofs of purely logical statements
ranging over operators. The tactics introduced in the following sections allow
the user to write and prove judgments on module functions. Many of them
appear in some form or another in the various fragments of \EasyCrypt's logic,
with varying interpretations. This section discusses those program tactics whose
interpretation is similar in all logical fragments.
\input{commonhoare}

\section{Hoare Logic}
\input{hoare}

\section{Probabilistic Hoare Logic}
\input{probhoare}

\section{Probabilistic Relational Hoare Logic}
\input{probrelhoare}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "easycrypt"
%%% End: