Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Benoît Viguier <beviguier AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] How to prove an inductive property on trees.
  • Date: Mon, 8 Feb 2016 02:48:44 +0900
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=beviguier AT gmail.com; spf=Pass smtp.mailfrom=beviguier AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f181.google.com
  • Ironport-phdr: 9a23:4liCnx+HLMjeFf9uRHKM819IXTAuvvDOBiVQ1KB90OMcTK2v8tzYMVDF4r011RmSDdqdsa8P0rKP+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStGU1Zn8jrjrs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGCGC4HyaTlIokxVVAgXfpEXwU4nwvTb7u/BV1yyTPMmwRrcxD2fxp5x3QQPl3X9UfwUy93va35R9

Good Evening Coq-club,

I'm trying to work on general trees (not binary) with an iterators semantics and therefore to formalize simple properties.
See attached file.

TL;DR (do not copy paste it, better use the .v file):
Inductive Tree : Set :=
| Node : nat -> list Tree -> Tree.

Fixpoint vals (t:Tree) : list nat := match t with
| Node n l => n :: (consListAll Tree nat vals l)
end. 
(* return the list of the values in the tree *) 

Fixpoint NumVal (t:Tree) := match t with
| Node n l => 1 + SumAll Tree NumVal l
end.
(* recursively count the values in the tree *)

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...

Any advices to get out of it ?

Kind regards.

------
Benoît

Attachment: example.v
Description: Binary data




Archive powered by MHonArc 2.6.18.

Top of Page