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 <masterancpp@gmail.com>
---
 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


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


From 3577c7dc9d3013d401c45a7628b0ff4b6fd0ec67 Mon Sep 17 00:00:00 2001
From: Raito Bezarius
Date: Fri, 12 Apr 2024 19:11:16 +0200
Subject: feat: upgrade and close all proofs except Preorder on U32

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

(limited to 'AvlVerification/BinarySearchTree.lean')

diff --git a/AvlVerification/BinarySearchTree.lean b/AvlVerification/BinarySearchTree.lean
index 954f21f..2b17d52 100644
--- a/AvlVerification/BinarySearchTree.lean
+++ b/AvlVerification/BinarySearchTree.lean
@@ -10,34 +10,45 @@ 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
+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 BST [LT T]: AVLTree T -> Prop
-| none : BST none
+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
-  -> BST left -> BST right -> BST (some (AVLNode.mk a left right))
+  -> Invariant left -> Invariant right -> Invariant (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 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}: BST t -> BST t.left := by
+theorem left [LT T] {t: AVLTree T}: Invariant t -> Invariant t.left := by
   intro H
   induction H with 
-  | none => exact BST.none
+  | none => exact Invariant.none
   | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.left]; assumption
 
-theorem right [LT T] {t: AVLTree T}: BST t -> BST t.right := by
+theorem right [LT T] {t: AVLTree T}: Invariant t -> Invariant t.right := by
   intro H
   induction H with 
-  | none => exact BST.none
+  | none => exact Invariant.none
   | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.right]; assumption
 
 end BST
-- 
cgit v1.2.3