diff options
author | Raito Bezarius | 2024-03-28 17:59:35 +0100 |
---|---|---|
committer | Raito Bezarius | 2024-03-28 20:30:56 +0100 |
commit | 5e35e3875884ca4be63f253d9e8d7f2fc71b3527 (patch) | |
tree | ce607fcdda121b87b133791d5e708c6809559a20 /AvlVerification/BinarySearchTree.lean | |
parent | 33a92dac2635ead90cb84c16023355a7d679d434 (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.lean | 37 |
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 |