(* Search trees and sorting algorithm using them. *) (* For the module G54DTP, Dependently Typed Programming. *) (* Venanzio Capretta, February 2011. *) Require Import List. Require Import ZArith. Open Scope Z_scope. (* Inductive definition of the type of search trees: *) (* Binary trees with integer labels on the nodes. *) Inductive STree : Set := leaf : STree | node : Z -> STree -> STree -> STree. Definition my_tree : STree := node 4 (node (-2) leaf (node 3 leaf leaf)) (node 7 leaf leaf). (* The boolean are a simple enumeration type. *) Print bool. (* We can check equality of integers with this function. *) Check Z_eq_dec. (* Searching an element inside a search tree. It works if the search tree is correctly ordered. *) Fixpoint look_for (x:Z)(t:STree): bool := match t with leaf => false | node y tl tr => if (Z_eq_dec x y) then true else if (Z_le_gt_dec x y) then (look_for x tl) else (look_for x tr) end. Eval compute in (look_for 6 my_tree). Eval compute in (look_for 3 my_tree). (* A search tree is ordered if: all nodes in the left subtree are smaller or equal to the root, all nodes in the right subtree are larger than the root, the subtrees are recursively ordered. *) (* Inserting a element in a tree. We assume that the input tree is already ordered. *) Fixpoint tree_insert (x:Z)(t:STree): STree := match t with leaf => node x leaf leaf | node y ltr rtr => if (Z_le_gt_dec x y) then (node y (tree_insert x ltr) rtr) else (node y ltr (tree_insert x rtr)) end. (* Transforming a list into an ordered tree. *) Fixpoint list_tree (l:list Z): STree := match l with nil => leaf | cons x l' => tree_insert x (list_tree l') end. (* Flattening a tree into a list, preserving the order. *) Fixpoint flatten (t:STree): list Z := match t with leaf => nil | node x ltr rtr => (flatten ltr) ++ (x :: flatten rtr) end. (* Insertion sort using trees. *) Definition ins_sort : list Z -> list Z := fun l => flatten (list_tree l). Eval compute in (ins_sort (2::1::9::6::7::4::nil)). (* Using balanced trees guarantees optimal complexity. *) (* Idea: bnodes are balanced, unodes are unbalanced: bnodes have the same number of elements in their children; unodes have one more child on the left than on the right. *) Inductive BTree : Set := bleaf : BTree | bnode : Z -> BTree -> BTree -> BTree | unode : Z -> BTree -> BTree -> BTree. (* To maintain balance: if the node is balanced, we insert to the left; if the node is unbalanced, we insert to the right. *) Fixpoint binsert (x:Z)(t:BTree): BTree := match t with bleaf => bnode x bleaf bleaf | bnode y ltr rtr => if (Z_le_gt_dec x y) then (unode y (binsert x ltr) rtr) else (unode x (binsert y ltr) rtr) | unode y ltr rtr => if (Z_le_gt_dec x y) then (bnode x ltr (binsert y rtr)) else (bnode y ltr (binsert x rtr)) end. Fixpoint list_btree (l:list Z): BTree := match l with nil => bleaf | cons x l' => binsert x (list_btree l') end. Fixpoint bflatten (t:BTree): list Z := match t with bleaf => nil | bnode x ltr rtr => (bflatten ltr) ++ (x :: bflatten rtr) | unode x ltr rtr => (bflatten ltr) ++ (x :: bflatten rtr) end. Definition bsort : list Z -> list Z := fun l => bflatten (list_btree l). Eval compute in (ins_sort (2::1::9::6::7::4::nil)).