Merge pull request #3 from RaitoBezarius/bst-find

feat: `find` and `insert` reinforced proofs

4 files changed, 0 insertions, 406 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
diff --git a/AvlVerification/Insert.lean b/AvlVerification/Insert.lean
deleted file mode 100644
index f5b7958..0000000
--- a/AvlVerification/Insert.lean
+++ /dev/null
@@ -1,173 +0,0 @@
-import AvlVerification.Tree
-import AvlVerification.BinarySearchTree
-import AvlVerification.Specifications
-
-namespace Implementation
-
-open Primitives
-open avl_verification
-open Tree (AVLTree AVLTree.set)
-open Specifications (OrdSpecDualityEq ordOfOrdSpec ltOfRustOrder gtOfRustOrder)
-
--- example: OrdSpec OrdU32 := ordSpecOfTotalityAndDuality _ 
---   (by 
---   -- Totality
---   intro a b
---   unfold Ord.cmp
---   unfold OrdU32
---   unfold OrdU32.cmp
---   if hlt : a < b then 
---     use .Less
---     simp [hlt]
---   else
---     if heq: a = b
---     then
---     use .Equal
---     simp [hlt]
---     rw [heq]
---     -- TODO: simp [hlt, heq] breaks everything???
---     else
---       use .Greater
---       simp [hlt, heq]
---   ) (by 
---   -- Duality
---   intro a b Hgt
---   if hlt : b < a then
---     unfold Ord.cmp
---     unfold OrdU32
---     unfold OrdU32.cmp
---     simp [hlt]
---   else
---     unfold Ord.cmp at Hgt
---     unfold OrdU32 at Hgt
---     unfold OrdU32.cmp at Hgt
---     have hnlt : ¬ (a < b) := sorry
---     have hneq : ¬ (a = b) := sorry
---     exfalso
---     apply hlt
---     -- I need a Preorder on U32 now.
---     sorry)
-
-variable (T: Type) (H: avl_verification.Ord T) (Ospec: @OrdSpecDualityEq T H)
-
-@[pspec]
-theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop)
-  (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ok o)
-  (a: T) (t: Option (AVLNode T)):
-  ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ok ⟨ added, t_new ⟩
---  ∧ AVLTree.set t'.2 = insert a (AVLTree.set t)
-  ∧ (BST.ForallNode p t -> p a -> BST.ForallNode p t_new)
-  := by match t with
-  | none =>
-    simp [AVLTreeSet.insert_loop, AVLTree.set, setOf]
-    intros _ Hpa
-    constructor; all_goals try simp [BST.ForallNode.none]
-    exact Hpa
-  | some (AVLNode.mk b left right) =>
-    rw [AVLTreeSet.insert_loop]
-    simp only []
-    progress keep Hordering as ⟨ ordering ⟩
-    cases ordering
-    all_goals simp only []
-    {
-      progress keep Htree as ⟨ added₁, right₁, Hnode ⟩
-      refine' ⟨ added₁, ⟨ some (AVLNode.mk b left right₁), _ ⟩ ⟩
-      simp only [true_and]
-      intros Hptree Hpa
-      constructor
-      exact Hptree.left
-      exact Hptree.label
-      exact Hnode Hptree.right Hpa
-    }
-    {
-      simp; tauto
-    }
-    {
-      -- TODO: investigate wlog.
-      -- Symmetric case of left.
-      progress keep Htree as ⟨ added₁, left₁, Hnode ⟩
-      refine' ⟨ added₁, ⟨ some (AVLNode.mk b left₁ right), _ ⟩ ⟩
-      simp only [true_and]
-      intros Hptree Hpa
-      constructor
-      exact Hnode Hptree.left Hpa
-      exact Hptree.label
-      exact Hptree.right
-    }
-
-@[pspec]
-lemma AVLTreeSet.insert_loop_spec_global
-  (a: T) (t: Option (AVLNode T))
-  :
-  BST.Invariant t -> ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ok ⟨ added, t_new ⟩
-  ∧ BST.Invariant t_new ∧ AVLTree.set t_new = {a} ∪ AVLTree.set t := by 
-  intro Hbst
-  match t with
-  | none => simp [AVLTreeSet.insert_loop, AVLTree.set, setOf]
-  | some (AVLNode.mk b left right) =>
-    rw [AVLTreeSet.insert_loop]
-    simp only []
-    have : ∀ a b, ∃ o, H.cmp a b = .ok o := Ospec.infallible
-    progress keep Hordering as ⟨ ordering ⟩
-    cases ordering
-    all_goals simp only []
-    {
-      have ⟨ added₂, right₂, ⟨ H_result, ⟨ H_bst, H_set ⟩ ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a right (BST.right Hbst)
-      progress keep Htree with AVLTreeSet.insert_loop_spec_local as ⟨ added₁, right₁, Hnode ⟩
-      exact (fun x => b < x)
-      rewrite [Htree] at H_result; simp at H_result
-      refine' ⟨ added₁, ⟨ some (AVLNode.mk b left right₁), _ ⟩ ⟩
-      simp only [true_and]
-      split_conjs
-      cases' Hbst with _ _ _ H_forall_left H_forall_right H_bst_left H_bst_right
-      constructor
-      exact H_forall_left
-      apply Hnode; exact H_forall_right
-      exact (ltOfRustOrder H b a Hordering)
-      exact H_bst_left
-      convert H_bst
-      exact H_result.2
-      simp [AVLTree.set_some]
-      rewrite [H_result.2, H_set]
-      simp
-    }
-    {
-      simp; split_conjs
-      . tauto
-      . simp [Ospec.equivalence _ _ Hordering]
-    }
-    {
-      have ⟨ added₂, left₂, ⟨ H_result, ⟨ H_bst, H_set ⟩ ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a left (BST.left Hbst)
-      progress keep Htree with AVLTreeSet.insert_loop_spec_local as ⟨ added₁, left₁, Hnode ⟩
-      exact (fun x => x < b)
-      rewrite [Htree] at H_result; simp at H_result
-      refine' ⟨ added₁, ⟨ some (AVLNode.mk b left₁ right), _ ⟩ ⟩
-      simp only [true_and]
-      split_conjs
-      cases' Hbst with _ _ _ H_forall_left H_forall_right H_bst_left H_bst_right
-      constructor
-      apply Hnode; exact H_forall_left
-      exact (gtOfRustOrder H b a Hordering)
-      exact H_forall_right
-      convert H_bst
-      exact H_result.2
-      exact H_bst_right
-      simp [AVLTree.set_some]
-      rewrite [H_result.2, H_set]
-      simp [Set.singleton_union, Set.insert_comm, Set.insert_union]
-    }
-
-@[pspec]
-def AVLTreeSet.insert_spec 
-  (a: T) (t: AVLTreeSet T):
-  BST.Invariant t.root -> (∃ t' added,t.insert _ H a = Result.ok (added, t')
-  -- it's still a binary search tree.
-  ∧ BST.Invariant t'.root
-  ∧ AVLTree.set t'.root = {a} ∪ AVLTree.set t.root)
-  := by
-  rw [AVLTreeSet.insert]; intro Hbst
-  progress keep h as ⟨ t', Hset ⟩; 
-  simp; assumption
-
-end Implementation
-
diff --git a/AvlVerification/Specifications.lean b/AvlVerification/Specifications.lean
deleted file mode 100644
index ac2d056..0000000
--- a/AvlVerification/Specifications.lean
+++ /dev/null
@@ -1,98 +0,0 @@
-import «AvlVerification»
-
-namespace Primitives
-
-namespace Result
-
-def map {A B: Type} (x: Result A) (f: A -> B): Result B := match x with
-| .ok y => .ok (f y)
-| .fail e => .fail e
-| .div => .div
-
-@[inline]
-def isok {A: Type} : Result A -> Bool
-| .ok _ => true
-| .fail _ => false
-| .div => false
-
-@[inline]
-def get? {A: Type}: (r: Result A) -> isok r -> A
-| .ok x, _ => x
-
-end Result
-
-end Primitives
-
-namespace avl_verification
-
-def Ordering.toLeanOrdering (o: avl_verification.Ordering): _root_.Ordering := match o with 
-| .Less => .lt
-| .Equal => .eq
-| .Greater => .gt
-
-def Ordering.ofLeanOrdering (o: _root_.Ordering): avl_verification.Ordering := match o with
-| .lt => .Less
-| .eq => .Equal
-| .gt => .Greater
-
-end avl_verification
-
-namespace Specifications
-
-open Primitives
-open Result
-
-variable {T: Type} (H: outParam (avl_verification.Ord T))
-
--- TODO: reason about raw bundling vs. refined bundling.
--- raw bundling: hypothesis with Rust extracted objects.
--- refined bundling: lifted hypothesis with Lean native objects.
-class OrdSpecInfaillible where
-  infallible: ∀ a b, ∃ (o: avl_verification.Ordering), H.cmp a b = .ok o
-
-class OrdSpecDuality extends OrdSpecInfaillible H where
-  duality: ∀ a b, H.cmp a b = .ok .Greater -> H.cmp b a = .ok .Less
-
-class OrdSpecRel (R: outParam (T -> T -> Prop)) extends OrdSpecInfaillible H where
-  equivalence: ∀ a b, H.cmp a b = .ok .Equal -> R a b
-
-class OrdSpecDualityEq extends OrdSpecDuality H, OrdSpecRel H Eq
-
-instance: Coe (avl_verification.Ordering) (_root_.Ordering) where
-  coe a := a.toLeanOrdering
-
-def ordOfOrdSpec (H: avl_verification.Ord T) (spec: OrdSpecInfaillible H): Ord T where
-  compare x y := (H.cmp x y).get? (by
-    cases' (spec.infallible x y) with o Hcmp
-    rewrite [isok, Hcmp]
-    simp only
-  )
-
-instance [spec: OrdSpecInfaillible H]: Ord T := ordOfOrdSpec H spec
-instance [OrdSpecInfaillible H]: LT T := ltOfOrd
-
-theorem ltOfRustOrder {Spec: OrdSpecInfaillible H}: 
-  haveI O := ordOfOrdSpec H Spec
-  haveI := @ltOfOrd _ O
-  ∀ a b, H.cmp a b = .ok .Less -> a < b := by
-  intros a b
-  intro Hcmp
-  rw [LT.lt]
-  simp [ltOfOrd]
-  rw [compare]
-  simp [ordOfOrdSpec]
-  -- https://proofassistants.stackexchange.com/questions/1062/what-does-the-motive-is-not-type-correct-error-mean-in-lean
-  simp_rw [Hcmp, get?, avl_verification.Ordering.toLeanOrdering]
-  rfl
-
-theorem gtOfRustOrder {Spec: OrdSpecDuality H}: 
-  haveI O := ordOfOrdSpec H Spec.toOrdSpecInfaillible
-  haveI := @ltOfOrd _ O
-  ∀ a b, H.cmp a b = .ok .Greater -> b < a := by
-  intros a b
-  intro Hcmp
-  apply ltOfRustOrder
-  exact (Spec.duality _ _ Hcmp)
-
-
-end Specifications
diff --git a/AvlVerification/Tree.lean b/AvlVerification/Tree.lean
deleted file mode 100644
index 8a043a1..0000000
--- a/AvlVerification/Tree.lean
+++ /dev/null
@@ -1,81 +0,0 @@
-import «AvlVerification»
-
-namespace Tree
-
-variable {T: Type}
-
-open avl_verification
-
--- Otherwise, Lean cannot prove termination by itself.
-@[reducible]
-def AVLTree (U: Type) := Option (AVLNode U)
-def AVLTree.nil: AVLTree T := none
-
-def AVLTree.val (t: AVLTree T): Option T := match t with
-| none => none
-| some (AVLNode.mk x _ _) => some x
-
-def AVLTree.left (t: AVLTree T): AVLTree T := match t with
-| none => none
-| some (AVLNode.mk _ left _) => left
-
-def AVLTree.right (t: AVLTree T): AVLTree T := match t with
-| none => none
-| some (AVLNode.mk _ _ right) => right
-
-def AVLNode.left (t: AVLNode T): AVLTree T := match t with
-| AVLNode.mk _ left _ => left
-
-def AVLNode.right (t: AVLNode T): AVLTree T := match t with
-| AVLNode.mk _ _ right => right
-
-def AVLNode.val (t: AVLNode T): T := match t with
-| AVLNode.mk x _ _ => x
-
-mutual
-def AVLTree.height_node (tree: AVLNode T): Nat := match tree with
-| AVLNode.mk y left right => 1 + AVLTree.height left + AVLTree.height right
-
-def AVLTree.height (tree: AVLTree T): Nat := match tree with 
-| none => 0
-| some n => 1 + AVLTree.height_node n
-end
-
-def AVLTreeSet.nil: AVLTreeSet T := { root := AVLTree.nil }
-
--- Automatic synthesization of this seems possible at the Lean level?
-instance: Inhabited (AVLTree T) where
-  default := AVLTree.nil
-
-instance: Inhabited (AVLTreeSet T) where
-  default := AVLTreeSet.nil
-
-instance: Coe (Option (AVLNode T)) (AVLTree T) where
-  coe x := x
-
--- TODO: ideally, it would be nice if we could generalize
--- this to any `BinaryTree` typeclass.
-
-def AVLTree.mem (tree: AVLTree T) (x: T) :=
-  match tree with
-  | none => False
-  | some (AVLNode.mk y left right) => x = y ∨ AVLTree.mem left x ∨ AVLTree.mem right x
-
-@[simp]
-def AVLTree.mem_none: AVLTree.mem none = ({}: Set T) := rfl
-
-@[simp]
-def AVLTree.mem_some {x: T} {left right: AVLTree T}: AVLTree.mem (some (AVLNode.mk x left right)) = (({x}: Set T) ∪ AVLTree.mem left ∪ AVLTree.mem right) := by
-  ext y
-  rw [AVLTree.mem]
-  simp [Set.insert_union]
-  simp [Set.insert_def, Set.setOf_set, Set.mem_def, Set.union_def]
-
--- TODO(reinforcement): ∪ is actually disjoint if we prove this is a binary search tree.
-
-def AVLTree.set (t: AVLTree T): Set T := _root_.setOf (AVLTree.mem t)
-
-@[simp]
-def AVLTree.set_some {x: T} {left right: AVLTree T}: AVLTree.set (some (AVLNode.mk x left right)) = {x} ∪ AVLTree.set left ∪ AVLTree.set right := sorry
-
-end Tree