Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Dependent types and equality

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Dependent types and equality


chronological Thread 
  • From: Pierre-Marie Pédrot <pierremarie.pedrot AT ens-lyon.fr>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Dependent types and equality
  • Date: Thu, 30 Sep 2010 22:54:26 +0200

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




Archive powered by MhonArc 2.6.16.

Top of Page