Stream: Elpi users & devs

Topic: Proof obligations


view this post on Zulip Enzo Crance (Nov 19 2021 at 13:55):

Hello. Out of curiosity, is there a way for an Elpi command to create proof obligations instead of failing, when some of the required arguments are missing?
Say a command takes 2 arguments: Elpi MyCommand A (f : A -> Prop). and one gives only a type T as first argument, but no second argument. Is there a way to open proof mode to tell the user we need a T -> Prop, instead of failing and saying that on the error channel?

view this post on Zulip Enrico Tassi (Nov 19 2021 at 15:09):

Right now there is no way to open a proof in Elpi. My worry is that then one would like to run some arbitrary code at Qed, and that is not very nice.

view this post on Zulip Paolo Giarrusso (Aug 12 2022 at 19:18):

I'm also curious how hard would this be... without this, in my case I can get by saying sth like:

Lemma foo a b c : FracSplittable_2 (bar a b c).
Proof. ... . Qed.
MyCommand foo.

but this would be a bit nicer:

MyCommand FracSplittable bar.
Proof. ... . Qed.

so the command could generate a type, present proof obligations, and post-process the definition (mostly to derive corollaries and install them as TC instances).

view this post on Zulip Enrico Tassi (Aug 12 2022 at 20:31):

Maybe hooking into the obligations machinery is not too much work, but I'm not a big fan.
Doing it properly with Proof/Qed requires some cleanup on the coq side which has very low priority for me.


Last updated: Feb 04 2023 at 02:03 UTC