coincidence_count_list: simpler termination proof

examples/coincidence_count_list.mlw

@@ -8,7 +8,7 @@
     elements that appear in both sequences (in linear time and constant
     space).
 
-    See also coincidence_count for a version using arrays.
+    See also coincidence_count.mlw for a version using arrays.
 
     Authors: Jean-Christophe Filliâtre (CNRS)
 *)
@@ -19,7 +19,6 @@ module CoincidenceCount
   use import set.Fset
   use import list.Elements
   use list.Mem as L
-  use import list.Length
   use import int.Int
 
   clone export list.Sorted
@@ -29,7 +28,7 @@ module CoincidenceCount
     requires { sorted a }
     requires { sorted b }
     ensures  { result == inter (elements a) (elements b) }
-    variant  { length a + length b }
+    variant  { a, b }
   =
     match a, b with
     | Cons ha ta, Cons hb tb ->
@@ -44,3 +43,69 @@ module CoincidenceCount
     end
 
 end
+
+(* the same, with elements of any type *)
+
+module CoincidenceCountAnyType
+
+  use import list.List
+  use import set.Fset
+  use import list.Elements
+  use list.Mem as L
+  use import int.Int
+
+  clone import relations.TotalStrictOrder
+
+  clone export list.Sorted
+     with type t = t, predicate le = rel, goal Transitive.Trans
+
+  let rec coincidence_count (a b: list t) : set t
+    requires { sorted a }
+    requires { sorted b }
+    ensures  { result == inter (elements a) (elements b) }
+    variant  { a, b }
+  =
+    match a, b with
+    | Cons ha ta, Cons hb tb ->
+       if ha = hb then
+         add ha (coincidence_count ta tb)
+       else if rel ha hb then
+         coincidence_count ta b
+       else
+         coincidence_count a tb
+    | _ ->
+       empty
+    end
+
+end
+
+(* the same, using only lists *)
+
+module CoincidenceCountList
+
+  use import list.List
+  use import list.Mem
+  use import int.Int
+
+  clone export list.Sorted
+     with type t = int, predicate le = (<), goal Transitive.Trans
+
+  let rec coincidence_count (a b: list int) : list int
+    requires { sorted a }
+    requires { sorted b }
+    ensures  { forall x. mem x result <-> mem x a /\ mem x b }
+    variant  { a, b }
+  =
+    match a, b with
+    | Cons ha ta, Cons hb tb ->
+       if ha = hb then
+         Cons ha (coincidence_count ta tb)
+       else if ha < hb then
+         coincidence_count ta b
+       else
+         coincidence_count a tb
+    | _ ->
+       Nil
+    end
+
+end

examples/coincidence_count_list/why3session.xml

@@ -6,14 +6,14 @@
 <prover id="1" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Eprover" version="1.8-001" timelimit="6" steplimit="0" memlimit="1000"/>
 <file name="../coincidence_count_list.mlw" expanded="true">
-<theory name="CoincidenceCount" sum="4d4c890e56bb604a55ec2e21b7ac9a92" expanded="true">
- <goal name="Transitive.Trans" expanded="true">
+<theory name="CoincidenceCount" sum="e1c38f7c433de1db1bf331338e6cd93a">
+ <goal name="Transitive.Trans">
  <proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
  </goal>
- <goal name="WP_parameter coincidence_count" expl="VC for coincidence_count" expanded="true">
- <transf name="split_goal_wp" expanded="true">
+ <goal name="WP_parameter coincidence_count" expl="VC for coincidence_count">
+ <transf name="split_goal_wp">
   <goal name="WP_parameter coincidence_count.1" expl="1. variant decrease">
-  <proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
   </goal>
   <goal name="WP_parameter coincidence_count.2" expl="2. precondition">
   <proof prover="0"><result status="valid" time="0.00" steps="18"/></proof>
@@ -22,11 +22,10 @@
   <proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
   </goal>
   <goal name="WP_parameter coincidence_count.4" expl="4. postcondition">
-  <proof prover="0"><result status="valid" time="1.98" steps="2625"/></proof>
-  <proof prover="3"><result status="timeout" time="5.99"/></proof>
+  <proof prover="0"><result status="valid" time="1.18" steps="2625"/></proof>
   </goal>
   <goal name="WP_parameter coincidence_count.5" expl="5. variant decrease">
-  <proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
   </goal>
   <goal name="WP_parameter coincidence_count.6" expl="6. precondition">
   <proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
@@ -34,11 +33,11 @@
   <goal name="WP_parameter coincidence_count.7" expl="7. precondition">
   <proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
   </goal>
-  <goal name="WP_parameter coincidence_count.8" expl="8. postcondition" expanded="true">
-  <proof prover="0"><result status="valid" time="2.36" steps="4210"/></proof>
+  <goal name="WP_parameter coincidence_count.8" expl="8. postcondition">
+  <proof prover="0"><result status="valid" time="1.73" steps="3685"/></proof>
   </goal>
   <goal name="WP_parameter coincidence_count.9" expl="9. variant decrease">
-  <proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
   </goal>
   <goal name="WP_parameter coincidence_count.10" expl="10. precondition">
   <proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
@@ -46,8 +45,8 @@
   <goal name="WP_parameter coincidence_count.11" expl="11. precondition">
   <proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
   </goal>
-  <goal name="WP_parameter coincidence_count.12" expl="12. postcondition" expanded="true">
-  <proof prover="0"><result status="valid" time="3.56" steps="6215"/></proof>
+  <goal name="WP_parameter coincidence_count.12" expl="12. postcondition">
+  <proof prover="0"><result status="valid" time="1.76" steps="3635"/></proof>
   </goal>
   <goal name="WP_parameter coincidence_count.13" expl="13. postcondition">
   <proof prover="3"><result status="valid" time="0.04"/></proof>
@@ -59,5 +58,65 @@
  </transf>
  </goal>
 </theory>
+<theory name="CoincidenceCountAnyType" sum="78e504df0782d826d8b4c2b2ed1accd6">
+ <goal name="Transitive.Trans">
+ <proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
+ </goal>
+ <goal name="WP_parameter coincidence_count" expl="VC for coincidence_count">
+ <proof prover="0"><result status="valid" time="4.92" steps="12209"/></proof>
+ <transf name="split_goal_wp">
+  <goal name="WP_parameter coincidence_count.1" expl="1. variant decrease">
+  <proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
+  </goal>
+  <goal name="WP_parameter coincidence_count.2" expl="2. precondition">
+  <proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
+  </goal>
+  <goal name="WP_parameter coincidence_count.3" expl="3. precondition">
+  <proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
+  </goal>
+  <goal name="WP_parameter coincidence_count.4" expl="4. postcondition">
+  <proof prover="0"><result status="valid" time="1.00" steps="2400"/></proof>
+  </goal>
+  <goal name="WP_parameter coincidence_count.5" expl="5. variant decrease">
+  <proof prover="0"><result status="valid" time="0.02" steps="13"/></proof>
+  </goal>
+  <goal name="WP_parameter coincidence_count.6" expl="6. precondition">
+  <proof prover="0"><result status="valid" time="0.02" steps="19"/></proof>
+  </goal>
+  <goal name="WP_parameter coincidence_count.7" expl="7. precondition">
+  <proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
+  </goal>
+  <goal name="WP_parameter coincidence_count.8" expl="8. postcondition">
+  <proof prover="0"><result status="valid" time="0.68" steps="1750"/></proof>
+  </goal>
+  <goal name="WP_parameter coincidence_count.9" expl="9. variant decrease">
+  <proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
+  </goal>
+  <goal name="WP_parameter coincidence_count.10" expl="10. precondition">
+  <proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
+  </goal>
+  <goal name="WP_parameter coincidence_count.11" expl="11. precondition">
+  <proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
+  </goal>
+  <goal name="WP_parameter coincidence_count.12" expl="12. postcondition">
+  <proof prover="0"><result status="valid" time="0.52" steps="1837"/></proof>
+  </goal>
+  <goal name="WP_parameter coincidence_count.13" expl="13. postcondition">
+  <proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
+  </goal>
+  <goal name="WP_parameter coincidence_count.14" expl="14. postcondition">
+  <proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
+  </goal>
+ </transf>
+ </goal>
+</theory>
+<theory name="CoincidenceCountList" sum="66d71efd5b320baab93930df25784477">
+ <goal name="Transitive.Trans">
+ <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+ <goal name="WP_parameter coincidence_count" expl="VC for coincidence_count">
+ <proof prover="0"><result status="valid" time="0.24" steps="657"/></proof>
+ </goal>
+</theory>
 </file>
 </why3session>