Is there any means of converting Prop to bool? I know that forall a b : nat, a <? b -> a < b, but is this thing is valid at all: forall a b: nat, a < b -> a <? b? If not, are there any restrictions I should add, to make this real? And, for other operators that have both Prop and bool counterparts, can they be converted in such way?
Is there a strong relation with bools and Prop in Coq?
Viewed 75
1 Answers
Having a relation between a predicate in Prop and one in bool means that the property in question is decidable. Basically you have a function which decides if the property is true or false.
This is not the case for all propositions (unless you assume some principle that entails it) but does hold for <? and <.
This relation is usually crystallised thanks to the reflect predicate.
Inductive reflect (P : Prop) : bool -> Set :=
| ReflectT : P -> reflect P true
| ReflectF : ~ P -> reflect P false.
In your case you have
Nat.ltb_spec0: forall x y : nat, reflect (x < y) (x <? y)
I encourage you to look it up.
Related