The Coq mailing list

[Benoît Viguier <beviguier AT gmail.com>]

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