The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I think the general answer is that bools can convey information, Props 
can't.  Props are most useful for expressing invariants, while bools are 
data.

This distinction is important in two places: within proofs and in 
extraction results.  Within proofs, if Props are used, they can be case 
analyzed, but only when the conclusion is itself a Prop (or when the 
Prop being case analyzed is not potentially informative, as when it has 
zero or one constructor with no informative fields).  Bools have no such 
case analysis restrictions.

For extraction, the fact that Props can't convey information is used by 
Coq to erase all Props.  This is very useful when one wishes to generate 
code (such as OCaml code) from Coq definitions such that the generated 
code does not carry any "proof burden" in terms of resource-consuming 
activity that does not alter the definition's external behavior.  Such 
proof burden can be prohibitively high if not erased.  Note, however, 
that if Coq had a much better extraction erasure algorithm (as in, for 
example, Idris), one could potentially get the same extraction behavior 
using bools instead of Props.

My advice is that if you are formalizing software in Coq, especially 
with the goal of extraction, then use Props for invariants.  Even when 
you don't have the goal of extraction, it is often useful to have an 
enforced separation between data and invariants as a way to make your 
intentions clearer.

-- Jonathan


On 06/21/2017 01:18 PM, John L. Singleton wrote:
> I posted the following question on Stackoverflow: 
> https://stackoverflow.com/questions/44638724/general-advice-about-when-to-use-prop-and-when-to-use-bool/
>
> On the suggestion of one of the commenters I am also asking this question 
> here.
>   
> I am formalizing a grammar which is essentially one over boolean expressions. In Coq, you can get boolean-like things in Prop or more explicitly in bool.
>
> So for example, I could write:
>
> true && true
>
> Or
>
> True /\ True
>
> The problem is that in proofs (which is what I really care about) I can do a 
> case analysis in domain bool, but in Prop this is not possible (since all 
> members are not enumerable, I suppose). Giving up this tactic and similar 
> rewriting tactics seems like a huge drawback even for very simple proofs.
>
> In general, what situations would one choose Prop over bool for formalizing? 
> I realize this is a broad question, but I feel like this is not addressed in 
> the Coq manual sufficiently. I am interested in real world experience people 
> have had going down both routes.
>
> Thanks,
> JLS