The Coq mailing list

["Vincent Siles" <vsiles AT lix.polytechnique.fr>]

>> Quoting Babak Moazzez 
>>Â <babakmoazzez AT yahoo.com>:
>>
>> > Hi.
>> >
>> > I am trying to define a function in Coq that adds two lists
>> > together. for this purpose , I need to use a structure which is
>> > very familiar in any programming language:
>> >
>> > if (p=q) then do ....
>> >
>> > but in Coq I cannot use this since (p=q) is not a boolean value
>> > but just a proposition which needs to be proved if it is true.
>> >
>> > Can anybody tell me what to do?
>
> For these purpouse, I think coq lacks some meta-programming features:
> it would be very nice to have meta-types:
> boolean_equality: forall (T: fully-computationnal-type), T -> T -> bool
> boolean_equality_to_eq
> : forall (T: fully-computationnal-type) (a b: T),
>   if boolean_equality a b then a = b else a <> b
>
There is a simple way to do this for a lot of inductive types (but as you
said, it is a really difficult problem to make a solution for all
fully-computationnal types) with the "Scheme Equality" command:
http://coq.inria.fr/refman/Reference-Manual011.html#@command220


Coq < Scheme Equality for nat.
nat_beq is defined
nat_eq_dec is defined

Coq < Check nat_beq.
nat_beq
     : nat -> nat -> bool

Coq < Check nat_eq_dec.
nat_eq_dec
     : forall n m : nat, {n = m} + {n <> m}

It also work for some inductive types with parameter:

Coq < Scheme Equality for list.
list_beq is defined
list_eq_dec is defined

Coq < Check list_beq.
list_beq
     : forall A : Type, (A -> A -> bool) -> list A -> list A -> bool

In this case, the equality on lists of A ask for an decidable equality on A.
list_eq_dec also depend on "A_dec_eq" style hypothesis.

This solution works for a large range of simple inductive types, and most
of the data structure we use in common programming. But it may fail if the
structure of the inductive type is to complex.

Best regards,
Vincent Siles
Phd student - Ecole Polytechnique