coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] General Advice about When to Use Prop and When to use bool

From: "John Wiegley" <johnw AT newartisans.com>
To: "John L. Singleton" <jsinglet AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] General Advice about When to Use Prop and When to use bool
Date: Wed, 21 Jun 2017 10:26:12 -0700
Authentication-results: mail3-smtp-sop.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-pg0-f46.google.com
Ironport-phdr: 9a23:tCKE5RRpC1VNtXMVwlsu1rW859psv+yvbD5Q0YIujvd0So/mwa6yZxyN2/xhgRfzUJnB7Loc0qyN4v+mATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZbF/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0ligIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRBDI2icoUADeQPPeFboYnzqVQBogexCBKwBO/z0DJEmmP60Lcm3+knDArI3BYgH9ULsHnMotn7MKASUeCzzKLVzTrDbu1Z2Tj56IfWchEtr+yHULVyccrWyUkvEQ3Eg06WqYP7MTKazP4Ns3Sa7+p7T+2vjXUnpxttrTiow8chk4/EjZ8bxFDD8CV22oc1JdugRU59f9GlHoFftzuGN4t3WcMtWWdouD0gxrIavp67eS4Hw4kkyR7Hc/GKcYeF7gj+WOqPITp0nnFodbylixu98EWs0u/xW8iu3FpUoCdIncPAu3EJ2hDJ98SKRf9w80G80jiVzQ/T8PtLIUUsmKrbNZEhxrkwm4IWsUvZHy/2nFz6jLeZdkk44+So5evqb7T8qp+TMI90jQ7+MqAwlcClHes4NQ0OU3Ca+eS6yrLj4VX0TbdFg/Esj6XVrpDXKd4Yq6O3GQNY3Ycu5w66Dzi80dQYmXcHLEhCeBKCl4XpOV/PIPHmAvewh1SjjjdqyuvJPr3kGJrNL3zDnK39crZ67k5Q0BAzwsxH55JIFrEBJ+r+VVP2tNzBFxM2Lwi0w/v8B9hmzYMfWWePAreDP6/IsF+I4PgvI+iWa4MPtjb9Matt2/m7x10+mVlVWe/h5poRZ3S1AvNgaQ3NY2HthNgFHHsisQ83Teisg1qHB219fXG3Cuge4TE9QL2nAIjHS5HnyOiD2ye9AbVQa39PEEyNCn7ubMOPXPJaO3HaGdNojjFRDevpcIQmzxz78Vaik7c=
Organization: New Artisans LLC

>>>>> "JLS" == John L Singleton
>>>>> <jsinglet AT gmail.com>
>>>>> writes:

JLS> In general, what situations would one choose Prop over bool for
JLS> formalizing? I realize this is a broad question, but I feel like this is
JLS> not addressed in the Coq manual sufficiently. I am interested in real
JLS> world experience people have had going down both routes.

One thing you can do is both, and then write a theory (perhaps using the
[reflect] type) to go between the two representations. There are always times
when one or the other is needed.

Btw, this is a general philosophy of the ssreflect library, which makes this
type of duality very natural to express and make use of.

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

[Coq-Club] General Advice about When to Use Prop and When to use bool, John L. Singleton, 06/21/2017
- Re: [Coq-Club] General Advice about When to Use Prop and When to use bool, John Wiegley, 06/21/2017
- Re: [Coq-Club] General Advice about When to Use Prop and When to use bool, Jonathan Leivent, 06/21/2017