Soy algo nuevo en Coq.

Estoy tratando de implementar una versión genérica de ordenación por inserción. Estoy implementando es como un módulo que toma un comparador como parámetro. Este comparador implementa operadores de comparación (como is_eq, is_le, is_neq, etc.).

En la ordenación por inserción, para poder insertar, debo comparar dos elementos en la lista de entrada y, en función del resultado de la comparación, insertar el elemento en la ubicación correcta.

Mi problema es que las implementaciones de los operadores de comparación sontype -> type -> prop (Necesito que sean así para la implementación de otros tipos / pruebas). Prefiero no creartype -> type -> bool Versiones de los operadores si se puede evitar.

¿Hay alguna manera de convertir unTrue | False prop a un bool para su uso en unaif ... then ... else ¿cláusula?

El tipo de módulo comparador:

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.

Una implementación para números naturales:

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.

La parte de inserción de la ordenación de inserción:

  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.

(Obviamente, el punto de inserción de inserción no funciona, ya que is_le devuelve Prop y no bool).

Cualquier ayuda es apreciada.