1 files changed, 133 insertions, 0 deletions
diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md
new file mode 100644
index 00000000..8f96ac22
--- /dev/null
+++ b/dev/doc/proof-engine.md
@@ -0,0 +1,133 @@
+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.