Using the tactic from Ltac2

So far, we had to use Camltac Eval to evaluate our tactic inside a proof. Another alternative would be to declare our tactic as an Ltac2 tactic, so that existing proof scripts could use it more easily.

Registering the tactic to Ltac2

We can create an Ltac2 tactic from a Camltac tactic by using the FFI module:

Tutorial.v

(* … *)

Camltac Run ocaml:{{
  Ltac2.FFI.(define "apply_search"
    (unit @-> tac unit)
    ApplySearch.run)
}}.

The unit @-> tac unit specifies the type to the Ltac2 FFI from OCaml.

We must also register our tactic on the Ltac2 side to be able to call it directly by name:

Tutorial.v

Require Import Ltac2.Ltac2.

Ltac2 @external apply_search : unit -> unit :=
  "rocq-camltac.plugin.runtime" "apply_search".

Calling the tactic

We can now directly call the tactic from Ltac2:

Goal forall A (x y z : list A),
  x ++ y = x ++ z -> y = z.
forall (A : Type) (x y z : list A), x ++ y = x ++ z -> y = z
Proof.
forall (A : Type) (x y z : list A), x ++ y = x ++ z -> y = z
  intros A x y z.
A: Type
x, y, z: list A
x ++ y = x ++ z -> y = z
  apply_search ().
Try this: 
Stdlib.Lists.List.app_inv_head
A: Type
x, y, z: list A
x ++ y = x ++ z -> y = z

Using Ltac2 notations, we can even obtain the original apply? syntax:

Ltac2 Notation "apply?" := apply_search ().

Goal forall A (x y z : list A),
  x ++ y = x ++ z -> y = z.
forall (A : Type) (x y z : list A), x ++ y = x ++ z -> y = z
Proof.
forall (A : Type) (x y z : list A), x ++ y = x ++ z -> y = z
  intros A x y z.
A: Type
x, y, z: list A
x ++ y = x ++ z -> y = z
  apply?.
Try this: 
Stdlib.Lists.List.app_inv_head
A: Type
x, y, z: list A
x ++ y = x ++ z -> y = z