The Coq mailing list

[David Delahaye <delahaye AT cs.chalmers.se>]

    Hello,

> I am trying to write a tactic ``Group'' similar to ``Ring'' for
> (non abelian) groups.  I use the following definition for groups:
>
>   Record Group : Type := {
>     the_group :> Type;
>     op : the_group -> the_group -> the_group;
>     idt : the_group;
>     inv : the_group -> the_group;
>     group_assoc : (x,y,z: the_group) (op x (op y z))==(op (op x y) z);
>     group_l_idt : (x: the_group) (op idt x) == x;
>     group_r_idt : (x: the_group) (op x idt) == x;
>     group_l_inv : (x: the_group) (op (inv x) x) == idt;
>     group_r_inv : (x: the_group) (op x (inv x)) == idt
>   }.
>
> My idea was to imitate the example given in the Coq manual for the
> tactic Quote [8.6 Quote].  The problem is that I would like to use
> Quote for term of type Group, but Quote can be applied only to the
> goal.
>
> My question is: can I do it directly in Coq without using OCaml?

    Quotation functions can now be completely written using the "new" toplevel
tactic language (of versions V7). So, this can be done in Coq without using
Ocaml, neither the tactic Quote (which becomes a bit obsolete). Your idea,
which consists in imitating Ring, seems to be good, but actually you try to
imitate the "wrong" tactic and, in particular, the code of the tactic Field
(for commutative fields) might be of some interests for you. Field is also a
reflexive tactic, but it has been coded using only the tactic language and, as
can be expected, the quotation function takes a term to be reflected as an
argument. The corresponding code is available in file Field_Tactic.v (in
directory ./contrib/field, relative to the root directory of Coq sources).

    I hope this helps.

    David.

---------------------------------------
David Delahaye, 
delahaye AT cs.chalmers.se
http://www.cs.chalmers.se/~delahaye/