diff --git a/examples/programs/generate_all_trees.mlw b/examples/programs/generate_all_trees.mlw new file mode 100644 index 0000000000000000000000000000000000000000..33d2800024061eee33991e1ac4aeac2853969242 --- /dev/null +++ b/examples/programs/generate_all_trees.mlw @@ -0,0 +1,90 @@ + +(* + Generate all binary trees of size n. + + 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 +*) + +module GenerateAllTrees + + use import int.Int + use import list.List + use import list.Mem + use import list.Append + use import module array.Array + + type tree = Empty | Node tree tree + + function size (t: tree) : int = match t with + | Empty -> 0 + | Node l r -> 1 + size l + size r + end + + lemma size_nonneg: forall t: tree. size t >= 0 + + lemma size_left: + forall t: tree. size t > 0 -> + exists l r: tree. t = Node l r /\ size l < size t + + predicate all_trees (n: int) (l: list tree) = + forall t: tree. size t = n <-> mem t l + + lemma all_trees_0: all_trees 0 (Cons Empty Nil) + + (* 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 = + { } + match l1 with + | Nil -> Nil + | Cons t1 l1 -> + let rec loop2 (l2: list tree) : list tree = + {} + match l2 with + | Nil -> Nil + | Cons t2 l2 -> Cons (Node t1 t2) (loop2 l2) + end + { 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 <-> + (exists l r: tree. t = Node l r /\ mem l l1 /\ mem r l2) } + in + loop1 l1 + { 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) = + { n >= 0 } + let a = make (n+1) Nil in + a[0] <- Cons Empty Nil; + for i = 1 to n do + invariant { (forall k: int. 0 <= k < i -> all_trees k a[k]) } + a[i] <- Nil; + for j = 0 to i-1 do + invariant { + (forall k: int. 0 <= k < i -> all_trees k a[k]) /\ + (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] + done + done; + a + { forall i: int. 0 <= i <= n -> all_trees i result[i] } + +end + +(* +Local Variables: +compile-command: "unset LANG; make -C ../.. examples/programs/generate_all_trees.gui" +End: +*) + diff --git a/examples/programs/generate_all_trees/generate_all_trees_WP_GenerateAllTrees_all_trees_0_1.v b/examples/programs/generate_all_trees/generate_all_trees_WP_GenerateAllTrees_all_trees_0_1.v new file mode 100644 index 0000000000000000000000000000000000000000..c31dac1622ba697a8aadfcfd0855c8021ac80abd --- /dev/null +++ b/examples/programs/generate_all_trees/generate_all_trees_WP_GenerateAllTrees_all_trees_0_1.v @@ -0,0 +1,156 @@ +(* 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))). + +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. + +Definition all_trees(n:Z) (l:(list tree)): Prop := forall (t:tree), + ((size t) = n) <-> (mem t l). + +(* YOU MAY EDIT THE CONTEXT BELOW *) + +(* DO NOT EDIT BELOW *) + +Theorem all_trees_0 : (all_trees 0%Z (Cons Empty (Nil:(list tree)))). +(* YOU MAY EDIT THE PROOF BELOW *) +red; intuition. +destruct t; simpl; auto. +unfold size in H; fold size in H. +right; generalize (size_nonneg t1); generalize (size_nonneg t2); omega. +simpl in H; destruct H; intuition. +subst; simpl; auto. +Qed. +(* DO NOT EDIT BELOW *) + + diff --git a/examples/programs/generate_all_trees/generate_all_trees_WP_GenerateAllTrees_size_nonneg_1.v b/examples/programs/generate_all_trees/generate_all_trees_WP_GenerateAllTrees_size_nonneg_1.v new file mode 100644 index 0000000000000000000000000000000000000000..b781d10a12ad039b2a0c3d49df147619e97a6e71 --- /dev/null +++ b/examples/programs/generate_all_trees/generate_all_trees_WP_GenerateAllTrees_size_nonneg_1.v @@ -0,0 +1,147 @@ +(* 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))). + +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. + +(* YOU MAY EDIT THE CONTEXT BELOW *) + +(* DO NOT EDIT BELOW *) + +Theorem size_nonneg : forall (t:tree), (0%Z <= (size t))%Z. +(* YOU MAY EDIT THE PROOF BELOW *) +induction t; intuition. +unfold size; fold size; omega. +Qed. +(* DO NOT EDIT BELOW *) + + diff --git a/examples/programs/generate_all_trees/why3session.xml b/examples/programs/generate_all_trees/why3session.xml new file mode 100644 index 0000000000000000000000000000000000000000..3f850f5e435c32e97992f8d91e559e4204b81ad3 --- /dev/null +++ b/examples/programs/generate_all_trees/why3session.xml @@ -0,0 +1,545 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +