Searching for exact matches#

In this step, we’re going to build a first version of the tactic that uses the Search machinery to look for lemmas that apply could use. This first version will be restricted to only showing theorems that match our conclusion exactly.

Getting the conclusion#

The first step is to obtain the conclusion of the current goal. There are several ways to do this, but the simplest one is to use the pattern-matching syntax match%rocq goal with:

Tutorial.v#
3Camltac Module ApplySearch := ocaml:{{
4  let run () =
5    match%rocq goal with
6    | _, {| ?conclusion |} ->
7      search conclusion
8}}.

Here, the wildcard _ means that hypotheses are not matched on.

Creating a search pattern#

Our conclusion is a constr, but the search command expects a pattern instead. So, we’ll convert our term to a pattern using Patternops.pattern_of_constr:

Tutorial.v#
 3Camltac Module ApplySearch := ocaml:{{
 4  let run () =
 5    match%rocq goal with
 6    | _, {| ?conclusion |} ->
 7      let* env = Tactic.env in
 8      let* sigma = Tactic.sigma in
 9      let pattern = Patternops.pattern_of_constr env sigma conclusion in
10      search env sigma pattern
11}}.

Notice how we’re now taking two additional arguments:

  • env is the environment, of type Environ.env, that map identifiers and variables to their declaration.

  • sigma, of type Evd.evar_map, is the evar map that map existential variables to their definition.

Searching for applicable lemmas#

Now, we perform the search using Rocq APIs by calling the Search.search_pattern function:

Tutorial.v#
 3Camltac Module ApplySearch := ocaml:{{
 4  let search env sigma pattern =
 5    let results = ref [] in
 6    let collect_result res _ _ _ _ = results := res :: !results in
 7    Search.search_pattern env sigma pattern (SearchOutside []) collect_result;
 8    !results
 9
10  (* … *)
11}}.

We also need to be able to print our results:

Tutorial.v#
10  (* … *)
11
12  let print_results = function
13    | [] -> Feedback.msg_info (Pp.str "No theorem could be applied.")
14    | results ->
15       let open Pp in
16       let pr_ref ref = Libnames.pr_path (Ltac2.Env.path ref) in
17       let pp = List.fold_left
18         (fun acc res -> acc ++ fnl () ++ pr_ref res)
19         (str "Try this: ") results in
20       Feedback.msg_info pp
21
22  (* … *)

Notice how we used the Ltac2.Env.path function from Ltac2; in Camltac, you can freely mix Ltac2 functions with Rocq ones.

Putting everything together#

Your Tutorial.v file should look like the following:

Tutorial.v#
 1Require Import Camltac.Camltac.
 2
 3Camltac Module ApplySearch := ocaml:{{
 4  let search env sigma pattern =
 5    let results = ref [] in
 6    let collect_result res _ _ _ _ = results := res :: !results in
 7    Search.search_pattern env sigma pattern (SearchOutside []) collect_result;
 8    !results
 9
10  let print_results = function
11    | [] -> Feedback.msg_info (Pp.str "No theorem could be applied.")
12    | results ->
13       let open Pp in
14       let pr_ref ref = Libnames.pr_path (Ltac2.Env.path ref) in
15       let pp = List.fold_left
16         (fun acc res -> acc ++ fnl () ++ pr_ref res)
17         (str "Try this: ") results in
18       Feedback.msg_info pp
19
20  let run () =
21    match%rocq goal with
22    | _, {| ?conclusion |} ->
23      let* env = Tactic.env in
24      let* sigma = Tactic.sigma in
25      let pattern = Patternops.pattern_of_constr env sigma conclusion in
26      print_results (search env sigma pattern);
27      return ()
28}}.

By this point, you should be able to step over the module definition without any error.

To check what we wrote, we can test this version in a small proof script:

From Stdlib Require List.
Open Scope list_scope.


forall (A : Type) (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

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

  apply List.app_inv_head.
Qed.