diff options
author | Ryan Lahfa | 2024-04-23 14:26:27 +0200 |
---|---|---|
committer | GitHub | 2024-04-23 14:26:27 +0200 |
commit | d3ea366adcd71d0ef15ffbc5d35ca998aa53f19a (patch) | |
tree | d9da70f7564ea73ceacf880b78473c89f617bba7 /AvlVerification/BinarySearchTree.lean | |
parent | 0f49a61cc33bddf2cc69bc8915b95c915dc5f987 (diff) | |
parent | b650710ad3f8c14b713bdf52f684f472115dce2f (diff) |
Merge pull request #3 from RaitoBezarius/bst-find
feat: `find` and `insert` reinforced proofs
Diffstat (limited to 'AvlVerification/BinarySearchTree.lean')
-rw-r--r-- | AvlVerification/BinarySearchTree.lean | 54 |
1 files changed, 0 insertions, 54 deletions
diff --git a/AvlVerification/BinarySearchTree.lean b/AvlVerification/BinarySearchTree.lean deleted file mode 100644 index 2b17d52..0000000 --- a/AvlVerification/BinarySearchTree.lean +++ /dev/null @@ -1,54 +0,0 @@ -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)) - -theorem ForallNode.left {p: T -> Prop} {t: AVLTree T}: ForallNode p t -> ForallNode p t.left := by - intro Hpt - cases Hpt with - | none => simp [AVLTree.left, ForallNode.none] - | some a left right f_pleft f_pa f_pright => simp [AVLTree.left, f_pleft] - -theorem ForallNode.right {p: T -> Prop} {t: AVLTree T}: ForallNode p t -> ForallNode p t.right := by - intro Hpt - cases Hpt with - | none => simp [AVLTree.right, ForallNode.none] - | some a left right f_pleft f_pa f_pright => simp [AVLTree.right, f_pright] - -theorem ForallNode.label {a: T} {p: T -> Prop} {left right: AVLTree T}: ForallNode p (AVLNode.mk a left right) -> p a := by - intro Hpt - cases Hpt with - | some a left right f_pleft f_pa f_pright => exact f_pa - --- This is the binary search invariant. -inductive Invariant [LT T]: AVLTree T -> Prop -| none : Invariant none -| some (a: T) (left: AVLTree T) (right: AVLTree T) : - ForallNode (fun v => v < a) left -> ForallNode (fun v => a < v) right - -> Invariant left -> Invariant right -> Invariant (some (AVLNode.mk a left right)) - -@[simp] -theorem singleton_bst [LT T] {a: T}: Invariant (some (AVLNode.mk a none none)) := by - apply Invariant.some - all_goals simp [ForallNode.none, Invariant.none] - -theorem left [LT T] {t: AVLTree T}: Invariant t -> Invariant t.left := by - intro H - induction H with - | none => exact Invariant.none - | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.left]; assumption - -theorem right [LT T] {t: AVLTree T}: Invariant t -> Invariant t.right := by - intro H - induction H with - | none => exact Invariant.none - | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.right]; assumption - -end BST |