The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-09-15 5:05 GMT+02:00 John Wiegley <johnw AT newartisans.com>:

Hello,

I'm finding the following theorem difficult, and wonder if anyone could offer
guidance or solution:

  Theorem fin_list : forall n (l : list (fin n)), NoDup l -> length l <= n.

I started by induction on "NoDup l", but I'm not sure how to relate length l
and fin n.  I arrive here:

  n : nat
  x : fin n
  l : list (fin n)
  H : ~ In x l
  H0 : NoDup l
  IHNoDup : length l <= n
  ============================
   length (x :: l) <= n

We should know that length l < n, because a member of the set is not present,
but I can't see a way to derive this fact.

Thanks,
  John

I think, I would rather have tried induction on "n".

If I were to do the proof, I would do something like:

1. forall (l:list (fin 0)), NoDup l -> length l <= 0
   Take such l, by cases on l, either it is nil, and thus 1. holds,
   or it has a head which belongs to (fin 0) which is the empty set,
   so it is contradictory.
2. (forall (l:list (fin n)), NoDup l -> length l <= n) ->
   (forall (l:list (fin (S n))), NoDup l -> length l <= S n).
   Name H the hypothesis, and take (l:list (fin (S n))) such that
   (K:NoDup l).
   By cases on K, either l is empty list, and you can easily conclude,
   either l can be written as (hd::tl) with NoDup tl and hd does not
   belong to tl. You can then define a injection f which sends any
   (x:fin (S n)) such that (x≠hd) to some (y:fin n). As hd does not belong to
   tl, you can prove that (NoDup tl -> NoDup (f tl)), thus by H,
   (length (map f tl) <= n) and, as (length (map f x) = length x),
   (length tl <= n). From that, you can conclude that (length (hd::tl) <= S n).

Another proof, would be done in using a sorting algorithm, you first sort your list, thus not changing its length, nor multiplicity of its element.
Using the injection (ord : forall n, fin n -> nat) which returns the "number of the element in (fin n)"
Then you prove something like: (forall n (l:list (fin n)), sorted l -> forall m, ord (head l) <= m -> length l <= m).
Then, as (ord x <= n) for any x in (fin n), you can conclude.