Is is possible to implement a Coq tactic that inspects a HintDb? If so, how?

Question

For example, I would like a tactic that would iterate over all the resolve hints in a given HintDb and for each resolve hint h, it would do a pose h. . Is this possible? If so, how?

Jason Gross Jason Gross · Accepted Answer · 2017-10-02T05:13:14

In Coq, there is not (unless you do fancy things with shelve and backtracking), but it is pretty straightforward in OCaml. For example, in the Fiat project, we have such tactics. For Coq 8.7:

In hint_db_extra_tactics.ml:

module WITH_DB =
  struct
    open Tacticals.New
    open Names
    open Ltac_plugin

  (* [tac] : string representing identifier *)
  (* [args] : tactic arguments *)
  (* [ltac_lcall] : Build a tactic expression calling a variable let-bound to a tactic == [F] args *)
  let ltac_lcall tac args =
    Tacexpr.TacArg(Loc.tag @@ Tacexpr.TacCall(Loc.tag @@ (Misctypes.ArgVar(Loc.tag @@ Names.Id.of_string tac),args)))

  (* [ltac_letin] : Build a let tactic expression. let x := e1 in e2 *)
  let ltac_letin (x, e1) e2 =
    Tacexpr.TacLetIn(false,[(Loc.tag @@ Names.Id.of_string x),e1],e2)

  (* [ltac_apply] : Run a tactic with arguments... *)
  let ltac_apply (f: Tacinterp.Value.t) (arg:Tacinterp.Value.t) =
    let open Geninterp in
    let ist = Tacinterp.default_ist () in
    let id = Id.of_string "X" in
    let idf = Id.of_string "F" in
    let ist = { ist with Tacinterp.lfun = Id.Map.add idf f (Id.Map.add id arg ist.lfun) } in
    let arg = Tacexpr.Reference (Misctypes.ArgVar (Loc.tag id)) in
    Tacinterp.eval_tactic_ist ist
      (ltac_lcall "F" [arg])

  (* Lift a constructor to an ltac value. *)
  let to_ltac_val c = Tacinterp.Value.of_constr c

  let with_hint_db dbs tacK =
    let open Proofview.Notations in
    (* [dbs] : list of hint databases *)
    (* [tacK] : tactic to run on a hint *)
    Proofview.Goal.nf_enter begin
        fun gl ->
        let syms = ref [] in
        let _ =
          List.iter (fun l ->
                     (* Fetch the searchtable from the database*)
                     let db = Hints.searchtable_map l in
                     (* iterate over the hint database, pulling the hint *)
                     (* list out for each. *)
                     Hints.Hint_db.iter (fun _ _ hintlist ->
                                         syms := hintlist::!syms) db) dbs in
        (* Now iterate over the list of list of hints, *)
        List.fold_left
          (fun tac hints ->
           List.fold_left
             (fun tac (hint : Hints.full_hint) ->
              let hint1 = hint.Hints.code in
              Hints.run_hint hint1
                       (fun hint2 ->
                              (* match the type of the hint to pull out the lemma *)
                              match hint2 with
                                Hints.Give_exact ((lem, _, _) , _)
                              | Hints.Res_pf ((lem, _, _) , _)
                              | Hints.ERes_pf ((lem, _, _) , _) ->
                                 let this_tac = ltac_apply tacK (Tacinterp.Value.of_constr lem) in
                                 tclORELSE this_tac tac
                              | _ -> tac))
             tac hints)
          (tclFAIL 0 (Pp.str "No applicable tactic!")) !syms
      end

  let add_resolve_to_db lem db =
    let open Proofview.Notations in
    Proofview.Goal.nf_enter begin
        fun gl ->
        let _ = Hints.add_hints true db (Hints.HintsResolveEntry [({ Vernacexpr.hint_priority = Some 1 ; Vernacexpr.hint_pattern = None },false,true,Hints.PathAny,lem)]) in
        tclIDTAC
      end

end

In hint_db_extra_plugin.ml4:

open Hint_db_extra_tactics
open Stdarg
open Ltac_plugin
open Tacarg

DECLARE PLUGIN "hint_db_extra_plugin"

TACTIC EXTEND foreach_db
  | [ "foreach" "[" ne_preident_list(l) "]" "run" tactic(k) ]  ->
     [ WITH_DB.with_hint_db l k ]
       END

TACTIC EXTEND addto_db
  | [ "add" constr(name) "to" ne_preident_list(l) ]  ->
     [ WITH_DB.add_resolve_to_db (Hints.IsConstr (name, Univ.ContextSet.empty)) l]
       END;;

In hint_db_extra_plugin.mllib:

Hint_db_extra_tactics
Hint_db_extra_plugin

In HintDbExtra.v:

Declare ML Module "hint_db_extra_plugin".

Using this to solve the example posed in the problem statement, we can add:

In _CoqProject:

-R . Example
-I .
HintDbExtra.v
PoseDb.v
hint_db_extra_plugin.ml4
hint_db_extra_plugin.mllib
hint_db_extra_tactics.ml

In PoseDb.v:

Require Import HintDbExtra.

Ltac unique_pose v :=
  lazymatch goal with
  | [ H := v |- _ ] => fail
  | _ => pose v
  end.

Goal True.
  repeat foreach [ core ] run unique_pose.

If you want to run a tactic on each hint in the hint database (rather than running a tactic on each hint in succession, until you find one that succeeds), you can change the tclORELSE in with_hint_db to some sort of sequencing operator (e.g., tclTHEN).

Is is possible to implement a Coq tactic that inspects a HintDb? If so, how?

1 Answers