[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