Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Well-founded induction over finite sets

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Well-founded induction over finite sets


chronological Thread 
  • 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.



Archive powered by MhonArc 2.6.16.

Top of Page