reflection.tex

\section{Views and reflection}\label{sec:views}

The bookkeeping facilities presented in section \ref{sec:book} are
crafted to ease simultaneous introductions and generalizations of facts and
casing,
naming $\dots$ operations. It also a common practice to make a stack
operation immediately followed by an \emph{interpretation} of the fact
being pushed,
that is, to apply a lemma to this fact before passing it
to a tactic for decomposition, application and so on.


% possibly

% Small scale reflection consists in using a two levels
% approach locally when developing formal proofs. This means that a
% fact, which may be an assumption, or the goal itself, will often be
% \emph{interpreted} before being passed to a tactic
% for decomposition, application and so on.

\ssr{} provides a convenient, unified syntax to combine these
interpretation operations with the proof stack operations. This
\emph{view mechanism} relies on the combination of the \C{/} view
switch with bookkeeping tactics and tacticals.

\subsection{Interpreting eliminations}

The view syntax combined with the \C{elim} tactic specifies an
elimination scheme to
be used instead of the default, generated, one. Hence the \ssr{} tactic:
\begin{lstlisting}
  elim/V.
\end{lstlisting}
corresponds to the standard \Coq{} tactic:
\begin{lstlisting}
  intro top; elim top using V; clear top.
\end{lstlisting}
where \C{top} is a fresh name and \C{V} any second-order lemma.

Since an elimination view supports the two bookkeeping tacticals of
discharge and introduction (see section \ref{sec:book}), the \ssr{} tactic:
\begin{lstlisting}
  elim/V: x => y.
\end{lstlisting}
corresponds to the standard \Coq{} tactic:
\begin{lstlisting}
  elim x using V; clear x; intro y.
\end{lstlisting}
where \C{x} is a variable in the context, \C{y} a fresh name and \C{V}
any second order lemma; \ssr{} relaxes the syntactic restrictions of
the \Coq{} \L+elim+. The first pattern following \L+:+ can be a \L+_+
wildcard if the conclusion of the view \L+V+ specifies a pattern for
its last argument (e.g., if \L+V+ is a functional induction lemma
generated by the \L+Function+ command).

The elimination view mechanism is compatible with the equation name
generation (see section \ref{ssec:equations}).

The following script illustrate a toy example of this feature. Let us
define a function adding an element at the end of a list:
\begin{lstlisting}
  Require Import List.

  Variable d : Type.

  Fixpoint |*add_last*|(s : list d) (z : d) {struct s} : list d :=
    match s with
    | nil =>  z :: nil
    | cons x s' => cons x (add_last s' z)
    end.
\end{lstlisting}

One can define an alternative, reversed, induction principle on inductively
defined \C{list}s, by proving the following lemma:

\begin{lstlisting}
  Lemma |*last_ind_list*| : forall (P : list d -> Type),
  P nil ->
  (forall (s : list d) (x : d), P s -> P (add_last s x)) -> forall s : list d, P s.
\end{lstlisting}

Then the combination of elimination views with equation names result
in a concise syntax for reasoning inductively using the user
defined elimination scheme. The script:
\begin{lstlisting}
  Goal forall (x : d)(l : list d), l = l.
  move=> x l.
  elim/last_ind_list E : l=> [| u v]; last first.
\end{lstlisting}
generates two subgoals: the first one to prove \C{nil = nil} in a
context featuring \C{E : l = nil} and the second to prove
\C{add_last u v = add_last u v}, in a context containing
\C{E : l = add_last u v}.

User provided eliminators (potentially generated with the
\C{Function} \Coq{}'s command) can be combined with the type family switches
described in section~\ref{ssec:typefam}. Consider an eliminator
\C{foo_ind} of type:
\begin{lstlisting}
  foo_ind : forall $\dots$, forall x : T, P p$_1$ $\dots$ p$_m$
\end{lstlisting}
and consider the tactic
\begin{lstlisting}
  elim/foo_ind: e$_1$ $\dots$ / e$_n$
\end{lstlisting}
The \C{elim/} tactic distinguishes two cases:
\begin{description}
\item[truncated eliminator] when \C{x} does not occur in \C{P p$_1 \dots$ p$_m$}
  and the type of \C{e$_n$} unifies with \C{T} and \C{e$_n$} is not \C{_}.
  In that case, \C{e$_n$} is passed to the eliminator as the last argument
  (\C{x} in \C{foo_ind}) and \C{e$_{n-1} \dots$ e$_1$} are used as patterns
  to select in the goal the occurrences that will be bound by the
  predicate \C{P}, thus it must be possible to unify the sub-term of
  the goal matched by \C{e$_{n-1}$} with \C{p$_m$}, the one matched by
  \C{e$_{n-2}$} with \C{p$_{m-1}$} and so on.
\item[regular eliminator] in all the other cases. Here it must be
  possible to unify the term matched by
  \C{e$_n$} with \C{p$_m$}, the one matched by
  \C{e$_{n-1}$} with \C{p$_{m-1}$} and so on. Note that
  standard eliminators have the shape \C{$\dots$forall x, P $\dots$ x}, thus
  \C{e$_n$} is the pattern identifying the eliminated term, as expected.
\end{description}
As explained in  section~\ref{ssec:typefam}, the initial prefix of
\C{e$_i$} can be omitted.

Here an example of a regular, but non trivial, eliminator:
\begin{lstlisting}
  Function |*plus*| (m n : nat) {struct n} : nat :=
     match n with 0 => m | S p => S (plus m p) end.
\end{lstlisting}
The type of \C{plus_ind} is
\begin{lstlisting}
plus_ind : forall (m : nat) (P : nat -> nat -> Prop),
  (forall n : nat, n = 0 -> P 0 m) ->
  (forall n p : nat, n = p.+1 -> P p (plus m p) -> P p.+1 (plus m p).+1) ->
    forall n : nat, P n (plus m n)
\end{lstlisting}
Consider the following goal
\begin{lstlisting}
  Lemma |*exF*| x y z: plus (plus x y) z = plus x (plus y z).
\end{lstlisting}
The following tactics are all valid and perform the same elimination
on that goal.
\begin{lstlisting}
  elim/plus_ind: z / (plus _ z).
  elim/plus_ind: {z}(plus _ z).
  elim/plus_ind: {z}_.
  elim/plus_ind: z / _.
\end{lstlisting}
In the two latter examples, being the user provided pattern a wildcard, the
pattern inferred from the type of the eliminator is used instead.  For both
cases it is \C{(plus _ _)} and matches the subterm \C{plus (plus x y)$\;$z} thus
instantiating the latter \C{_} with \C{z}.  Note that the tactic
\C{elim/plus_ind: y / _} would have resulted in an error, since \C{y} and \C{z}
do no unify but the type of the eliminator requires the second argument of
\C{P} to be the same as the second argument of \C{plus} in the second
argument of \C{P}.

Here an example of a truncated eliminator. Consider the goal
\begin{lstlisting}
  p : nat_eqType
  n : nat
  n_gt0 : 0 < n
  pr_p : prime p
 =================
  p %| \prod_(i <- prime_decomp n | i \in prime_decomp n) i.1 ^ i.2 ->
    exists2 x : nat * nat, x \in prime_decomp n & p = x.1
\end{lstlisting}
and the tactic
\begin{lstlisting}
elim/big_prop: _ => [| u v IHu IHv | [q e] /=].
\end{lstlisting}
where the type of the eliminator is
\begin{lstlisting}
big_prop: forall (R : Type) (Pb : R -> Type) (idx : R) (op1 : R -> R -> R),
  Pb idx ->
  (forall x y : R, Pb x -> Pb y -> Pb (op1 x y)) ->
  forall (I : Type) (r : seq I) (P : pred I) (F : I -> R),
  (forall i : I, P i -> Pb (F i)) ->
    Pb (\big[op1/idx]_(i <- r | P i) F i)
\end{lstlisting}
Since the pattern for the argument of \C{Pb} is not specified, the inferred one
is used instead: \C{(\\big[_/_]_(i <- _ | _ i) _ i)}, and after the
introductions, the following goals are generated.
\begin{lstlisting}
subgoal 1 is:
 p %| 1 -> exists2 x : nat * nat, x \in prime_decomp n & p = x.1
subgoal 2 is:
 p %| u * v -> exists2 x : nat * nat, x \in prime_decomp n & p = x.1
subgoal 3 is:
 (q, e) \in prime_decomp n -> p %| q ^ e ->
   exists2 x : nat * nat, x \in prime_decomp n & p = x.1
\end{lstlisting}
Note that the pattern matching algorithm instantiated all the variables
occurring in the pattern.

\subsection{Interpreting assumptions}\label{ssec:assumpinterp}

Interpreting an assumption in the context of a proof is applying it a
correspondence lemma before generalizing, and/or decomposing it.
For instance, with the extensive use of boolean reflection (see
section \ref{ssec:boolrefl}), it is
quite frequent to need to decompose the logical interpretation of (the
boolean expression of) a
fact, rather than the fact itself.
This can be achieved by a combination of \C{move : _ => _}
switches, like in the following script, where \C{||} is a standard
  \Coq{} notation for the boolean disjunction:
\begin{lstlisting}
  Variables P Q : bool -> Prop.
  Hypothesis |*P2Q*| : forall a b, P (a || b) -> Q a.

  Goal forall a, P (a || a) -> True.
  move=> a HPa; move: {HPa}(P2Q _ _ HPa) => HQa.
\end{lstlisting}
which transforms the hypothesis \C{HPn : P n} which has been
introduced from the initial statement into \C{HQn : Q n}.
This operation is so common that the tactic shell has
specific syntax for it.
The following scripts:
\begin{lstlisting}
  Goal forall a, P (a || a) -> True.
  move=> a HPa; move/P2Q: HPa => HQa.
\end{lstlisting}
or more directly:
\begin{lstlisting}
  Goal forall a, P (a || a) -> True.
  move=> a; move/P2Q=> HQa.
\end{lstlisting}
are equivalent to the former one. The former script shows how to
interpret a fact (already in the context), thanks to the discharge
tactical (see section \ref{ssec:discharge}) and the latter, how to
interpret the top assumption of a goal. Note
that the number of wildcards to be inserted to find the correct
application of the view lemma to the hypothesis has been automatically
inferred.

The view mechanism is compatible with the \C{case} tactic and with the
equation name generation mechanism (see section \ref{ssec:equations}):
\begin{lstlisting}
  Variables P Q: bool -> Prop.
  Hypothesis |*Q2P*| : forall a b, Q (a || b) -> P a \/ P b.

  Goal forall a b, Q (a || b) -> True.
  move=> a b; case/Q2P=> [HPa | HPb].
\end{lstlisting}
creates two new subgoals whose contexts no more contain
\C{HQ : Q (a || b)} but respectively \C{HPa : P a} and
\C{HPb : P b}. This view tactic
performs:
\begin{lstlisting}
  move=> a b HQ; case: {HQ}(Q2P _ _ HQ) => [HPa | HPb].
\end{lstlisting}

The term on the right of the \C{/} view switch is called a \emph{view
  lemma}. Any \ssr{} term coercing to a product type can be used as a
view lemma.


The examples we have given so far explicitly provide the direction of the
translation to be performed. In fact, view lemmas need not to be
oriented. The view mechanism is able to detect which
application is relevant for the current goal. For instance, the
script:
\begin{lstlisting}
  Variables P Q: bool -> Prop.
  Hypothesis |*PQequiv*| : forall a b, P (a || b) <-> Q a.

  Goal forall a b, P (a || b) -> True.
  move=> a b; move/PQequiv=> HQab.
\end{lstlisting}
has the same behavior as the first example above.

The view mechanism can insert automatically a \emph{view hint} to
transform the double implication into the expected simple implication.
The last script is in fact equivalent to:
\begin{lstlisting}
  Goal forall a b, P (a || b) -> True.
  move=> a b; move/(iffLR (PQequiv _ _)).
\end{lstlisting}
where:
\begin{lstlisting}
  Lemma |*iffLR*| : forall P Q, (P <-> Q) -> P -> Q.
\end{lstlisting}


\subsubsection*{Specializing assumptions}
The special case when the \emph{head symbol} of the view lemma is a
wildcard is used to interpret an assumption by \emph{specializing}
it. The view mechanism hence offers the possibility to
apply a higher-order assumption to some given arguments.

For example, the script:
\begin{lstlisting}
  Goal forall z, (forall x y, x + y = z -> z = x) -> z = 0.
  move=> z; move/(_ 0 z).
\end{lstlisting}
changes the goal into:
\begin{lstlisting}
  (0 + z = z -> z = 0) -> z = 0
\end{lstlisting}




\subsection{Interpreting goals}\label{ssec:goalinterp}

In a similar way, it is also often convenient to interpret a goal by changing
it into an equivalent proposition. The view mechanism of \ssr{} has a
special syntax \C{apply/} for combining simultaneous goal
interpretation operations and
bookkeeping steps in a single tactic.

With the hypotheses of section \ref{ssec:assumpinterp}, the following
script, where \C{\~\~} denotes the boolean negation:
\begin{lstlisting}
  Goal forall a, P ((~~ a) || a).
  move=> a; apply/PQequiv.
\end{lstlisting}
transforms the goal into \C{Q (~~ a)}, and is equivalent to:
\begin{lstlisting}
  Goal forall a, P ((~~ a) || a).
  move=> a; apply: (iffRL (PQequiv _ _)).
\end{lstlisting}
where \C{|*iffLR*|} is the analogous of \C{|*iffRL*|} for the converse
implication.

Any \ssr{} term whose type coerces to a double implication can be used
as a view for goal interpretation.

Note that the goal interpretation view mechanism supports both
\C{apply} and \C{exact} tactics. As expected, a goal interpretation
view command \C{exact/$term$} should solve the current goal or it will
fail.


\emph{Warning} Goal interpretation view tactics are \emph{not} compatible
with the bookkeeping tactical \C{=>} since this would be redundant with
the \C{apply: $\N{term}$=> _} construction.

\subsection{Boolean reflection}\label{ssec:boolrefl}
In the Calculus of Inductive Construction, there is
an obvious distinction between logical propositions and boolean values.
On the one hand, logical propositions are objects
of \emph{sort} \C{Prop} which is the carrier of intuitionistic
reasoning. Logical connectives in \C{Prop} are \emph{types}, which give precise
information on the structure of their proofs; this information is
automatically exploited by \Coq{} tactics. For example, \Coq{} knows that a
proof of \C{A \\/ B} is either a proof of \C{A} or a proof of \C{B}.
The tactics \C{left} and \C{right} change the goal \C{A \\/ B}
to \C{A} and \C{B}, respectively; dualy, the tactic \C{case} reduces the goal
\C{A \\/ B => G} to two subgoals \C{A => G} and \C{B => G}.

On the other hand, \C{bool} is an inductive \emph{datatype}
with two constructors \C{true} and \C{false}.
Logical connectives on \C{bool} are \emph{computable functions}, defined by
their truth tables, using case analysis:
\begin{lstlisting}
  Definition (b1 $\color{red}{||}$ b2) := if b1 then true else b2.
\end{lstlisting}
Properties of such connectives are also established using case
analysis: the tactic \C{by case: b} solves the goal
\begin{lstlisting}
  b || ~~ b = true
\end{lstlisting}
by replacing \C{b} first by \C{true} and then by \C{false}; in either case,
the resulting subgoal reduces by computation to the trivial
\C{true = true}.

Thus, \C{Prop} and \C{bool} are truly complementary: the former
supports robust natural deduction, the latter allows brute-force
evaluation.
\ssr{} supplies
a generic mechanism to have the best of the two worlds and move freely
from a propositional version of a
decidable predicate to its boolean version.

First, booleans are injected into propositions
using the coercion mechanism:
\begin{lstlisting}
  Coercion |*is_true*| (b : bool) := b = true.
\end{lstlisting}
This allows any boolean formula~\C{b} to be used in a context
where \Coq{} would expect a proposition, e.g., after \C{Lemma $\dots$ : }.
It is then interpreted as \C{(is_true b)}, i.e.,
the  proposition \C{b = true}. Coercions are elided by the pretty-printer,
so they are essentially transparent to the user.


\subsection{The \C{reflect} predicate}\label{ssec:reflpred}

To get all the benefits of the boolean reflection, it is in fact
convenient to introduce the following inductive predicate
\C{reflect} to relate propositions and booleans:

\begin{lstlisting}
  Inductive |*reflect*| (P: Prop): bool -> Type :=
    | Reflect_true: P => reflect P true
    | Reflect_false: ~P => reflect P false.
\end{lstlisting}

The statement \C{(reflect P b)} asserts that \C{(is_true b)}
and \C{P} are logically equivalent propositions.

For instance, the following lemma:
\begin{lstlisting}
  Lemma |*andP*|: forall b1 b2, reflect (b1 /\ b2) (b1 && b2).
\end{lstlisting}
relates the boolean conjunction \C{&&} to
the logical one \C{/\\}.
Note that in \C{andP}, \C{b1} and \C{b2} are two boolean variables and
the proposition \C{b1 /\\ b2} hides two coercions.
The conjunction of \C{b1} and \C{b2} can then be viewed
as \C{b1 /\\ b2}  or as \C{b1 && b2}.


Expressing logical equivalences through this family of inductive types
makes possible to take benefit from \emph{rewritable equations}
associated to the case analysis of \Coq{}'s inductive types.

Since the standard equivalence predicate is defined in \Coq{} as:
\begin{lstlisting}
  Definition |*iff*| (A B:Prop) := (A -> B) /\ (B -> A).
\end{lstlisting}
where \C{/\\} is a notation for \C{and}:
\begin{lstlisting}
  Inductive |*and*| (A B:Prop) : Prop :=
    conj : A -> B -> and A B
\end{lstlisting}

This make case analysis very different according to the way an
equivalence property has been defined.


For instance, if we have proved the lemma:
\begin{lstlisting}
  Lemma |*andE*|: forall b1 b2, (b1 /\ b2) <-> (b1 && b2).
\end{lstlisting}
let us compare the respective behaviours of \C{andE} and \C{andP} on a
goal:
\begin{lstlisting}
  Goal forall b1 b2, if (b1 && b2) then b1 else ~~(b1||b2).
\end{lstlisting}

The command:
\begin{lstlisting}
  move=> b1 b2; case (@andE b1 b2).
\end{lstlisting}
generates a single subgoal:
\begin{lstlisting}
  (b1 && b2 -> b1 /\ b2) -> (b1 /\ b2 -> b1 && b2) ->
                   if b1 && b2 then b1 else ~~ (b1 || b2)
\end{lstlisting}

while the command:
\begin{lstlisting}
  move=> b1 b2; case (@andP b1 b2).
\end{lstlisting}
generates two subgoals, respectively \C{b1 /\\ b2 -> b1} and
\C{\~ (b1 /\\ b2) -> \~\~ (b1 || b2)}.



Expressing reflection relation through the \C{reflect} predicate
is hence a very convenient way to deal with classical reasoning, by
case analysis. Using the \C{reflect} predicate allows moreover to
program rich specifications inside
its two constructors, which will be automatically taken into account
during destruction. This formalisation style gives far more
efficient specifications than quantified (double) implications.


A naming convention in \ssr{} is to postfix the name of view lemmas with \C{P}.
For example, \C{orP} relates  \C{||} and \C{\\/}, \C{negP} relates
\C{\~\~} and \C{\~}.

The view mechanism is compatible with \C{reflect} predicates.

For example, the script
\begin{lstlisting}
  Goal forall a b : bool, a -> b -> a /\\ b.
  move=> a b Ha Hb; apply/andP.
\end{lstlisting}
changes the goal \C{a /\\ b} to \C{a && b} (see section \ref{ssec:goalinterp}).

Conversely, the script
\begin{lstlisting}
  Goal forall a b : bool, a /\ b -> a.
  move=> a b; move/andP.
\end{lstlisting}
changes the goal \C{a /\\ b -> a} into \C{a && b -> a} (see section
\ref{ssec:assumpinterp}).


The same tactics can also be used to perform the converse
operation, changing a boolean conjunction into a logical one. The view
mechanism guesses the direction of the
transformation to be used i.e., the constructor of the \C{reflect}
predicate which should be chosen.

\subsection{General mechanism for interpreting goals and assumptions}


\subsubsection*{Specializing assumptions}

The \ssr{}
tactic:
\begin{lstlisting}
  move/(_ $\N{term}_1 \dots \N{term}_n$)
\end{lstlisting}
is equivalent to the tactic:
\begin{lstlisting}
  intro top; generalize (top $\N{term}_1 \dots \N{term}_n$); clear top.
\end{lstlisting}
where \C{top} is a fresh name for introducing the top assumption of
the current goal.

\subsubsection*{Interpreting assumptions}
\label{sssec:hypview}
The general form of an assumption view tactic is:

$$[\C{move}|\C{case}]\C{/}\N{term}_0\C{.}$$

The term $\N{term}_0$, called the \emph{view lemma} can be:
\begin{itemize}
\item a (term coercible to a) function;
\item a (possibly quantified) implication;
\item a (possibly quantified) double implication;
\item a (possibly quantified) instance of the \C{reflect} predicate
  (see section \ref{ssec:reflpred}).
\end{itemize}

Let \C{top} be the top assumption in the goal.

There are three steps in the behaviour of an assumption view tactic:
\begin{itemize}
\item It first introduces \L+top+.
\item If the type of $\N{term}_0$ is neither a double implication nor
  an instance of the \C{reflect} predicate, then the tactic
  automatically generalises a term of the form:
  \begin{lstlisting}
    ($\N{term}_0\ \N{term}_1\ \dots\ \N{term}_n$)
  \end{lstlisting}
  where the terms $\N{term}_1\ \dots\ \N{term}_n$ instantiate the
  possible quantified variables of $\N{term}_0$, in order for
  \C{($\N{term}_0\ \N{term}_1\ \dots\  \N{term}_n$ top)} to be well typed.
\item If the type of $\N{term}_0$ is an equivalence, or
  an instance of the \C{reflect} predicate, it generalises a term of
  the form:
  \begin{lstlisting}
    ($\N{term}_{vh}$ ($\N{term}_0\ \N{term}_1 \dots \N{term}_n$))
  \end{lstlisting}
  where the term $\N{term}_{vh}$ inserted is called an
  \emph{assumption interpretation view hint}.
\item It finally clears \C{top}.
\end{itemize}
For a \C{case/$\N{term}_0$} tactic, the generalisation step is
replaced by a case analysis step.

\emph{View hints} are declared by the user (see section
\ref{ssec:vhints}) and are stored in the \C{Hint View} database.
The proof engine automatically
detects from the shape of the top assumption \C{top} and of the view
lemma $\N{term}_0$ provided to the tactic the appropriate view hint in
the database to be inserted.

If $\N{term}_0$ is a double implication, then the view hint \C{A} will
be one of the defined view hints for implication. These hints are by
default the ones present in the file {\tt ssreflect.v}:
\begin{lstlisting}
  Lemma |*iffLR*| : forall P Q, (P <-> Q) -> P -> Q.
\end{lstlisting}
which transforms a double  implication into the left-to-right one, or:
\begin{lstlisting}
  Lemma |*iffRL*| : forall P Q, (P <-> Q) -> Q -> P.
\end{lstlisting}
which produces the converse implication. In both cases, the two first
\C{Prop} arguments are implicit.

If $\N{term}_0$ is an instance of the \C{reflect} predicate, then \C{A}
will be one of the defined view hints  for the \C{reflect}
predicate,  which are by
default the ones present in the file {\tt ssrbool.v}.
These hints are not only used for choosing the appropriate direction of
the translation, but they also allow complex transformation, involving
negations.
 For instance the hint:
\begin{lstlisting}
  Lemma |*introN*| : forall (P : Prop) (b : bool), reflect P b -> ~ P -> ~~ b.
\end{lstlisting}
makes the following script:
\begin{lstlisting}
  Goal forall a b : bool, a -> b -> ~~ (a && b).
  move=> a b Ha Hb. apply/andP.
\end{lstlisting}
transforms the goal into \C{ \~ (a /\ b)}.
In fact\footnote{The current state of the proof shall be displayed by
  the \C{Show Proof} command of \Coq{} proof mode.}
this last script does not exactly use the hint \C{introN}, but the
more general hint:
\begin{lstlisting}
  Lemma |*introNTF*| : forall (P : Prop) (b c : bool),
      reflect P b -> (if c then ~ P else P) -> ~~ b = c
\end{lstlisting}
The lemma \C{|*introN*|} is an instantiation of \C{introNF} using
 \C{c := true}.

Note that views, being part of $\N{i-pattern}$, can be used to interpret
assertions too. For example the following script asserts \C{a \&\& b}
but actually used its propositional interpretation.
\begin{lstlisting}
  Lemma |*test*| (a b : bool) (pab : b && a) : b.
  have /andP [pa ->] : (a && b) by rewrite andbC.
\end{lstlisting}

\subsubsection*{Interpreting goals}
A goal interpretation view tactic of the form:

$$\C{apply/}\N{term}_0\C{.}$$
applied to a goal \C{top} is interpreted in the following way:
\begin{itemize}
\item If the type of $\N{term}_0$ is not an instance of the
  \C{reflect} predicate, nor an equivalence,
  then the term $\N{term}_0$ is applied to the current goal \C{top},
  possibly inserting implicit arguments.
\item If the type of $\N{term}_0$ is an instance of the \C{reflect}
  predicate or an equivalence, then
a \emph{goal interpretation view hint} can possibly be inserted, which
corresponds to the application of a term
\C{($\N{term}_{vh}$ ($\N{term}_0$ _ $\dots$ _))} to the current
goal, possibly inserting implicit arguments.
\end{itemize}

Like assumption interpretation view hints, goal interpretation ones
are user defined lemmas stored (see section \ref{ssec:vhints}) in the
\C{Hint View} database bridging
the possible gap between the type of $\N{term}_0$ and the type of the
goal.


\subsection{Interpreting equivalences}
Equivalent boolean propositions are simply \emph{equal} boolean terms.
A special construction helps the user to prove boolean equalities by
considering them as logical double implications (between their coerced
versions), while
performing at the same time logical operations on both sides.

The syntax of double views is:
$$\C{apply/}\N{term}_l\C{/}\N{term}_r\C{.}$$

The term $\N{term}_l$ is the view lemma applied to the left hand side of the
equality, $\N{term}_r$ is the one applied to the right hand side.

In this context, the identity view:
\begin{lstlisting}
Lemma |*idP*| : reflect b1 b1.
\end{lstlisting}
is useful, for example the tactic:
\begin{lstlisting}
  apply/idP/idP.
\end{lstlisting}
transforms the goal
\L+~~ (b1 || b2)= b3+
 into two subgoals, respectively
 \L+~~  (b1 || b2) -> b3+ and \\
\L+b3 -> ~~  (b1 || b2).+

The same goal can be decomposed in several ways, and the user may
choose the most convenient interpretation. For instance, the tactic:
\begin{lstlisting}
  apply/norP/idP.
\end{lstlisting}
applied on the same goal \C{\~\~ (b1 || b2)= b3} generates the subgoals
\L+~~  b1 /\ ~~  b2 -> b3+ and\\
\L+b3 -> ~~  b1 /\ ~~  b2+.


\subsection{Declaring new \C{Hint View}s}\label{ssec:vhints}

The database of hints for the view mechanism is extensible via a
dedicated vernacular command. As library {\tt ssrbool.v} already
declares a corpus of hints, this feature is probably useful only for
users who define their own logical connectives. Users can declare
their own hints following the syntax used in {\tt ssrbool.v}:

\begin{lstlisting}
  Hint View for $\N{tactic}$/ $\N{ident}$[|$\N{num}$].
\end{lstlisting}
where \C{$\N{tactic} \in \{$move, apply$\}$}, $\N{ident}$ is the
name of the lemma to be declared as a hint, and $\N{num}$ a natural
number. If \L+move+ is used as $\N{tactic}$, the hint is declared for
assumption interpretation tactics, \L+apply+ declares hints for goal
interpretations.
Goal interpretation view hints are declared for both simple views and
left hand side views. The optional natural number $\N{num}$ is the
number of implicit arguments to be considered for the declared hint
view lemma \C{name_of_the_lemma}.

The command:
\begin{lstlisting}
  Hint View for apply// $\N{ident}$[|$\N{num}$].
\end{lstlisting}
with a double slash \L+//+, declares hint views for right hand sides of
double views.


\noindent See the files {\tt ssreflect.v} and {\tt ssrbool.v} for examples.

\subsection{Multiple views}\label{ssec:multiview}

The hypotheses and the goal can be interpreted applying multiple views in
sequence. Both \C{move} and \C{apply} can be followed by an arbitrary number
of \C{/}$\N{term}_i$. The main difference between the following two tactics
\begin{lstlisting}
  apply/v1/v2/v3.
  apply/v1; apply/v2; apply/v3.
\end{lstlisting}
is that the former applies all the views to the principal goal.
Applying a view with hypotheses generates new goals, and the second line
would apply the view \C{v2} to all the goals generated by \C{apply/v1}.
Note that the NO-OP intro pattern \C{-} can be used to separate two
views, making the two following examples equivalent:
\begin{lstlisting}
  move=> /v1; move=> /v2.
  move=> /v1-/v2.
\end{lstlisting}

The tactic \C{move} can be used together with the \C{in}
tactical to pass a given hypothesis to a lemma. For example, if
\C{P2Q : P -> Q } and \C{Q2R : Q -> R}, the following
tactic turns the hypothesis \C{p : P} into \C{P : R}.
\begin{lstlisting}
  move/P2Q/Q2R in p.
\end{lstlisting}

If the list of views is of length two, \C{Hint View}s for interpreting
equivalences are indeed taken into account, otherwise only single
\C{Hint View}s are used.