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?
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.