Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Destructing and constructing inductive types
  • Date: Tue, 18 Oct 2016 17:20:35 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=klaus.ostermann AT uni-tuebingen.de; spf=None smtp.mailfrom=klaus.ostermann AT uni-tuebingen.de; spf=None smtp.helo=postmaster AT mx04.uni-tuebingen.de
  • Ironport-phdr: 9a23:FhXC4h0uOaX8QLNysmDT+DRfVm0co7zxezQtwd8ZseseLPad9pjvdHbS+e9qxAeQG96KsbQZ16GG6uigATVGusnR9ihaMdRlbFwst4Y/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbre9JomHhMOukuu25pf7YgNShTP7b6khAg+xqFDyssALmsNFMbo80B7ApH0AL+dSzH5zY1WIgxvm4862+rZ+9SUVp+8s/c9GXqj8Oag1G+8LRA86Onw4sZW4/SLIShGCsyMR
Hello Dominique,

my problem is presumably merely caused by my lack of expertise,
but to illustrate my point, what is the simplest way to prove
trivial lemmas like this one?

Goal forall a b (p : nat * nat),
a = b -> fst p = a -> p = (b, snd p).

Klaus


Am 18/10/16 um 12:40 schrieb Dominique Larchey-Wendling:
> 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


Archive powered by MHonArc 2.6.18.

Top of Page