The Coq mailing list

["John L. Singleton" <jsinglet AT gmail.com>]

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