[Why3-club] permut_trans

Jean-Jacques Levy jean-jacques.levy at inria.fr
Tue Mar 18 09:21:11 CET 2014

Dear Why3 Friends,

in 0.83, ‘permut_trans’ is defined in ‘theories.map’ but not in ‘modules.array’. 

It seems the provers jump to ‘permut_trans’ in maps and forget to try it in arrays. But when added for arrays, the provers find it. 

What’s about adding ‘permut_trans' to 'modules.array' with simple (provable) lemma ?
lemma permut_sub_trans:
  forall a1 a2 a3: array 'a, l u: int.
  permut_sub a1 a2 l u -> permut_sub a2 a3 l u -> 
  permut_sub a1 a3 l u
(in fact, I’m still not getting why 'theories.map’ is needed for arrays, but I must be wrong... )

Best, -JJ-

More information about the Why3-club mailing list