summaryrefslogtreecommitdiff
path: root/AvlVerification/BinarySearchTree.lean
diff options
context:
space:
mode:
authorRaito Bezarius2024-03-28 17:59:35 +0100
committerRaito Bezarius2024-03-28 20:30:56 +0100
commit5e35e3875884ca4be63f253d9e8d7f2fc71b3527 (patch)
treece607fcdda121b87b133791d5e708c6809559a20 /AvlVerification/BinarySearchTree.lean
parent33a92dac2635ead90cb84c16023355a7d679d434 (diff)
refactor: generalize the theory and perform some lifts
Move forward the "HSpec" idea, move around files, construct the hierarchy of trees, etc. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
Diffstat (limited to '')
-rw-r--r--AvlVerification/BinarySearchTree.lean37
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