Ich bin ein bisschen neu in Coq.

Ich versuche, eine generische Version von Insertion Sort zu implementieren. Ich implementiere es als Modul, das einen Komparator als Parameter verwendet. Dieser Komparator implementiert Vergleichsoperatoren (wie is_eq, is_le, is_neq usw.).

Beim Sortieren nach Einfügung muss ich zum Einfügen zwei Elemente in der Eingabeliste vergleichen und basierend auf dem Ergebnis des Vergleichs das Element an der richtigen Position einfügen.

Mein Problem ist, dass die Implementierungen der Vergleichsoperatoren sindtype -> type -> prop (Ich brauche sie, um andere Typen / Beweise zu implementieren). Ich würde lieber nicht schaffentype -> type -> bool Versionen der Betreiber, wenn es vermieden werden kann.

Gibt es eine Möglichkeit, aTrue | False zu einem bool stützen für den einsatz in aif ... then ... else Klausel?

Der Komparator Modultyp:

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.

Eine Implementierung für natürliche Zahlen:

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.

Der Einfügeteil der Einfügesortierung:

  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.

(Offensichtlich funktioniert der Einfügefixpunkt nicht, da is_le Prop und nicht bool zurückgibt.)

Jede Hilfe wird geschätzt.