The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

The formalization of Relation pointed to here does not explicitly use
setoids, but implicitly uses a distinct notion of equality/equivalence
from Coq's native equality (which might be unnecessary with function
eta-equality added in 8.4) when it formulates theorems such as the
following one in terms of equivalence:

  Theorem rtc_rsc_coincide :
           forall (X:Type) (R: relation X) (x y : X),
      clos_refl_trans R x y <-> refl_step_closure R x y.

What is really being meant here is
   forall X (R : Relation X), equiv_rel (clos_refl_trans R)
(refl_step_closure R).

for the obvious notion of relation equivalence, equipped with which
relations form a setoid.

On Sat, Dec 29, 2012 at 8:57 PM, Kristopher Micinski
<krismicinski AT gmail.com>
 wrote:
> Basically, whenever you start running into problems with coq's intensional
> equality. Coq makes the trade off of intensional equality for decidable type
> checking, but there are always sticky situations where you need more
> elaborate representations, hence setoids.
>
> On Dec 29, 2012 2:49 PM, "Victor Porton" 
> <porton AT narod.ru>
>  wrote:
>>
>> http://www.cs.berkeley.edu/~megacz/coq-categories/ uses setoids.
>>
>> http://www.seas.upenn.edu/~cis500/current/sf/Rel.v does not use setoids.
>>
>> Why these are different with their basic underlining data types?
>>
>> In which cases setoids should be used and in which not?
>>
>> --
>> Victor Porton - http://portonvictor.org