coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about inhabited

From: "John Wiegley" <johnw AT newartisans.com>
To: Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Question about inhabited
Date: Fri, 28 Apr 2017 22:38:59 -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:tRM5CB/B9GrEDf9uRHKM819IXTAuvvDOBiVQ1KB31e8cTK2v8tzYMVDF4r011RmSDNmds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2e2//5Lebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiCgZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsaS2RfQ8heVSJPAoS/YYsBAeUOMvpXoYbmqlsStBuzHxWgCP/1xzJKgHL9wK000/4mEQHDxAEsEdYAsHPUrNXzKawdUeG1w7fHzTXHcfxX2Tnx45XPfxAjpvGMXbRwcMTKxEkpCQzEgE+fqZb5PzOUzeQCqW6b7/F6We2zjG4nrhh8rz6yzckijYnJg5gaylHC9ShhxoY6O9O5R1RhYd64EZtQrDuVN41tQs84X25ovyM6xqUHuZ69ZigKyY4oywTRa/yddYWD/xHtVP6JLDtmmH5ofKizihWy/ES61OHwS8q53ExFoydKitXBtHEA2wbN5sWJRfZx5Eas1DKV2wzO5exJJUY5nrfBJZE72L4/jJ8TvFzDHiDonEX2i7ebdkA+9eip7+Tre7Lmpp6AO4NthAHzPasjltawAeQ/NQgOUGyb9vqm2LL/+k35Ra1GjvwwkqbHrJDXPdoXqrK9DgNP0Ysu6wyzAym73Nkbh3UKI11IdAqCj4fzOlHOJP74De24g1SpiDprxf7HPrz/DZXCKnjMjrfgcK1y605Z0gUzzNRf64hIBbEGJfL/QlXxu8DADh8lLwy0xP7qB8l61oMHQG6AHquZML7JvlKT/eIuI+yMZJcPtzrnKvgl4eTujX4jllMHc6mpx8hfVHftMf1rP0yfKVXtht0MC3tC6gU3QfDjjhuNUDpZamyud686/XQ/GYWgS4nZENODmruEiW2ZGZ1QLl9HB1+IHGaiP9GGXPcKdwqUL9BoiCAFTrGnUMkq0hT451yy8KZuMueBon5QjpnkztUgorSLzRw=
Organization: New Artisans LLC

>>>>> "GG" == Gaetan Gilbert
>>>>> <gaetan.gilbert AT ens-lyon.fr>
>>>>> writes:

GG> It's a reformulation of functional choice (as defined in
GG>
https://coq.inria.fr/library/Coq.Logic.ChoiceFacts.html#FunctionalChoice),proof
GG> in attached file.

Thank you, Gaëtan, that worked nicely. I just had to include another module:

Require Import Coq.Logic.ClassicalChoice.
Require Import Coq.Logic.ChoiceFacts.

Lemma inhabited_forall' : inhabited_forall.
Proof.
apply choice_to_inhab.
apply non_dep_dep_functional_choice.
repeat intro.
apply choice, H.
Qed.

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

[Coq-Club] Question about inhabited, John Wiegley, 04/28/2017
- Re: [Coq-Club] Question about inhabited, Gaetan Gilbert, 04/28/2017
  - Re: [Coq-Club] Question about inhabited, John Wiegley, 04/29/2017