coq - 是否可以实施检查 HintDb 的 Coq 策略？如果是这样，怎么做？

Question

例如，我想要一种策略，它会遍历给定 HintDb 中的所有解析提示，并且对于每个解析提示h，它会执行一个pose h.. 这可能吗？如果是这样，怎么做？

Answer 1

在 Coq 中，没有（除非您使用shelve和回溯做一些花哨的事情），但在 OCaml 中它非常简单。比如在菲亚特项目中，我们就有这样的战术。对于 Coq 8.7：

在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

在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;;

在hint_db_extra_plugin.mllib：

Hint_db_extra_tactics
Hint_db_extra_plugin

在HintDbExtra.v：

Declare ML Module "hint_db_extra_plugin".

使用它来解决问题陈述中提出的示例，我们可以添加：

在_CoqProject：

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

在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.

如果您想对提示数据库中的每个提示运行一个策略（而不是连续对每个提示运行一个策略，直到找到一个成功的提示），您可以将tclORELSEin更改with_hint_db为某种排序运算符（例如，tclTHEN）。