The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Gert Smolka wrote:
> Am 28.06.2011 15:50, schrieb Paolo Herms:
>
>    Try dependent destruction k.
>    You first need to Require Import Program.Equality.
>
> Thanks.  This does the job but uses the assumption
> JMeq_eq : forall (A : Type) (x y : A), x ~= y -> x = y
>
> Is there a proof without assumptions?

Yes:

Definition out n (k : Fin n) :=
  match k in Fin n return match n return Fin n -> Type with
                            | O => fun _ => Empty_set
                            | S n' => fun k => {k' | k = FinS _ k'} + 
{k = FinO _}
                          end k with
    | FinO _ => inright _ (refl_equal _)
    | FinS _ _ => inleft _ (exist _ _ (refl_equal _))
  end.

Definition Fin1 (k : Fin 1) : k = FinO 0 :=
  match out _ k with
    | inleft (exist k' _) => match out _ k' with end
    | inright pf => pf
  end.