相关疑难解决方法(0)

我对Coq很新.

我正在尝试实现插入排序的通用版本.我正在实现的是将Comparator作为参数的模块.此Comparator实现比较运算符(例如is_eq,is_le,is_neq等).

在插入排序中,为了插入,我必须比较输入列表中的两个元素,并根据比较结果将元素插入到正确的位置.

我的问题是比较运算符的实现是type -> type -> prop(我需要它们像这样实现其他类型/证明).type -> type -> bool如果可以避免,我宁愿不创建运算符的版本.

有没有办法将True | False道具转换为布尔用于if ... then ... else条款？

比较器模块类型:

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). …