The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

Is now a while that I'm tring to put my head around the coq system,
and I'm realizing that often there is a
"feasable" way to do/model stuff and a other ways can be harder or
near impossible.
This does not surprise me, since it happens in near all programming languages.
The think that surprise me is that it looks like is often simpler to
redefine "stuff" from scratch w.r.t. using pre existent work - well
defined abstractions.

To make an example, suppose that I want to model a tree with a finite
set of children for each node.
The mathematically more accurate way is to model the set of children
as a finite set of trees.
however, it looks like going this way is a near suicide, and modelling
the tree with a (mutually re-defined in place) list of children, is
much simpler.
If, and only if, I will ever need the assumption that trees that
differs only for the order of children are identical, I will define an
equivalence relation over trees.

My question is, why is that?
Is coq-gallina designed in this way on purpose?
Is caused by an ill-designed collection library?
With dependent typing, should not be *simpler* to say that children
are syntactically ordered and than a tree require the proof that the
children are in order?
For the best of my understanding, today is *possible* to go that way,
but not *simpler*.

For my understanding, coq support as "built in" syntactical equality,
but not syntactical ordering. Why? (that would make defining a
"normalized f-set structure" much esier, right?)

Marco.