From 3469d1e0e5e44c29484ff2f843c0863afa502eea Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Wed, 13 Dec 2023 19:43:48 +0100 Subject: Rename file to BinaryHeap, as it isn't a BTree --- Common/BTreeHeap.lean | 172 ------------------------------------------------- Common/BinaryHeap.lean | 172 +++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 172 insertions(+), 172 deletions(-) delete mode 100644 Common/BTreeHeap.lean create mode 100644 Common/BinaryHeap.lean (limited to 'Common') diff --git a/Common/BTreeHeap.lean b/Common/BTreeHeap.lean deleted file mode 100644 index e9424d3..0000000 --- a/Common/BTreeHeap.lean +++ /dev/null @@ -1,172 +0,0 @@ -namespace BTreeHeap - -/--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) - -/--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 - 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 - | 0, .leaf => 0 - | (_+_+1), BTreeHeap.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) ↦ - match m, t with - | 0, _ => "" - | (_+_+1), BTreeHeap.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) - let total_chars_this_line := elems_in_last_line * mw + 2*(elems_in_last_line)+1 - let left_offset := (total_chars_this_line - mw) / 2 - let whitespaces := max left_offset 1 - let whitespaces := List.replicate whitespaces ' ' - let thisline := whitespaces.asString ++ thisElem ++ whitespaces.asString ++"\n" - let leftLines := (print_line mw left (lines-1) ).splitOn "\n" - let rightLines := (print_line mw right (lines-1) ).splitOn "\n" ++ [""] - let combined := leftLines.zip (rightLines) - let combined := combined.map λ (a : String × String) ↦ a.fst ++ a.snd - thisline ++ combined.foldl (· ++ "\n" ++ ·) "" - 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 - -/--Creates an empty BTreeHeap. Needs the heap predicate as parameter.-/ -abbrev BTreeHeap.empty {α : Type u} (lt : α → α → Bool ) := BTreeHeap.leaf (α := α) (lt := lt) - -/--Adds a new element to a given BTreeHeap.-/ -def BTreeHeap.insert (elem : α) (heap : BTreeHeap α lt o) : BTreeHeap α lt (o+1) := - match o, heap with - | 0, .leaf => BTreeHeap.branch elem (BTreeHeap.leaf) (BTreeHeap.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. - -- the left tree is full, if (n+1) is a power of two AND n != m - let leftIsFull : Bool := (n+1).nextPowerOfTwo = n+1 - if r : m < n ∧ leftIsFull then - have s : (m + 1 < n + 1) = (m < n) := by simp_arith - have q : m + 1 ≤ n := by apply Nat.le_of_lt_succ - rewrite[Nat.succ_eq_add_one] - rewrite[s] - simp[r] - let result := branch a left (right.insert elem) (q) - result - else - have q : m ≤ n+1 := by apply (Nat.le_of_succ_le) - simp_arith[p] - let result := branch a (left.insert elem) right q - have letMeSpellItOutForYou : n + 1 + m + 1 = n + m + 1 + 1 := by simp_arith - 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)) := - match o, heap with - | 0, .leaf => none - | (n+m+1), .branch a left right _ => - if a == elem then - let result := Fin.ofNat' currentIndex (by simp_arith) - some result - else - let found_left := left.indexOfAux elem (currentIndex + 1) - let found_left : Option (Fin (n+m+1+currentIndex)) := found_left.map λ a ↦ Fin.ofNat' a (by simp_arith) - let found_right := - found_left - <|> - (right.indexOfAux elem (currentIndex + n + 1)).map ((λ a ↦ Fin.ofNat' a (by simp_arith)) : _ → Fin (n+m+1+currentIndex)) - 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) := - indexOfAux elem heap 0 - -private inductive Direction -| left -| right -deriving Repr - -theorem two_n_not_zero_n_not_zero (n : Nat) (p : ¬2*n = 0) : (¬n = 0) := by - cases n - case zero => contradiction - case succ => simp - -def BTreeHeap.popLast {α : Type u} {lt : α → α → Bool} (heap : BTreeHeap α lt (o+1)) : (α × BTreeHeap α lt o) := - match o, heap with - | (n+m), .branch a (left : BTreeHeap α lt n) (right : BTreeHeap α lt m) m_le_n => - if p : 0 = (n+m) then - (a, p▸BTreeHeap.leaf) - else - --let leftIsFull : Bool := (n+1).nextPowerOfTwo = n+1 - let rightIsFull : Bool := (m+1).nextPowerOfTwo = m+1 - have m_gt_0_or_rightIsFull : m > 0 ∨ rightIsFull := by cases m <;> simp_arith - if r : m < n ∧ rightIsFull then - --remove left - match n, left with - | (l+1), left => - let (res, (newLeft : BTreeHeap α 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) - else - --remove right - have : m > 0 := by - cases m_gt_0_or_rightIsFull - case inl => assumption - case inr h => simp_arith [h] at r - -- p, r, m_le_n combined - -- r and m_le_n yield m == n and p again done - simp_arith - --clear left right heap lt a h rightIsFull - have n_eq_m : n = m := Nat.le_antisymm r m_le_n - rewrite[n_eq_m] at p - simp_arith at p - apply Nat.zero_lt_of_ne_zero - simp_arith[p] - apply (two_n_not_zero_n_not_zero m) - intro g - have g := Eq.symm g - revert g - assumption - match m, right with - | (l+1), right => - let (res, (newRight : BTreeHeap α 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) - -/--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 := - -- 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)) - |> ins 3 - |> ins 7 - |> ins 12 - |> ins 2 - |> ins 8 - |> ins 97 - |> ins 2 - |> ins 64 - |> ins 71 - |> ins 21 - |> ins 3 - |> ins 4 - |> ins 199 - |> ins 24 - |> ins 3 - -#eval TestHeap -#eval TestHeap.popLast -#eval TestHeap.indexOf 71 diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean new file mode 100644 index 0000000..7e2724b --- /dev/null +++ b/Common/BinaryHeap.lean @@ -0,0 +1,172 @@ +namespace BinaryHeap + +/--A heap, represented as a binary indexed tree. The heap predicate is a type parameter, the index is the element count.-/ +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 (BinaryHeap α lt n) where + toString := λt ↦ + --not very fast, doesn't matter, is for debugging + let rec max_width := λ {m : Nat} (t : (BinaryHeap α lt m)) ↦ match m, t with + | 0, .leaf => 0 + | (_+_+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 : (BinaryHeap α lt m)) (lines : Nat) ↦ + match m, t with + | 0, _ => "" + | (_+_+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) + let total_chars_this_line := elems_in_last_line * mw + 2*(elems_in_last_line)+1 + let left_offset := (total_chars_this_line - mw) / 2 + let whitespaces := max left_offset 1 + let whitespaces := List.replicate whitespaces ' ' + let thisline := whitespaces.asString ++ thisElem ++ whitespaces.asString ++"\n" + let leftLines := (print_line mw left (lines-1) ).splitOn "\n" + let rightLines := (print_line mw right (lines-1) ).splitOn "\n" ++ [""] + let combined := leftLines.zip (rightLines) + let combined := combined.map λ (a : String × String) ↦ a.fst ++ a.snd + thisline ++ combined.foldl (· ++ "\n" ++ ·) "" + print_line max_width t lines_left + +/-- Extracts the element count. For when pattern matching is too much work. -/ +def BinaryHeap.length : BinaryHeap α lt n → Nat := λ_ ↦ n + +/--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 BinaryHeap.-/ +def BinaryHeap.insert (elem : α) (heap : BinaryHeap α lt o) : BinaryHeap α lt (o+1) := + match o, heap with + | 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. + -- the left tree is full, if (n+1) is a power of two AND n != m + let leftIsFull : Bool := (n+1).nextPowerOfTwo = n+1 + if r : m < n ∧ leftIsFull then + have s : (m + 1 < n + 1) = (m < n) := by simp_arith + have q : m + 1 ≤ n := by apply Nat.le_of_lt_succ + rewrite[Nat.succ_eq_add_one] + rewrite[s] + simp[r] + let result := branch a left (right.insert elem) (q) + result + else + have q : m ≤ n+1 := by apply (Nat.le_of_succ_le) + simp_arith[p] + let result := branch a (left.insert elem) right q + have letMeSpellItOutForYou : n + 1 + m + 1 = n + m + 1 + 1 := by simp_arith + letMeSpellItOutForYou ▸ result + + +/--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 _ => + if a == elem then + let result := Fin.ofNat' currentIndex (by simp_arith) + some result + else + let found_left := left.indexOfAux elem (currentIndex + 1) + let found_left : Option (Fin (n+m+1+currentIndex)) := found_left.map λ a ↦ Fin.ofNat' a (by simp_arith) + let found_right := + found_left + <|> + (right.indexOfAux elem (currentIndex + n + 1)).map ((λ a ↦ Fin.ofNat' a (by simp_arith)) : _ → Fin (n+m+1+currentIndex)) + found_right + +/--Finds the first occurance of a given element in the heap and returns its index.-/ +def BinaryHeap.indexOf {α : Type u} {lt : α → α → Bool} [BEq α] (elem : α) (heap : BinaryHeap α lt o) : Option (Fin o) := + indexOfAux elem heap 0 + +private inductive Direction +| left +| right +deriving Repr + +theorem two_n_not_zero_n_not_zero (n : Nat) (p : ¬2*n = 0) : (¬n = 0) := by + cases n + case zero => contradiction + case succ => simp + +def BinaryHeap.popLast {α : Type u} {lt : α → α → Bool} (heap : BinaryHeap α lt (o+1)) : (α × BinaryHeap α lt o) := + match o, heap with + | (n+m), .branch a (left : BinaryHeap α lt n) (right : BinaryHeap α lt m) m_le_n => + if p : 0 = (n+m) then + (a, p▸BinaryHeap.leaf) + else + --let leftIsFull : Bool := (n+1).nextPowerOfTwo = n+1 + let rightIsFull : Bool := (m+1).nextPowerOfTwo = m+1 + have m_gt_0_or_rightIsFull : m > 0 ∨ rightIsFull := by cases m <;> simp_arith + if r : m < n ∧ rightIsFull then + --remove left + match n, left with + | (l+1), left => + 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▸BinaryHeap.branch a newLeft right s) + else + --remove right + have : m > 0 := by + cases m_gt_0_or_rightIsFull + case inl => assumption + case inr h => simp_arith [h] at r + -- p, r, m_le_n combined + -- r and m_le_n yield m == n and p again done + simp_arith + --clear left right heap lt a h rightIsFull + have n_eq_m : n = m := Nat.le_antisymm r m_le_n + rewrite[n_eq_m] at p + simp_arith at p + apply Nat.zero_lt_of_ne_zero + simp_arith[p] + apply (two_n_not_zero_n_not_zero m) + intro g + have g := Eq.symm g + revert g + assumption + match m, right with + | (l+1), right => + 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, BinaryHeap.branch a left newRight s) + +/--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 → 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 + |> ins 2 + |> ins 8 + |> ins 97 + |> ins 2 + |> ins 64 + |> ins 71 + |> ins 21 + |> ins 3 + |> ins 4 + |> ins 199 + |> ins 24 + |> ins 3 + +#eval TestHeap +#eval TestHeap.popLast +#eval TestHeap.indexOf 71 -- cgit v1.2.3