coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "John Wiegley" <johnw AT newartisans.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Need help with Finite proof involving existentials
Date: Wed, 03 Aug 2016 10:28:35 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f44.google.com
Ironport-phdr: 9a23:5Wcb2RNr7jX5EgVEuLol6mtUPXoX/o7sNwtQ0KIMzox0KP/+rarrMEGX3/hxlliBBdydsKMczbqO+Pm5ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd+KyZTvnLnro9X6WEZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq4QTLpCDT1gPXpmytfssEyJbwyP4DMjU2gZlhdZSUCR7hb6WIjZtCblv/Bh2TKTO9awRrcxD2fxp5x3QQPl3X9UfwUy93va35R9
Organization: New Artisans LLC

For any who were following along, with Jason Gross' help I was able to get the
proof through, which states that mapping over a Finite set results in a Finite
set:

https://github.com/jwiegley/notes/blob/master/Map.v

The trick was to hinge the proof on the Surjectivity of such mappings.

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

Re: [Coq-Club] Need help with Finite proof involving existentials, John Wiegley, 08/01/2016
- Re: [Coq-Club] Need help with Finite proof involving existentials, Jason Gross, 08/01/2016
- <Possible follow-up(s)>
- Re: [Coq-Club] Need help with Finite proof involving existentials, John Wiegley, 08/03/2016