Rename file to BinaryHeap, as it isn't a BTree

2 files changed, 30 insertions, 30 deletions

diff --git a/Common.lean b/Common.lean
index 32b40ec..1eedec8 100644
--- a/Common.lean
+++ b/Common.lean
@@ -5,4 +5,4 @@ import Common.String
 import Common.List
 import Common.Char
 import Common.Euclid
-import Common.BTreeHeap
+import Common.BinaryHeap
diff --git a/Common/BTreeHeap.lean b/Common/BinaryHeap.lean
index e9424d3..7e2724b 100644
--- a/Common/BTreeHeap.lean
+++ b/Common/BinaryHeap.lean
@@ -1,23 +1,23 @@
-namespace BTreeHeap
+namespace BinaryHeap
 
 /--A heap, represented as a binary indexed tree. The heap predicate is a type parameter, the index is the element count.-/
-inductive BTreeHeap (α : Type u) (lt : α → α → Bool): Nat → Type u
-  | leaf : BTreeHeap α lt 0
-  | branch : (val : α) → (left : BTreeHeap α lt n) → (right : BTreeHeap α lt m) → m ≤ n →  BTreeHeap α lt (n+m+1)
+inductive BinaryHeap (α : Type u) (lt : α → α → Bool): Nat → Type u
+  | leaf : BinaryHeap α lt 0
+  | branch : (val : α) → (left : BinaryHeap α lt n) → (right : BinaryHeap α lt m) → m ≤ n →  BinaryHeap α lt (n+m+1)
 
 /--Please do not use this for anything meaningful. It's a debug function, with horrible performance.-/
-instance {α : Type u} {lt : α → α → Bool} [ToString α] : ToString (BTreeHeap α lt n) where
+instance {α : Type u} {lt : α → α → Bool} [ToString α] : ToString (BinaryHeap α lt n) where
   toString := λt ↦
     --not very fast, doesn't matter, is for debugging
-    let rec max_width := λ {m : Nat} (t : (BTreeHeap α lt m)) ↦ match m, t with
+    let rec max_width := λ {m : Nat} (t : (BinaryHeap α lt m)) ↦ match m, t with
     | 0, .leaf => 0
-    | (_+_+1), BTreeHeap.branch a left right _ => max (ToString.toString a).length $ max (max_width left) (max_width right)
+    | (_+_+1), BinaryHeap.branch a left right _ => max (ToString.toString a).length $ max (max_width left) (max_width right)
     let max_width := max_width t
     let lines_left := Nat.log2 (n+1).nextPowerOfTwo
-    let rec print_line := λ (mw : Nat) {m : Nat} (t : (BTreeHeap α lt m)) (lines : Nat)  ↦
+    let rec print_line := λ (mw : Nat) {m : Nat} (t : (BinaryHeap α lt m)) (lines : Nat)  ↦
       match m, t with
       | 0, _ => ""
-      | (_+_+1), BTreeHeap.branch a left right _ =>
+      | (_+_+1), BinaryHeap.branch a left right _ =>
         let thisElem := ToString.toString a
         let thisElem := (List.replicate (mw - thisElem.length) ' ').asString ++ thisElem
         let elems_in_last_line := if lines == 0 then 0 else 2^(lines-1)
@@ -34,15 +34,15 @@ instance {α : Type u} {lt : α → α → Bool} [ToString α] : ToString (BTree
     print_line max_width t lines_left
 
 /-- Extracts the element count. For when pattern matching is too much work. -/
-def BTreeHeap.length : BTreeHeap α lt n → Nat := λ_ ↦ n
+def BinaryHeap.length : BinaryHeap α lt n → Nat := λ_ ↦ n
 
-/--Creates an empty BTreeHeap. Needs the heap predicate as parameter.-/
-abbrev BTreeHeap.empty {α : Type u} (lt : α → α → Bool ) := BTreeHeap.leaf (α := α) (lt := lt)
+/--Creates an empty BinaryHeap. Needs the heap predicate as parameter.-/
+abbrev BinaryHeap.empty {α : Type u} (lt : α → α → Bool ) := BinaryHeap.leaf (α := α) (lt := lt)
 
-/--Adds a new element to a given BTreeHeap.-/
-def BTreeHeap.insert (elem : α) (heap : BTreeHeap α lt o) : BTreeHeap α lt (o+1) :=
+/--Adds a new element to a given BinaryHeap.-/
+def BinaryHeap.insert (elem : α) (heap : BinaryHeap α lt o) : BinaryHeap α lt (o+1) :=
   match o, heap with
-  | 0, .leaf => BTreeHeap.branch elem (BTreeHeap.leaf) (BTreeHeap.leaf) (by simp)
+  | 0, .leaf => BinaryHeap.branch elem (BinaryHeap.leaf) (BinaryHeap.leaf) (by simp)
   | (n+m+1), .branch a left right p =>
     let (elem, a) := if lt elem a then (a, elem) else (elem, a)
     -- okay, based on n and m we know if we want to add left or right.
@@ -64,8 +64,8 @@ def BTreeHeap.insert (elem : α) (heap : BTreeHeap α lt o) : BTreeHeap α lt (o
       letMeSpellItOutForYou ▸ result
 
 
-/--Helper function for BTreeHeap.indexOf.-/
-def BTreeHeap.indexOfAux {α : Type u} {lt : α → α → Bool} [BEq α] (elem : α) (heap : BTreeHeap α lt o) (currentIndex : Nat) : Option (Fin (o+currentIndex)) :=
+/--Helper function for BinaryHeap.indexOf.-/
+def BinaryHeap.indexOfAux {α : Type u} {lt : α → α → Bool} [BEq α] (elem : α) (heap : BinaryHeap α lt o) (currentIndex : Nat) : Option (Fin (o+currentIndex)) :=
   match o, heap with
   | 0, .leaf => none
   | (n+m+1), .branch a left right _ =>
@@ -82,7 +82,7 @@ def BTreeHeap.indexOfAux {α : Type u} {lt : α → α → Bool} [BEq α] (elem
       found_right
 
 /--Finds the first occurance of a given element in the heap and returns its index.-/
-def BTreeHeap.indexOf {α : Type u} {lt : α → α → Bool} [BEq α] (elem : α) (heap : BTreeHeap α lt o) : Option (Fin o) :=
+def BinaryHeap.indexOf {α : Type u} {lt : α → α → Bool} [BEq α] (elem : α) (heap : BinaryHeap α lt o) : Option (Fin o) :=
   indexOfAux elem heap 0
 
 private inductive Direction
@@ -95,11 +95,11 @@ theorem two_n_not_zero_n_not_zero (n : Nat) (p : ¬2*n = 0) : (¬n = 0) := by
   case zero => contradiction
   case succ => simp
 
-def BTreeHeap.popLast {α : Type u} {lt : α → α → Bool} (heap : BTreeHeap α lt (o+1)) : (α × BTreeHeap α lt o) :=
+def BinaryHeap.popLast {α : Type u} {lt : α → α → Bool} (heap : BinaryHeap α lt (o+1)) : (α × BinaryHeap α lt o) :=
   match o, heap with
-  | (n+m), .branch a (left : BTreeHeap α lt n) (right : BTreeHeap α lt m) m_le_n =>
+  | (n+m), .branch a (left : BinaryHeap α lt n) (right : BinaryHeap α lt m) m_le_n =>
     if p : 0 = (n+m) then
-      (a, p▸BTreeHeap.leaf)
+      (a, p▸BinaryHeap.leaf)
     else
       --let leftIsFull : Bool := (n+1).nextPowerOfTwo = n+1
       let rightIsFull : Bool := (m+1).nextPowerOfTwo = m+1
@@ -108,12 +108,12 @@ def BTreeHeap.popLast {α : Type u} {lt : α → α → Bool} (heap : BTreeHeap
         --remove left
         match n, left with
         | (l+1), left =>
-          let (res, (newLeft : BTreeHeap α lt l)) := left.popLast
+          let (res, (newLeft : BinaryHeap α lt l)) := left.popLast
           have q : l + m + 1 = l + 1 +m := by simp_arith
           have s : m ≤ l := match r with
           | .intro a _ => by apply Nat.le_of_lt_succ
                              simp[a]
-          (res, q▸BTreeHeap.branch a newLeft right s)
+          (res, q▸BinaryHeap.branch a newLeft right s)
       else
         --remove right
         have : m > 0 := by
@@ -136,21 +136,21 @@ def BTreeHeap.popLast {α : Type u} {lt : α → α → Bool} (heap : BTreeHeap
                         assumption
         match m, right with
         | (l+1), right =>
-          let (res, (newRight : BTreeHeap α lt l)) := right.popLast
+          let (res, (newRight : BinaryHeap α lt l)) := right.popLast
           have s : l ≤ n := by have x := (Nat.add_le_add_left (Nat.zero_le 1) l)
                                have x := Nat.le_trans x m_le_n
                                assumption
-          (res, BTreeHeap.branch a left newRight s)
+          (res, BinaryHeap.branch a left newRight s)
 
-/--Removes the element at a given index. Use `BTreeHeap.indexOf` to find the respective index.-/
-def BTreeHeap.removeAt {α : Type u} {lt : α → α → Bool} {o : Nat} (index : Fin (o+1)) (heap : BTreeHeap α lt (o+1)) : BTreeHeap α lt o :=
+/--Removes the element at a given index. Use `BinaryHeap.indexOf` to find the respective index.-/
+def BinaryHeap.removeAt {α : Type u} {lt : α → α → Bool} {o : Nat} (index : Fin (o+1)) (heap : BinaryHeap α lt (o+1)) : BinaryHeap α lt o :=
   -- first remove the last element and remember its value
   sorry
 
 -------------------------------------------------------------------------------------------------------
 
-private def TestHeap := let ins : {n: Nat} → Nat → BTreeHeap Nat (λ (a b : Nat) ↦ a < b) n → BTreeHeap Nat (λ (a b : Nat) ↦ a < b) (n+1) := BTreeHeap.insert
-  ins 5 (BTreeHeap.empty (λ (a b : Nat) ↦ a < b))
+private def TestHeap := let ins : {n: Nat} → Nat → BinaryHeap Nat (λ (a b : Nat) ↦ a < b) n → BinaryHeap Nat (λ (a b : Nat) ↦ a < b) (n+1) := BinaryHeap.insert
+  ins 5 (BinaryHeap.empty (λ (a b : Nat) ↦ a < b))
   |> ins 3
   |> ins 7
   |> ins 12