The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

My solution was to use induction on n instead, using a function to
filter out FinO from l and invert FinS on the rest.  Here's a brief
outline of my definitions and main subsidiary lemmas (let me know if
you'd like me to fill in more details - let me just say that "destruct
x using Fin_0_inv" and "destruct x using Fin_Sn_inv" was useful at
several places):

Inductive Fin : nat -> Set :=
| FinO : forall {n:nat}, Fin (S n)
| FinS : forall {n:nat}, Fin n -> Fin (S n).

Definition Fin_0_inv (P : Fin 0 -> Type) :
  forall x:Fin 0, P x :=
fun x =>
match x in (Fin z) return
  (match z return (Fin z -> Type) with
   | 0 => P
   | S _ => fun _ => unit
   end x) with
| FinO _ => tt
| FinS _ _ => tt
end.

Definition Fin_Sn_inv {n:nat} (P : Fin (S n) -> Type)
  (PO : P FinO) (PS : forall y:Fin n, P (FinS y)) :
  forall x:Fin (S n), P x :=
fun x =>
match x in (Fin Sn) return
  (match Sn return (Fin Sn -> Type) with
   | 0 => fun _ => unit
   | S n' => fun x => forall (P : Fin (S n') -> Type),
     P FinO -> (forall y:Fin n', P (FinS y)) ->
     P x
   end x) with
| FinO _ => fun P PO PS => PO
| FinS _ y => fun P PO PS => PS y
end P PO PS.

Definition FinS_inv {n:nat} (x:Fin (S n)) :
  option (Fin n) :=
Fin_Sn_inv (fun _ => option (Fin n)) None (@Some _) x.

Fixpoint map_FinS_inv {n:nat} (l : list (Fin (S n))) :
  list (Fin n) :=
match l with
| nil => nil
| cons x l' =>
  let recval := map_FinS_inv l' in
  match FinS_inv x with
  | Some y => cons y recval
  | None => recval
  end
end.

Lemma map_FinS_inv_len_NoDup :
  forall {n:nat} (l : list (Fin (S n))),
  NoDup l -> length l <= S (length (map_FinS_inv l)).

Lemma map_FinS_inv_NoDup : forall {n:nat} (l : list (Fin (S n))),
  NoDup l -> NoDup (map_FinS_inv l).
-- 
Daniel Schepler

On Sun, Sep 14, 2014 at 8:05 PM, John Wiegley 
<johnw AT newartisans.com>
 wrote:
> 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