Я новичок в Coq.

Я пытаюсь реализовать универсальную версию сортировки вставки. Я реализую это как модуль, который принимает 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 "<=" := is_le (at level 70).

  Parameter eqDec : forall x y : X, { x = y } + { x <> y }.

  Axiom is_le_trans : forall (x y z:X), is_le x y -> is_le y z -> is_le x z.

End ComparatorSig.

Реализация для натуральных чисел:

Module IntComparator <: Comparator.ComparatorSig.
  Definition X := nat.
  Definition is_le x y := x <= y.
  Definition is_eq x y := eq_nat x y.
  Definition is_neq x y:= ~ is_eq  x y.

  Definition eqDec := eq_nat_dec.

  Definition is_le_trans := le_trans.
End IntComparator.

Часть вставки сортировки вставки:

  Fixpoint insert (x : IntComparator .X) (l : list IntComparator .X) :=
    match l with
      | nil => x :: nil
      | h :: tl => if IntComparator.is_le x h then x :: h :: tl else h :: (insert x tl)
    end.

(очевидно, точка фиксации вставки не работает, поскольку is_le возвращает Prop, а не bool).

Любая помощь приветствуется.