计算 Coq 列表中不同元素的数量

Question

我正在尝试编写一个函数，该函数接受自然数列表并返回其中不同元素的数量作为输出。例如，如果我有列表 [1,2,2,4,1]，我的函数 DifElem 应该输出“3”。我已经尝试了很多东西，我得到的最接近的是：

Fixpoint DifElem (l : list nat) : nat :=
   match l with
   | [] => 0
   | m::tm => 
   let n := listWidth tm in
   if (~ In m tm) then S n else n
end.

我的逻辑是这样的：如果 m 不在列表的尾部，则向计数器加一。如果是，不要添加到计数器中，所以我只会数一次：当它最后一次出现时。我得到错误：

Error: The term "~ In m tm" has type "Prop"
which is not a (co-)inductive type.

In 是 Coq 的 list 标准库的一部分 Coq.Lists.List. 它在那里定义为：

Fixpoint In (a:A) (l:list A) : Prop :=
   match l with
   | [] => False
   | b :: m => b = a \/ In a m
end.

我认为我不太了解如何在定义中使用 If then 语句，Coq 的文档并没有提供足够的帮助。

我还尝试使用同一个库中的nodup 进行此定义：

Definition Width (A : list nat ) := length (nodup ( A ) ).

在这种情况下，我得到的错误是：

The term "A" has type "list nat" while it is expected to have
type "forall x y : ?A0, {x = y} + {x <> y}".

而且我对这里发生的事情感到很困惑。感谢您为解决此问题提供的帮助。

Answer 1

您似乎混淆了命题 (Prop) 和布尔值 (bool)。我将尝试用简单的术语来解释：proposition 是您证明的东西（根据 Martin-Lof 的解释，它是一组证明），而 boolean 是只能包含 2 个值的数据类型 (true / false)。当只有两种可能的结果并且不需要附加信息时，布尔值在计算中很有用。您可以在@Ptival 的this answer 中找到有关此主题的更多信息，或者在 B.C. 的 Software Foundations 书中对此进行详细介绍。皮尔斯等人。 （参见Propositions and Booleans 部分）。

实际上，nodup 是这里的方法，但 Coq 希望你提供一种方法来决定输入列表中元素的相等性。如果你看一下nodup的定义：

Hypothesis decA: forall x y : A, {x = y} + {x <> y}.

Fixpoint nodup (l : list A) : list A :=
  match l with
    | [] => []
    | x::xs => if in_dec decA x xs then nodup xs else x::(nodup xs)
  end.  

您会注意到一个假设decA，它成为nodup 函数的附加参数，因此您需要传递eq_nat_dec（可判定相等性fot nats），例如，像这样：@987654338 @。

所以，这里有一个可能的解决方案：

Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.
Import ListNotations.

Definition count_uniques (l : list nat) : nat :=
  length (nodup eq_nat_dec l).

Eval compute in count_uniques [1; 2; 2; 4; 1].
(* = 3 : nat *)

注意：nodup 函数从 Coq v8.5 开始工作。

Answer 2

除了 Anton 使用标准库的解决方案之外，我想指出的是，mathcomp 为这个用例提供了特别好的支持，以及关于 count 和 uniq 的非常完整的理论。你的函数变成：

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.

Definition count_uniques (T : eqType) (s : seq T) := size (undup s).

其实我觉得count_uniques这个名字是多余的，我宁愿在需要的地方直接使用size (undup s)。

Answer 3

使用集合：

Require Import MSets.
Require List. Import ListNotations.

Module NatSet := Make Nat_as_OT.

Definition no_dup l := List.fold_left (fun s x => NatSet.add x s) l NatSet.empty.
Definition count_uniques l := NatSet.cardinal (no_dup l).

Eval compute in count_uniques [1; 2; 2; 4; 1].