м вид новичка в Coq.I '

Я пытаюсь реализовать универсальную версию сортировки вставки. Я'Я реализую как модуль, который принимает Comparator в качестве параметра. Этот Comparator реализует операторы сравнения (такие как is_eq, is_le, is_neq и т. Д.).

В сортировке вставки, чтобы вставить, я должен сравнить два элемента в списке ввода, и, основываясь на результате сравнения, вставить элемент в правильное местоположение.

Моя проблема в том, что реализации операторов сравненияtype -> type -> prop (Мне нужно, чтобы они были такими для реализации других типов / доказательств). Я'не хочу создаватьtype -> type -> bool версии операторов, если этого можно избежать.

Есть ли способ конвертироватьTrue | False опора для bool для использования вif ... then ... else статья?

Тип модуля сравнения:

Module Type ComparatorSig.

  Parameter X: Set.
  Parameter is_eq : X -> X -> Prop.
  Parameter is_le : X -> X -> Prop.
  Parameter is_neq :  X -> X -> Prop.

  Infix "=" := is_eq (at level 70).
  Infix "" := (~ is_eq) (at level 70).
  Infix "