Prop_or_Set - coq/coq GitHub Wiki
Prop vs Set
There are several philosophies to follow to help you decide whether to make your type in Prop or in Set
How Many Objects Per Type Philosophy
If your type could have two or more distinguishable objects, put it in Set
otherwise put it in Prop
. In Coq (without additional axioms) extensionally equivalent functions are indistinguishable. According to this philosophy (lt a b)
should be in Prop
because there can be only one proof that a < b
for natural numbers. For (constructive) real number a < b
should be in Set
because in this case there are multiple proofs that a < b
. Indeed the (constructive) logarithm function, ln(x)
, requires a proof that 0 < x
to be in Set because the logarithm function requires a (constructive) proof that its argument is positive to operate. See the online documentation and publications for C-CoRN, which uses a special type CProp
for computationally meaningful propositions.
The basis of this philosophy is that an object from a type with at most one object contributes no information, and therefore may safely be removed during program extraction.
A consequence of this philosophy is that or
should never be used because A \/ B
could have two objects even if A
and B
both only have at most one object. Instead, use {A} + {B}
. Similar considerations apply to exists
; use {x : T | P}
instead. See ExistsConsideredHarmful.
Exists: from Prop to Set
Even if the existence of an object in Prop doesn't give a witness, we can write an algorithm to find it for some types. The main difficulty is to prove to Coq that the algorithm is correct and will terminate because we know that such a witness exists.
See ExistsFromPropToSet.