coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: David Pereira <dpereira AT liacc.up.pt>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Well-founded induction over finite sets
- Date: Fri, 22 Oct 2010 18:46:08 +0100
Dear all,
I am trying to do some proofs about well-founded relations over finite sets,
and I am a bit lost.
In particular, what I need is to prove that the proper inclusion on elements
of the powerset of a set [s] is a well-founded relation.
Do any of you know of a Coq implementation that deals with this kind of
proofs, or any other Coq code dealign with well-founded relations on finite
sets that I can use as documentation?
Thanks in advance.
David.
- [Coq-Club] Well-founded induction over finite sets, David Pereira
- Re: [Coq-Club] Well-founded induction over finite sets, Stéphane Lescuyer
- [Coq-Club] Dirty feature request,
AUGER Cedric
- Re: [Coq-Club] Dirty feature request, Greg Morrisett
- Re: [Coq-Club] Dirty feature request,
Randy Pollack
- Re: [Coq-Club] Dirty feature request, AUGER Cedric
- Re: [Coq-Club] Dirty feature request, Jeff Vaughan
Archive powered by MhonArc 2.6.16.