Coq - use Prop (True | False) em if… then… else
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.