Jestem trochę nowy w Coq.

Usiłuję zaimplementować ogólną wersję sortowania wstawiania. Wdrażam to jako moduł, który przyjmuje parametr jako komparator. Ten komparator implementuje operatory porównania (takie jak is_eq, is_le, is_neq itp.).

W przypadku wstawiania, aby wstawić, muszę porównać dwa elementy na liście wejściowej i na podstawie wyniku porównania wstawić element do właściwej lokalizacji.

Moim problemem jest to, że implementacje operatorów porównania sątype -> type -> prop (Potrzebuję, aby były one podobne do implementacji innych typów / proofów). Wolałbym nie tworzyćtype -> type -> bool wersje operatorów, jeśli można tego uniknąć.

Czy istnieje sposób na konwersjęTrue | False prop do bool do użycia wif ... then ... else klauzula?

Typ modułu porównawczego:

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.

Implementacja liczb naturalnych:

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.

Część wstawiania sortowania wstawiania:

  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.

(oczywiście, insert fixpoint nie działa, ponieważ is_le zwraca Return i nie bool).

Każda pomoc jest doceniana.