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?
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:
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
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).