coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.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 *)
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...
------
Attachment:
example.v
Description: Binary data
- [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.