proof-engine.md

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.

val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> 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. *)

What the function does is first evaluate the t 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.

let cut c =
  Proofview.Goal.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 begin fun sigma ->
      (** All evars generated by this block will be added as goals *)
      let sigma, f = 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 = 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] *)
    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 mimic 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.