The Coq mailing list

[Claudio Sacerdoti Coen <sacerdot AT cs.unibo.it>]

 Hi,

> I need to add inductives predicates defined within sort Set as morphisms 
> but as
> we saw below this is not possible using the cvs version of Coq
> How can we solve that?

 the problem is not that you cannot define predicates of type Set as
 morphisms, but that you cannot define them as relations (setoids).
 Indeed, the solution would be to declare eqSet as a setoid, but this is
 not accepted by Coq since it is not a Coq relation (i.e. it does not have
 type T -> T -> Prop for some T).

 The latter limitation is hard-coded in the current reflexive implementation
 of the tactic. Simply replacing relation with a suitable relationT
 predicate in the Coq source does not work because of contravariance issues
 in the typing relation and renaming of hypotheses by tactics.

 I am investigating whether these issues can be solved, but this will
 require a bit of time.

                                        Regards,
                                        C.S.C.


-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail: 
sacerdot AT cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------