coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: AUGER Cédric <sedrikov AT gmail.com>
- To: Marco Servetto <marco.servetto AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Serialization in Coq
- Date: Sat, 9 Mar 2013 00:06:56 +0100
Le Sat, 9 Mar 2013 11:50:47 +1300,
Marco Servetto
<marco.servetto AT gmail.com>
a écrit :
> Sorry for the little explanation I wrote in my former message.
> >>But for "canonical" sets/maps (that is which admits only one
> >>representation, that is extensional equality is exactly syntactical
> >>equality), yes that can work.
> I was referring to those "canonical ones"
> >> Note however, that FMap/FSet already provide stuff to establish a
> >>link between extensionnal equality and a boolean equality on maps.
> And that is exactly where I was "attaccking" when I said
> > May be the "right" representation of a finite collection is not the
> > collection of the term but the collection of their serialization?
>
> Trying to be more explicit this time:
> If it was easy to define serialization and deserialization functions
> for any finite datatype,
> then a similar FMap/FSet implementation can be working on the
> serialized version,
> requiring no extra instrumentation of the datatipe itself.
> That is, today using the polymorphic list type and proving properties
> over such lists is order of magnitude easier than doing the same over
> finite sets (with canonical representation)
> If it was possible to see every datatype as his syntactical
> representation, (that of course defines a total ordering) a simple
> ordered list without repetition *is* a set with canonical
> representation.
Ok, that means you have to define your set as something like:
Record finite_set (t : Type) (Ht : serializable t) : Type :=
{ fset : list t
; FsetOrdered : ordered_list (order t Ht) fset
}.
(where ordered_list and order have to be defined)
And yes, this type can be made serializable (if ordered_list is a
function returning either True or False, to ensure proof-irrelevance on
it), so we could have canonicity on finite_set. Not sure it is very
convenient though…
Also I remember having written a "canonical map" for positives by
hacking the FMapPositive one (I think this version is in S. Lescuyer
Containers Library).
- [Coq-Club] Serialization in Coq, AUGER Cédric, 03/08/2013
- Re: [Coq-Club] Serialization in Coq, Marco Servetto, 03/08/2013
- Re: [Coq-Club] Serialization in Coq, AUGER Cédric, 03/08/2013
- Re: [Coq-Club] Serialization in Coq, Marco Servetto, 03/08/2013
- Re: [Coq-Club] Serialization in Coq, AUGER Cédric, 03/09/2013
- Re: [Coq-Club] Serialization in Coq, Marco Servetto, 03/08/2013
- Re: [Coq-Club] Serialization in Coq, AUGER Cédric, 03/08/2013
- Re: [Coq-Club] Serialization in Coq, Marco Servetto, 03/08/2013
Archive powered by MHonArc 2.6.18.