The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 2 Nov 2012 20:20:43 +0100,
AUGER Cédric 
<sedrikov AT gmail.com>
 a écrit :

> Honestly, I would really like to have some strong meta-language,
> allowing me to be able to define "deriving classes" in Coq (something
> a little like "deriving" command in Haskell datatypes).
> 
> Then I could imagine some definitions like:
> 
> Meta eq_dec (i : mutual_inductive) (l : list string) : function :=
>  <Here put your code like you would do in Ocaml plugins>
> .
> (* generates a decision procedure for equality *)
> 
> Inductive bool : Set := True | False
> ; deriving eq_dec ["bool_eq_dec"].
> 
> >>
> bool_eq_dec : forall (b b0 : bool), {b = b0} + {b <> b0}.
> <<
> 
> Inductive nat : Set := O | S : nat -> nat
> : deriving eq_dec ["nat_eq_dec"], induction ["nat_eq_ind"]
> >>
> nat_eq_dec : forall (n n0 : nat), {n = n0} + {n <> n0}
> nat_induction : forall (P : nat -> Prop),
>                 P O -> (forall n, P n -> P (S n)) ->
>                 forall n, P n
> <<
> 
> Record Arrow (A B : Set) : Set := { fun : A -> B }
> ; deriving eq_dec ["Arrow_eq_dec"].
> >>
> Failure <the error message you would have put by defining it, since
> you cannot define such a function in Coq>
> <<
> 
> Inductive lex_ord: A*B -> A*B -> Prop :=
>    | lex_ord_left: forall a1 b1 a2 b2,
>        ordA a1 a2 -> lex_ord (a1,b1) (a2,b2)
>    | lex_ord_right: forall a b1 b2,
>        ordB b1 b2 -> lex_ord (a,b1) (a,b2)
> ; deriving inversion.
> >>
> lex_ord_inv_1 : A*B -> A*B -> Type
> lex_ord_inv_2 : A*B -> A*B -> Type
> lex_ord_inv_t : A*B -> A*B -> Prop
> lex_ord_inv : forall (p p0 : A*B), lex_ord p p0 -> lex_ord_inv_t p p0
> <<
> 
> Print lex_ord_inv_1, lex_ord_inv_2, lex_ord_inv_t.
> >>
> Record lex_ord_inv_1 (p p0 : A * B) : Type :=
>   { lex_ord_inv_1_a1 : A
>   ; lex_ord_inv_1_b1 : B
>   ; lex_ord_inv_1_a2 : A
>   ; lex_ord_inv_1_b2 : B
>   ; lex_ord_inv_1_o : ordA lex_ord_inv_1_a1 lex_ord_inv_1_a2
>   ; lex_ord_inv_1_link_p : p = (lex_ord_inv_1_a1, lex_ord_inv_1_b1)
>   ; lex_ord_inv_1_link_p0 : p0 = (lex_ord_inv_1_a2, lex_ord_inv_1_b2)
>   }.
> Record lex_ord_inv_2 (p p0 : A * B) : Type :=
>   { lex_ord_inv_2_a : A
>   ; lex_ord_inv_2_b1 : B
>   ; lex_ord_inv_2_b2 : B
>   ; lex_ord_inv_2_o : ordB lex_ord_inv_2_b1 lex_ord_inv_2_b2
>   ; lex_ord_inv_2_link_p : p = (lex_ord_inv_2_a, lex_ord_inv_2_b1)
>   ; lex_ord_inv_2_link_p0 : p0 = (lex_ord_inv_2_a, lex_ord_inv_2_b2)
>   }.
> Inductive lex_ord_inv_t (p p0 : A * B) : Prop :=
>   | lex_ord_inv_t_1 : lex_ord_inv_1 p p0 -> lex_ord_inv_t p p0
>   | lex_ord_inv_t_2 : lex_ord_inv_2 p p0 -> lex_ord_inv_t p p0.
> <<
> 
> With such features, you could have full control of what terms are
> generated by Coq. For instance, you may not wish to auto-generate
> "bool_rec" "bool_rect" "bool_ind" as it is yet the case (I know there
> is some special directive to avoid this dummy generation, something
> like "Unset Induction Scheme" or some similar name), and you could
> define serialization like "deriving Show/deriving Read" in Haskell, as
> well as decidable equality (well there is the "decide equality
> tactic", but you still have to write down the name and the type of
> this function, plus call the tactic).

Hush, I recently saw in the documentation that there is some similar
stuff in Coq.
(coq/html/refman/Reference-Manual015.html)

But you only have it for Equality, Inversion and Induction.

For me there still lacks the ability to manipulate directly coq ASTs
inside Coq (in a less restricted language of course which you can only
use to generate terms, not to prove anything; in particular, you may
not requiring termination proofs; if an infinite loop occurs, then it
is your fault, like when you apply non terminating tactic scripts, and
the system still remains safe).

For the documentation, I think the index of Commands is not really
handy as you have commands indexed under Set only (Set Elimination
Schemes for instance), or under both Set and Unset (most of the cases).
I think that it is somewhat redundant, having a single "Unset <flag>
(see Set <flag>)" would avoid this redundancy.

On my trunk version, "Set Equality Schemes." does not do anything, but
"Set Equality Scheme." (remove the final 's') does. It generates only
boolean equality though, not the decidable equality (unlike "Scheme
Equality <some_inductive>".). I think it would be better to always have
an 's' at the end of these commands for names consistency.

This is also a sad thing that "Equality" generation relies on induction
principles, as that means that "Unset Elimination Schemes." conflicts
with "Scheme Equality <some_inductive>." (which may explain why "Set
Equality Scheme." does not produce the "eq_dec" part, the "beq"
generation remaining compatible as it does not use induction
principles).