Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Sets in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Sets in Coq


chronological Thread 
  • From: Vladimir Voevodsky <(e6fa90e88c%hidden_head%e6fa90e88c)vladimir(e6fa90e88c%hidden_at%e6fa90e88c)ias.edu(e6fa90e88c%hidden_end%e6fa90e88c)>
  • To: Christian Doczkal <(e6fa90e88c%hidden_head%e6fa90e88c)doczkal(e6fa90e88c%hidden_at%e6fa90e88c)ps.uni-sb.de(e6fa90e88c%hidden_end%e6fa90e88c)>
  • Cc: "'Coq Club'" <(e6fa90e88c%hidden_head%e6fa90e88c)coq-club(e6fa90e88c%hidden_at%e6fa90e88c)pauillac.inria.fr(e6fa90e88c%hidden_end%e6fa90e88c)>
  • Subject: Re: [Coq-Club] Sets in Coq
  • Date: Wed, 9 Dec 2009 12:04:19 -0500
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

In my opinion the type "Set" in Coq is redundant.  So if you plan to develop 
such a library it is much more useful to do it for Type.

Vladimir. 






On Dec 9, 2009, at 10:46 AM, Christian Doczkal wrote:

> 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





Archive powered by MhonArc 2.6.16.

Top of Page