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?

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.

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

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 22 2024 at 04:02 UTC