Heap: Nomenclature and namespace changes.

1 files changed, 25 insertions, 25 deletions

diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean
index b319d47..fe47c10 100644
--- a/Common/BinaryHeap.lean
+++ b/Common/BinaryHeap.lean
@@ -47,11 +47,6 @@ def HeapPredicate {α : Type u} {n : Nat} (heap : CompleteTree α n) (le : α �
                               | .zero => true
                               | .succ o => le v (h.root (Nat.succ_pos o))
 
-structure BinaryHeap (α : Type u) (le : α → α → Bool) (n : Nat) where
-  tree : CompleteTree α n
-  valid : HeapPredicate tree le
-  wellDefinedLe : transitive_le le ∧ total_le le
-
 /--Please do not use this for anything meaningful. It's a debug function, with horrible performance.-/
 instance {α : Type u} [ToString α] : ToString (CompleteTree α n) where
   toString := λt ↦
@@ -354,12 +349,6 @@ theorem CompleteTree.heapPushIsHeap {α : Type u} {elem : α} {heap : CompleteTr
       <;> simp only [instDecidableEqBool, Bool.decEq, h, and_self]
 end
 
-def BinaryHeap.insert {α : Type u} {lt : α → α → Bool} {n : Nat} : α → BinaryHeap α lt n → BinaryHeap α lt (n+1)
-| elem, BinaryHeap.mk tree valid wellDefinedLe =>
-  let valid := tree.heapPushIsHeap valid wellDefinedLe.left wellDefinedLe.right
-  let tree := tree.heapPush lt elem
-  {tree, valid, wellDefinedLe}
-
 /--Helper function for CompleteTree.indexOf.-/
 def CompleteTree.indexOfAux {α : Type u} (heap : CompleteTree α o) (pred : α → Bool) (currentIndex : Nat) : Option (Fin (o+currentIndex)) :=
   match o, heap with
@@ -497,7 +486,7 @@ private theorem CompleteTree.heqSameRightLen {α : Type u} {n m : Nat} {a : Comp
   rfl
 
 /--Shows that the index and value returned by heapRemoveLastWithIndex are consistent.-/
-theorem CompleteTree.heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : Nat} (heap : CompleteTree α (o+1)) : heap.get heap.heapRemoveLastWithIndex.snd.snd = heap.heapRemoveLastWithIndex.snd.fst := by
+private theorem CompleteTree.heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : Nat} (heap : CompleteTree α (o+1)) : heap.get heap.heapRemoveLastWithIndex.snd.snd = heap.heapRemoveLastWithIndex.snd.fst := by
   unfold heapRemoveLastWithIndex heapRemoveLastAux
   split
   rename_i n m v l r m_le_n max_height_difference subtree_full
@@ -722,12 +711,6 @@ private theorem CompleteTree.heapRemoveLastIsHeap {α : Type u} {heap : Complete
 private theorem CompleteTree.heapRemoveLastWithIndexIsHeap {α : Type u} {heap : CompleteTree α (o+1)} {le : α → α → Bool} (h₁ : HeapPredicate heap le) (h₂ : transitive_le le) (h₃ : total_le le) : HeapPredicate (heap.heapRemoveLastWithIndex.fst) le :=
   heapRemoveLastAuxIsHeap _ _ _ h₁ h₂ h₃
 
-private def BinaryHeap.heapRemoveLast {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le (n+1)) → BinaryHeap α le n × α
-| {tree, valid, wellDefinedLe} =>
-  let result := tree.heapRemoveLast
-  let resultValid := CompleteTree.heapRemoveLastIsHeap valid wellDefinedLe.left wellDefinedLe.right
-  ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd)
-
 /--
   Helper for CompleteTree.heapUpdateAt. Makes proofing heap predicate work in Lean 4.9
   -/
@@ -1162,12 +1145,6 @@ theorem CompleteTree.heapPopIsHeap {α : Type u} {n : Nat} (le : α → α → B
   unfold heapPop
   cases n <;> simp[h₂, heapUpdateRootIsHeap, wellDefinedLe]
 
-def BinaryHeap.RemoveRoot {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le (n+1)) → (BinaryHeap α le n × α)
-| {tree, valid, wellDefinedLe} =>
-  let result := tree.heapPop le
-  let resultValid := CompleteTree.heapPopIsHeap le tree valid wellDefinedLe
-  ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd)
-
 /--Removes the element at a given index. Use `CompleteTree.indexOf` to find the respective index.-/
 def CompleteTree.heapRemoveAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin (n+1)) (heap : CompleteTree α (n+1)) : CompleteTree α n × α :=
   --Since we cannot even temporarily break the completeness property, we go with the
@@ -1204,7 +1181,29 @@ theorem CompleteTree.heapRemoveAtIsHeap {α : Type u} {n : Nat} (le : α → α
     split
     <;> apply heapUpdateAtIsHeap <;> simp_all
 
-def BinaryHeap.RemoveAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le (n+1)) → (Fin (n+1)) → (BinaryHeap α le n × α)
+end BinaryHeap
+-------------------------------------------------------------------------------------------------------
+
+structure BinaryHeap (α : Type u) (le : α → α → Bool) (n : Nat) where
+  tree : BinaryHeap.CompleteTree α n
+  valid : BinaryHeap.HeapPredicate tree le
+  wellDefinedLe : BinaryHeap.transitive_le le ∧ BinaryHeap.total_le le
+
+namespace BinaryHeap
+
+def push {α : Type u} {lt : α → α → Bool} {n : Nat} : α → BinaryHeap α lt n → BinaryHeap α lt (n+1)
+| elem, .mk tree valid wellDefinedLe =>
+  let valid := tree.heapPushIsHeap valid wellDefinedLe.left wellDefinedLe.right
+  let tree := tree.heapPush lt elem
+  {tree, valid, wellDefinedLe}
+
+def pop {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le (n+1)) → (BinaryHeap α le n × α)
+| {tree, valid, wellDefinedLe} =>
+  let result := tree.heapPop le
+  let resultValid := CompleteTree.heapPopIsHeap le tree valid wellDefinedLe
+  ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd)
+
+def RemoveAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le (n+1)) → (Fin (n+1)) → (BinaryHeap α le n × α)
 | {tree, valid, wellDefinedLe}, index =>
   let result := tree.heapRemoveAt le index
   let resultValid := CompleteTree.heapRemoveAtIsHeap le index tree valid wellDefinedLe
@@ -1212,6 +1211,7 @@ def BinaryHeap.RemoveAt {α : Type u} {le : α → α → Bool} {n : Nat} : (Bin
 
 -------------------------------------------------------------------------------------------------------
 
+
 private def TestHeap :=
   let ins : {n: Nat} → Nat → CompleteTree Nat n → CompleteTree Nat (n+1) := λ x y ↦ CompleteTree.heapPush (.≤.) x y
   ins 5 CompleteTree.empty