The Coq mailing list

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

Le Sat, 9 Mar 2013 09:16:07 +1300,
Marco Servetto 
<marco.servetto AT gmail.com>
 a écrit :

> I found the general idea quite interesting.
> I wonder if could be possible to use serialization as an unifying
> theoretical tool for finite sets and maps that can be easily be
> provable (sintactically) equal.
> That is, to show that a=b in coq you need syntactical equivalence or
> to "import more axioms"
> (sorry for my imprecise and confounding coq-terminolgy)
> If (some) terms could be easily converted (back and forth) in a list
> of chars/tokens that represents the syntactic definition of the term,
> than lots of stuff with finite data-structure would become trivial.

Yes and no. That was my first point.
If you define a finite set by a list of elements, set equality is not
syntactic, so my serialization cannot be useful. But for "canonical"
sets/maps (that is which admits only one representation, that is
extensional equality is exactly syntactical equality), yes that can
work. Note however, that FMap/FSet already provide stuff to establish a
link between extensionnal equality and a boolean equality on maps.

> 
> May be the "right" representation of a finite collection is not the
> collection of the term but the collection of their serialization?

I do not understand what you mean here.

> 
> 
> 
> On 9 March 2013 07:55, AUGER Cédric 
> <sedrikov AT gmail.com>
>  wrote:
> > Hi all, I often found useful to have serialization in Coq.
> >
> > I mean to have some type data:
> >
> > Inductive data :=
> > | Leaf : data
> > | Node : data → data → data.
> >
> > (or another variant, just this one is cool as it allows easy
> > product…)
> >
> > And for a serializable type t, two functions:
> >
> > serialize : t → data
> > deserialize : data → t
> > (or data → option t)
> >
> > and a proof of
> > ∀ x, deserialize (serialize x) = x
> > (or ∀ x, deserialize (serialize x) = Some x)
> >
> > This would have the following good points:
> > → for any serializable data, we have decidable equality for free
> > → for any serializable data, we can give a comparision function (not
> > necessarily the one, you want for a special usage, but well, it can
> > be handy for FSetAVL and related stuff)
> > → to implement an exception mechanism (the exception type can be
> > "data" and is solved dynamically with the deserialization, thus
> > allowing to pass exceptions of a unknown type at definition time of
> > the function) → avoid quadratic stuff in usual boolean equalities
> > (a type with n constructors will require n² branches)
> >
> > A type class for serialization is easy to do, but automatic
> > generation (in Ocaml code, like *_rec, *_rect, *_ind, *_beq) would
> > be a real plus I think, although of course many terms won't be
> > serializable.
> >
> > Not being a Coq source code hacker, I do not know how hard it can
> > be, especially dealing with dependant types and mutual recursion. I
> > guess, it could make some interesting internship for a student.