coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Need help with Finite proof involving existentials

From: "John Wiegley" <johnw AT newartisans.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Need help with Finite proof involving existentials
Date: Wed, 27 Jul 2016 16:49:05 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=johnw AT newartisans.com; spf=None smtp.mailfrom=johnw AT newartisans.com; spf=None smtp.helo=postmaster AT Maia.local
Ironport-phdr: 9a23:IIPaKBMC4/tvtPctD5Al6mtUPXoX/o7sNwtQ0KIMzox0KP/4rarrMEGX3/hxlliBBdydsKMczbSI+Pi8EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuS9aU0Zr8j7z60qaQSj0AvCC6b7J2IUf+hiTqne5Sv7FfLL0swADCuHpCdrce72ppIVWOg0S0vZ/or9YwuxhX7vkm7otLVbjwV6U+V71RSjo8YE4v48i+/zvETQ3H2XoRXWEbg1AAVwrC7BfldpH8rSLgqutm0S+Be8bxSOZnCnyZ8653RUqw2288PDkj/TSPhw==
Organization: New Artisans LLC

Hello,

Can anyone help me with the following goal:

A : Type
B : Type
f : A -> B -> B
r : Ensemble (A * B)
Finite0 : Finite (A * B) r
============================
Finite (A * B) (fun x : A * B => exists b : B, In (A * B) r (fst x, b))

It would seem that "finitude" must carry, since the goal does not add any
elements, but I am having difficulties with the existential variable. Is
there any way to proceed?

Thank you,
--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[Coq-Club] Need help with Finite proof involving existentials, John Wiegley, 07/27/2016
- Re: [Coq-Club] Need help with Finite proof involving existentials, Frédéric Besson, 07/28/2016
  - Re: [Coq-Club] Need help with Finite proof involving existentials, Jason Gross, 07/28/2016