Coq 中内置策略（case、destruct、inversion 等）的确切定义

Question

如何才能看到 Coq 中内置策略的具体实现？更具体地说，是否有替代方法Print Ltac <user-defined-tactics>可以在 Coq 中查找内置策略的确切定义？

Answer 1

不，没有其他选择Print Ltac。在某种程度上，这是因为内置策略是在 OCaml 中实现的，并且它们组成的部分并不总是可以用 Ltac 中更原始的策略来表达（而且这样的翻译几乎永远不会准确）。我知道找到定义的唯一方法是进行源头挖掘。如果您搜索，例如，您会在以下行"destruct"中找到plugins/ltac/g_tactic.ml4

  | IDENT "destruct"; icl = induction_clause_list ->
  TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(false,false,icl))

这表示它destruct被解析为原子策略节点TacInductionDestruct。搜索TacInductionDestruct给出了一个实现plugins/ltac/tacinterp.ml：

  (* Derived basic tactics *)
  | TacInductionDestruct (isrec,ev,(l,el)) ->
      (* spiwack: some unknown part of destruct needs the goal to be
         prenormalised. *)
      Proofview.Goal.nf_enter begin fun gl ->
        let env = Proofview.Goal.env gl in
        let sigma = project gl in
        let sigma,l =
          List.fold_left_map begin fun sigma (c,(ipato,ipats),cls) ->
            (* TODO: move sigma as a side-effect *)
             (* spiwack: the [*p] variants are for printing *)
            let cp = c in
            let c = interp_destruction_arg ist gl c in
            let ipato = interp_intro_pattern_naming_option ist env sigma ipato in
            let ipatsp = ipats in
            let sigma,ipats = interp_or_and_intro_pattern_option ist env sigma ipats in
            let cls = Option.map (interp_clause ist env sigma) cls in
            sigma,((c,(ipato,ipats),cls),(cp,(ipato,ipatsp),cls))
          end sigma l
        in
        let l,lp = List.split l in
        let sigma,el =
          Option.fold_left_map (interp_open_constr_with_bindings ist env) sigma el in
        Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
        (name_atomic ~env
          (TacInductionDestruct(isrec,ev,(lp,el)))
            (Tactics.induction_destruct isrec ev (l,el)))
      end

Tactics.induction_destruct您可以在 中找到 的实现tactics/tactics.ml。

大多数原始策略以两种方式之一开始：要么有一个条目，其中g_tactic.ml4说明如何将该策略解析为原子策略节点，要么有某个TACTIC EXTEND地方，例如 for revert，我们在plugins/ltac/coretactics.ml4

TACTIC EXTEND revert
  [ "revert" ne_hyp_list(hl) ] -> [ Tactics.revert hl ]
END

如果定义是 Ltac AST 中的一个节点，那么要查找的位置是tacinterp.ml，它描述了如何解释这些策略。无论哪种方式，您都可以继续追踪 OCaml 定义以了解策略是如何实施的。