The Coq mailing list

[Pierre-Marie Pédrot <pierremarie.pedrot AT ens-lyon.fr>]

Dear Coq users,

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}.

I have been unable to prove it without using JMeq axioms, and I did not
succeed in proving it through hand-fed terms either. Yet, it works out
of the box in Agda.

Is there an axiom-free proof of this property, and what should it be ? I
did not find anything relevant while skimming CPDT. Do you have any
useful pointer ?

PMP

Attachment: signature.asc
Description: OpenPGP digital signature