The Coq mailing list

[e AT x80.org (Emilio Jesús Gallego Arias)]

Hi Kenneth,

Kenneth Roe 
<kendroe AT hotmail.com>
 writes:

> I would like to create a Coq command that introduces a proof
> environment.  I would like to create a command "rewrite_rule" that
> takes three parameters (A,B,C).  This rule should create a proof
> obligation (A -> B=C).  As an example I would like to the user the
> rule in the following manner:
>
> rewrite_rule (mem(a,(b::c))) (mem(a,c)) (not(a=b)).
> Proof. simps. reflexivity. Qed.
>
> My starting point in the ml-plugin is to have this declaration for the 
> command:
>
>
> VERNAC COMMAND EXTEND AR
> | [ "rewrite_rule" constr(left) constr(right) constr(cone)] -> [ 
> Stuff.rewrite_rule left right conditions ]
> END
>
> What should the shell of the implementation look like?

Indeed, this is a delicate operation to implement due to the need to
inform Coq that your command will start a proof. So you have to take
care of two things:

- parsing:

  In `VERNAC EXTEND` you must pass a "classifier" that tells Coq that
  the command is going to open a proof. The way to do this is:

`VERNAC COMMAND EXTEND Foo CLASSIFIED BY classify_foo`

where `classify_foo` is for example:

`let classify_foo _ = Vernacexpr.(VtStartProof 
("Classic",GuaranteeOpacity,list_of_ids), VtLater)`

That should do the job in 8.7, but this interface is likely to change
soon [sorry for that], ping us on Gitter if you have further question.

If you are in 8.8, I recommend using the new:

`VERNAC COMMAND FUNCTIONAL EXTEND` declaration
[see examples in the source code]

- On the actual implementation side, you must use `start_proof` and
  friends. Unfortunately there are several functions called
  `start_proof`, different on the level of "side-effects" they perform,
  I think you should be good with the one in `Lemmas`.

Best,
E.