diff options
| author | Raito Bezarius | 2024-04-04 17:29:44 +0200 |
|---|---|---|
| committer | Raito Bezarius | 2024-04-04 17:29:44 +0200 |
| commit | 9da83df6319b806d584da9ae5c6da260fcae56a8 (patch) | |
| tree | 021350154bc7d40d8d4b48fe86002069618316b1 | |
| parent | 5e35e3875884ca4be63f253d9e8d7f2fc71b3527 (diff) | |
refactor: define some projectors for ForallNode
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
Diffstat (limited to '')
| -rw-r--r-- | AvlVerification/BinarySearchTree.lean | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/AvlVerification/BinarySearchTree.lean b/AvlVerification/BinarySearchTree.lean index 130fd73..954f21f 100644 --- a/AvlVerification/BinarySearchTree.lean +++ b/AvlVerification/BinarySearchTree.lean @@ -10,6 +10,12 @@ 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 := sorry + +theorem ForallNode.right {p: T -> Prop} {t: AVLTree T}: ForallNode p t -> ForallNode p t.right := sorry + +theorem ForallNode.label {a: T} {p: T -> Prop} {left right: AVLTree T}: ForallNode p (AVLNode.mk a left right) -> p a := sorry + -- This is the binary search invariant. inductive BST [LT T]: AVLTree T -> Prop | none : BST none |