Hello. I am trying to generate a record of proofs, with the ones further down in the record depending on the first ones. It means all of them must be clean proof terms because they appear in goals of the next fields, except the last proof.

It would be easier for me to generate the Ltac code for this last field instead of a Coq term, because it is starting to be too big to be able to easily infer how to generalise things just looking at the Coq term.

Is it possible to generate such things as an `ltac:(...)`

Coq term with Coq-Elpi, and give the whole Elpi term back to Coq with `coq.env.add-const`

?

AFAICT, you can call typecheck on terms with holes by representing the holes as elpi variables, then turn those holes into goals. Here's an incomplete snippet from code we wrote:

```
std.assert-ok! (coq.elaborate-skeleton {{ NoDup lp:{{ECtorList}} }} _ ETyNoDup) "[mk-finite] [TyNoDup]",
std.assert-ok! (coq.typecheck {{ lp:{{BoNoDup}} : lp:{{ETyNoDup}} }} _) "typechecking [NoDup] failed",
coq.ltac.collect-goals BoNoDup [SealedGoalNoDup] [],
coq.ltac.open (coq.ltac.call "solve_finite_nodup" []) SealedGoalNoDup [],
@using! "Type" =>
coq.env.add-const {calc (InstanceName ^ "_subproof_nodup")} BoNoDup ETyNoDup @opaque! CNoDup,
```

I hope that helps at least as a list of pointers; many of these APIs are explained in the tactic tutorial, even if the above is used in a command: https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_tactic.html

That is indeed the right way. I believe this bridge between commands and tactics is not explained in the tutorials, but I should mention it (I believe it was not available or tested back then).

ah, I learned it from my colleagues — who must have learned it from https://coq.zulipchat.com/#narrow/stream/253928-Elpi-users-.26-devs/topic/.E2.9C.94.20Generating.20terms.20via.20ltac.20in.20an.20.5BElpi.20Command.5D

Last updated: Apr 14 2024 at 11:02 UTC