Fixed and proved theory list

2eb4ca28 · Léon Gondelman · 1975bbfd · 2eb4ca28 · 2eb4ca28 · 2eb4ca28
Commit 2eb4ca28 authored Sep 18, 2014 by Léon Gondelman
30 changed files
--- a/examples/cursor/why3session.xml
+++ b/examples/cursor/why3session.xml
@@ -41,7 +41,7 @@
 </transf>
 </goal>
 </theory>
-<theory name="IntListCursor" sum="6a86c159c9325e79070f5efce8debf6a">
+<theory name="IntListCursor" sum="3be4879452794a876cc462ddd755a3de">
 <goal name="WP_parameter create" expl="VC for create">
 <proof prover="1"><result status="valid" time="0.02"/></proof>
 </goal>
@@ -52,7 +52,7 @@
 <proof prover="1"><result status="valid" time="0.02"/></proof>
 </goal>
 </theory>
-<theory name="TestListCursor" sum="650f68ba6185c1da3bf7ea3cb4c3d7e3">
+<theory name="TestListCursor" sum="c8893f4016f1f1e3c221e4142f94eed3">
 <goal name="WP_parameter list_sum" expl="VC for list_sum">
 <transf name="split_goal_wp">
  <goal name="WP_parameter list_sum.1" expl="1. loop invariant init">
@@ -85,7 +85,7 @@
 </transf>
 </goal>
 </theory>
-<theory name="IntArrayCursor" sum="5e45c85fd72714bc8c3150cb7084a6c1" expanded="true">
+<theory name="IntArrayCursor" sum="c77cddb83b83b50f0453ae017ebaaabf" expanded="true">
 <goal name="WP_parameter create" expl="VC for create">
 <proof prover="1"><result status="valid" time="0.01"/></proof>
 </goal>
@@ -126,7 +126,7 @@
 </transf>
 </goal>
 </theory>
-<theory name="TestArrayCursor" sum="6c32bfa8b7b8e063fd2046eb493d82bf">
+<theory name="TestArrayCursor" sum="1818e28aa2ccadd10a21d99b8b296439">
 <goal name="WP_parameter array_sum_array_to_list" expl="VC for array_sum_array_to_list">
 <proof prover="1"><result status="valid" time="0.04"/></proof>
 </goal>

--- a/examples/cursor/why3shapes.gz
+++ b/examples/cursor/why3shapes.gz
--- a/examples/finite_tarski/why3shapes.gz
+++ b/examples/finite_tarski/why3shapes.gz
--- a/examples/insertion_sort_list.mlw
+++ b/examples/insertion_sort_list.mlw
@@ -7,7 +7,9 @@ module InsertionSort
  predicate le elt elt

  clone relations.TotalPreOrder with type t = elt, predicate rel = le
-  clone export list.Sorted      with type t = elt, predicate le  = le
+  clone export list.Sorted      with type t = elt, predicate le  = le,
+   goal Transitive.Trans
+
  use import list.List
  use import list.Permut


--- a/examples/insertion_sort_list/why3session.xml
+++ b/examples/insertion_sort_list/why3session.xml
@@ -5,7 +5,10 @@
 <prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="10" memlimit="1000"/>
 <prover id="1" name="CVC4" version="1.3" timelimit="10" memlimit="1000"/>
 <file name="../insertion_sort_list.mlw" expanded="true">
-<theory name="InsertionSort" sum="a68ab62da2fba48733e0e9f8699021f8" expanded="true">
+<theory name="InsertionSort" sum="18eee291d33ec7eb040007ff367abb3c" expanded="true">
+ <goal name="Transitive.Trans" expanded="true">
+ <proof prover="0" timelimit="5"><result status="valid" time="0.01"/></proof>
+ </goal>
 <goal name="WP_parameter insert" expl="VC for insert" expanded="true">
 <transf name="split_goal_wp" expanded="true">
  <goal name="WP_parameter insert.1" expl="1. postcondition">
@@ -27,10 +30,10 @@
  <proof prover="0"><result status="valid" time="0.03"/></proof>
  </goal>
  <goal name="WP_parameter insert.7" expl="7. postcondition">
-  <proof prover="0"><result status="valid" time="0.50"/></proof>
+  <proof prover="0"><result status="valid" time="0.58"/></proof>
  </goal>
  <goal name="WP_parameter insert.8" expl="8. postcondition" expanded="true">
-  <proof prover="1"><result status="valid" time="0.20"/></proof>
+  <proof prover="1"><result status="valid" time="0.42"/></proof>
  </goal>
 </transf>
 </goal>

--- a/examples/insertion_sort_list/why3shapes.gz
+++ b/examples/insertion_sort_list/why3shapes.gz
--- a/examples/linked_list_rev/why3session.xml
+++ b/examples/linked_list_rev/why3session.xml
@@ -4,30 +4,26 @@
 <why3session shape_version="4">
 <prover id="0" name="Coq" version="8.4pl4" timelimit="5" memlimit="0"/>
 <prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="4000"/>
-<prover id="2" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="0"/>
-<prover id="3" name="Z3" version="2.19" timelimit="5" memlimit="0"/>
-<prover id="4" name="CVC3" version="2.2" timelimit="5" memlimit="0"/>
-<prover id="5" name="Z3" version="3.2" timelimit="5" memlimit="4000"/>
-<prover id="6" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="4000"/>
-<prover id="7" name="CVC4" version="1.3" timelimit="5" memlimit="4000"/>
+<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="4000"/>
+<prover id="3" name="CVC4" version="1.3" timelimit="5" memlimit="4000"/>
 <file name="../linked_list_rev.mlw" expanded="true">
 <theory name="ListReverse" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
 </theory>
-<theory name="InPlaceRev" sum="3c1c96a3f0506ade10b9b7f2051e8742" expanded="true">
+<theory name="InPlaceRev" sum="fd2061728df4ef10ceafdbfcc7847ac8" expanded="true">
 <goal name="list_seg_frame" expanded="true">
- <proof prover="0" edited="linked_list_rev_WP_InPlaceRev_list_seg_frame_1.v"><result status="valid" time="1.13"/></proof>
+ <proof prover="0" edited="linked_list_rev_WP_InPlaceRev_list_seg_frame_1.v" obsolete="true"><result status="valid" time="1.13"/></proof>
 </goal>
 <goal name="list_seg_functional" expanded="true">
- <proof prover="0" edited="linked_list_rev_WP_InPlaceRev_list_seg_functional_1.v"><result status="valid" time="1.08"/></proof>
+ <proof prover="0" edited="linked_list_rev_WP_InPlaceRev_list_seg_functional_1.v" obsolete="true"><result status="valid" time="1.08"/></proof>
 </goal>
 <goal name="list_seg_sublistl" expanded="true">
- <proof prover="0" edited="linked_list_rev_WP_InPlaceRev_list_seg_sublistl_1.v"><result status="valid" time="1.05"/></proof>
+ <proof prover="0" edited="linked_list_rev_WP_InPlaceRev_list_seg_sublistl_1.v" obsolete="true"><result status="valid" time="1.05"/></proof>
 </goal>
 <goal name="list_seg_no_repet" expanded="true">
- <proof prover="0" edited="linked_list_rev_WP_InPlaceRev_list_seg_no_repet_1.v"><result status="valid" time="1.07"/></proof>
+ <proof prover="0" edited="linked_list_rev_WP_InPlaceRev_list_seg_no_repet_1.v" obsolete="true"><result status="valid" time="1.07"/></proof>
 </goal>
- <goal name="WP_parameter in_place_reverse" expl="VC for in_place_reverse" expanded="true">
- <transf name="split_goal_wp" expanded="true">
+ <goal name="WP_parameter in_place_reverse" expl="VC for in_place_reverse">
+ <transf name="split_goal_wp">
  <goal name="WP_parameter in_place_reverse.1" expl="1. loop invariant init">
  <proof prover="2" memlimit="1000"><result status="valid" time="0.02"/></proof>
  </goal>
@@ -39,36 +35,28 @@
  </goal>
  <goal name="WP_parameter in_place_reverse.4" expl="4. loop invariant init">
  <proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
-  <proof prover="3"><result status="valid" time="0.02"/></proof>
-  <proof prover="4"><result status="valid" time="0.01"/></proof>
-  <proof prover="5" memlimit="0"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="WP_parameter in_place_reverse.5" expl="5. assertion">
-  <proof prover="2"><result status="valid" time="0.20"/></proof>
+  <proof prover="2" memlimit="1000"><result status="valid" time="0.36"/></proof>
  </goal>
  <goal name="WP_parameter in_place_reverse.6" expl="6. loop invariant preservation">
-  <proof prover="2" memlimit="1000"><result status="valid" time="0.19"/></proof>
+  <proof prover="2" memlimit="1000"><result status="valid" time="0.33"/></proof>
  </goal>
  <goal name="WP_parameter in_place_reverse.7" expl="7. loop invariant preservation">
-  <proof prover="2" memlimit="1000"><result status="valid" time="0.09"/></proof>
+  <proof prover="2" memlimit="1000"><result status="valid" time="0.15"/></proof>
  </goal>
  <goal name="WP_parameter in_place_reverse.8" expl="8. loop invariant preservation">
  <proof prover="1"><result status="valid" time="0.12"/></proof>
-  <proof prover="5"><result status="valid" time="0.10"/></proof>
-  <proof prover="7"><result status="valid" time="0.13"/></proof>
+  <proof prover="3"><result status="valid" time="0.13"/></proof>
  </goal>
  <goal name="WP_parameter in_place_reverse.9" expl="9. loop invariant preservation">
  <proof prover="1" memlimit="1000"><result status="valid" time="0.09"/></proof>
-  <proof prover="2" memlimit="1000"><result status="valid" time="0.91"/></proof>
  </goal>
  <goal name="WP_parameter in_place_reverse.10" expl="10. loop variant decrease">
-  <proof prover="6"><result status="valid" time="0.10"/></proof>
+  <proof prover="2"><result status="valid" time="0.10"/></proof>
  </goal>
  <goal name="WP_parameter in_place_reverse.11" expl="11. postcondition">
  <proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
-  <proof prover="2"><result status="valid" time="0.22"/></proof>
-  <proof prover="4"><result status="valid" time="0.02"/></proof>
  </goal>
 </transf>
 </goal>

--- a/examples/linked_list_rev/why3shapes.gz
+++ b/examples/linked_list_rev/why3shapes.gz
--- a/examples/mergesort_list.mlw
+++ b/examples/mergesort_list.mlw
@@ -15,7 +15,8 @@ module Elt
  type elt
  predicate le elt elt
  clone relations.TotalPreOrder with type t = elt, predicate rel = le
-  clone export list.Sorted      with type t = elt, predicate le  = le
+  clone export list.Sorted      with type t = elt, predicate le  = le,
+  goal Transitive.Trans

 end


--- a/examples/mergesort_list/why3session.xml
+++ b/examples/mergesort_list/why3session.xml
--- a/examples/mergesort_list/why3shapes.gz
+++ b/examples/mergesort_list/why3shapes.gz
--- a/examples/mergesort_queue.mlw
+++ b/examples/mergesort_queue.mlw
@@ -16,7 +16,8 @@ module MergesortQueue
  type elt
  predicate le elt elt
  clone relations.TotalPreOrder with type t = elt, predicate rel = le
-  clone export list.Sorted      with type t = elt, predicate le  = le
+  clone export list.Sorted      with type t = elt, predicate le  = le,
+  goal Transitive.Trans

  let merge (q1: t elt) (q2: t elt) (q: t elt)
    requires { q.elts = Nil /\ sorted q1.elts /\ sorted q2.elts }

--- a/examples/mergesort_queue/why3session.xml
+++ b/examples/mergesort_queue/why3session.xml
--- a/examples/mergesort_queue/why3shapes.gz
+++ b/examples/mergesort_queue/why3shapes.gz
--- a/examples/sorted_list/why3session.xml
+++ b/examples/sorted_list/why3session.xml
@@ -2,11 +2,11 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Alt-Ergo" version="0.95.1" timelimit="20" memlimit="0"/>
+<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
 <file name="../sorted_list.mlw" expanded="true">
-<theory name="FindInSortedList" sum="9315da3cc3b88fe0c4ad3f06aad610f4" expanded="true">
+<theory name="FindInSortedList" sum="a6b267074f636ad1d1f4475349be62a0" expanded="true">
 <goal name="Sorted_not_mem" expanded="true">
- <proof prover="0"><result status="valid" time="0.01"/></proof>
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
 </goal>
 <goal name="WP_parameter find" expl="VC for find" expanded="true">
 <proof prover="0"><result status="valid" time="0.02"/></proof>

--- a/examples/sorted_list/why3shapes.gz
+++ b/examples/sorted_list/why3shapes.gz
--- a/examples/stdlib/list/list_Permut_Permut_length_1.v
+++ b/examples/stdlib/list/list_Permut_Permut_length_1.v
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require int.Int.
+
+(* Why3 assumption *)
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
+Existing Instance list_WhyType.
+Implicit Arguments Nil [[a]].
+Implicit Arguments Cons [[a]].
+
+Parameter num_occ: forall {a:Type} {a_WT:WhyType a}, a -> (list a) -> Z.
+
+Axiom num_occ_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
+  a)),
+  match l with
+  | Nil => ((num_occ x l) = 0%Z)
+  | (Cons y r) => ((x = y) -> ((num_occ x l) = (1%Z + (num_occ x r))%Z)) /\
+      ((~ (x = y)) -> ((num_occ x l) = (0%Z + (num_occ x r))%Z))
+  end.
+
+(* Why3 assumption *)
+Fixpoint mem {a:Type} {a_WT:WhyType a} (x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil => False
+  | (Cons y r) => (x = y) \/ (mem x r)
+  end.
+
+Axiom Mem_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
+  a)), (mem x l) <-> (0%Z < (num_occ x l))%Z.
+
+(* Why3 assumption *)
+Fixpoint infix_plpl {a:Type} {a_WT:WhyType a} (l1:(list a)) (l2:(list
+  a)) {struct l1}: (list a) :=
+  match l1 with
+  | Nil => l2
+  | (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
+  end.
+
+Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
+  (l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
+  l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
+
+Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
+  ((infix_plpl l (Nil : (list a))) = l).
+
+(* Why3 assumption *)
+Fixpoint length {a:Type} {a_WT:WhyType a} (l:(list a)) {struct l}: Z :=
+  match l with
+  | Nil => 0%Z
+  | (Cons _ r) => (1%Z + (length r))%Z
+  end.
+
+Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
+  a)), (0%Z <= (length l))%Z.
+
+Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
+  ((length l) = 0%Z) <-> (l = (Nil : (list a))).
+
+Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
+  (l2:(list a)), ((length (infix_plpl l1
+  l2)) = ((length l1) + (length l2))%Z).
+
+Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
+  a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x
+  l2)).
+
+Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
+  a)), (mem x l) -> exists l1:(list a), exists l2:(list a),
+  (l = (infix_plpl l1 (Cons x l2))).
+
+Axiom Append_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
+  (l1:(list a)) (l2:(list a)), ((num_occ x (infix_plpl l1 l2)) = ((num_occ x
+  l1) + (num_occ x l2))%Z).
+
+(* Why3 assumption *)
+Fixpoint reverse {a:Type} {a_WT:WhyType a} (l:(list a)) {struct l}: (list
+  a) :=
+  match l with
+  | Nil => (Nil : (list a))
+  | (Cons x r) => (infix_plpl (reverse r) (Cons x (Nil : (list a))))
+  end.
+
+Axiom reverse_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
+  (l2:(list a)) (x:a), ((infix_plpl (reverse (Cons x l1))
+  l2) = (infix_plpl (reverse l1) (Cons x l2))).
+
+Axiom reverse_cons : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
+  (x:a), ((reverse (Cons x l)) = (infix_plpl (reverse l) (Cons x (Nil : (list
+  a))))).
+
+Axiom cons_reverse : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
+  (x:a), ((Cons x (reverse l)) = (reverse (infix_plpl l (Cons x (Nil : (list
+  a)))))).
+
+Axiom reverse_reverse : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
+  a)), ((reverse (reverse l)) = l).
+
+Axiom reverse_mem : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
+  (x:a), (mem x l) <-> (mem x (reverse l)).
+
+Axiom Reverse_length : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
+  ((length (reverse l)) = (length l)).
+
+Axiom reverse_num_occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
+  (l:(list a)), ((num_occ x l) = (num_occ x (reverse l))).
+
+(* Why3 assumption *)
+Definition permut {a:Type} {a_WT:WhyType a} (l1:(list a)) (l2:(list
+  a)): Prop := forall (x:a), ((num_occ x l1) = (num_occ x l2)).
+
+Axiom Permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
+  (permut l l).
+
+Axiom Permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
+  (l2:(list a)), (permut l1 l2) -> (permut l2 l1).
+
+Axiom Permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
+  (l2:(list a)) (l3:(list a)), (permut l1 l2) -> ((permut l2 l3) -> (permut
+  l1 l3)).
+
+Axiom Permut_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
+  a)) (l2:(list a)), (permut l1 l2) -> (permut (Cons x l1) (Cons x l2)).
+
+Axiom Permut_swap : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
+  (l:(list a)), (permut (Cons x (Cons y l)) (Cons y (Cons x l))).
+
+Axiom Permut_cons_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
+  (l1:(list a)) (l2:(list a)), (permut (infix_plpl (Cons x l1) l2)
+  (infix_plpl l1 (Cons x l2))).
+
+Axiom Permut_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
+  (l2:(list a)) (l3:(list a)), (permut (infix_plpl (infix_plpl l1 l2) l3)
+  (infix_plpl l1 (infix_plpl l2 l3))).
+
+Axiom Permut_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
+  (l2:(list a)) (k1:(list a)) (k2:(list a)), (permut l1 k1) -> ((permut l2
+  k2) -> (permut (infix_plpl l1 l2) (infix_plpl k1 k2))).
+
+Axiom Permut_append_swap : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list
+  a)) (l2:(list a)), (permut (infix_plpl l1 l2) (infix_plpl l2 l1)).
+
+Axiom Permut_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
+  a)) (l2:(list a)), (permut l1 l2) -> ((mem x l1) -> (mem x l2)).
+
+(* Why3 goal *)
+Theorem Permut_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list
+  a)) (l2:(list a)), (permut l1 l2) -> ((length l1) = (length l2)).
+intros a a_WT l1 l2 h1.
+
+Qed.
+
--- a/examples/stdlib/list/list_Permut_Permut_length_2.v
+++ b/examples/stdlib/list/list_Permut_Permut_length_2.v
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require int.Int.
+
+(* Why3 assumption *)
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
+Existing Instance list_WhyType.
+Implicit Arguments Nil [[a]].
+Implicit Arguments Cons [[a]].
+
+Parameter num_occ: forall {a:Type} {a_WT:WhyType a}, a -> (list a) -> Z.
+
+Axiom num_occ_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
+  a)),
+  match l with
+  | Nil => ((num_occ x l) = 0%Z)
+  | (Cons y r) => ((x = y) -> ((num_occ x l) = (1%Z + (num_occ x r))%Z)) /\
+      ((~ (x = y)) -> ((num_occ x l) = (0%Z + (num_occ x r))%Z))
+  end.
+
+Axiom Num_Occ_Positive : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
+  (l:(list a)), (0%Z <= (num_occ x l))%Z.
+
+(* Why3 assumption *)
+Fixpoint mem {a:Type} {a_WT:WhyType a} (x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil => False
+  | (Cons y r) => (x = y) \/ (mem x r)
+  end.
+
+Axiom Mem_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
+  a)), (mem x l) <-> (0%Z < (num_occ x l))%Z.
+
+(* Why3 assumption *)
+Fixpoint infix_plpl {a:Type} {a_WT:WhyType a} (l1:(list a)) (l2:(list
+  a)) {struct l1}: (list a) :=
+  match l1 with
+  | Nil => l2
+  | (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
+  end.
+
+Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
+  (l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
+  l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
+
+Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
+  ((infix_plpl l (Nil : (list a))) = l).
+
+(* Why3 assumption *)
+Fixpoint length {a:Type} {a_WT:WhyType a} (l:(list a)) {struct l}: Z :=
+  match l with
+  | Nil => 0%Z
+  | (Cons _ r) => (1%Z + (length r))%Z
+  end.
+
+Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
+  a)), (0%Z <= (length l))%Z.
+
+Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
+  ((length l) = 0%Z) <-> (l = (Nil : (list a))).
+
+Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
+  (l2:(list a)), ((length (infix_plpl l1
+  l2)) = ((length l1) + (length l2))%Z).
+
+Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
+  a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x
+  l2)).
+
+Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
+  a)), (mem x l) -> exists l1:(list a), exists l2:(list a),
+  (l = (infix_plpl l1 (Cons x l2))).
+
+Axiom Append_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
+  (l1:(list a)) (l2:(list a)), ((num_occ x (infix_plpl l1 l2)) = ((num_occ x
+  l1) + (num_occ x l2))%Z).
+
+(* Why3 assumption *)
+Fixpoint reverse {a:Type} {a_WT:WhyType a} (l:(list a)) {struct l}: (list
+  a) :=
+  match l with
+  | Nil => (Nil : (list a))
+  | (Cons x r) => (infix_plpl (reverse r) (Cons x (Nil : (list a))))
+  end.
+
+Axiom reverse_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
+  (l2:(list a)) (x:a), ((infix_plpl (reverse (Cons x l1))
+  l2) = (infix_plpl (reverse l1) (Cons x l2))).
+
+Axiom reverse_cons : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
+  (x:a), ((reverse (Cons x l)) = (infix_plpl (reverse l) (Cons x (Nil : (list
+  a))))).
+
+Axiom cons_reverse : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
+  (x:a), ((Cons x (reverse l)) = (reverse (infix_plpl l (Cons x (Nil : (list
+  a)))))).
+
+Axiom reverse_reverse : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
+  a)), ((reverse (reverse l)) = l).
+
+Axiom reverse_mem : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
+  (x:a), (mem x l) <-> (mem x (reverse l)).
+
+Axiom Reverse_length : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
+  ((length (reverse l)) = (length l)).
+
+Axiom reverse_num_occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
+  (l:(list a)), ((num_occ x l) = (num_occ x (reverse l))).
+
+(* Why3 assumption *)
+Definition permut {a:Type} {a_WT:WhyType a} (l1:(list a)) (l2:(list
+  a)): Prop := forall (x:a), ((num_occ x l1) = (num_occ x l2)).
+
+Axiom Permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
+  (permut l l).
+
+Axiom Permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
+  (l2:(list a)), (permut l1 l2) -> (permut l2 l1).
+
+Axiom Permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
+  (l2:(list a)) (l3:(list a)), (permut l1 l2) -> ((permut l2 l3) -> (permut
+  l1 l3)).
+
+Axiom Permut_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
+  a)) (l2:(list a)), (permut l1 l2) -> (permut (Cons x l1) (Cons x l2)).
+
+Axiom Permut_swap : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
+  (l:(list a)), (permut (Cons x (Cons y l)) (Cons y (Cons x l))).
+
+Axiom Permut_cons_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
+  (l1:(list a)) (l2:(list a)), (permut (infix_plpl (Cons x l1) l2)
+  (infix_plpl l1 (Cons x l2))).
+
+Axiom Permut_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
+  (l2:(list a)) (l3:(list a)), (permut (infix_plpl (infix_plpl l1 l2) l3)
+  (infix_plpl l1 (infix_plpl l2 l3))).
+
+Axiom Permut_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
+  (l2:(list a)) (k1:(list a)) (k2:(list a)), (permut l1 k1) -> ((permut l2
+  k2) -> (permut (infix_plpl l1 l2) (infix_plpl k1 k2))).
+
+Axiom Permut_append_swap : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list
+  a)) (l2:(list a)), (permut (infix_plpl l1 l2) (infix_plpl l2 l1)).
+
+Axiom Permut_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
+  a)) (l2:(list a)), (permut l1 l2) -> ((mem x l1) -> (mem x l2)).
+
+(* Why3 goal *)
+Theorem Permut_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list
+  a)) (l2:(list a)), (permut l1 l2) -> ((length l1) = (length l2)).
+intros a a_WT l1 l2 h1.
+Require Import Why3.
+Ltac cvc := why3 "CVC4,1.4,".
+generalize dependent l2.
+induction l1; intros.
+destruct l2.
+trivial.
+cvc.
+pose (h2 := h1).
+clearbody h2.
+specialize (h1 a0).
+assert (mem a0 l2) by cvc.
+apply mem_decomp in H.
+destruct H as [l3 [l4 H]].
+assert (permut l1 (infix_plpl l3 l4)).
+intro.
+cvc.
+cvc.
+Qed.
+
--- a/examples/stdlib/list/why3session.xml
+++ b/examples/stdlib/list/why3session.xml
--- a/examples/stdlib/list/why3shapes.gz
+++ b/examples/stdlib/list/why3shapes.gz
--- a/examples/tower_of_hanoi.mlw
+++ b/examples/tower_of_hanoi.mlw
@@ -66,7 +66,8 @@ module Tower_of_Hanoi
  use import list.Length

  use import list.RevAppend
-  clone import list.RevSorted with type t = int, predicate le = (<)
+  clone import list.RevSorted with type t = int, predicate le = (<),
+  goal Transitive.Trans

  type tower = {
    mutable rod : list int;

--- a/examples/tower_of_hanoi/why3session.xml
+++ b/examples/tower_of_hanoi/why3session.xml
--- a/examples/tower_of_hanoi/why3shapes.gz
+++ b/examples/tower_of_hanoi/why3shapes.gz
--- a/examples/unraveling_a_card_trick/why3session.xml
+++ b/examples/unraveling_a_card_trick/why3session.xml
--- a/examples/unraveling_a_card_trick/why3shapes.gz
+++ b/examples/unraveling_a_card_trick/why3shapes.gz
--- a/examples/vstte10_aqueue/why3session.xml
+++ b/examples/vstte10_aqueue/why3session.xml
@@ -2,33 +2,33 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Alt-Ergo" version="0.95.1" timelimit="20" memlimit="0"/>
-<file name="../vstte10_aqueue.mlw">
-<theory name="AmortizedQueue" sum="b357314754b0898c4e610c0bb61806fb">
- <goal name="WP_parameter empty" expl="VC for empty">
- <proof prover="0"><result status="valid" time="0.02"/></proof>
+<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
+<file name="../vstte10_aqueue.mlw" expanded="true">
+<theory name="AmortizedQueue" sum="60e0a38eed52550859b9a34330155b5a" expanded="true">
+ <goal name="WP_parameter empty" expl="VC for empty" expanded="true">
+ <proof prover="0"><result status="valid" time="0.01"/></proof>
 </goal>
- <goal name="WP_parameter head" expl="VC for head">
- <proof prover="0"><result status="valid" time="0.12"/></proof>
+ <goal name="WP_parameter head" expl="VC for head" expanded="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
 </goal>