[Why3-club] Consistency of map theory

Benedikt Huber benedikt.huber at gmail.com
Thu Nov 22 15:12:35 CET 2012


On 11/22/2012 02:34 PM, Santiago Zanella wrote:
> I believe the culprit is a typo in the permut_eq lemma:
>    lemma permut_eq :
>      forall a1 a2 : map int 'a. forall l u : int.
>      permut_sub a1 a2 l u ->
>      forall i:int. (i < l \/ u <= i) -> a2[i] = a1[i]
> The last line should read
>      forall i:int. (i < u \/ l <= i) -> a2[i] = a1[i]
Dear Santiago,
The line you proposed (disjunction in the ancedent)
 >      forall i:int. (i < u \/ l <= i) -> a2[i] = a1[i]
would mean that, given l <= u, if permut_sub a1 a2 l u, then a1 and a2 
are equal...

As Alan pointed out, permut_eq and the reflexive case of permut_sub 
assume different interpretations of "permut_sub", and thus either one or 
the other needs to be fixed. I still wonder: wouldn't it be a good idea 
to prove the lemma's in why3 theories?

Kind Regards, Benedikt



More information about the Why3-club mailing list