Coq - 在if ... then ... else中使用Prop(True | False)

Question

我对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).

  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.

自然数的实现:

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.

插入排序的插入部分:

  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.

(显然,插入修复点不起作用,因为is_le返回Prop而不是bool).

任何帮助表示赞赏.

Answer 1

你似乎对Prop有点困惑.

is_le x y是Prop类型,是声明x is less or equal to y.这并不能证明这种说法是正确的.证明这种说法是正确的p : is_le x y,就是这种类型的居民(即证明该陈述的真相).

这就是模式匹配没有多大意义的原因IntComparator.is_le x h.

更好的界面如下:

Module Type ComparatorSig.

  Parameter X: Set.
  Parameter is_le : X -> X -> Prop.
  Parameter is_le_dec : forall x y, { is_le x y } + { ~ is_le x y }.

特别is_le_dec是,属性的类型是属性的决策过程is_le,也就是说,它返回证明x <= y或证据~ (x <= y).由于这是一个带有两个构造函数的类型,您可以利用if糖:

... (if IntComparator.is_le_dec x h then ... else ...) ...

从某种意义上说,这是一种增强的功能bool,可以为其所决定的内容提供见证.有问题的类型被调用sumbool,你可以在这里了解它:http: //coq.inria.fr/library/Coq.Init.Specif.html#sumbool

通常,谈论True或False执行代码没有意义.

首先,因为它们存在Prop,这意味着它们不能与计算相关,因为它们将被删除.

第二,因为他们不是唯一的居民Prop.虽然true并且false是唯一的类型值bool,这意味着您可以进行模式匹配,但类型Prop包含无限数量的元素(您可以想象的所有语句),因此尝试对类型元素进行模式匹配是没有意义的Prop.