coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Destructing and constructing inductive types

From: Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] Destructing and constructing inductive types
Date: Tue, 18 Oct 2016 12:10:54 +0200
Authentication-results: mail3-smtp-sop.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 mx03.uni-tuebingen.de
Ironport-phdr: 9a23:931u9BQkC+oTNzqEOUXgheCwB9psv+yvbD5Q0YIujvd0So/mwa64YBGN2/xhgRfzUJnB7Loc0qyN4vqmBDBLu8zJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/mjabvp9aJOU1hv3mUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqLjOq88ULZwDTI8Mmlz6te4mwPESF6s4nIBSS0xiQZFGQ3M6heyCpT1uzbh8O1mxCSAOMTwS5gpXzXn87pmQh7uhyoBcTI0pjKEwvdshb5W9Ury7yd0xJTZNdmY

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"?

Klaus

[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