summaryrefslogtreecommitdiff
path: root/AvlVerification/BinarySearchTree.lean
diff options
context:
space:
mode:
authorRyan Lahfa2024-04-23 14:26:27 +0200
committerGitHub2024-04-23 14:26:27 +0200
commitd3ea366adcd71d0ef15ffbc5d35ca998aa53f19a (patch)
treed9da70f7564ea73ceacf880b78473c89f617bba7 /AvlVerification/BinarySearchTree.lean
parent0f49a61cc33bddf2cc69bc8915b95c915dc5f987 (diff)
parentb650710ad3f8c14b713bdf52f684f472115dce2f (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.lean54
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