The Coq mailing list

[Venanzio Capretta <Venanzio.Capretta AT mathstat.uottawa.ca>]

Thank Solange and Milad for your suggestions.
As I mentioned in the original question, I am using an alternative 
representation based on vectors as functions from finite sets:

Parameter Finite: nat->Set.
Parameter nat_index: (n,m:nat)(lt m n) -> (Finite n).
Parameter index_nat: (n:nat)(Finite n) -> nat.
Hypothesis index_lt:
(n:nat; i:(Finite n))(lt (index_nat n i) n).
Hypothesis inverse_nat:
(n,m:nat; p:(lt m n))(index_nat n (nat_index n m p))=m.
Hypothesis inverse_index:
(n:nat; i:(Finite n))(nat_index n (index_nat n i) (index_lt n i))=i.

Definition Vector[X:Set]: nat -> Set:=
[n](Finite n)->X.

(* There are a couple of obvious implementations of Finite, definied by
  Fixpoint or by Inductive.
*)

Variable label : Set.
Variable child: (a:label)(Vector label (size a)).
(* It is also easy to define "child" from "children", that uses lists. *)

CoInductive Tree: Set :=
Node: label->(n:nat)(Vector Tree n)->Tree.

CoFixpoint makeTree: label -> Tree:=
[a](Node a (size a) [i](makeTree (child a i))).

My question was specifically about the type Tree defined using lists.
I think this example is an argument in favor of the "coinductive types 
as final coalgebras" definition against the "guarded by constructors" 
conception.
It seems to me that implementing the coinductive principle stating that 
there is a unique morphism from any coalgebra to the inductive type 
would be much easier than extendin the definition of "guarded by 
constructors".

Maybe this could be a suggestion for future versions of Coq.

-- Venanzio