BST Prover

ProveBST.hs

module Main where

data Tree a = Leaf | Node a (Tree a) (Tree a)

isBST :: Tree Double -> Bool
isBST = fst . isBST'
    where isBST' Leaf = (True, Nothing)
          isBST' (Node n left right) =
                let (l, lminmax) = isBST' left
                    ~(r, rminmax) = isBST' right
                in if l && r then minimax n lminmax rminmax else (False, Nothing)
          minimax n Nothing Nothing = (True, pure (n, n))
          minimax n Nothing (Just (rmin, rmax)) = (n < rmin, pure (n, rmax))
          minimax n (Just (lmin, lmax)) Nothing = (n >= lmax, pure (lmin, n))
          minimax n (Just (lmin, lmax)) (Just (rmin, rmax)) = (n >= lmax && n < rmin, pure (lmin, rmax))

tree1 = Node 7
          (Node 3
            Leaf
            (Node 5
              (Node 4 Leaf Leaf)
              (Node 6 Leaf Leaf)))
          (Node 9
            (Node 2 Leaf Leaf)
            (Node 10 Leaf Leaf))

tree2 = Node 7
          (Node 3
            (Node 2 Leaf Leaf)
            (Node 5
              (Node 4 Leaf Leaf)
              (Node 6 Leaf Leaf))) -- (Node 8 Leaf Leaf)))
          (Node 9 Leaf (Node 10 Leaf Leaf))
          
tree3 = Node 7 Leaf Leaf

tree4 = Leaf