coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Destructing and constructing inductive types

From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Destructing and constructing inductive types
Date: Tue, 18 Oct 2016 12:40:17 +0200
Organization: LORIA

On 10/18/2016 12:10 PM, Klaus Ostermann wrote:
> Lemmas like this can be formulated for every inductive datatypes:
>
> forall p, (fst p, snd p) = p
>
> I find that I often need such lemmas for rewriting terms while proving
> stuff in Coq.
>
> It is annoying to prove such lemmas by hand for every datatype.

destruct p does not fit your needs ?

Dominique

[Coq-Club] Destructing and constructing inductive types, Klaus Ostermann, 10/18/2016
- Re: [Coq-Club] Destructing and constructing inductive types, Dominique Larchey-Wendling, 10/18/2016
  - Re: [Coq-Club] Destructing and constructing inductive types, Klaus Ostermann, 10/18/2016
    - Re: [Coq-Club] Destructing and constructing inductive types, Laurent Thery, 10/18/2016
    - Re: [Coq-Club] Destructing and constructing inductive types, Dominique Larchey-Wendling, 10/18/2016
- Re: [Coq-Club] Destructing and constructing inductive types, Emilio Jesús Gallego Arias, 10/19/2016