Stream: Coq users

Topic: Call a Ltac tactic in a vernac command?


view this post on Zulip Chantal Keller (Apr 20 2021 at 14:34):

Hello
Is there a way to call a Ltac tactic in a vernac command? I would like to do something like:

Foo bar.

which first applies a Ltac tactic on bar returning bar', then applies a vernacular command (written in OCaml) on bar'.
Thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Apr 20 2021 at 16:51):

Hi @Chantal Keller , if you are willing to use >= 8.13 and to write you command on OCaml too, you can use the Declare.Proof.start API, then call the tactic, see the docs https://coq.github.io/doc/master/api/coq-core/Declare/Proof/index.html

That will give you the "proof state", which is required for tactics to run; then you have Declare.Proof.by and some other helpers. But indeed, it is unfortunately a quite heavy operation these days yet, in particular tactics can do a lot of stuff [universes, side-effect constants, etc...] that you need to reconcile after the tactic has ran; we are trying to much improve the API so hopefully something like Coq 8.15 feels a much better to use.

view this post on Zulip Chantal Keller (Apr 21 2021 at 07:02):

Thank you Emilio. So there is a way to get in OCaml a tactic written in Ltac and to apply it?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2021 at 11:43):

Yup, you should be able to do ltac -> Proofview.tactic so you can use Declare.Proof.by , what's the provenance of the ltac snippet?


Last updated: Mar 29 2024 at 12:02 UTC