map.MapPermut, array.ArrayPermut: incorporate new lemmas

Comment out the lemmas about symmetry of permutation:
they perturb our provers and are of little interest in
the case of successive array permutations.

modules/array.mlw

@@ -153,9 +153,8 @@ module ArrayPermut
   use import ArrayEq
 
   predicate exchange (a1 a2: array 'a) (i j: int) =
-    a1.length = a2.length /\ 0 <= i < a1.length /\ 0 <= j < a1.length /\
-    a1[i] = a2[j] /\ a1[j] = a2[i] /\
-    (forall k:int. 0 <= k < a1.length -> k <> i -> k <> j -> a1[k] = a2[k])
+    a1.length = a2.length /\
+    M.exchange a1.elts a2.elts 0 a1.length i j
   (** [exchange a1 a2 i j] means that arrays [a1] and [a2] only differ
       by the swapping of elements at indices [i] and [j] *)
 
@@ -179,29 +178,77 @@ module ArrayPermut
   (** [permut_all a1 a2 l u] is true when array [a1] is a permutation
       of array [a2]. *)
 
+  (** {3 lemmas about [permut_sub]} *)
+
+  (** permut_sub is reflexive, symmetric, transitive and contains
+      transpositions *)
+
+  lemma permut_sub_refl:
+    forall a: array 'a, l u: int.
+    0 <= l <= u <= length a -> permut_sub a a l u
+
+(*
+  lemma permut_sub_sym:
+    forall a1 a2: array 'a, l u: int.
+    permut_sub a1 a2 l u -> permut_sub a2 a1 l u
+*)
+
+  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
+
+  lemma exchange_permut_sub:
+    forall a1 a2: array 'a, i j l u: int.
+    exchange a1 a2 i j -> l <= i < u -> l <= j < u ->
+    0 <= l -> u <= length a1 -> permut_sub a1 a2 l u
+
+  lemma permut_sub_unmodified:
+    forall a1 a2: array 'a, l u: int.
+    permut_sub a1 a2 l u ->
+    forall i: int. (0 <= i < l \/ u <= i < length a1) -> a2[i] = a1[i]
+
+  (** we can always enlarge the interval *)
+
+  lemma permut_sub_weakening:
+    forall a1 a2: array 'a, l1 u1 l2 u2: int.
+    permut_sub a1 a2 l1 u1 -> 0 <= l2 <= l1 -> u1 <= u2 <= length a1 ->
+    permut_sub a1 a2 l2 u2
+
+  lemma permut_sub_compose:
+    forall a1 a2 a3: array 'a, l1 u1 l2 u2: int. u1 <= l2 ->
+    permut_sub a1 a2 l1 u1 ->
+    permut_sub a2 a3 l2 u2 ->
+    permut_sub a1 a3 l1 u2
+
+  (** {3 lemmas about [permut_all]} *)
+
+  (** permut_all is reflexive, symmetric, transitive and contains
+      transpositions *)
+
   lemma permut_all_refl:
     forall a: array 'a. permut_all a a
 
-  lemma exchange_permut_all:
-    forall a1 a2: array 'a, i j: int [exchange a1 a2 i j].
-    exchange a1 a2 i j -> permut_all a1 a2
-
+(*
   lemma permut_all_sym:
     forall a1 a2: array 'a.
     permut_all a1 a2 -> permut_all a2 a1
+*)
 
   lemma permut_all_trans:
     forall a1 a2 a3: array 'a.
     permut_all a1 a2 -> permut_all a2 a3 -> permut_all a1 a3
 
+  lemma exchange_permut_all:
+    forall a1 a2: array 'a, i j: int.
+    exchange a1 a2 i j -> permut_all a1 a2
+
+  (** identical arrays *)
+
   lemma array_eq_permut_all:
     forall a1 a2: array 'a.
     array_eq a1 a2 -> permut_all a1 a2
 
-  lemma permut_sub_weakening:
-    forall a1 a2: array 'a, l1 u1 l2 u2: int.
-    permut_sub a1 a2 l1 u1 -> 0 <= l2 <= l1 -> u1 <= u2 <= length a1 ->
-    permut_sub a1 a2 l2 u2
+  (** permutation on a sub-interval *)
 
   lemma permut_sub_permut_all:
     forall a1 a2: array 'a, l u: int.
@@ -219,8 +266,7 @@ module ArraySwap
     requires { 0 <= i < length a /\ 0 <= j < length a }
     writes   { a }
     ensures  { exchange (old a) a i j }
-    =
-    let v = a[i] in
+  = let v = a[i] in
     a[i] <- a[j];
     a[j] <- v
 

theories/map.why

@@ -91,7 +91,6 @@ theory MapInjection
 
 end
 
-
 (** {2 Map Permutation (indexed by integers)} *)
 theory MapPermut
 
@@ -99,6 +98,11 @@ theory MapPermut
   use import Map
   use import MapEq
 
+  predicate exchange (a1 a2: map int 'a) (l u i j: int) =
+    l <= i < u /\ l <= j < u /\
+    a1[i] = a2[j] /\ a1[j] = a2[i] /\
+    (forall k:int. l <= k < u -> k <> i -> k <> j -> a1[k] = a2[k])
+
   inductive permut (map int 'a) (map int 'a) int int =
   | permut_refl : (* a1[l..u[ and a2[l..u[ are identical *)
       forall a1 a2 : map int 'a. forall l u : int.
@@ -108,10 +112,7 @@ theory MapPermut
       permut a1 a2 l u -> permut a2 a3 l u -> permut a1 a3 l u
   | permut_exchange : (* elements at indices i and j have been swapped *)
       forall a1 a2 : map int 'a. forall l u i j : int.
-      l <= i < u -> l <= j < u -> i <> j ->
-      a1[i] = a2[j] -> a1[j] = a2[i] ->
-      (forall k:int. l <= k < u -> k <> i -> k <> j -> a1[k] = a2[k]) ->
-      permut a1 a2 l u
+      exchange a1 a2 l u i j -> permut a1 a2 l u
   (** [permut m1 m2 l u] is true when the segment
       [m1(l..u-1)] is a permutation of the segment [m2(l..u-1)].
       Values outside of the interval (l..u-1) are ignored.
@@ -119,27 +120,28 @@ theory MapPermut
       It is defined inductively as the smallest equivalence relation
       that contains the exchanges *)
 
+(*
   (* symmetry can be proved *)
   lemma permut_sym:
     forall a1 a2 : map int 'a. forall l u : int.
     permut a1 a2 l u -> permut a2 a1 l u
+*)
 
-  lemma permut_exchange_set :
-    forall a: map int 'a. forall l u i j: int.
-    l <= i < u -> l <= j < u -> permut a a[i <- a[j]][j <- a[i]] l u
+  lemma exchange_set :
+    forall a: map int 'a, l u i j: int.
+    l <= i < u -> l <= j < u ->
+    exchange a a[i <- a[j]][j <- a[i]] l u i j
 
   lemma permut_exists :
-    forall a1 a2: map int 'a. forall l u: int.
-    permut a1 a2 l u ->
-    forall i: int. l <= i < u ->
-    exists j: int. l <= j < u /\ a2[i] = a1[j]
+    forall a1 a2: map int 'a, l u i: int.
+    permut a1 a2 l u -> l <= i < u ->
+    exists j: int. l <= j < u /\ a1[j] = a2[i]
 
-(*
+(* THIS IS FALSE WHEN m < l < u
   lemma permut_concat:
     forall a1 a2: map int 'a, l m u: int.
     permut a1 a2 l m -> permut a1 a2 m u -> permut a1 a2 l u
 *)
-
 end
 
 (** {2 Sum of elements of a map (indexed by integers)} *)