Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to prove an inductive property on trees.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to prove an inductive property on trees.


Chronological Thread 
  • 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/>.



Archive powered by MHonArc 2.6.18.

Top of Page