The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Tue, 4 Jun 2013 08:48:23 +1200,
Marco Servetto 
<marco.servetto AT gmail.com>
 a écrit :

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

I do not understand what you mean by "in-place".
And as you didn't explain what you mean by "finite set of", I do not
see why it could be a near suicide. A list of children is a way to have
a "finite set of".

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

I would say as an answer, that if you want to compute with your tree,
you will probably need a way to get a child from a given node.

So you will probably need a "some_child : tree → option tree",
returning None if you are on a leaf and some child else.

Now, we are deterministic, so if you use two trees which are intended
to be equal, t1 and t2, you will want to ensure that "some_child t1 ≡
some_child t2". That means that you need to choose wisely your child
so that it does not depend on the representation of the tree. That
reminds me a little of axiom of choice (but it definetely is not that
axiom). And there is no way I see to ensure existence of such a
function without doing some ordering on the structures.

> Is coq-gallina designed in this way on purpose?
> Is caused by an ill-designed collection library?

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?

That can solve a lot of problems, and also give you some headache to
ensure that when you build some tree you keep the ordering property
true.

> 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?)

Coq does not support built-in syntactical equality.
At most you can say it supports unification.
Load your ide with -nois argument, and you will see that "=" is not
defined, and you can define it inside the language without requiring
anything built-in. The only things I consider built-in in Coq are
"Prop", "Set" and "Type", and some notations (like those for the nat
type, even though nat type is not a built-in type). All the rest can be
defined inside Gallina. Plus this equality is in Prop, not in bool,
which means you cannot really compute with it (in particular, the only
functions of type "∀ T:Type, T → T → bool" that I can construct in Coq
are constant functions).

> 
> Marco.