The Coq mailing list

[(e6fa90e88c%hidden_head%e6fa90e88c)Carlos.SIMPSON(e6fa90e88c%hidden_at%e6fa90e88c)unice.fr(e6fa90e88c%hidden_end%e6fa90e88c)]

Dear Christian Doczkal,
  I did something like this. See the files at the top of the
page 
http://math.unice.fr/~carlos/themes/verif.html

The project is explained in some preprints and papers:

---Explaining Gabriel-Zisman localization to the computer 
Journal of Automated Reasoning,  Volume 36 number 3
(2006), 259 - 285

---Files for Gabriel-Zisman localization , arXiv:math/0506470 

---Set-theoretical mathematics in Coq , arXiv:math/0402336

A more in-depth study has recently been done by Jose Grimm, see:
J. Grimm, 
Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory 
of Sets,
HAL : inria-00408143, version 2

---Carlos Simpson
http://hal.archives-ouvertes.fr/inria-00408143/
 

Selon Christian Doczkal 
<(e6fa90e88c%hidden_head%e6fa90e88c)doczkal(e6fa90e88c%hidden_at%e6fa90e88c)ps.uni-sb.de(e6fa90e88c%hidden_end%e6fa90e88c)>:

> Hello
> 
> I'm planning some development with uses sets in various places and my
> (preliminary) experience is that the Sets libraries that ship with Coq
> are somewhat cumbersome to work with. 
> 
> Has anyone used this for some (larger) development? I'm not overly
> worried about having to assume classical logic and various
> extensionality axioms. I'm more interested in increased automation for
> the set reasoning part.
> 
> The tactic "eauto with sets" only works in relatively few cases, even
> after including Finete_sets_faacts which in turn exports almost about
> the whole library on sets.
> 
> (Notation is also not an issue, this I have taken care of)
> 
> -- 
> Regards
> Christian Doczkal
> 
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>