The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

Hi, Eddy --

I have been writing a plugin that builds a representation of kernel terms as a Coq datatype.

https://github.com/gmalecha/template-coq

To make it reasonable, I have syntax like:

Quote Definition d'' := Eval compute in id_nat.

which constructs a top-level definition, [d''], that has the syntax of id_nat. The code calls a function called [declare_definition] which I borrowed from the containers library:

https://github.com/gmalecha/template-coq/blob/master/src/reify.ml4#L555

That might be helpful to you.

On Tue, Oct 21, 2014 at 1:16 PM, Eddy Westbrook <westbrook AT kestrel.edu> wrote:

Hi,

Thanks for the reply. Yes, I saw VERNAC COMMAND EXTEND in some of the plugins, and was going to start looking into it. Good to know that the syntax is changing, though!

As for what I am trying to do, I am trying to capture some of the deductive synthesis tool we use here at Kestrel in Coq. To do this, I was hoping to start by making a notation to capture the ideas for constructing type classes from the paper “Type Classes for Mathematics in Type Theory” by Spitters and der Weegen: something like the Class command with the record syntax, except that a helper typeclass is created (with a unique name) for each predicative component. (Maybe this would also require some notation to indicate which components are meant to be in Prop?) In addition to this, I would also like this notation to create a meta-level description, which is an element of a type I have defined that describes the typeclass.

I was thinking something like this:

Spec Group :=
  G : Type;
  zero : G;
  plus : G -> G -> G;
  inv : G -> G;
  plus_assoc : forall x y z, plus x (plus y z) = plus (plus x y) z;
  zero_id : forall x, plus x zero = x;
  inv_zero : forall x, plus x (inv x) = zero
}.

This would be equivalent to the following top-level declarations:

Class Group_G : Type := { G : Type }.
Class Group_zero `{Group_G} : Type := { zero : G -> G -> G }.
Class Group_plus `{Group_zero} : Type := { plus : G -> G -> G }.
Class Group_inv `{Group_plus} : Type := { inv : G -> G }.
Class Group `{Group_inv} : Prop := { plus_assoc : …; ... }
Definition Group_spec_descr : SpecDescr := … (* and element of the inductive type SpecDescr generated from the above *)

Is this sort of thing do-able? Any pointers on this would be very helpful.

Thanks,
-Eddy

On Oct 20, 2014, at 10:48 AM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

> On 20/10/2014 19:38, Eddy Westbrook wrote:
>> I am interested in adding my own top-level declaration forms, like
>> “Program Definition” and “Functional Scheme”, which generate
>> obligations and/or add definitions to the current section / module.
>> Is there any documentation on how to do this? Presumably, I could
>> define such a thing as a separate ML module that could be loaded into
>> Coq, without modifying the Coq source itself. I have been looking a
>> little at the plugins/ directory for some examples, but it would be
>> much easier to wade through that code with a little bit of guidance.
>
> For the definition of an extra command, you need to use the VERNAC
> COMMAND EXTEND macro in a ml4 file. According to the version of Coq you
> are using (i.e. up to 8.4 included vs. trunk), the exact syntax of this
> macro differs. You should look at ml4 files containing such macros to
> grasp the idea. The tactics/extratactics.ml4 file may be a good start.
>
> For the adding definition part, it may be rather complicated, depending
> on the precise use case you have in mind. Maybe you could share some
> details on this list?
>
> PMP
>

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/