Enzo Crance (Nov 19 2021 at 13:55): 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?
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.
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).
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: Oct 13 2024 at 01:02 UTC