coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [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.