% !TeX root = easycrypt.tex

Tactics can be combined together, composed and modified by
\define[tactical]{tacticals}. Tacticals do not correspond to any deduction rule
but make the proof process smoother, and sometimes permit the reuse of proofs
with similar patterns, but where the fine minutiae might differ.

\newcommand{\addTclTacticPlain}[2]{\addTacticPlain{#1}{#2}}
\newcommand{\addTclTacticIdx}[1]{\addTacticIdx{tactical}{#1}}
\newcommand{\addTclTactic}[2]{\addTactic{tactical}{#1}{#2}}

\warningbox{The precedence rules for tacticals may sometime appear
counterintuitive. They are currently not listed below in any particular order,
and this documentation does not currently describe the precendence rules.
We are working on improving this.}

%seq
\addTclTacticPlain{Tactics sequencing}{\ec{t1; t2}}
Execute \ec{t1} and then \ec{t2} on all the subgoals generated by
\ec{t1}.

%try
\addTclTacticPlain{Failure recovery}{\ec{try t}}
\addTclTacticIdx{try}
Execute the tactic \ec{t} if it succeeds; do noting if it fails.

\paragraph{Remark}
By default, \EasyCrypt proofs are run in \ec{strict} mode. In this mode,
\ec{smt} failures cannot be caught using \ec{try}. This allows \EasyCrypt
to always build the proof tree correctly, even in weak check mode, where
\ec{smt} calls are assumed to succeed. Inside a strict proof, weak check mode
can be turned on and off at will, allowing for the fast replay of proof
sections during development. In any event, we recommend \emph{never} using
\ec{try smt}: a little thought is much more cost-effective than a bunch of
\ec{smt}.

%repetition
\addTclTacticPlain{Tactics repetition}{\ec{do !t}}
\addTclTacticIdx{do}
Apply \ec{t} to the current goal, then repeatedly apply it to all subgoals,
stopping only when it fails. An error is produced it \ec{t} does not apply to
the current goal.

\paragraph{Variants}\strut\\

\noindent\begin{tabularx}{\textwidth}{@{}ll@{}}
 {\ec{do ?t}} & apply {\ec{t}} 0 or more times, until it fails\\
 {\ec{do n !t}} & apply {\ec{t}} with depth exactly {\ec{n}}\\
 {\ec{do n ?t}} & apply {\ec{t}} with depth at most {\ec{n}}
\end{tabularx}

\warningbox{In some cases, \ec{do ?t} may lead to non-termination for obvious
reasons. Please report any occurrence that seems abnormal.}

%selection
\addTclTacticPlain{Goal selection}{\ec{t1; first t2}}
\addTclTacticIdx{first}
\addTclTacticIdx{last}
Apply the tactic \ec{t1}, then apply \ec{t2} on the first subgoal
generated by \ec{t1}. An error is produced if no subgoals have been
generated by \ec{t1}.

\paragraph{Variants}\strut\\

\noindent\begin{tabularx}{\textwidth}{@{}ll@{}}
 {\ec{t1; first n t2}} & apply {\ec{t2}} on the first {\ec{n}} subgoals
   generated by {\ec{t1}}\\
 {\ec{t1; last t2}} & apply {\ec{t2}} on the last subgoal
   generated by {\ec{t1}}\\
 {\ec{t1; last n t2}} & apply {\ec{t2}} on the last {\ec{n}} subgoals
   generated by {\ec{t1}}\\
 {\ec{t; first n last}} & \parbox{200pt}{reorder the subgoals generated by {\ec{t}}, moving
   the first n to the end of the list}
\end{tabularx}

%closing
\addTclTacticPlain{Closing goals}{\ec{by t}}
\addTclTacticIdx{by}
Apply the tactic \ec{t} if all the subgoals it generates can be discharged by
\ec{simplify}, fail otherwise.