1 files changed, 37 insertions, 0 deletions
diff --git a/AvlVerification/BinarySearchTree.lean b/AvlVerification/BinarySearchTree.lean
new file mode 100644
index 0000000..130fd73
--- /dev/null
+++ b/AvlVerification/BinarySearchTree.lean
@@ -0,0 +1,37 @@
+import AvlVerification.Tree
+
+namespace BST
+
+open Primitives (Result)
+open avl_verification (AVLNode Ordering)
+open Tree (AVLTree AVLNode.left AVLNode.right AVLNode.val)
+
+inductive ForallNode (p: T -> Prop): AVLTree T -> Prop
+| none : ForallNode p none
+| some (a: T) (left: AVLTree T) (right: AVLTree T) : ForallNode p left -> p a -> ForallNode p right -> ForallNode p (some (AVLNode.mk a left right))
+
+-- This is the binary search invariant.
+inductive BST [LT T]: AVLTree T -> Prop
+| none : BST none
+| some (a: T) (left: AVLTree T) (right: AVLTree T) : 
+  ForallNode (fun v => v < a) left -> ForallNode (fun v => a < v) right
+  -> BST left -> BST right -> BST (some (AVLNode.mk a left right))
+
+@[simp]
+theorem singleton_bst [LT T] {a: T}: BST (some (AVLNode.mk a none none)) := by
+  apply BST.some
+  all_goals simp [ForallNode.none, BST.none] 
+
+theorem left [LT T] {t: AVLTree T}: BST t -> BST t.left := by
+  intro H
+  induction H with 
+  | none => exact BST.none
+  | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.left]; assumption
+
+theorem right [LT T] {t: AVLTree T}: BST t -> BST t.right := by
+  intro H
+  induction H with 
+  | none => exact BST.none
+  | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.right]; assumption
+
+end BST