计算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列表标准库的一部分Coq.Lists.List.它定义为:

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

我认为我不太了解如何使用如果在定义中的语句,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).我将尝试用简单的术语来解释:命题是你证明的东西(根据Martin-Lof的解释,它是一组证明),而布尔值是一种只能容纳2个值(true/ false)的数据类型.当只有两种可能的结果且不需要添加信息时,布尔值可用于计算.您可以在@Ptival的这个答案中找到更多关于此主题的内容,或者在BC Pierce等人的软件基础书中找到关于此主题的详细部分.(参见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(decidable equality fot nats),例如,如下所示:nodup eq_nat_dec l.

所以,这是一个可能的解决方案:

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].