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

Question

我对 Coq 有点陌生。

我正在尝试实现插入排序的通用版本。我正在实现的是作为一个以比较器为参数的模块。这个 Comparator 实现了比较运算符(例如 is_eq、is_le、is_neq 等)。

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

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

有什么方法可以转换 True | False用于 if ... then ... else 的 bool 属性条款？

比较器模块类型:

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 的类型是属性(property)的决策程序 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 类型的元素进行模式匹配是没有意义的.