Tutorial on the new proof engine for ML tactic writers
======================================================

Starting from Coq 8.5, a new proof engine has been introduced, replacing the old
meta-based engine which had a lot of drawbacks, ranging from expressivity to
soundness, the major one being that the type of tactics was transparent. This
was pervasively abused and made virtually impossible to tweak the implementation
of the engine.

The old engine is deprecated and is slowly getting removed from the source code.

The new engine relies on a monadic API defined in the `Proofview` module. Helper
functions and higher-level operations are defined in the `Tacmach` and
`Tacticals` modules, and end-user tactics are defined amongst other in the
`Tactics` module.

At the root of the engine is a representation of proofs as partial terms that
can contain typed holes, called evars, short for *existential variable*. An evar
is essentially defined by its context and return type, that we will write
`?e : [Γ ⊢ _ : A]`. An evar `?e` must be applied to a substitution `σ` of type
`Γ` (i.e. a list of terms) to produce a term of type `A`, which is done by
applying `EConstr.mkEvar`, and which we will write `?e{σ}`.

The engine monad features a notion of global state called `evar_map`, defined in
the `Evd` module, which is the structure containing the incremental refinement
of evars. `Evd` is a low-level API and its use is discouraged in favour of the
`Evarutil` module which provides more abstract primitives.

In addition to this state, the monad also features a goal state, that is
an ordered list of current holes to be filled. While these holes are referred
to as goals at a high-enough level, they are actually no more than evars. The
API provided to deal with these holes can be found in the `Proofview.Goal`
module. Tactics are naturally operating on several goals at once, so that it is
usual to use the `Proofview.Goal.enter` function and its variants to dispatch a
tactic to each of the goals under focus.

Primitive tactics by term refining
-------------------------------------

A typical low-level tactic will be defined by plugging partial terms in the
goal holes thanks to the `Refine` module, and in particular to the
`Refine.refine` primitive.

```ocaml
val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic
(** In [refine typecheck t], [t] is a term with holes under some
    [evar_map] context. The term [t] is used as a partial solution
    for the current goal (refine is a goal-dependent tactic), the
    new holes created by [t] become the new subgoals. Exceptions
    raised during the interpretation of [t] are caught and result in
    tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)
```

In a first approximation, we can think of `'a Sigma.run` as
`evar_map -> 'a * evar_map`. What the function does is first evaluate the
`Constr.t Sigma.run` argument in the current proof state, and then use the
resulting term as a filler for the proof under focus. All evars that have been
created by the invocation of this thunk are then turned into new goals added in
the order of their creation.

To see how we can use it, let us have a look at an idealized example, the `cut`
tactic. Assuming `X` is a type, `cut X` fills the current goal `[Γ ⊢ _ : A]`
with a term `let x : X := ?e2{Γ} in ?e1{Γ} x` where `x` is a fresh variable and
`?e1 : [Γ ⊢ _ : X -> A]` and `?e2 : [Γ ⊢ _ : X]`. The current goal is solved and
two new holes `[e1, e2]` are added to the goal state in this order.

```ocaml
let cut c =
  let open Sigma in
  Proofview.Goal.nf_enter { enter = begin fun gl ->
    (** In this block, we focus on one goal at a time indicated by gl *)
    let env = Proofview.Goal.env gl in
    (** Get the context of the goal, essentially [Γ] *)
    let concl = Proofview.Goal.concl gl in
    (** Get the conclusion [A] of the goal *)
    let hyps = Tacmach.New.pf_ids_of_hyps gl in
    (** List of hypotheses from the context of the goal *)
    let id = Namegen.next_name_away Anonymous hyps in
    (** Generate a fresh identifier *)
    let t = mkArrow c (Vars.lift 1 concl) in
    (** Build [X -> A]. Note the lifting of [A] due to being on the right hand
        side of the arrow. *)
    Refine.refine { run = begin fun sigma ->
      (** All evars generated by this block will be added as goals *)
      let Sigma (f, sigma, p) = Evarutil.new_evar env sigma t in
      (** Generate ?e1 : [Γ ⊢ _ : X -> A], add it to sigma, and return the
          term [f := Γ ⊢ ?e1{Γ} : X -> A] with the updated sigma. The identity
          substitution for [Γ] is extracted from the [env] argument, so that
          one must be careful to pass the correct context here in order for the
          resulting term to be well-typed. The [p] return value is a proof term
          used to enforce sigma monotonicity. *)
      let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c in
      (** Generate ?e2 : [Γ ⊢ _ : X] in sigma and return
          [x := Γ ⊢ ?e2{Γ} : X]. *)
      let r = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 r, [|mkRel 1|])) in
      (** Build [r := Γ ⊢ let id : X := ?e2{Γ} in ?e1{Γ} id : A] *)
      Sigma (r, sigma, p +> q)
      (** Fills the current hole with [r]. The [p +> q] thingy ensures
          monotonicity of sigma. *)
    end }
  end }
```

The `Evarutil.new_evar` function is the preferred way to generate evars in
tactics. It returns a ready-to-use term, so that one does not have to call
the `mkEvar` primitive. There are lower-level variants whose use is dedicated to
special use cases, *e.g.* whenever one wants a non-identity substitution. One
should take care to call it with the proper `env` argument so that the evar
and term it generates make sense in the context they will be plugged in.

For the sake of completeness, the old engine was relying on the `Tacmach.refine`
function to provide a similar feature. Nonetheless, it was using untyped metas
instead of evars, so that it had to mangle the argument term to actually produce
the term that would be put into the hole. For instance, to work around the
untypedness, some metas had to be coerced with a cast to enforce their type,
otherwise leading to runtime errors. This was working for very simple
instances, but was unreliable for everything else.

High-level composition of tactics
------------------------------------

It is possible to combine low-level refinement tactics to create more powerful
abstractions. While it was the standard way of doing things in the old engine
to overcome its technical limitations (namely that one was forced to go through
a limited set of derivation rules), it is recommended to generate proofs as
much as possible by refining in ML tactics when it is possible and easy enough.
Indeed, this prevents dependence on fragile constructions such as unification.

Obviously, it does not forbid the use of tacticals to mimick what one would do
in Ltac. Each Ltac primitive has a corresponding ML counterpart with simple
semantics. A list of such tacticals can be found in the `Tacticals` module. Most
of them are a porting of the tacticals from the old engine to the new one, so
that if they share the same name they are expected to have the same semantics.