HintDbを検査するCoq方式を実装することは可能ですか？もしそうなら、どうですか？

Question

たとえば、与えられたHintDb内のすべての解決ヒントを反復する方法と、解決ヒントhのそれぞれについて、pose h.を実行します。これは可能ですか？もしそうなら、どうですか？

Answer 1

Coqでは、shelveでファンシーなことをしてバックトラックしない限り、そうではありませんが、OCamlではかなり簡単です。たとえば、Fiatプロジェクトでは、そのような戦術があります。コック8.7の場合：

hint_db_extra_tactics.mlで

：

hint_db_extra_plugin.ml4で

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.mllibで

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

：HintDbExtra.vで

Hint_db_extra_tactics 
Hint_db_extra_plugin 

：

0問題文の中で提起された例を解決するために、これを使用し

、我々は追加することができます。

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

を実行したい場合ヒントデータベースのヒントごとに戦術（成功するヒントが見つかるまで、ヒントごとに戦術を連続して実行するのではなく）を変更することができます。何らかの並べ替え演算子（例えば、tclTHEN）へのwith_hint_dbの。