[Why3-club] Consistency of map theory

Benedikt Huber benedikt.huber at gmail.com
Fri Nov 23 19:56:41 CET 2012


On 11/22/2012 08:21 PM, Guillaume Melquiond wrote:
> Le jeudi 22 novembre 2012 ? 13:05 +0100, Benedikt Huber a ?crit :
>> Hello!
>>
>> I recently started playing around with Why3 (using coq+Z3), and I'm
>> really impressed so far.
>>
>> However, I believe that the lemma 'permut_eq' (theory map.why) is wrong.
> I will change it back and see how much of the testsuite breaks.
>
>> In general, maybe it would be desirable to proof all the lemmas in
>> theories provided with why3 to avoid problems like this?
>
> Sure. And if you take a look at the lib/coq subdirectory of why3, you
> will notice that the work has already started. Unfortunately, no one has
> handled map.why yet.
Thank you for taking care of the bug report.

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?

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.

Kind regards,
Benedikt




More information about the Why3-club mailing list