% !TeX root = easycrypt.tex

\newcommand{\addAmbTacticNoIdx}[1]{\addTacticNoIdx{#1}}
\newcommand{\addAmbTacticIdx}[1]{\addTacticIdx{ambient}{#1}}
\newcommand{\addAmbTactic}[2]{\addTactic{ambient}{#1}{#2}}

\EasyCrypt's ambient logic is based on non-dependent higher-order logic.

\warningbox{
Note that, in the following, the rules are displayed assuming that all patterns
have been fully matched and instantiated. The pattern-matching process is
described separately, in a section that Pierre-Yves still has to write.}

\subsection{Convertibility}\label{convertible}

\EasyCrypt's ambient logic enjoys a mechanism that identifies all formulas
that are \define{convertible}, that is, formulas that are equal up to a given
amount of computations. The computational power of \EasyCrypt is defined
as the closure by equivalence of the following rewriting system augmented with
a set of logical simplification rules denoted by $\rightarrow_\Lambda$.

\begin{center}
\begin{tabular}{l@{$\quad$}l@{$\quad$}ll}
{\rawec{(fun (x : t), phi1)\ phi2}} & $\rightarrow_\beta$ &
  \multicolumn{2}{@{}l}{{\rawec{phi2} \{\rawec{x} $\leftarrow$ \rawec{phi1}\}}}\\
{\rawec{if (true) \{ phi1 \} else \{ phi2 \}}} & $\rightarrow_\iota$ &
  {\rawec{phi1}}\\
{\rawec{if (false) \{ phi1 \} else \{ phi2 \}}} & $\rightarrow_\iota$ &
  \multicolumn{2}{@{}l}{{\rawec{phi2}}}\\
{\rawec{let (x1, ..., xn) = (phi1, ..., phin) in phi}} & $\rightarrow_\iota$ &
  \multicolumn{2}{@{}l}{{\rawec{phi} \{ \rawec{x1, ..., xn} $\leftarrow$ \rawec{phi1, ..., phin} \}}}\\
{\rawec{let x = phi1 in phi2}} & $\rightarrow_\zeta$ &
  \multicolumn{2}{@{}l}{{\rawec{phi2} \{ \rawec{x} $\leftarrow$ \rawec{phi1} \}}}\\
{\rawec{o}} & $\rightarrow_\delta^{\Env,\Gamma}$ &
  {\rawec{e}} & if {\rawec{op o := e}} $\in \Env$\\
{\rawec{x}} & $\rightarrow_\delta^{\Env,\Gamma}$ &
  {\rawec{phi}} & if {\rawec{x := phi}} $\in \Gamma$\\
\end{tabular}
\end{center}

We write $\rightarrow_\delta$ for $\rightarrow_\delta^{\Env;\Gamma}$ if
$\Env; \Gamma$ is clear from context. We write $\rightarrow_{\Env;\Gamma}$ for
the union of all the $\beta\iota\delta\zeta\Lambda$-rewrite rules. As usual,
$\leftrightarrow^*_{\Env;\Gamma}$ denotes the closure by equivalence of
$\rightarrow_{\Env;\Gamma}$.

%change
\addAmbTactic{change}{\tacarg{f}{formula}}
Change the current goal to the $\leftrightarrow^*$-equivalent one \ec{f}
\begin{displaymath}
  \infrule{\phi_1 \leftrightarrow^*_{\Env;\Gamma} \phi_2 \quad
           \Env; \Gamma \vdash \phi_1}
          {\Env; \Gamma \vdash \phi_2}[{\color{Blue} \textsf{change}}\ \phi_1]
\end{displaymath}

%simplify
\addAmbTactic{simplify}{\tacarg{names}{ident*} | \ec{delta}?}
 \addAmbTacticIdx{beta}
 \addAmbTacticIdx{iota}
 \addAmbTacticIdx{zeta}
 \addAmbTacticIdx{logic}
 Change the goal with its $\beta\iota\zeta\Lambda$-head normal-form, followed
 by one step of parallel, strong $\delta$-reduction if \ec{delta} is given.
 The $\delta$-reduction can be restricted to a set of defined symbols by
 replacing \ec{delta} by a non-empty sequence of targeted symbols. You can
 selectively change the goal with its $\beta$-head normal form
 (resp. $\iota$, $\zeta$, $\Lambda$-head normal form) by using the tactic
 \ec{beta} (resp. \ec{iota}, \ec{zeta}, \ec{logic}). These tactics can be
combined together, separated by spaces, to perform head reduction by any
combination of the rule sets.

%delta
\addAmbTactic{delta}{\tacarg{names}{ident*}}
Perform one step of parallel, strong $\delta$-reduction, restricted to
the symbols listed in \ec{names}. If \ec{names} is empty, all symbols are
$\delta$-reduced.

\subsection{Bookkeeping tactics}

The following bookkeeping tactics are used to move terms between context and
goal, and to introduce new variables from known expressions.

%generalize
\addAmbTactic{generalize}{\tacarg{p}{pattern}}
Search for the first subterm of the goal matching \ec{p} and leading
to the full instantiation of the pattern. Then, do a logical
generalization of all the instantiated occurrences of \ec{p}
in the goal. An occurence selector can be used (see \ec{rewrite}).

\begin{displaymath}
  \infrule{\Env; \Gamma \vdash p \quad
           \Env; \Gamma \vdash \forall x, \phi(x)}
          {\Env; \Gamma \vdash \phi(p)}[{\color{Blue} \textsf{generalize}}\ p]
\end{displaymath}

%pose
\addAmbTactic{pose}{\tacarg{x}{ident} \rawec{:=} \tacarg{p}{pattern}}
Search for the first subterm of the goal matching \ec{p} and leading
to the full instantiation of the pattern. Then introduce, after
instantiation, the local definition \rawec{x := p} and abstract
all instantiated occurrences of \ec{p} in the goal by \ec{x}. An
occurence selector can be used (see \ec{rewrite}).
\begin{displaymath}
  \infrule{\Env; \Gamma \vdash p \quad
           \Env; \Gamma, x := p \vdash \phi(x)}
          {\Env; \Gamma \vdash \phi(p)}[{\color{Blue} \textsf{pose}}\ x := p]
\end{displaymath}

%intros
\addAmbTactic{intros}{}
This is the identity tactic, corresponding to \SsReflect's $\mathsf{move}$
tactic. It does nothing.

\warningbox{Actual intro-patterns are documented separately, in a section
Pierre-Yves still has to write.}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% LOGIC
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Logic}

%assumption
\addAmbTactic{assumption}{}
Search in the context for a hypothesis that is convertible to the goal.
If one exists, the goal is closed. If no such hypothesis exists, the tactic fails.
\begin{displaymath}
  \infrule{(h : \phi) \in \Gamma}{\Env; \Gamma \vdash \phi}[{\color{Red} \textsf{assumption}}]
\end{displaymath}

%reflexivity
\addAmbTactic{reflexivity}{}
Solve goals of the form \ec{b = b} for any term \ec{b}.
\begin{displaymath}
  \infrule{ }{\Env; \Gamma \vdash b = b}[{\color{Red} \textsf{reflexivity}}]
\end{displaymath}

%split
\addAmbTactic{split}{}
Break an intrinsically conjunctive goal into its component subgoals.
For instance, it can:
 \begin{itemize}
  \item close any goal that is convertible to \ec{true} or provable
        by \ec{reflexivity},

  \begin{displaymath}
  \infrule{\Env; \Gamma \vdash a \conv[\Env;\Gamma] true}{a}[{\color{Blue} \textsf{split}}]
  ~~~~~~
  \infrule{\Env; \Gamma \vdash a \conv[\Env;\Gamma] b}{a = b}[{\color{Blue} \textsf{split}}]
  \end{displaymath}
       
  \item replace a logical equivalence by the direct and indirect implication,

  \begin{displaymath}
  \infrule{\Env; \Gamma \vdash \phi_1 \Rightarrow \phi_2 \quad
           \Env; \Gamma \vdash \phi_2 \Rightarrow \phi_1}
          {\Gamma \vdash \phi_1 \Leftrightarrow \phi_2}[{\color{Blue} \textsf{split}}]
  \end{displaymath}
  
  \item replace a goal of the form \rawec{f1 /\\ f2} (or \rawec{f1 \&\& f2})
        by the two subgoals for \ec{f1} and \ec{f2},

  \begin{displaymath}
  \infrule{\Env; \Gamma \vdash \phi_1 \quad
           \Env; \Gamma \vdash \phi_2}
          {\Env; \Gamma \vdash \phi_1 \land \phi_2}[{\color{Blue} \textsf{split}}]
  ~~~~~~
  \infrule{\Env; \Gamma \vdash \phi_1 \quad
           \Env; \Gamma \vdash \phi_1 \Rightarrow \phi_2}
          {\Env; \Gamma \vdash \phi_1 \&\& \phi_2}[{\color{Blue} \textsf{split}}]
  \end{displaymath}
        
  \item replace an equality between $n$-tuples by $n$ equalities
        on their components.

  \begin{displaymath}
  \infrule{\Env; \Gamma \vdash a_1 = b_1  \quad \cdots \quad
           \Env; \Gamma \vdash a_n = b_n}
          {\Gamma \vdash (a_1, ..., a_n) = (b_1, ..., b_n)}[{\color{Blue} \textsf{split}}]
  \end{displaymath}
\end{itemize}

%left / right
\addAmbTacticNoIdx{left / right}{}
\addAmbTacticIdx{left}
\addAmbTacticIdx{right}
Reduce a disjunctive goal to its left (resp. right) member.
\begin{displaymath}
  \infrule{\Env; \Gamma \vdash \phi_1}{\Env; \Gamma \vdash \phi_1 \lor \phi_2}[{\color{Blue} \textsf{left}}]
  ~~~~~~
  \infrule{\Env; \Gamma \vdash \phi_2}{\Env; \Gamma \vdash \phi_1 \lor \phi_2}[{\color{Blue} \textsf{right}}]
\end{displaymath}

%case
\addAmbTactic{case}{(\tacarg{f}{formula})}
Do an excluded-middle case analysis on \ec{f}, substituting \ec{f} in the goal
when possible.
\begin{displaymath}
  \infrule{\Env; \Gamma \vdash b \Rightarrow \phi(true) \quad
           \Env; \Gamma \vdash \neg b \Rightarrow \phi(false)}
          {\Env; \Gamma \vdash \phi(b)}[{\color{Blue} \textsf{case}}\ (b)]
\end{displaymath}

%cut
\addAmbTactic{cut}{\tacarg{ip}{intro-pattern} : \tacarg{C}{formula}}
Logical cut. Generate two subgoals: one for the cut formula $C$,
and one for $C \Rightarrow G$ where $G$ is the current goal. Moreover,
the intro-pattern \ec{ip} is applied to the second subgoal.
\begin{displaymath}
  \infrule{\Env; \Gamma \vdash \phi_2 \quad
           \Env; \Gamma \vdash \phi_2 \Rightarrow \phi_1}
          {\Env; \Gamma \vdash \phi_1}[{\color{Blue} \textsf{cut}}\ \phi_2]
\end{displaymath}

\paragraph{Variants}\strut\\

\noindent\begin{tabularx}{\textwidth}{@{}ll@{}}
 {\ec{cut ip: f by t}} & use {\ec{t}} to close the first subgoal generated by {\ec{cut}}
\end{tabularx}

%elim
\addAmbTactic{elim}{}

Apply the elimination principle for the top assumption.

\paragraph{Variants}
\strut\\

\noindent\begin{tabularx}{\textwidth}{@{}ll@{}}
 {\ec{elim h}} & generalize {\ec{h}} before eliminating it\\
 {\ec{elim/h}} & use elimination principle {\ec{h}}\\
 {\ec{elim/h1 h2}} & generalize {\ec{h2}} before eliminating it using {\ec{h1}}
\end{tabularx}

\warningbox{This is incomplete, and should make precise what an ``elimination
principle'' is.}

%apply
\addAmbTactic{apply}{\tacarg{p}{proof-term}}
Modus Ponens. If \ec{p} is a proof-term for the pattern (formula)
  \begin{center}
    \ec{forall (x1 : t1) ... (xn : tn), A1 -> ... -> An -> B}
  \end{center}
  \noindent then \tacname{} tries to match B with the current G. If the
  match succeeds and leads to the full instantiation of the pattern,
  then the goal is replaced, after instantiation, with the $n$ subgoals
  \ec{A1, ..., An}.

%rewrite
\addAmbTactic{rewrite}{\ec{rw}${}_1$ ... \ec{rw}${}_n$\\ \indent where the
\ec{rw}${}_i$ are
\begin{itemize}
\item one of \ec{//}, \ec{/=}, \ec{//=},
\item a proof-term, or
\item a pattern prefixed by \ec{/} (slash).
\end{itemize}
The two last forms can be prefixed by a direction indicator (the sign
\ec{-}), followed by an occurrence selector (\ec{\{i1 ... in\}}),
followed (for proof-terms only) by a repetition marker
(\ec{!}, \ec{?}, \ec{n!} or \ec{n?}). All these prefixes are optional.}

Depending on the form of \ec{rw}, \tacname{} \ec{rw} does the following:
  \begin{itemize}
   \item For \ec{//}, \ec{/=}, and \ec{//=}, see \ec{intros}.
   \item If \ec{rw} is a proof-term for the pattern
     \begin{center}
      \ec{forall (x1 : t1) ... (xn : tn), A1 -> ... -> An -> f1 = f2}
     \end{center}
     \noindent then \tacname{} searches for the first subterm of the goal
     matching \ec{f1} and resulting in the full instantiation of the pattern.
     It then replaces, after instantiation of the pattern, all the occurrences
     of \ec{f1} by \ec{f2} in the goal, and creates $n$ new subgoals for the
     \ec{Ai}'s. If no subterms of the goal match \ec{f1} or if the pattern
     cannot be fully instantiated by matching, the tactic fails.
     The tactic works the same if the pattern ends by \ec{f1 <=> f2}. If the
     direction indicator \ec{-} is given, \tacname{} works in the reverse
     direction, searching for a match of \ec{f2} and then replacing all
     occurrences of \ec{f2} by \ec{f1}.
   \item If \ec{rw} is a \ec{/}-prefixed pattern of the form \ec{(o p1 ... pn)},
     with \ec{o} a defined symbol, then \tacname{} searches for the first subterm
     of the goal matching \ec{(o p1 ... pn)} and resulting in the full instantiation
     of the pattern. It then replaces, after instantiation of the pattern, all
     the occurrences of \ec{(o p1 ... pn)} by the $\beta\delta$ head-normal form
     of \ec{(o p1 ... pn)}, where the $\delta$-reduction is restricted to subterms
     headed by the symbol \ec{o}. If no subterms of the goal match \ec{(o p1 ... pn)} or
     if the pattern cannot be fully instantiated by matching, the tactic fails. If the
     direction indicator \ec{-} is given, \tacname{} works in the reverse
     direction, searching for a match of the $\beta\delta_{\rm o}$ head-normal
     of \ec{(o p1 ... pn)} and then replacing all occurrences of this head-normal
     form with \ec{(o p1 ... pn)}.
  \end{itemize}
  
  \smallskip
  
  The occurrence selector \ec{\{i1 ... in\}} restricts which occurrences
  of the matching pattern are replaced in the goal. If given, only the
  \ec{i1}-th, ..., \ec{in}-th ones are replaced (considering that the goal is
  traversed in DFS mode). Note that this selection applies after the matching has
  been done.
  
  \medskip
  
  Repetition markers allow the repetition of the same rewriting. For instance,
  \tacname{} \ec{!rw} leads to \ec{do!} \tacname{} \ec{rw}. See \ec{do} for
  more information.
  
  \medskip

  Last, \tacname{} \ec{rw}${}_1$ ... \ec{rw}${}_n$ is equivalent to
  \tacname{} \ec{rw}${}_1$; ...; \tacname{} \ec{rw}${}_n$.

\warningbox{In addition to occurrence selectors and repetitions, one can also
avoid breaking chains of rewrites using focus selectors, which are currently
not documented.}

%subst
\addAmbTactic{subst}{\tacarg{x}{ident}?}
Search for the first equation of the form \ec{x = f} or \ec{f = x} in the context
 and replace all the occurrences of \ec{x} by \ec{f} everywhere in the context and the
 goal before clearing it. If no identifier is given, repeatedly apply the tactic to
 all identifiers for which such an equation exists.

%congr
\addAmbTactic{congr}{}
Replace a goal of the form \ec{f t1 ... tn = f u1 ... un} with the subgoals
\ec{ti = ui} for all \ec{i}. Subgoals solvable by \ec{reflexivity} are
automatically closed.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% AUTO
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Automation}

%smt
\addAmbTactic{smt}{}
Try to solve the goal using SMT solvers. The goal is sent along with all the
lemmas proved so far plus the local hypotheses.
 
\warningbox{Not all lemmas can be translated in such a way that they can
be sent to the SMT provers. For instance, any formulas involving modules
are ignored, and can therefore not be solved using \ec{smt}.}

\paragraph{Variants}\strut\\

\noindent\begin{tabularx}{\textwidth}{@{}ll@{}}
 {\ec{smt nolocal}} & do not send local hypotheses to the solvers\\
 {\ec{smt "prover"}} & only use the indicated prover (several provers can be given)\\
\end{tabularx}

A hint database can be given when calling \ec{smt}, indicating precisely which
axioms and lemmas should be sent to the solvers. The hint database mechanism
will be documented separately.

%progress
\addAmbTactic{progress}{\ec{tactic}?}
Break the goal into multiple \emph{simpler} ones by repeatedly applying
\ec{split}, \ec{subst} and \ec{intros}. If a tactic is given to \tacname{},
it is tentatively applied after each step.

\warningbox{The optional parameter to \tacname{} may cause
performance issues (with \ec{smt}, in particular). It is recommended
to avoid using it.}

%trivial
\addAmbTactic{trivial}{}
Try to solve the goal by calling \ec{try assumption; progress; assumption}.
This tactic is called by the intro-pattern \ec{//}.