The Coq mailing list

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

Le Fri, 7 Jun 2013 09:37:30 +1200,
Marco Servetto 
<marco.servetto AT gmail.com>
 a écrit :

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

Yes, that is often the case.
But in both cases you will have pros and cons.
Some people tend to prefer to use first solution and others to use the
second.

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

And I think that you also want more than that to make it usable.
The "mathematical notion" can easily be written (removing the finiteness
constraint, and assuming relaxation of some Coq constraint)

Inductive tree : Set :=
  | Leaf: something -> tree
  | Node: (tree -> Prop) (*set of trees*) -> something -> tree

Well, you have no way to visit a child with it. You won't go much far
with that.

I think that you need a way to pick-up some child.
And probably once you got a child, you want an other one you did not
have yet selected.
And probably once you can do that, you want some ensurance that you can
visit all the children this way.

So with that informations, I think that what you want for your finite
set is something like:

Record finite_set :=
 { set : tree -> Prop
 ; next_child : option { t : tree | set t } ->
                option { t : tree | set t }
                (* first child you can get is "next_child None"
                   which may return "None" if "set" is empty. *)
 ; cardinal : nat
 ; all_reached : forall t, set t ->
                 exists n, match next_child^n None with
                           | Some c => proj1_sig c = t
                           | None => False
                           end
  }.

And once you have done that, you find out that what you wanted was
simply a list… (well without duplication). Keep your distance with bare
mathematical formalism, a lot of things are implicit, hidden, or wrong
without anyone noticing. A set is just a membership function, it is
often enough for specification, but hardly ever useful when defining
structures you want to inspect.

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

We do not have to "re-encode", but to "encode".
And for me, finite set is not an "obviously well known concept".

http://en.wikipedia.org/wiki/Finite_set

For instance, Dedekind definition of finiteness may not be what you
think with "finite set".

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

I will let others reply to that, I do not want to start a troll with
word playings. For me it covers some other concepts like normalization,
eta-expansion, and you can have a "x = u" as hypothesis without being
able to prove False, even if "x" and "u" are not syntactically equal
(they are different letters).

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

It does not belong to what I call "built-in", but every one has its
definition. The keyword "Definition" is not something you can
manipulate in Coq. I do not consider it built-in. "Type" is something
you manipulate in Coq (you can pass it to a function for instance),
and you need it to be initially present. So "Type" belongs to what I
call built-ins. "=" needs not to be initially present, you can define
it (and this is the way it is done) with:

Inductive eq {T : Type} (x : T) : T -> Prop := eq_refl : eq x x.

Start a session with "-nois" argument, and you will see that you cannot
use "=" unless you define it. But "Type" is still there even with
"-nois" argument.

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

Such a construction would be highly non-canonical. There are many ways
to define a syntactical (total) ordering and none of them can be
considered natural. And if you want partial orders, you won't have a
way to sort a list in a unique way, so I bet your problem will remain.

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

Sorry, I do not see the point in this.

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

There alrealy are libraries to deal with sorted lists in the standard
library as far as I can remember.