quicksort proof in progress

examples/programs/quicksort.mlw

@@ -38,8 +38,10 @@ module Quicksort
       quick_rec t l (!m - 1);
       quick_rec t (!m + 1) r
     end end
-    { (l <= r /\ sorted_sub t l (r+1) /\ permut_sub t (old t) l (r+1)) \/
-      (l > r /\ array_eq t (old t)) }
+    { sorted_sub t l (r+1) /\ permut_sub t (old t) l (r+1)
+      (***
+      (l <= r /\ sorted_sub t l (r+1) /\ permut_sub t (old t) l (r+1)) \/
+      (l > r /\ array_eq t (old t)) ***) }
 
   let quicksort (t : array int) =
     { }

examples/programs/quicksort/quicksort_WP_Quicksort_WP_parameter_quick_rec_2.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Definition unit  := unit.
+
+Parameter mark : Type.
+
+Parameter at1: forall (a:Type), a -> mark  -> a.
+
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a  -> a.
+
+Implicit Arguments old.
+
+Inductive ref (a:Type) :=
+  | mk_ref : a -> ref a.
+Implicit Arguments mk_ref.
+
+Definition contents (a:Type)(u:(ref a)): a :=
+  match u with
+  | mk_ref contents1 => contents1
+  end.
+Implicit Arguments contents.
+
+Parameter map : forall (a:Type) (b:Type), Type.
+
+Parameter get: forall (a:Type) (b:Type), (map a b) -> a  -> b.
+
+Implicit Arguments get.
+
+Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b  -> (map a b).
+
+Implicit Arguments set.
+
+Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
+  a2) = b1).
+
+Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
+  a2) = (get m a2)).
+
+Parameter const: forall (b:Type) (a:Type), b  -> (map a b).
+
+Set Contextual Implicit.
+Implicit Arguments const.
+Unset Contextual Implicit.
+
+Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
+  b1):(map a b)) a1) = b1).
+
+Inductive array (a:Type) :=
+  | mk_array : Z -> (map Z a) -> array a.
+Implicit Arguments mk_array.
+
+Definition elts (a:Type)(u:(array a)): (map Z a) :=
+  match u with
+  | mk_array _ elts1 => elts1
+  end.
+Implicit Arguments elts.
+
+Definition length (a:Type)(u:(array a)): Z :=
+  match u with
+  | mk_array length1 _ => length1
+  end.
+Implicit Arguments length.
+
+Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
+Implicit Arguments get1.
+
+Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
+  match a1 with
+  | mk_array xcl0 _ => (mk_array xcl0 (set (elts a1) i v))
+  end.
+Implicit Arguments set1.
+
+Definition sorted_sub(a:(map Z Z)) (l:Z) (u:Z): Prop := forall (i1:Z) (i2:Z),
+  (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 <  u)%Z) -> ((get a i1) <= (get a
+  i2))%Z.
+
+Definition sorted_sub1(a:(array Z)) (l:Z) (u:Z): Prop := (sorted_sub (elts a)
+  l u).
+
+Definition sorted(a:(array Z)): Prop := (sorted_sub (elts a) 0%Z (length a)).
+
+Definition map_eq_sub (a:Type)(a1:(map Z a)) (a2:(map Z a)) (l:Z)
+  (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i <  u)%Z) -> ((get a1
+  i) = (get a2 i)).
+Implicit Arguments map_eq_sub.
+
+Definition exchange (a:Type)(a1:(map Z a)) (a2:(map Z a)) (i:Z)
+  (j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1 j)) /\
+  forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2 k))).
+Implicit Arguments exchange.
+
+Axiom exchange_set : forall (a:Type), forall (a1:(map Z a)), forall (i:Z)
+  (j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i j).
+
+Inductive permut_sub{a:Type}  : (map Z a) -> (map Z a) -> Z -> Z -> Prop :=
+  | permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
+      (map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u)
+  | permut_sym : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
+      (permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u)
+  | permut_trans : forall (a1:(map Z a)) (a2:(map Z a)) (a3:(map Z a)),
+      forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> ((permut_sub a2 a3 l
+      u) -> (permut_sub a1 a3 l u))
+  | permut_exchange : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z)
+      (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i <  u)%Z) -> (((l <= j)%Z /\
+      (j <  u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 a2 l u))).
+Implicit Arguments permut_sub.
+
+Axiom permut_weakening : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z
+  a)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\
+  (r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)).
+
+Axiom permut_eq : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)),
+  forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((i <  l)%Z \/
+  (u <= i)%Z) -> ((get a2 i) = (get a1 i)).
+
+Axiom permut_exists : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)),
+  forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\
+  (i <  u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j <  u)%Z) /\ ((get a2
+  i) = (get a1 j)).
+
+Definition exchange1 (a:Type)(a1:(array a)) (a2:(array a)) (i:Z)
+  (j:Z): Prop := (exchange (elts a1) (elts a2) i j).
+Implicit Arguments exchange1.
+
+Definition permut_sub1 (a:Type)(a1:(array a)) (a2:(array a)) (l:Z)
+  (u:Z): Prop := (permut_sub (elts a1) (elts a2) l u).
+Implicit Arguments permut_sub1.
+
+Definition permut (a:Type)(a1:(array a)) (a2:(array a)): Prop :=
+  ((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2) 0%Z
+  (length a1)).
+Implicit Arguments permut.
+
+Axiom exchange_permut : forall (a:Type), forall (a1:(array a)) (a2:(array a))
+  (i:Z) (j:Z), (exchange1 a1 a2 i j) -> (((length a1) = (length a2)) ->
+  (((0%Z <= i)%Z /\ (i <  (length a1))%Z) -> (((0%Z <= j)%Z /\
+  (j <  (length a1))%Z) -> (permut a1 a2)))).
+
+Definition array_eq_sub (a:Type)(a1:(array a)) (a2:(array a)) (l:Z)
+  (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u).
+Implicit Arguments array_eq_sub.
+
+Definition array_eq (a:Type)(a1:(array a)) (a2:(array a)): Prop :=
+  ((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z (length a1)).
+Implicit Arguments array_eq.
+
+Axiom array_eq_sub_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
+  a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l u) -> (permut_sub1 a1 a2 l u).
+
+Axiom array_eq_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
+  a)), (array_eq a1 a2) -> (permut a1 a2).
+
+Theorem WP_parameter_quick_rec : forall (t:Z), forall (l:Z), forall (r:Z),
+  forall (t1:(map Z Z)), ((0%Z <= l)%Z /\ (r <  t)%Z) -> ((l <  r)%Z ->
+  (((0%Z <= l)%Z /\ (l <  t)%Z) -> let result := (get t1 l) in
+  (((l + 1%Z)%Z <= r)%Z -> forall (m:Z), forall (t2:(map Z Z)),
+  ((forall (j:Z), ((l <  j)%Z /\ (j <= m)%Z) -> ((get t2 j) <  result)%Z) /\
+  ((forall (j:Z), ((m <  j)%Z /\ (j <  (r + 1%Z)%Z)%Z) -> (result <= (get t2
+  j))%Z) /\ ((permut_sub t2 t1 l (r + 1%Z)%Z) /\ (((get t2 l) = result) /\
+  ((l <= m)%Z /\ (m <  (r + 1%Z)%Z)%Z))))) -> ((((0%Z <= l)%Z /\
+  (l <  t)%Z) /\ ((0%Z <= m)%Z /\ (m <  t)%Z)) -> forall (t3:(map Z Z)),
+  (exchange t3 t2 l m) -> ((((0%Z <= ((1%Z + r)%Z - l)%Z)%Z /\
+  (((1%Z + (m - 1%Z)%Z)%Z - l)%Z <  ((1%Z + r)%Z - l)%Z)%Z) /\
+  ((0%Z <= l)%Z /\ ((m - 1%Z)%Z <  t)%Z)) -> forall (t4:(map Z Z)),
+  ((sorted_sub t4 l ((m - 1%Z)%Z + 1%Z)%Z) /\ (permut_sub t4 t3 l
+  ((m - 1%Z)%Z + 1%Z)%Z)) -> ((((0%Z <= ((1%Z + r)%Z - l)%Z)%Z /\
+  (((1%Z + r)%Z - (m + 1%Z)%Z)%Z <  ((1%Z + r)%Z - l)%Z)%Z) /\
+  ((0%Z <= (m + 1%Z)%Z)%Z /\ (r <  t)%Z)) -> forall (t5:(map Z Z)),
+  ((sorted_sub t5 (m + 1%Z)%Z (r + 1%Z)%Z) /\ (permut_sub t5 t4 (m + 1%Z)%Z
+  (r + 1%Z)%Z)) -> ((sorted_sub t5 l (r + 1%Z)%Z) /\ (permut_sub t5 t1 l
+  (r + 1%Z)%Z)))))))).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros n l r t1.
+intros (hl, hr) hlr hl2 v hlr2.
+intros m t2 (inv1, (inv2, (inv3, (inv4, inv5)))).
+intros (_, hm) t3 exch.
+intros _ t4 (lsorted, lpermut).
+intros _ t5 (rsorted, rpermut).
+split.
+(* sorted *)
+red; intros.
+assert (h: (l <= i1 < m \/ m <= i1 <= r)%Z) by omega. destruct h.
+assert (h: (l <= i2 < m \/ m <= i2 <= r)%Z) by omega. destruct h.
+assert (eq: get t4 i1 = get t5 i1).
+apply permut_eq with (m+1)%Z (r+1)%Z; auto.
+omega.
+rewrite <- eq; clear eq.
+assert (eq: get t4 i2 = get t5 i2).
+apply permut_eq with (m+1)%Z (r+1)%Z; auto.
+omega.
+rewrite <- eq; clear eq.
+apply lsorted; omega.
+assert (vi1: (get t5 i1 < v)%Z).
+assert (eq: get t4 i1 = get t5 i1).
+apply permut_eq with (m+1)%Z (r+1)%Z; auto.
+omega.
+rewrite <- eq; clear eq.
+assert (exists i3:Z, l <= i3 < m-1+1 /\ get t4 i1 = get t3 i3)%Z.
+apply permut_exists.
+apply permut_sym; auto.
+omega.
+destruct H2 as (i3, (hi3, eq3)).
+rewrite eq3; clear eq3.
+assert (case: (i3 = l \/ l < i3)%Z) by omega. destruct case.
+subst i3.
+destruct exch as (h,_). rewrite h.
+apply inv1; omega.
+destruct exch as (_,(_,h)). rewrite h; try omega.
+apply inv1; omega.
+assert (vi2: (v <= get t5 i2)%Z).
+
+(* TODO*) admit. admit. admit.
+
+(* permut *)
+apply permut_trans with t4.
+apply permut_weakening with (m+1)%Z (r+1)%Z; auto.
+omega.
+apply permut_trans with t3.
+apply permut_weakening with l (m-1+1)%Z; auto.
+omega.
+apply permut_trans with t2; auto.
+apply permut_exchange with l m; auto.
+omega.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/quicksort/why3session.xml

@@ -3,180 +3,198 @@
 <why3session name="examples/programs/quicksort/why3session.xml">
  <file name="../quicksort.mlw" verified="false" expanded="true">
   <theory name="WP Quicksort" verified="false" expanded="true">
-   <goal name="WP_parameter swap" expl="correctness of parameter swap" sum="6177fbb045afcf4dbfe918aa3a4337ee" proved="true" expanded="true">
+   <goal name="WP_parameter swap" expl="correctness of parameter swap" sum="41390d74df59a170f969e943142ebb7b" proved="true" expanded="false">
     <proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.04"/>
     </proof>
    </goal>
-   <goal name="WP_parameter quick_rec" expl="correctness of parameter quick_rec" sum="33da4af0e03d306ea4861ba8983ee47a" proved="false" expanded="true">
+   <goal name="WP_parameter quick_rec" expl="correctness of parameter quick_rec" sum="2f04ccb117a031bd5daf3e98f89776c0" proved="false" expanded="true">
     <transf name="split_goal" proved="false" expanded="true">
-     <goal name="WP_parameter quick_rec.1" expl="precondition" sum="406d10654eb3a0e3153a5154e1416295" proved="true" expanded="true">
+     <goal name="WP_parameter quick_rec.1" expl="precondition" sum="2128872765b9e63529d56c8f00f741cf" proved="true" expanded="false">
       <proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
-       <result status="valid" time="0.02"/>
+       <result status="valid" time="0.03"/>
       </proof>
      </goal>
-     <goal name="WP_parameter quick_rec.2" expl="precondition" sum="f2219051933746e17a42c36018543678" proved="true" expanded="true">
-      <proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
-       <result status="valid" time="0.01"/>
+     <goal name="WP_parameter quick_rec.2" expl="precondition" sum="a92145a59251cade4bb1f55edce63318" proved="true" expanded="false">
+      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+       <result status="valid" time="0.02"/>
       </proof>
      </goal>
-     <goal name="WP_parameter quick_rec.3" expl="precondition" sum="10ef2a9d59686b359aa70d47cff8a53c" proved="true" expanded="true">
+     <goal name="WP_parameter quick_rec.3" expl="precondition" sum="62a92bc5b3bcc29f4214850e701bf5c6" proved="true" expanded="false">
       <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.01"/>
+       <result status="valid" time="0.03"/>
       </proof>
      </goal>
-     <goal name="WP_parameter quick_rec.4" expl="precondition" sum="a318468fc8062152bff539867913bb29" proved="true" expanded="true">
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+     <goal name="WP_parameter quick_rec.4" expl="precondition" sum="11fcbd195bdee57e10dda0553e6067e8" proved="true" expanded="false">
+      <proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
      </goal>
-     <goal name="WP_parameter quick_rec.5" expl="normal postcondition" sum="effb9ac6c1ee8132f333e6b98224f429" proved="true" expanded="true">
-      <transf name="split_goal" proved="true" expanded="true">
-       <goal name="WP_parameter quick_rec.5.1" expl="normal postcondition" sum="effb9ac6c1ee8132f333e6b98224f429" proved="true" expanded="true">
-        <proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
-         <result status="valid" time="0.02"/>
-        </proof>
-       </goal>
-      </transf>
-     </goal>
-     <goal name="WP_parameter quick_rec.6" expl="for loop initialization" sum="427cf244289471467b5d4eeb83987f39" proved="true" expanded="true">
+     <goal name="WP_parameter quick_rec.5" expl="normal postcondition" sum="253f3ac4e7d9985a21253ab65216f753" proved="true" expanded="false">
       <proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
-       <result status="valid" time="0.01"/>
+       <result status="valid" time="0.03"/>
+      </proof>
+     </goal>
+     <goal name="WP_parameter quick_rec.6" expl="for loop initialization" sum="33fdbbac9132a019ef34e8f4a691dfd2" proved="true" expanded="false">
+      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+       <result status="valid" time="0.03"/>
       </proof>
      </goal>
-     <goal name="WP_parameter quick_rec.7" expl="for loop preservation" sum="07ab46cd0c0ee28eb4d1f08cc02f2c8d" proved="true" expanded="true">
-      <transf name="split_goal" proved="true" expanded="true">
-       <goal name="WP_parameter quick_rec.7.1" expl="for loop preservation" sum="4ea12c8c31265a91a505243d49d45967" proved="true" expanded="true">
+     <goal name="WP_parameter quick_rec.7" expl="for loop preservation" sum="bbb5a3e612f28c69d77eda6dcfdab469" proved="true" expanded="false">
+      <transf name="split_goal" proved="true" expanded="false">
+       <goal name="WP_parameter quick_rec.7.1" expl="for loop preservation" sum="655f80290f02065c5c6491b70cf5d87f" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
-         <result status="valid" time="0.01"/>
+         <result status="valid" time="0.03"/>
         </proof>
        </goal>
-       <goal name="WP_parameter quick_rec.7.2" expl="for loop preservation" sum="18ad8cb0f70f2f58845a2e754bdccf9d" proved="true" expanded="true">
+       <goal name="WP_parameter quick_rec.7.2" expl="for loop preservation" sum="47a4757bb36ca6b1da1c9fc0d9300996" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
          <result status="valid" time="0.02"/>
         </proof>
        </goal>
-       <goal name="WP_parameter quick_rec.7.3" expl="for loop preservation" sum="911ce471e4e03d6d518859114b506ad1" proved="true" expanded="true">
+       <goal name="WP_parameter quick_rec.7.3" expl="for loop preservation" sum="daefec39dc532fc5f75c60d25b05c860" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
-         <result status="valid" time="0.02"/>
+         <result status="valid" time="0.06"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter quick_rec.7.4" expl="for loop preservation" sum="8365add859b7fc6b7751cebaae7998df" proved="true" expanded="false">
+        <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.06"/>
         </proof>
        </goal>
-       <goal name="WP_parameter quick_rec.7.4" expl="for loop preservation" sum="b450261e5bd6ca2d661e97802ff609af" proved="true" expanded="true">
+       <goal name="WP_parameter quick_rec.7.5" expl="for loop preservation" sum="abad3a5259827b8db9c93975900c4e92" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
-         <result status="valid" time="0.04"/>
+         <result status="valid" time="0.38"/>
         </proof>
        </goal>
-       <goal name="WP_parameter quick_rec.7.5" expl="for loop preservation" sum="08076db715ad6104e661bba5924b914d" proved="true" expanded="true">
+       <goal name="WP_parameter quick_rec.7.6" expl="for loop preservation" sum="cf16f95c99beac80f39e0911ca1e2782" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
-         <result status="valid" time="0.24"/>
+         <result status="valid" time="0.03"/>
         </proof>
        </goal>
-       <goal name="WP_parameter quick_rec.7.6" expl="for loop preservation" sum="9b73c6a9f6e082107f9baebb2c8eed55" proved="true" expanded="true">
+       <goal name="WP_parameter quick_rec.7.7" expl="for loop preservation" sum="e0afe3b0f7f1ea30444b356e06cc0d54" proved="true" expanded="false">
+        <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.03"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter quick_rec.7.8" expl="for loop preservation" sum="eb4f74147248cfd954499ebcff54f851" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
          <result status="valid" time="0.02"/>
         </proof>
        </goal>
-       <goal name="WP_parameter quick_rec.7.7" expl="for loop preservation" sum="41c7cd211f59e59e68518f917d9f7701" proved="true" expanded="true">
+       <goal name="WP_parameter quick_rec.7.9" expl="for loop preservation" sum="f82e3d55421de136ef70daa1f9d54cbf" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
          <result status="valid" time="0.02"/>
         </proof>
        </goal>
-       <goal name="WP_parameter quick_rec.7.8" expl="for loop preservation" sum="858a8d8e1012e8548515b56508208231" proved="true" expanded="true">
+       <goal name="WP_parameter quick_rec.7.10" expl="for loop preservation" sum="5110d3e06851da1bccd8a887c56fbeb1" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
          <result status="valid" time="0.02"/>
         </proof>
        </goal>
-       <goal name="WP_parameter quick_rec.7.9" expl="for loop preservation" sum="95e2e45c6127a7271638547bcfb5e046" proved="true" expanded="true">
+       <goal name="WP_parameter quick_rec.7.11" expl="for loop preservation" sum="8c4889f9e3a75e8d50a770bfbdbcd53b" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
          <result status="valid" time="0.02"/>
         </proof>
        </goal>
-       <goal name="WP_parameter quick_rec.7.10" expl="for loop preservation" sum="929c3b1abcacff2aede569f8b49f7b4f" proved="true" expanded="true">
+       <goal name="WP_parameter quick_rec.7.12" expl="for loop preservation" sum="84ca83db53a372b70b313ba907dc1335" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
          <result status="valid" time="0.02"/>
         </proof>
        </goal>
-       <goal name="WP_parameter quick_rec.7.11" expl="for loop preservation" sum="ee911edbd6e4c05aa8f2ed082f7b1b22" proved="true" expanded="true">
+       <goal name="WP_parameter quick_rec.7.13" expl="for loop preservation" sum="504e1a24f4602e12e5ba828192b7afd1" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
          <result status="valid" time="0.02"/>
         </proof>
        </goal>
-       <goal name="WP_parameter quick_rec.7.12" expl="for loop preservation" sum="66f69655c8bf2711379369eb6821d574" proved="true" expanded="true">
+       <goal name="WP_parameter quick_rec.7.14" expl="for loop preservation" sum="d3533190a9683b687debd0dc4439ce2f" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
          <result status="valid" time="0.02"/>
         </proof>
        </goal>
-       <goal name="WP_parameter quick_rec.7.13" expl="for loop preservation" sum="b089bc56dc2ed0cdd184619815c8845e" proved="true" expanded="true">
+      </transf>
+     </goal>
+     <goal name="WP_parameter quick_rec.8" expl="precondition" sum="930dcb0361ff734c776ac152a8ba2cd6" proved="true" expanded="false">
+      <transf name="split_goal" proved="true" expanded="false">
+       <goal name="WP_parameter quick_rec.8.1" expl="correctness of parameter quick_rec" sum="102e4dccb9780aadbf336a18ff05b181" proved="true" expanded="false">
+        <proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
+         <result status="valid" time="0.02"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter quick_rec.8.2" expl="correctness of parameter quick_rec" sum="3175fe7d96c78faf53f4d06650326f8f" proved="true" expanded="false">
+        <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+         <result status="valid" time="0.03"/>
+        </proof>
+       </goal>
+       <goal name="WP_parameter quick_rec.8.3" expl="correctness of parameter quick_rec" sum="527f992b83556919e8162b855e12da31" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
-         <result status="valid" time="0.01"/>
+         <result status="valid" time="0.02"/>
         </proof>
        </goal>
-       <goal name="WP_parameter quick_rec.7.14" expl="for loop preservation" sum="1a88a3685706218b200f35ea848bd4c6" proved="true" expanded="true">
+       <goal name="WP_parameter quick_rec.8.4" expl="correctness of parameter quick_rec" sum="25c732cfdffb9bfb3dda9fe5f3348cf6" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
          <result status="valid" time="0.02"/>
         </proof>
        </goal>
       </transf>
      </goal>
-     <goal name="WP_parameter quick_rec.8" expl="precondition" sum="9190ad77db4576960cadd05a2499cb61" proved="true" expanded="true">
-      <proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
-       <result status="valid" time="0.02"/>
-      </proof>
-     </goal>
-     <goal name="WP_parameter quick_rec.9" expl="precondition" sum="e37d265f6cba539592d2bd29fc4fcc17" proved="true" expanded="true">
+     <goal name="WP_parameter quick_rec.9" expl="precondition" sum="cc4134c28e8e9547e93a966e9bd06657" proved="true" expanded="false">
       <proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
-       <result status="valid" time="0.02"/>
+       <result status="valid" time="0.05"/>
       </proof>
      </goal>
-     <goal name="WP_parameter quick_rec.10" expl="precondition" sum="49966da3f6ce0f3a491a4b8853960bbf" proved="true" expanded="true">
-      <transf name="split_goal" proved="true" expanded="true">
-       <goal name="WP_parameter quick_rec.10.1" expl="correctness of parameter quick_rec" sum="cfbbf230a65e5d494b3562815841ed69" proved="true" expanded="true">
+     <goal name="WP_parameter quick_rec.10" expl="precondition" sum="18f26feed6123bee3894cecc6a784daa" proved="true" expanded="false">
+      <transf name="split_goal" proved="true" expanded="false">
+       <goal name="WP_parameter quick_rec.10.1" expl="correctness of parameter quick_rec" sum="61b027ec1e8bc663410d16f7168fa884" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
          <result status="valid" time="0.02"/>
         </proof>
        </goal>
-       <goal name="WP_parameter quick_rec.10.2" expl="correctness of parameter quick_rec" sum="e3d82586cc9da3bf50ca6fbd07f1744c" proved="true" expanded="true">
+       <goal name="WP_parameter quick_rec.10.2" expl="correctness of parameter quick_rec" sum="a962b4be8e9da1a5937ea90da805e2eb" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
-         <result status="valid" time="0.02"/>
+         <result status="valid" time="0.03"/>
         </proof>
        </goal>
-       <goal name="WP_parameter quick_rec.10.3" expl="correctness of parameter quick_rec" sum="fa2f9f5a725f918d0d710645cac645b1" proved="true" expanded="true">
+       <goal name="WP_parameter quick_rec.10.3" expl="correctness of parameter quick_rec" sum="0a0de4d9d70e705c6c853294f61853bc" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
-         <result status="valid" time="0.02"/>
+         <result status="valid" time="0.03"/>
         </proof>
        </goal>
-       <goal name="WP_parameter quick_rec.10.4" expl="correctness of parameter quick_rec" sum="1d6a7b2f1f81b8ef6ab988d51b850faf" proved="true" expanded="true">
+       <goal name="WP_parameter quick_rec.10.4" expl="correctness of parameter quick_rec" sum="b583af5f63b8fc08897dbe7631e07f0d" proved="true" expanded="false">
         <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
-         <result status="valid" time="0.01"/>
+         <result status="valid" time="0.03"/>
         </proof>
        </goal>
       </transf>
      </goal>
-     <goal name="WP_parameter quick_rec.11" expl="normal postcondition" sum="36e6ec9c499a1e91838afe1b8b2e0eaa" proved="false" expanded="true">
+     <goal name="WP_parameter quick_rec.11" expl="normal postcondition" sum="dc6640f4ea90f410552d83809f223c48" proved="false" expanded="true">
+      <proof prover="coq" timelimit="10" edited="quicksort_WP_Quicksort_WP_parameter_quick_rec_1.v" obsolete="false"><undone/>
+       
+      </proof>
      </goal>
-     <goal name="WP_parameter quick_rec.12" expl="normal postcondition" sum="25de8b5856d6ddd6e4d28d31313ffcb9" proved="true" expanded="true">
+     <goal name="WP_parameter quick_rec.12" expl="normal postcondition" sum="deb726a67cafda30fb8280d213d8720f" proved="true" expanded="false">
       <proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
-       <result status="valid" time="0.03"/>
+       <result status="valid" time="0.06"/>
       </proof>
      </goal>
     </transf>
    </goal>
-   <goal name="WP_parameter quicksort" expl="correctness of parameter quicksort" sum="fb3352351bc2938392247b070b73ab2b" proved="true" expanded="true">
-    <transf name="split_goal" proved="true" expanded="true">
-     <goal name="WP_parameter quicksort.1" expl="precondition" sum="b99a9c90c7ca121192728f342615c25d" proved="true" expanded="true">
+   <goal name="WP_parameter quicksort" expl="correctness of parameter quicksort" sum="e9e88b245a388202b4da5d4ac52614dd" proved="true" expanded="false">
+    <transf name="split_goal" proved="true" expanded="false">
+     <goal name="WP_parameter quicksort.1" expl="precondition" sum="f4f0efc9e37dec6a59b47985d7604518" proved="true" expanded="false">
       <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
      </goal>
-     <goal name="WP_parameter quicksort.2" expl="normal postcondition" sum="e6fb9fda57d1131f269e8a2450335abc" proved="true" expanded="true">
+     <goal name="WP_parameter quicksort.2" expl="normal postcondition" sum="b6245460d33e307fee79e69ec7c5ea72" proved="true" expanded="false">
       <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.02"/>
+       <result status="valid" time="0.03"/>
       </proof>
       <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.05"/>
+       <result status="valid" time="0.07"/>
       </proof>
       <proof prover="z3" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.04"/>
+       <result status="valid" time="0.06"/>
       </proof>
      </goal>
     </transf>

theories/map.why

@@ -106,7 +106,7 @@ theory MapPermut
 
   lemma permut_eq :
     forall a1 a2 : map int 'a. forall l u : int.
-    l <= u -> permut_sub a1 a2 l u ->
+    permut_sub a1 a2 l u ->
     forall i:int. (i < l \/ u <= i) -> a2[i] = a1[i]
 
   lemma permut_exists :