a stronger lemma in list.Sorted

updated proof sesssions mergesort_list in progress

a stronger lemma in list.Sorted
updated proof sesssions mergesort_list in progress
2d72ce3d · Jean-Christophe Filliâtre · aa823b11 · 2d72ce3d · 2d72ce3d · 2d72ce3d
Commit 2d72ce3d authored Apr 01, 2014 by Jean-Christophe Filliâtre
7 changed files
--- a/examples/insertion_sort_list/why3session.xml
+++ b/examples/insertion_sort_list/why3session.xml
@@ -24,7 +24,7 @@
    locfile="../insertion_sort_list.mlw"
    loclnum="13" loccnumb="10" loccnume="16"
    expl="VC for insert"
-    sum="cc3fc1c2b87387b1c4fa4533d749cd4e"
+    sum="2ab5530925627c4937e0de61cca52b1e"
    proved="true"
    expanded="true"
    shape="CapermutaConsV0V1V2AasortedV2LaConsV0aNilaNiliapermutaConsV0V1V6AasortedV6LaConsV3V5IapermutaConsV0V4V5AasortedV5FAasortedV4ACfaNilainfix =V7V4aConswVV1apermutaConsV0V1V8AasortedV8LaConsV0V1aleV0V3aConsVVV1IasortedV1F">
@@ -39,7 +39,7 @@
      locfile="../insertion_sort_list.mlw"
      loclnum="13" loccnumb="10" loccnume="16"
      expl="1. postcondition"
-      sum="d94333f89c188ca295e2771d3c06616e"
+      sum="26c695c439fabd3de02286b4f293e7e6"
      proved="true"
      expanded="false"
      shape="postconditionCasortedV2LaConsV0aNilaNiltaConsVVV1IasortedV1F">
@@ -59,7 +59,7 @@
      locfile="../insertion_sort_list.mlw"
      loclnum="13" loccnumb="10" loccnume="16"
      expl="2. postcondition"
-      sum="a90aefb24c56deed211a9a5adbe9a4bc"
+      sum="9e061c4e7ee2ace6beb1b5e9c012cd39"
      proved="true"
      expanded="false"
      shape="postconditionCapermutaConsV0V1V2LaConsV0aNilaNiltaConsVVV1IasortedV1F">
@@ -79,7 +79,7 @@
      locfile="../insertion_sort_list.mlw"
      loclnum="13" loccnumb="10" loccnume="16"
      expl="3. postcondition"
-      sum="978c39769aacdd812aff5e13ab053fce"
+      sum="57036f30e830ba4cbbdf65329150ae67"
      proved="true"
      expanded="false"
      shape="postconditionCtaNilasortedV4LaConsV0V1IaleV0V2aConsVVV1IasortedV1F">
@@ -99,7 +99,7 @@
      locfile="../insertion_sort_list.mlw"
      loclnum="13" loccnumb="10" loccnume="16"
      expl="4. postcondition"
-      sum="f6f2cc2d6a9a3e28c44ec8b6004aca92"
+      sum="755568401b59eb8004687a922692036e"
      proved="true"
      expanded="false"
      shape="postconditionCtaNilapermutaConsV0V1V4LaConsV0V1IaleV0V2aConsVVV1IasortedV1F">
@@ -119,7 +119,7 @@
      locfile="../insertion_sort_list.mlw"
      loclnum="13" loccnumb="10" loccnume="16"
      expl="5. variant decrease"
-      sum="34644657d76f754487955c41435534f2"
+      sum="c8a1534df83fe53605c22aa1c7272c65"
      proved="true"
      expanded="false"
      shape="variant decreaseCtaNilCfaNilainfix =V4V3aConswVV1INaleV0V2aConsVVV1IasortedV1F">
@@ -139,7 +139,7 @@
      locfile="../insertion_sort_list.mlw"
      loclnum="13" loccnumb="10" loccnume="16"
      expl="6. precondition"
-      sum="027752c77210629ac8042ee30c63b913"
+      sum="46429d97e19638c9c02454b481b6e6d7"
      proved="true"
      expanded="false"
      shape="preconditionCtaNilasortedV3INaleV0V2aConsVVV1IasortedV1F">
@@ -159,7 +159,7 @@
      locfile="../insertion_sort_list.mlw"
      loclnum="13" loccnumb="10" loccnume="16"
      expl="7. postcondition"
-      sum="8d29fdf017af31d90092c8aaf0cf9b50"
+      sum="423312fc8a78607a5599ddf0b1ffd470"
      proved="true"
      expanded="false"
      shape="postconditionCtaNilasortedV5LaConsV2V4IapermutaConsV0V3V4AasortedV4FIasortedV3INaleV0V2aConsVVV1IasortedV1F">
@@ -171,7 +171,7 @@
       memlimit="1000"
       obsolete="false"
       archived="false">
-       <result status="valid" time="1.15"/>
+       <result status="valid" time="0.50"/>
      </proof>
     </goal>
     <goal
@@ -179,7 +179,7 @@
      locfile="../insertion_sort_list.mlw"
      loclnum="13" loccnumb="10" loccnume="16"
      expl="8. postcondition"
-      sum="b8fe894d268a2476800098cc339892b5"
+      sum="e75d8326069d6d6391739d9c81cacbed"
      proved="true"
      expanded="true"
      shape="postconditionCtaNilapermutaConsV0V1V5LaConsV2V4IapermutaConsV0V3V4AasortedV4FIasortedV3INaleV0V2aConsVVV1IasortedV1F">
@@ -201,7 +201,7 @@
    locfile="../insertion_sort_list.mlw"
    loclnum="23" loccnumb="10" loccnume="24"
    expl="VC for insertion_sort"
-    sum="b1a299800b4664e15a2afe7c1f44ba06"
+    sum="2b90568e336e3cbfb046f2050c83c132"
    proved="true"
    expanded="true"
    shape="CapermutV0V1AasortedV1LaNilaNilapermutV0V5AasortedV5IapermutaConsV2V4V5AasortedV5FAasortedV4IapermutV3V4AasortedV4FACfaNilainfix =V6V3aConswVV0aConsVVV0F">
@@ -216,7 +216,7 @@
      locfile="../insertion_sort_list.mlw"
      loclnum="23" loccnumb="10" loccnume="24"
      expl="1. postcondition"
-      sum="817683103cb88e976105ad6982bc7290"
+      sum="18c25e7f68de2e72d45f2e0907d9adba"
      proved="true"
      expanded="false"
      shape="postconditionCasortedV1LaNilaNiltaConsVVV0F">
@@ -236,7 +236,7 @@
      locfile="../insertion_sort_list.mlw"
      loclnum="23" loccnumb="10" loccnume="24"
      expl="2. postcondition"
-      sum="17c1bc20bcc98a2a62255d08f0629ffd"
+      sum="1555231f2b79045ffd75b11235e469c1"
      proved="true"
      expanded="false"
      shape="postconditionCapermutV0V1LaNilaNiltaConsVVV0F">
@@ -256,7 +256,7 @@
      locfile="../insertion_sort_list.mlw"
      loclnum="23" loccnumb="10" loccnume="24"
      expl="3. variant decrease"
-      sum="49daa7aafece9356fa313a12cbd9e9b0"
+      sum="8a447ef6328a2fdb85dc0aeb984dc6de"
      proved="true"
      expanded="false"
      shape="variant decreaseCtaNilCfaNilainfix =V3V2aConswVV0aConsVVV0F">
@@ -276,7 +276,7 @@
      locfile="../insertion_sort_list.mlw"
      loclnum="23" loccnumb="10" loccnume="24"
      expl="4. precondition"
-      sum="42a3ae045178dfa95e3983d955cf627b"
+      sum="107d2ae80e4e5f13c8eadf3131aee2ee"
      proved="true"
      expanded="false"
      shape="preconditionCtaNilasortedV3IapermutV2V3AasortedV3FaConsVVV0F">
@@ -296,7 +296,7 @@
      locfile="../insertion_sort_list.mlw"
      loclnum="23" loccnumb="10" loccnume="24"
      expl="5. postcondition"
-      sum="c66d62770e5611b4672191a30fe07831"
+      sum="9939ef6177d7435224746e2b13d887c6"
      proved="true"
      expanded="false"
      shape="postconditionCtaNilasortedV4IapermutaConsV1V3V4AasortedV4FIasortedV3IapermutV2V3AasortedV3FaConsVVV0F">
@@ -316,7 +316,7 @@
      locfile="../insertion_sort_list.mlw"
      loclnum="23" loccnumb="10" loccnume="24"
      expl="6. postcondition"
-      sum="ba5c17e2bd3c3448478bf9f75692ba7a"
+      sum="c44c4abe0a0483801f2b4d24ad14978b"
      proved="true"
      expanded="false"
      shape="postconditionCtaNilapermutV0V4IapermutaConsV1V3V4AasortedV4FIasortedV3IapermutV2V3AasortedV3FaConsVVV0F">

--- a/examples/mergesort_list.mlw
+++ b/examples/mergesort_list.mlw
@@ -18,6 +18,8 @@ module Elt

 end

+(** recursive (and naive) merging of two sorted lists *)
+
 module Merge (* : MergeSpec *)

  clone export Elt
@@ -72,9 +74,15 @@ module EfficientMerge (* : MergeSpec *)

 end

+(** Mergesort.
+
+    This implementation splits the input list in two according to even- and
+    odd-order elements (see function [split] below). Thus it is not stable.
+    For a stable implementation, see below module [OCamlMergesort]. *)
+
 module Mergesort

-  clone import Merge
+  clone import Merge (* or EfficientMerge *)

  let split (l0: list 'a) : (list 'a, list 'a)
    requires { length l0 >= 2 }
@@ -103,6 +111,10 @@ module Mergesort

 end

+(** {2 OCaml's List.sort}
+
+*)
+
 module OCamlMergesort

  clone export Elt
@@ -110,25 +122,6 @@ module OCamlMergesort
  use import list.Reverse
  use import list.RevAppend

-  function prefix int (list 'a) : list 'a
-
-  axiom prefix_def1:
-    forall l: list 'a. prefix 0 l = Nil
-  axiom prefix_def2:
-    forall n: int, x: 'a, l: list 'a. n > 0 ->
-    prefix n (Cons x l) = Cons x (prefix (n-1) l)
-
-  let rec chop (n: int) (l: list 'a) : list 'a
-    requires { 0 <= n <= length l }
-    ensures  { l = prefix n l ++ result }
-    variant  { n }
-  =
-    if n = 0 then l else
-    match l with
-      | Cons _ t -> chop (n-1) t
-      | Nil -> absurd
-    end
-
  lemma sorted_reverse_cons:
    forall acc x1. sorted (reverse acc) ->
    (forall x. mem x acc -> le x x1) -> sorted (reverse (Cons x1 acc))
@@ -154,6 +147,9 @@ module OCamlMergesort
                   else rev_merge l1 t2 (Cons h2 accu)
    end

+  lemma sorted_reverse_mem:
+    forall x l. sorted (reverse (Cons x l)) -> forall y. mem y l -> le y x
+
  lemma sorted_reverse_cons2:
    forall x l. sorted (reverse (Cons x l)) -> sorted (reverse l)

@@ -172,6 +168,25 @@ module OCamlMergesort
                         else rev_merge_rev l1 t2 (Cons h2 accu)
    end

+  function prefix int (list 'a) : list 'a
+
+  axiom prefix_def1:
+    forall l: list 'a. prefix 0 l = Nil
+  axiom prefix_def2:
+    forall n: int, x: 'a, l: list 'a. n > 0 ->
+    prefix n (Cons x l) = Cons x (prefix (n-1) l)
+
+  let rec chop (n: int) (l: list 'a) : list 'a
+    requires { 0 <= n <= length l }
+    ensures  { l = prefix n l ++ result }
+    variant  { n }
+  =
+    if n = 0 then l else
+    match l with
+      | Cons _ t -> chop (n-1) t
+      | Nil -> absurd
+    end
+
  val sort (n: int) (l: list elt) : list elt
    requires { 2 <= n <= length l }
    ensures  { sorted result }

--- a/examples/mergesort_list/why3session.xml
+++ b/examples/mergesort_list/why3session.xml
--- a/examples/mergesort_queue/why3session.xml
+++ b/examples/mergesort_queue/why3session.xml
--- a/examples/sorted_list/why3session.xml
+++ b/examples/sorted_list/why3session.xml
@@ -19,7 +19,7 @@
    name="Sorted_not_mem"
    locfile="../sorted_list.mlw"
    loclnum="9" loccnumb="8" loccnume="22"
-    sum="752c0d2c53d038c5764d6395b51584b7"
+    sum="c82f4c2802ef03b2cc478898b23b9255"
    proved="true"
    expanded="true"
    shape="NamemV0aConsV1V2IasortedaConsV1V2Iainfix &lt;V0V1F">
@@ -37,7 +37,7 @@
    locfile="../sorted_list.mlw"
    loclnum="13" loccnumb="10" loccnume="14"
    expl="VC for find"
-    sum="8e6f6ceca73f906fe4cb7ff94deec601"
+    sum="f6f632cddc57a43cc61b51ef02faadfe"
    proved="true"
    expanded="true"
    shape="CNamemV0V1aNiliiNamemV0V1amemV0V1qainfix =V4aTrueIamemV0V3qainfix =V4aTrueFAasortedV3ACfaNilainfix =V5V3aConswVV1ainfix &gt;V0V2amemV0V1ainfix =V0V2aConsVVV1IasortedV1F">

--- a/examples/tower_of_hanoi/why3session.xml
+++ b/examples/tower_of_hanoi/why3session.xml
--- a/theories/list.why
+++ b/theories/list.why
@@ -316,8 +316,8 @@ theory Sorted

  lemma sorted_append:
    forall l1 l2: list t.
-    sorted l1 -> sorted l2 ->
-    (forall x y: t. mem x l1 -> mem y l2 -> le x y) ->
+    (sorted l1 /\ sorted l2 /\ (forall x y: t. mem x l1 -> mem y l2 -> le x y))
+    <->
    sorted (l1 ++ l2)

 end