The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

One of the easiest way to prove that a relation is well-founded, when
possible, is to relate it to the natural order on integers.
In your case, the proper inclusion relation is such that

forall s s', s \subset s' -> cardinal s < cardinal s'

and by using the lemma Arith.Wf_nat.well_founded_lt_compat in standard
library you get the wellfounded proof you needed.

If you need examples of definitions by wellfounded induction in
general, you can take a look at the Function command in the ref
manual.

Stéphane L.

On Fri, Oct 22, 2010 at 7:46 PM, David Pereira 
<dpereira AT liacc.up.pt>
 wrote:
> 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.
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06