From 5e35e3875884ca4be63f253d9e8d7f2fc71b3527 Mon Sep 17 00:00:00 2001 From: Raito Bezarius Date: Thu, 28 Mar 2024 17:59:35 +0100 Subject: 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 --- AvlVerification/BinarySearchTree.lean | 37 +++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 AvlVerification/BinarySearchTree.lean (limited to 'AvlVerification/BinarySearchTree.lean') 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 -- cgit v1.2.3