new examples: generate all trees

parent 2a683f9c
(*
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:
*)
(* 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 *)
(* 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 *)
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment