Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • From: St�phane Lescuyer <stephane.lescuyer AT inria.fr>
  • To: David Pereira <dpereira AT liacc.up.pt>
  • Cc: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Well-founded induction over finite sets
  • Date: Sat, 23 Oct 2010 00:51:22 +0200

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




Archive powered by MhonArc 2.6.16.

Top of Page