The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Le 4 nov. 2011 à 18:46, Victor Porton a écrit :

> I am studying Coq and maybe now may attempt a practical exercise of writing 
> some theories.
> 
> I noticed that the Coq approach is to use setoids. In my opinion, it is 
> silly and contrary to what we do in informal mathematics.

Maybe informal mathematics is too informal? Logical equivalence is larger 
than propositional equality in Coq, just like isomorphism of types is not
equality of types.

> On the other hand we have a ZF(C) formalization:
> See a .tar file with the theory at:
> http://arxiv.ccsd.cnrs.fr/e-print/math/0402336v1
> from the article:
> http://arxiv.ccsd.cnrs.fr/abs/math/0402336v1

At the time this paper was written, support for reasoning with <-> was 
minimal,
but it is now much more easy to use. As they say, it would be more faithful to
use <-> instead of = for propositions, and now you can.

-- Matthieu