Eu sou meio novo no Coq.

Estou tentando implementar uma versão genérica da classificação de inserção. Estou implementando é como um módulo que leva um comparador como um parâmetro. Este Comparador implementa operadores de comparação (como is_eq, is_le, is_neq, etc.).

Na inserção de inserção, a fim de inserir, devo comparar dois elementos na lista de entrada e, com base no resultado da comparação, inserir o elemento no local correto.

Meu problema é que as implementações dos operadores de comparação sãotype -> type -> prop (eu preciso que eles sejam assim para a implementação de outros tipos / provas). Eu prefiro não criartype -> type -> bool versões dos operadores, se puder ser evitado.

Existe alguma maneira de converter umTrue | False prop para um bool para uso em umif ... then ... else cláusula?

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

Uma implementação para números naturais:

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.

A parte de inserção da classificação de inserção:

  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, o ponto de fixação de inserção não funciona, pois is_le é retorna Prop e não bool).

Qualquer ajuda é apreciada.