General tips on when to use Prop and when to use bool
I am formalizing a grammar that is essentially one above boolean expressions. In coq, you can get boolean 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 I'm really interested in) I can do a case analysis in the bool domain, but in Prop this is not possible (since all members are not listed, I suppose). The abandonment of these tactics and similar rewriting tactics seems to be a huge disadvantage even for very simple proofs.
In general, in what situations would one choose Prop over bool for formalization? I realize this is a broad question, but I feel it is not detailed enough in the Coq manual. I am interested in real world experiences that people have walked around both routes.
source to share
There are many different opinions on this. My personal concern is that you are often better off not making this choice: it makes sense to have two versions of a property, one in Prop
, the other in bool
.
Why do you need this? As you pointed out, booleans support case analysis in proofs and functions that are not in general sentences. However, Prop
it is more convenient to use in some cases. Suppose you have a T
finite value type. We can write a procedure
all : (T -> bool) -> bool
which decides if P : T -> bool
all elements have a boolean property T
. Imagine that we know that all P = true
for some property P
. We could use this fact to conclude that P x = true
for some value x
. To do this, we need to prove the lemma about all
:
allP : forall P : T -> bool,
all P = true <-> (forall x : T, P x = true)
This lemma connects two different formulations of the same property: Boolean and propositional. When reasoning about all
in proof, we can refer to allP
to convert freely between them. We can also have various lexical transformations:
allPn : forall P,
all P = false <-> (exists x, P x = false)
In fact, we can choose any Coq clause that refers to a boolean computation (how long, of course, since we can prove the two are logically equivalent). For example, if we want to have a proper induction principle associated with a Boolean property, we can look for an equivalent formulation as an inductively defined sentence.
The Math Components library is a good example of the development that follows this style. Indeed, because it is so prevalent there, the library provides a dedicated presentation engine for writing lexical translations like the ones above and applying them. In plain Coq, we can also use tactics rewrite
to make logical equivalence more convenient.
Of course, there are many situations where it makes no sense to have two formulations of the same property. Sometimes you are forced to use Prop
because the property you care about is insoluble. Sometimes you may feel like you won’t gain anything by writing your property in Prop
and keep it just as logical.
In addition to the Software Foundations chapter above, this answer discusses the difference between bool
and in Prop
more detail.
source to share