Stream: Elpi users & devs

Topic: Generating proof terms containing Ltac


view this post on Zulip 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?

view this post on Zulip 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,

view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 09:02):

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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: Apr 14 2024 at 11:02 UTC