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
However, when I parse
intro. I get the following result:
((Kername (MPfile (DirPath ((Id Notations) (Id Init) (Id Coq))))
(DirPath ()) (Id intro_#_4C69D577))
destruct H, I get:
(TacInductionDestruct false false
The resulted S-expressions show those tactics are not denoted by
What is the difference between the tactic denoted by
qualid in S-expression and those not denoted by
I am trying to find more tactics denoted by
quliad in Serapi, but I still have not find another.
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.
I know there are some tactics denoted by
That is not correct.
destruct are defined in
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
Ltac lia := Zify.zify; xlia zchecker. For example,
Lia.lia instead of just
From Coq Require Import Lia.
Goal forall n m, n + m = m + n.
Ltac also lets you override existing tactics, for example this redefines
split to print
Ltac split := idtac "xx".
Goal True /\ False.
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.
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
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.