The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Pierre-Marie Pédrot wrote:
> I've fighting for some days with equality and dependent types for very
> simple cases. I'm currently trying to fiddle with Fin, which defined as
> in CPDT :
>
> Inductive Fin : nat ->  Type :=
> | Fin0 : forall n, Fin (S n)
> | FinS : forall n, Fin n ->  Fin (S n).
>
> and I would like to find an axiom-free proof of decidability of equality
> for Fin :
>
> Lemma Fin_eq_dec : forall n (x y : Fin n), {x = y} + {x<>  y}.
>    

Here's an implementation.  It works for me in Coq 8.2pl2, in a file 
containing just the following, with your [Fin] definition beforehand.  
The main trick is in the inner [match] [return] annotations, which are 
themselves [match]es that return functions over the discriminee.

Definition argOf n (x : Fin n) : option (Fin (pred n)) :=
  match x with
    | Fin0 _ => None
    | FinS _ x' => Some x'
  end.

Theorem noteq_cong : forall n (x y : Fin n),
  x <> y
  -> FinS _ x <> FinS _ y.
  intros; intro Heq; generalize (f_equal (@argOf _) Heq); simpl; 
congruence.
Qed.

Hint Resolve noteq_cong.
Hint Extern 1 (_ <> _) => discriminate.

Definition Fin_eq_dec n (x y : Fin n) : {x = y} + {x <> y}.
  refine (fix F n (x : Fin n) : forall y : Fin n, {x = y} + {x <> y} :=
    match x in Fin n return forall y : Fin n, {x = y} + {x <> y} with
      | Fin0 _ => fun y => match y in Fin n' return match n' return Fin 
n' -> Type with
                                                      | O => fun _ => 
Empty_set
                                                      | S n'' => fun y 
=> {Fin0 _ = y} + {Fin0 _ <> y}
                                                    end y with
                             | Fin0 _ => left _ _
                             | _ => right _ _
                           end
      | FinS _ x' => fun y => match y in Fin n' return match n' return 
Fin n' -> Type with
                                                      | O => fun _ => 
Empty_set
                                                      | S n'' => fun y 
=> forall x' (Fx' : forall y', {x' = y'} + {x' <> y'}),
                                                        {FinS _ x' = y} 
+ {FinS _ x' <> y}
                                                       end y with
                                | Fin0 _ => fun _ _ => right _ _
                                | FinS _ y' => fun _ Fx' => if Fx' y' 
then left _ _ else right _ _
                              end _ (F _ x')
    end); subst; auto.
Defined.