CODEWITHSUNDEEP
coqcoq-tactic
Abhishek Kr Singh
Abhishek Kr Singh

Reputation: 99

The exact definition of an in built Tactic (case, destruct, inversion etc.) in Coq

How can one see the exact implementation of an in-built tactic in Coq ? More specifically is there an alternative to Print Ltac <user-defined-tactics> which works for locating the exact definition of in-built Tactics in Coq ?

Upvotes: 1

Views: 122

Answers (1)

Jason Gross
Jason Gross

Reputation: 6128

No, there is no alternative to Print Ltac. In part, this is because the built-in tactics are implemented in OCaml, and the parts they are made of aren't always expressible in terms of more primitive tactics in Ltac (and almost never would such a translation be exact). The only way I know to find the definitions is to go source-diving. If you search for, e.g., "destruct", you will find in plugins/ltac/g_tactic.ml4 the lines

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

which says that destruct gets parsed as the atomic tactic node TacInductionDestruct. Searching for TacInductionDestruct gives an implementation in 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

You can find the implementation of Tactics.induction_destruct in tactics/tactics.ml.

Most primitive tactics start in one of two ways: either there is an entry in g_tactic.ml4 which says how to parse that tactic as an atomic tactic node, or there is a TACTIC EXTEND somewhere, e.g., for revert, we have in plugins/ltac/coretactics.ml4

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

If the definition is as a node in the Ltac AST, then the place to look is tacinterp.ml, which describes how to interpret those tactics. Either way, you can continue chasing down OCaml definitions to see how tactics are implemented.

Upvotes: 5

Related Questions