generate_all_trees: no duplicate elements

examples/programs/generate_all_trees.mlw

@@ -5,8 +5,7 @@
    Given n, the program return an array a of size n+1 such that
    a[i] contains the list of all binary trees of size i.
 
-   TODO: - show that there is no duplicate in a[i]
-         - tail-recursive version of combine
+   TODO: tail-recursive version of combine
 *)
 
 module GenerateAllTrees
@@ -15,6 +14,7 @@ module GenerateAllTrees
   use import list.List
   use import list.Mem
   use import list.Append
+  use import list.Distinct
   use import module array.Array
 
   type tree = Empty | Node tree tree
@@ -31,35 +31,43 @@ module GenerateAllTrees
     exists l r: tree. t = Node l r /\ size l < size t
 
   predicate all_trees (n: int) (l: list tree) =
+    distinct l /\
     forall t: tree. size t = n <-> mem t l
 
   lemma all_trees_0: all_trees 0 (Cons Empty Nil)
 
+  lemma tree_diff:
+    forall l1 l2: tree. size l1 <> size l2 ->
+    forall r1 r2: tree. Node l1 r1 <> Node l2 r2
+
   (* combines two lists of trees l1 and l2 into the list of trees
      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 =
-      { }
+      { distinct l1 }
       match l1 with
       | Nil -> Nil
       | Cons t1 l1 ->
           let rec loop2 (l2: list tree) : list tree =
-            {}
+            { distinct l2 }
             match l2 with
             | Nil -> Nil
             | Cons t2 l2 -> Cons (Node t1 t2) (loop2 l2)
             end
-            { forall t:tree. mem t result <->
+            { distinct result /\
+              forall t:tree. mem t result <->
               (exists r: tree. t = Node t1 r /\ mem r l2) }
          in
          loop2 l2 ++ loop1 l1
       end
-      { forall t:tree. mem t result <->
+      { distinct result /\
+        forall t:tree. mem t result <->
         (exists l r: tree. t = Node l r /\ mem l l1 /\ mem r l2) }
     in
     loop1 l1
-    { forall t:tree. mem t result <->
+    { distinct result /\
+      forall t:tree. mem t result <->
       (exists l r: tree. t = Node l r /\ size l = i1 /\ size r = i2) }
 
   let all_trees (n: int) =
@@ -72,6 +80,7 @@ module GenerateAllTrees
       for j = 0 to i-1 do
         invariant {
           (forall k: int. 0 <= k < i -> all_trees k a[k]) /\
+          distinct a[i] /\
           (forall t: tree. mem t a[i] <->
            exists l r: tree. t = Node l r /\ size t = i /\ size l < j) }
         a[i] <- (combine j a[j] (i-1-j) a[i-1-j]) ++ a[i]

examples/programs/generate_all_trees/generate_all_trees_WP_GenerateAllTrees_WP_parameter_combine_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 qtmark : Type.
+
+Parameter at1: forall (a:Type), a -> qtmark -> a.
+
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a -> a.
+
+Implicit Arguments old.
+
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Set Contextual Implicit.
+Implicit Arguments Nil.
+Unset Contextual Implicit.
+Implicit Arguments Cons.
+
+Set Implicit Arguments.
+Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil => False
+  | (Cons y r) => (x = y) \/ (mem x r)
+  end.
+Unset Implicit Arguments.
+
+Set Implicit Arguments.
+Fixpoint infix_plpl (a:Type)(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.
+Unset Implicit Arguments.
+
+Axiom Append_assoc : forall (a:Type), 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), forall (l:(list a)), ((infix_plpl l
+  (Nil:(list a))) = l).
+
+Set Implicit Arguments.
+Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
+  match l with
+  | Nil => 0%Z
+  | (Cons _ r) => (1%Z + (length r))%Z
+  end.
+Unset Implicit Arguments.
+
+Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
+  (0%Z <= (length l))%Z.
+
+Axiom Length_nil : forall (a:Type), forall (l:(list a)),
+  ((length l) = 0%Z) <-> (l = (Nil:(list a))).
+
+Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
+  ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
+
+Axiom mem_append : forall (a:Type), 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), forall (x:a) (l:(list a)), (mem x l) ->
+  exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))).
+
+Inductive distinct{a:Type}  : (list a) -> Prop :=
+  | distinct_zero : (distinct (Nil:(list a)))
+  | distinct_one : forall (x:a), (distinct (Cons x (Nil:(list a))))
+  | distinct_many : forall (x:a) (l:(list a)), (~ (mem x l)) ->
+      ((distinct l) -> (distinct (Cons x l))).
+Implicit Arguments distinct.
+
+Axiom distinct_append : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
+  (distinct l1) -> ((distinct l2) -> ((forall (x:a), (mem x l1) -> ~ (mem x
+  l2)) -> (distinct (infix_plpl l1 l2)))).
+
+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 length1 (a:Type)(u:(array a)): Z :=
+  match u with
+  | (mk_array length2 _) => length2
+  end.
+Implicit Arguments length1.
+
+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.
+
+Inductive tree  :=
+  | Empty : tree 
+  | Node : tree -> tree -> tree .
+
+Set Implicit Arguments.
+Fixpoint size(t:tree) {struct t}: Z :=
+  match t with
+  | Empty => 0%Z
+  | (Node l r) => ((1%Z + (size l))%Z + (size r))%Z
+  end.
+Unset Implicit Arguments.
+
+Axiom size_nonneg : forall (t:tree), (0%Z <= (size t))%Z.
+
+Axiom size_left : forall (t:tree), (0%Z <  (size t))%Z -> exists l:tree,
+  exists r:tree, (t = (Node l r)) /\ ((size l) <  (size t))%Z.
+
+Definition all_trees(n:Z) (l:(list tree)): Prop := (distinct l) /\
+  forall (t:tree), ((size t) = n) <-> (mem t l).
+
+Axiom all_trees_0 : (all_trees 0%Z (Cons Empty (Nil:(list tree)))).
+
+Axiom tree_diff : forall (l1:tree) (l2:tree), (~ ((size l1) = (size l2))) ->
+  forall (r1:tree) (r2:tree), ~ ((Node l1 r1) = (Node l2 r2)).
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem WP_parameter_combine : forall (i1:Z), forall (l1:(list tree)),
+  forall (i2:Z), forall (l2:(list tree)), ((0%Z <= i1)%Z /\ ((all_trees i1
+  l1) /\ ((0%Z <= i2)%Z /\ (all_trees i2 l2)))) -> forall (l11:(list tree)),
+  (distinct l11) ->
+  match l11 with
+  | Nil => True
+  | (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)) ->
+          exists r:tree, (t = (Node t1 r)) /\ (mem r l21)
+      end
+  end.
+(* YOU MAY EDIT THE PROOF BELOW *)
+intuition.
+destruct l11; intuition.
+destruct l21; intuition.
+unfold mem in H6; fold mem in H6.
+destruct H6.
+exists t0; intuition.
+red; intuition.
+generalize (H8 t1); clear H8. intuition.
+destruct H8 as (r,h); exists r; intuition.
+red; intuition.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/generate_all_trees/generate_all_trees_WP_GenerateAllTrees_all_trees_0_1.v

@@ -69,6 +69,17 @@ Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
 Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) ->
   exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))).
 
+Inductive distinct{a:Type}  : (list a) -> Prop :=
+  | distinct_zero : (distinct (Nil:(list a)))
+  | distinct_one : forall (x:a), (distinct (Cons x (Nil:(list a))))
+  | distinct_many : forall (x:a) (l:(list a)), (~ (mem x l)) ->
+      ((distinct l) -> (distinct (Cons x l))).
+Implicit Arguments distinct.
+
+Axiom distinct_append : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
+  (distinct l1) -> ((distinct l2) -> ((forall (x:a), (mem x l1) -> ~ (mem x
+  l2)) -> (distinct (infix_plpl l1 l2)))).
+
 Parameter map : forall (a:Type) (b:Type), Type.
 
 Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
@@ -135,8 +146,11 @@ Unset Implicit Arguments.
 
 Axiom size_nonneg : forall (t:tree), (0%Z <= (size t))%Z.
 
-Definition all_trees(n:Z) (l:(list tree)): Prop := forall (t:tree),
-  ((size t) = n) <-> (mem t l).
+Axiom size_left : forall (t:tree), (0%Z <  (size t))%Z -> exists l:tree,
+  exists r:tree, (t = (Node l r)) /\ ((size l) <  (size t))%Z.
+
+Definition all_trees(n:Z) (l:(list tree)): Prop := (distinct l) /\
+  forall (t:tree), ((size t) = n) <-> (mem t l).
 
 (* YOU MAY EDIT THE CONTEXT BELOW *)
 
@@ -145,6 +159,7 @@ Definition all_trees(n:Z) (l:(list tree)): Prop := forall (t:tree),
 Theorem all_trees_0 : (all_trees 0%Z (Cons Empty (Nil:(list tree)))).
 (* YOU MAY EDIT THE PROOF BELOW *)
 red; intuition.
+apply distinct_one.
 destruct t; simpl; auto.
 unfold size in H; fold size in H.
 right; generalize (size_nonneg t1); generalize (size_nonneg t2); omega.