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