Counting number of different elements in a list in Coq

Question

I'm trying to write a function that takes a list of natural numbers and returns as output the amount of different elements in it. For example, if I have the list [1,2,2,4,1], my function DifElem should output "3". I've tried many things, the closest I've gotten is this:

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.

My logic is this: if m is not in the tail of the list then add one to the counter. If it is, do not add to the counter, so I'll only be counting once: when it's the last time it appears. I get the error:

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

In is part of Coq's list standard library Coq.Lists.List. It is defined there as:

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

I think I don't understand well enough how to use If then statements in definitions, Coq's documentation was not helpful enough.

I also tried this definition with nodup from the same library:

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

In this case what I get as error is:

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

And I'm quiet confused as to what's going on here. I'd appreciate your help to solve this issue.

Answer 1

You seem to be confusing propositions (Prop) and booleans (bool). I'll try to explain in simple terms: a proposition is something you prove (according to Martin-Lof's interpretation it is a set of proofs), and a boolean is a datatype which can hold only 2 values (true / false). Booleans can be useful in computations, when there are only two possible outcomes and no addition information is not needed. You can find more on this topic in this answer by @Ptival or a thorough section on this in the Software Foundations book by B.C. Pierce et al. (see Propositions and Booleans section).

Actually, nodup is the way to go here, but Coq wants you to provide a way of deciding on equality of the elements of the input list. If you take a look at the definition of 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.  

you'll notice a hypothesis decA, which becomes an additional argument to the nodup function, so you need to pass eq_nat_dec (decidable equality fot nats), for example, like this: nodup eq_nat_dec l.

So, here is a possible solution:

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 *)

Note: The nodup function works since Coq v8.5.

Answer 2

In addition to Anton's solution using the standard library I'd like to remark that mathcomp provides specially good support for this use case along with a quite complete theory on count and uniq. Your function becomes:

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.

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

In fact, I think the count_uniques name is redundant, I'd prefer to directly use size (undup s) where needed.