[Why3-club] Consistency of map theory

Guillaume Melquiond guillaume.melquiond at inria.fr
Fri Nov 23 20:20:57 CET 2012


Le vendredi 23 novembre 2012 à 19:56 +0100, Benedikt Huber a écrit :

> Generating the realizations for the map theory worked fine, just as 
> advertized in the manual ;) Now maybe a naive question, but how should 
> one define the map type without any assumptions on the type of the key 
> elements? Don't you need decidable equality for the key type in order to 
> define Map.set?

You do. This kind of requirement is why I have stayed away from
realizing some theories till now.

My long term goal is to improve the realization mechanism so that the
Coq printer can automatically associate specific type classes to Why3
realizations of types. It already does it systematically for the
inhabited property, but I would like to extend it to other properties
programmatically. For instance, whenever "map 'a 'b" would appear inside
a definition or a lemma statement, Why3 would add "DecidableEquality 'a"
as an implicit hypothesis.

> For inspiration, I took a look at the List theory realization. While it 
> does not need equality for the realized fragment, I wonder how one could 
> define num_occ, for example?
> 
>  > Definition num_occ: forall {a:Type} {a_WT:WhyType a},
>  >                     a -> (list a) -> Z.
> 
> The approach for Set (a -> Prop) looks interesting, but apparently I am 
> not experienced enough to devise a similar definition for maps, and 
> would appreciate any hints.

The set realization depends on three axioms at least, so it isn't that
interesting. As such, if you need a realization right now, my suggestion
would simply be to set decidable equality as an axiom and use it for
maps.

Best regards,

Guillaume




More information about the Why3-club mailing list