From 9da83df6319b806d584da9ae5c6da260fcae56a8 Mon Sep 17 00:00:00 2001
From: Raito Bezarius
Date: Thu, 4 Apr 2024 17:29:44 +0200
Subject: refactor: define some projectors for ForallNode

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
---
 AvlVerification/BinarySearchTree.lean | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'AvlVerification/BinarySearchTree.lean')

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
-- 
cgit v1.2.3

