coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: e+coq-club AT x80.org (Emilio Jesús Gallego Arias)
To: Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Destructing and constructing inductive types
Date: Wed, 19 Oct 2016 17:45:59 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e+coq-club AT x80.org; spf=Neutral smtp.mailfrom=e+coq-club AT x80.org; spf=None smtp.helo=postmaster AT cc-tupan-roaming-b.ensmp.fr
Ironport-phdr: 9a23:S13+ZRRZ1fgqXwI4tRv65lwfctpsv+yvbD5Q0YIujvd0So/mwa64ZxyN2/xhgRfzUJnB7Loc0qyN4vqmBDJLsMzJ8ChbNscTB1ld0YRetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1oOra9QdaK3Iyfntq/8JzLYghOmCH1IfYrdE33/k3tsZw1hYJ/Me4W0QfEuH5BfeIekWBsLE+I2RHn+sqq+Zdl9QxNvfNk69NNW6T8cKk+C7BVWmcIKWcwscCovh7aCACL+3E0QjVO1B1SDECFwRT7Wpb2+gn3rXhmkAaTOcn7Qrd8cC6j5rwqG0ygszsOKzNsqDKfscd3lq8O5Uv5/xE=
Organization: X80 Heavy Industries

Hi Klaus,

Klaus Ostermann
<klaus.ostermann AT uni-tuebingen.de>
writes:

> 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.
>
> Is there some way to get such a lemma "for free"?

Depending on your development, sometimes is possible to make such
equations hold by conversion, avoiding the need for a destruct, YMMV but
I have had success sometimes by being careful with my statements and
definitions.

> On 10/18/2016 05:20 PM, Klaus Ostermann wrote:
>> Goal forall a b (p : nat * nat),
>> a = b -> fst p = a -> p = (b, snd p).

In addition to Laurent proof, you could use a purely equational one:

Goal forall a b (p : nat * nat), a = b -> fst p = a -> p = (b, snd p).
Proof.
now intros a b p ha hfst; rewrite <- ha, <- hfst, <- surjective_pairing.
Qed.

[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