The Coq mailing list

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

> I do not understand what you mean by "in-place".
For example stuff like
Inductive tree : Set :=
  | Leaf: something -> tree
  | Node: treeChildren -> something -> tree
with treeChildren : Set :=
  | empty: treeChildren
  | Cons: tree -> treeChildren ->treeChildren

If I understand correctly is common wisdom in the coq community that
the mutually recursive definition defined over is easier to manage
then an "equivalent"

Inductive tree : Set :=
  | Leaf: something -> tree
  | Node: list tree -> something -> tree

Even for the simple user defined list type. If I understand correctly
for a proper set/finite set type it would be even worst.
> And as you didn't explain what you mean by "finite set of",
A finite set, is a set (as mathematical notion) that happen to be finite.
Moreover, I admit that intend more than that, I intend that also the
element of the three hava a finite representation as a coq/gallina
term,

> A list of children is a way to have a "finite set of".
That is the whole point.  "a way to have" imply that we have to
re-encode and conceptually re-design the obviously well known concept
of finite set every time.


> Coq does not support built-in syntactical equality.
> At most you can say it supports unification.
Yes, sorry I mean unification, but... is unification rooted over over
syntactical equality, right?
> 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.
Well, I assume that the "needed feature to define new concepts" must
be built-in too...

> Plus this equality is in Prop, not in bool...
Yes, I know that very well, but I wander, since (assuming) unification
is rooted over over syntactical equality,
we could have built in also a "is syntactically less then" property,
that would allow
in an easy way ordering of stuff, be clear, not a -meaningful- order
in any way, but, still an order.
Depending on what we believe functions and proofs means, that some
terms are not ordered, this would no be a problem too, simply
propositions t1 > t2, t2 > t1,  and t1=t2 would be all three
impossible to show.


> 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.
That is, a good "set" type would do it automatically, it would be
irrelevant what is the ordering property if it can be shown that one
possible ordering exists.