Есть ли сильная связь с bools и Prop в Coq?

Question

Есть ли какие-либо средства для преобразования Prop в bool? Я знаю, что forall a b : nat, a <? b -> a < b, но действительно ли это вообще так: forall a b: nat, a < b -> a <? b? Если нет, есть ли какие-то ограничения, которые я должен добавить, чтобы это стало реальностью? И для других операторов, которые имеют как Prop, так и bool аналоги, могут ли они быть преобразованы таким образом?

Answer 1

Наличие отношения между предикатом в Prop и одним в bool означает, что рассматриваемое свойство является разрешимым . По сути, у вас есть функция, которая решает, является ли свойство true или false.

. Это не относится ко всем предложениям (если вы не предполагаете какой-то принцип, который влечет за собой это), но действительно для <? и <. Это отношение обычно кристаллизуется благодаря предикату reflect.

Inductive reflect (P : Prop) : bool -> Set :=
| ReflectT : P -> reflect P true 
| ReflectF : ~ P -> reflect P false.

В вашем случае у вас есть

Nat.ltb_spec0: forall x y : nat, reflect (x < y) (x <? y)

Я призываю вас посмотреть его.