coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Dependent types and equality

From: Damien Pous <damien.pous AT gmail.com>
To: Pierre-Marie P�drot <pierremarie.pedrot AT ens-lyon.fr>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Dependent types and equality
Date: Thu, 30 Sep 2010 23:53:16 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; b=gmM+xzqD33k/b1Ul1p+gUl/VazTsEkfWyd1uQeKlQSwdWLQ8wbjVv8V3XJVMAs9Xzd lot+kUAAnQ7b2oAjkvfCqlyh/uDg3Wg7By2CKC1YbFToAWfmYmCNakcYBvWGcEd26e8n GKR+JszzoTOmC0xEje/IpVPhcrDVzw2vkROD0=

Hi,
Here is a (v8.3rc1) proof script that exploits the results from
Eqdep_dec and the fact that eq is decidable on nat:

Require Import Eqdep.
Require Import Eqdep_dec.

Inductive Fin : nat -> Type :=
| Fin0 : forall n, Fin (S n)
| FinS : forall n, Fin n -> Fin (S n).

Lemma Fin_eq_dec_aux: forall n x m y, {eq_dep nat Fin n x m
y}+{~eq_dep nat Fin n x m y}.
Proof.
  induction x as [n|n x IHx]; intros m y.
    destruct y as [m|m y].
      destruct (eq_nat_dec n m) as [E|E].
        subst. left. reflexivity.
        right. intro F. inversion F. apply E. assumption.
      right. intro F. inversion F.
    destruct y as [m|m y].
      right. intro F. inversion F.
      destruct (IHx m y) as [E|E].
        left. inversion E. subst. reflexivity.
        right. intro F. apply E. inversion F. subst. reflexivity.
Qed.

Lemma Fin_eq_dec : forall n (x y : Fin n), {x = y} + {x <> y}.
Proof.
  intros n x y.
  destruct (Fin_eq_dec_aux n x n y) as [H|H].
   left. apply (eq_dep_eq_dec eq_nat_dec). assumption.
   right. intro F. apply H. rewrite F. reflexivity.
Qed.

Print Assumptions Fin_eq_dec.

Damien

Le 30 septembre 2010 22:54, Pierre-Marie P�drot
<pierremarie.pedrot AT ens-lyon.fr>
a �crit :
> 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
>
>

Re: [Coq-Club] Dependent types and equality, Damien Pous
- <Possible follow-ups>
- Re: [Coq-Club] Dependent types and equality, Laurent Théry