[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