coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] How to prove an inductive property on trees.
- Date: Sun, 7 Feb 2016 12:52:25 -0500
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing.csail.mit.edu
- Ironport-phdr: 9a23:6qZGMxBZy+qVI95uEazFUyQJP3N1i/DPJgcQr6AfoPdwSP74r8bcNUDSrc9gkEXOFd2CrakU1KyM7uu5ATVIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/niKboptaKO1wArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5Je2kfl1JjAwzE9Bj+V9+luyfzs+FV0zKTPMmwSLEoHzmu8vE4G1fTlC4bOmthoynsgctqgfcDrQ==
On 02/07/2016 12:48 PM, Benoît Viguier
wrote:
I'm trying to reason by induction over the list of
the children (hence a :: l). But I'm stuck in the proof.
My induction hypothesis is :
length (vals (Node n l)) = NumVal (Node n l) But at the point of my reasoning I'm asked to prove :
length (vals a) = NumVal a Therefore I got a pretty loop in my demonstration...
I believe this is likely to be the standard problem that is treated in Section 3.8 of CPDT <http://adam.chlipala.net/cpdt/>. |
- [Coq-Club] How to prove an inductive property on trees., Benoît Viguier, 02/07/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Adam Chlipala, 02/07/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Dominique Larchey-Wendling, 02/07/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Dominique Larchey-Wendling, 02/07/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Adam Chlipala, 02/07/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Dominique Larchey-Wendling, 02/07/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Frédéric Blanqui, 02/09/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Adam Chlipala, 02/07/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Dominique Larchey-Wendling, 02/07/2016
Archive powered by MHonArc 2.6.18.