The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

Yes, that is clever.
By the way, I do not know why people use this definition of "fin" which I find rather inconvenient.

Inductive emptySet : Type := .

Fixpoint fin2 (n : nat) : Type := match n with O => emptySet | S n => option (fin2 n) end.

is a lot more convenient from my point of view.
Here, we do not have to do all these inversion stuff when inspecting an element.

2014-09-15 18:06 GMT+02:00 Daniel Schepler <dschepler AT gmail.com>:

On Mon, Sep 15, 2014 at 8:50 AM, John Wiegley <johnw AT newartisans.com> wrote:
> Thanks to you and Daniel, I am now much closer.  However, I'm still having
> difficulty with the above statement: what about the case where hd is not the
> greatest element of fin (S n)?  Then the fact that x <> hd doesn't help me,
> since hd could be an element which *should* be in y, rather than x.  It seems
> like your proof assumes an ordered set from greatest to last, when the
> original statement requires no ordering.  Daniel did make reference to the
> fact that having a sorting property could make things easier.

OK, here's a complete solution.  As opposed to what Auger suggested,
my proof essentially proceeds by cases depending on whether or not
FinO is in the list.  That makes it easier to define the injection {
x:Fin (S n) | x <> FinO } -> Fin n.

Require Import List.
Require Import Arith.

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_noO :
  forall {n:nat} (l : list (Fin (S n))),
  ~ In FinO l -> length (map_FinS_inv l) = length l.
Proof.
induction l; simpl.
+ reflexivity.
+ destruct a using Fin_Sn_inv; simpl; intuition.
Qed.

Lemma map_FinS_inv_len_NoDup :
  forall {n:nat} (l : list (Fin (S n))),
  NoDup l -> length l <= S (length (map_FinS_inv l)).
Proof.
induction 1; simpl.
+ repeat constructor.
+ destruct x using Fin_Sn_inv; simpl; intros.
  - rewrite map_FinS_inv_len_noO; trivial.
  - auto with arith.
Qed.

Lemma in_map_FinS_inv : forall {n:nat} (l : list (Fin (S n)))
  (y : Fin n), In y (map_FinS_inv l) -> In (FinS y) l.
Proof.
induction l; simpl.
+ trivial.
+ destruct a using Fin_Sn_inv; simpl.
  - auto.
  - destruct 1.
    * left; f_equal; trivial.
    * right; auto.
Qed.

Lemma map_FinS_inv_NoDup : forall {n:nat} (l : list (Fin (S n))),
  NoDup l -> NoDup (map_FinS_inv l).
Proof.
induction 1; simpl.
+ constructor.
+ destruct x using Fin_Sn_inv; simpl.
  - trivial.
  - constructor; trivial. contradict H. apply in_map_FinS_inv; trivial.
Qed.

Theorem fin_list : forall {n:nat} (l : list (Fin n)),
  NoDup l -> length l <= n.
Proof.
induction n.
+ destruct l.
  - trivial.
  - destruct f using Fin_0_inv.
+ intros. apply le_trans with (1 := map_FinS_inv_len_NoDup l H).
  auto using le_n_S, map_FinS_inv_NoDup.
Qed.
--
Daniel Schepler

--
.../Sedrikov\...