COQ中的指示器功能和半环

Question

我对Coq很陌生，我试图定义一个"通用"指示函数，像这样:

Function indicator (x : nat) : bool :=
  match x with
    | O => false
    | _ => true
  end.

这个很好。

我的问题是，我想要一个指示函数，返回false的任何半环的标识元素(我有一个个人的定义)，而不仅仅是自然数零，像这样:

Function indicator `(S : Semiring) (x : K) : bool :=
  match x with
    | ident => false
    | _ => true
  end.

其中K在半环S中定义为集合，ident在半环S中定义为单位元素。

这个不行。我得到了错误:

This clause is redundant

与match的最后一行下划线。然而，我不认为错误真的来自这里。我读到它可能来自

这行

    | ident => false

因为ident是一个变量，但我没有更多的线索。

Answer 1

nat是一个归纳类型，由两个构造函数创建:

Inductive nat: Set :=
    | O : nat
    | S : nat -> nat
 .

这意味着任何nat类型的居民总是由这两个构造函数的组合构建的。

您可以通过模式匹配来"检查"这个结构，就像您在第一个indicator定义中所做的那样。在第二种情况中，类型K是一个类型变量(您不希望拥有像nat那样的固定类型)，因此没有解释如何构建K的元素。然后，当您进行模式匹配时，您编写的ident只是一个绑定器，任何名称都具有相同的效果(_也是如此)。它没有链接到您的semiring的indent。Coq说这个子句是多余的，因为ident已经捕获了类型为K的任何元素，所以_的情况永远不会被调用。

如果你想为任何类型K编写这样的函数，你必须提供一种方法来比较K的元素(K -> K -> bool类型的东西)，并在你的指示符函数中使用它。语法我不太确定但你会有一些链接:

Record SemiRing : Type := mkSemiRing {    
    K: Type;
    ident : K;
    compare : K -> K -> bool;
    (* you might need the property that:
    forall x y, compare x y = true -> x = y
     *)
    op1 : K -> K -> K;
    op2 : K -> K -> K
    (* and all the laws of semiring... *)
}.
Definition indicator (ring: SemiRing) (x: K ring) : bool :=                                              
     if compare ring x (ident ring) then true else false.