Coq-如果...则使用Prop（True | False），然后...否则 [英] Coq - use Prop (True | False) in if ... then ... else

问题描述

我对Coq有点陌生。

我正在尝试实现插入排序的通用版本。我正在实现的是将比较器作为参数的模块。该比较器实现比较运算符（例如is_eq，is_le，is_neq等）。

I'm trying to implement a generic version of insertion sort. I'm implementing is as a module that takes a Comparator as a parameter. This Comparator implements comparison operators (such as is_eq, is_le, is_neq, etc.).

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

In insertion sort, in order to insert, I must compare two elements in the input list, and based on the result of the comparison, insert the element into the correct location.

我的问题是比较运算符的实现是类型->类型-> prop （我需要像这样实现其他类型/证明）。我不想创建 type->类型-> bool 版本的运算符是否可以避免。

My problem is that the implementations of the comparison operators are type -> type -> prop (i need them to be like this for implementation of other types/proofs). I'd rather not create type -> type -> bool versions of the operators if it can be avoided.

有什么方法可以转换 True |在 if ... then ... else 子句中使用布尔型的错误道具？

Is there any way to convert a True | False prop to a bool for use in a if ... then ... else clause?

比较器模块类型：

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）。

(obviously, the insert fixpoint doesn't work, since is_le is returns Prop and not bool).

感谢您的帮助。

推荐答案

您似乎是一个

is_le xy 是Prop类型的，它是语句 x小于或等于y 。不能证明此说法正确。该语句正确的证据将是 p：is_le xy ，即该类型的居民（即该语句的真实性的见证人）。

is_le x y is of type Prop, and is the statement x is less or equal to y. It is not a proof that this statement is correct. A proof that this statement is correct would be p : is_le x y, an inhabitant of that type (i.e. a witness of that statement's truth).

这就是为什么在 IntComparator.is_le xh 上进行模式匹配没有太大意义的原因。

This is why it does not make much sense to pattern match on 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 糖：

In particular, the type of is_le_dec is that of a decision procedure for the property is_le, that is, it returns either a proof that x <= y, or a proof that ~ (x <= y). Since this is a type with two constructors, you can leverage the if sugar:

...（如果是IntComparator.is_le_dec xh则是...否则...）...

从某种意义上讲，增强的 bool ，它返回一个见证者以供其尝试确定。有问题的类型称为 sumbool ，您可以在此处进行了解：
http://coq.inria.fr/library/Coq.Init.Specif.html#sumbool

This is, in some sense, an enhanced bool, which returns a witness for what it is trying to decide. The type in question is called sumbool and you can learn about it here: http://coq.inria.fr/library/Coq.Init.Specif.html#sumbool

通常，谈论 True 或 False 来执行代码。

In general, it does not make sense to talk about True or False in executing code.

首先，因为它们位于 Prop 中，这意味着它们

First, because these live in Prop, which means that they cannot be computationally relevant as they will be erased.

第二，因为它们不是 Prop 的唯一居民。 true 和 false 是 bool 类型的唯一值，这意味着您可以进行模式匹配，类型 Prop 包含无限数量的元素（您可以想象的所有语句），因此尝试进行模式匹配是没有意义的匹配类型为 Prop 的元素。

Second, because they are not the only inhabitants of Prop. While true and false are the only values of type bool, which implies you can pattern-match, the type Prop contains an infinite number of elements (all the statements you can imagine), thus it makes no sense to try and pattern-match on a element of type Prop.

这篇关于Coq-如果...则使用Prop（True | False），然后...否则的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！