diff options
Diffstat (limited to 'Common')
| -rw-r--r-- | Common/BinaryHeap.lean (renamed from Common/BTreeHeap.lean) | 58 |
1 files changed, 29 insertions, 29 deletions
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 |