Parsing Tactics via SerAPI

Using Coq
1

I am trying to use SerAPI to parse tactics and find useful information from the S-expressions.
I notice if I parse split, I will get the following sentence in S-expresssion:

(((v (Ser_Qualid (DirPath ()) (Id split)))

This line seems indicates split is denoted by qualid

However, when I parse intro. I get the following result:

       ((Kername (MPfile (DirPath ((Id Notations) (Id Init) (Id Coq))))
         (DirPath ()) (Id intro_#_4C69D577))

When parse destruct H, I get:

       (TacInductionDestruct false false

The resulted S-expressions show those tactics are not denoted by qualid.

What is the difference between the tactic denoted by qualid in S-expression and those not denoted by quliad?

I am trying to find more tactics denoted by quliad in Serapi, but I still have not find another.

2

Wasn’t the conclusion last time that split is not denoted by qualid? For destruct, that would be even stranger, since “destruct” alone isn’t a valid tactic.

1 Like
3

I know there are some tactics denoted by qualid like split and destruct.

That is not correct. split and destruct are defined in coretactics.mlg.

Except for those tactics extended by users, do all of such tactics are written in the file “coretactics.mlg”?

Built in tactics are defined under the simple_tactic nonterminal in g_tactic.mlg. In addition, anything in the *.mlg files between TACTIC EXTEND and END is added to simple_tactic. There are a considerable number in extratactics.mlg and, as you noticed, corestactics.mlg. Some of them are in optionally-loaded plugins, such as SSR.

“tactics extended by users” is a little vague. It could refer to tactics added in plugins using OCaml code or with Ltac. Syntactically, you can refer to an Ltac-defined tactic with a qualid, although I suspect that that’s not commonly done. lia is an Ltac tactic defined in Lia.v as Ltac lia := Zify.zify; xlia zchecker. For example, Lia.lia instead of just lia here:

From Coq Require Import Lia.
Goal forall n m, n + m = m + n.
Proof.
  Lia.lia.
Qed.

Ltac also lets you override existing tactics, for example this redefines split to print xx instead:

Ltac split := idtac "xx".
Goal True /\ False.
split.

It would help to give more context to your question–if you’re trying to understand the Coq code or thinking about creating a tool there are other details worth mentioning.

2 Likes
5

Thanks for your help! Sorry for my unclear question. I do not know my question is so complicated and have modified my original question to make it clear

6

No worries. Since SerAPI is a plugin that’s not currently in the Coq code base, that’s essential context. However, I don’t know much SerAPI. I haven’t used it. Perhaps someone else can help you.

7

@ZWY when you say SerAPI, do you mean Serapi_protocol (coq-serapi.Serapi.Serapi_protocol) ?