coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Inductive family of finite types

From: Paolo Herms <paolo.herms AT cea.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Inductive family of finite types
Date: Tue, 28 Jun 2011 15:50:12 +0200

On Tuesday 28 June 2011 15:25:44 Gert Smolka wrote:
> Inductive Fin : nat -> Type :=
> | FinO : forall n, Fin (S n)
> | FinS : forall n, Fin n -> Fin (S n).
>
> Unfortunately, I cannot prove
>
> Lemma Fin1 (k : Fin 1) :
> k = FinO 0.

Try dependent destruction k.
You first need to Require Import Program.Equality.
--
Paolo Herms
PhD Student - CEA-LIST Software Safety Lab. / INRIA ProVal Project
Paris, France

[Coq-Club] Inductive family of finite types, Gert Smolka
- Re: [Coq-Club] Inductive family of finite types, Adam Chlipala
- <Possible follow-ups>
- Re: [Coq-Club] Inductive family of finite types, Paolo Herms
  - Re: [Coq-Club] Inductive family of finite types, Gert Smolka
    - Re: [Coq-Club] Inductive family of finite types, Adam Chlipala
      - Re: [Coq-Club] Inductive family of finite types, Gert Smolka
        
        Re: [Coq-Club] Inductive family of finite types, Daniel Schepler
- Re: [Coq-Club] Inductive family of finite types, ahrens