Stream: Elpi users & devs

Topic: Generating proof terms containing Ltac

Enzo Crance (Jan 23 2023 at 08:44):

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?

Paolo Giarrusso (Jan 23 2023 at 09:01):

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,

Paolo Giarrusso (Jan 23 2023 at 09:02):

(taken from https://github.com/bedrocksystems/BRiCk/blob/5d27b524ce67385708371edaf471ebff2d4d97c4/theories/prelude/elpi/derive/finite.v)

Paolo Giarrusso (Jan 23 2023 at 09:10):

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

Enrico Tassi (Jan 23 2023 at 09:27):

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).

Paolo Giarrusso (Jan 23 2023 at 09:33):

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: Oct 13 2024 at 01:02 UTC