coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Equality for inductive type containing list

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Equality for inductive type containing list
Date: Thu, 6 Oct 2016 09:20:04 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:5htMJx2V3bukeg2VsmDT+DRfVm0co7zxezQtwd8ZsegVI/ad9pjvdHbS+e9qxAeQG96KsbQf0aGI6ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL2PbrnD61zMOABK3bVMzfbWvXNWIxJrun8mJuLTrKz1SgzS8Zb4gZD6Xli728vcsvI15N6wqwQHIqHYbM85fxGdvOE7B102kvpT4r9Zf9HFbvOtk/MpdW437eb45RPpWFmcIKWcwsebvNBzOSxe43noAFyA9lhNVDwXBpEXxWpr0vy3m8PJ8xAGVOMT3SfY/XjH0vPQjcwPhlCpSb21xy2rQkMEl1K8=

On 2016-10-06 07:53, Klaus Ostermann wrote:
> I tried to prove this theorem:
>
> Definition ty_eq_dec (t1 t2 : ty) : {t1 = t2} + {t1 <> t2}.
>
> using "decide equality", but this seems to go nowhere.

You need to be explicit about the recursion:

Notation id := nat.

Inductive ty: Set :=
| tvar : id -> ty
| tpoly : id -> list ty -> ty.

Definition ty_eq_dec : forall (t1 t2 : ty), {t1 = t2} + {t1 <> t2}.
Proof.
fix rec 1.
repeat decide equality.
Defined.

Clément.

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Equality for inductive type containing list, Klaus Ostermann, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Dominique Larchey-Wendling, 10/06/2016
  - Re: [Coq-Club] Equality for inductive type containing list, Clément Pit--Claudel, 10/06/2016
  - Re: [Coq-Club] Equality for inductive type containing list, Klaus Ostermann, 10/06/2016
    - Re: [Coq-Club] Equality for inductive type containing list, Dominique Larchey-Wendling, 10/06/2016
      - Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/06/2016
        
        Re: [Coq-Club] Equality for inductive type containing list, Maxime Dénès, 10/06/2016
        
        Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/06/2016
        
        Re: [Coq-Club] Equality for inductive type containing list, Pierre Courtieu, 10/06/2016
        Re: [Coq-Club] Equality for inductive type containing list, Abhishek Anand, 10/06/2016
        Re: [Coq-Club] Equality for inductive type containing list, Dominique Larchey-Wendling, 10/06/2016
        
        Re: [Coq-Club] Equality for inductive type containing list, Jonathan Leivent, 10/06/2016
        
        Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/06/2016