generate_all_trees: termination

examples/programs/generate_all_trees.mlw

@@ -16,6 +16,7 @@ module GenerateAllTrees
   use import list.Append
   use import list.Distinct
   use import module array.Array
+  use import list.Length
 
   type tree = Empty | Node tree tree
 
@@ -44,12 +45,12 @@ module GenerateAllTrees
      with a left sub-tree from l1 and a right sub-tree from l2 *)
   let combine (i1: int) (l1: list tree) (i2: int) (l2: list tree) =
     { 0 <= i1 /\ all_trees i1 l1 /\ 0 <= i2 /\ all_trees i2 l2 }
-    let rec loop1 (l1: list tree) : list tree =
+    let rec loop1 (l1: list tree) : list tree variant { length l1 } =
       { distinct l1 }
       match l1 with
       | Nil -> Nil
       | Cons t1 l1 ->
-          let rec loop2 (l2: list tree) : list tree =
+          let rec loop2 (l2: list tree) : list tree  variant { length l2 } =
             { distinct l2 }
             match l2 with
             | Nil -> Nil

examples/programs/generate_all_trees/generate_all_trees_WP_GenerateAllTrees_WP_parameter_combine_2.v

@@ -170,10 +170,11 @@ Theorem WP_parameter_combine : forall (i1:Z), forall (l1:(list tree)),
   | (Cons t1 l12) => forall (l21:(list tree)), (distinct l21) ->
       match l21 with
       | Nil => True
-      | (Cons t2 l22) => (distinct l22) -> forall (result:(list tree)),
-          ((distinct result) /\ forall (t:tree), (mem t result) <->
-          exists r:tree, (t = (Node t1 r)) /\ (mem r l22)) ->
-          forall (t:tree), (mem t (Cons (Node t1 t2) result)) ->
+      | (Cons t2 l22) => (((0%Z <= (length l21))%Z /\
+          ((length l22) <  (length l21))%Z) /\ (distinct l22)) ->
+          forall (result:(list tree)), ((distinct result) /\ forall (t:tree),
+          (mem t result) <-> exists r:tree, (t = (Node t1 r)) /\ (mem r
+          l22)) -> forall (t:tree), (mem t (Cons (Node t1 t2) result)) ->
           exists r:tree, (t = (Node t1 r)) /\ (mem r l21)
       end
   end.
@@ -185,7 +186,7 @@ unfold mem in H6; fold mem in H6.
 destruct H6.
 exists t0; intuition.
 red; intuition.
-generalize (H8 t1); clear H8. intuition.
+generalize (H10 t1); clear H8. intuition.
 destruct H8 as (r,h); exists r; intuition.
 red; intuition.
 Qed.