diff options
| -rw-r--r-- | BinaryHeap.lean | 88 | ||||
| -rw-r--r-- | BinaryHeap/Aux.lean | 78 | ||||
| -rw-r--r-- | BinaryHeap/Basic.lean | 61 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean | 8 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean | 4 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapOperations.lean | 16 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapProofs/HeapPop.lean | 4 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapProofs/HeapRemoveAt.lean | 2 | ||||
| -rw-r--r-- | BinaryHeap/Relations.lean | 19 |
9 files changed, 179 insertions, 101 deletions
diff --git a/BinaryHeap.lean b/BinaryHeap.lean index 4f52f23..64dc552 100644 --- a/BinaryHeap.lean +++ b/BinaryHeap.lean @@ -1,85 +1,3 @@ -/- - This file contains the Binary Heap type and its basic operations. --/ -import BinaryHeap.CompleteTree - -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 -deriving Repr - -namespace BinaryHeap - -/-- Creates an empty heap. O(1) -/ -def new (α : Type u) {le : α → α → Bool} (h₁ : transitive_le le) (h₂ : total_le le) : BinaryHeap α le 0 := - { - tree := CompleteTree.empty, - valid := CompleteTree.emptyIsHeap le - wellDefinedLe := ⟨h₁,h₂⟩ - } - -/-- Adds an element into a heap. O(log(n)) -/ -def push {α : Type u} {le : α → α → Bool} {n : Nat} : α → BinaryHeap α le n → BinaryHeap α le (n+1) -| elem, .mk tree valid wellDefinedLe => - let valid := tree.heapPushIsHeap valid wellDefinedLe.left wellDefinedLe.right - let tree := tree.heapPush le elem - {tree, valid, wellDefinedLe} - -/-- Removes the smallest element from the heap and returns it. O(log(n)) -/ -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) - -/-- Removes the element at the given (depth-first) index from the heap and returns it. O(log(n)) -/ -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 - ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd) - -/-- Updates the element at the given (depth-first) index and returns its previous value. O(log(n)) -/ -def updateAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le n) → (Fin n) → α → (BinaryHeap α le n × α) -| {tree, valid, wellDefinedLe}, index, value => - let result := tree.heapUpdateAt le index value - let resultValid := CompleteTree.heapUpdateAtIsHeap le index value tree valid wellDefinedLe.left wellDefinedLe.right - ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd) - -/-- Searches for an element in the heap and returns its index. **O(n)** -/ -def indexOf {α : Type u} {le : α → α → Bool} {n : Nat} : BinaryHeap α le n → (pred : α → Bool) → Option (Fin n) -| {tree, valid := _, wellDefinedLe := _}, pred => - tree.indexOf pred - -instance : GetElem (BinaryHeap α le n) (Nat) α (λ _ index ↦ index < n) where - getElem := λ heap index h₁ ↦ heap.tree.get ⟨index, h₁⟩ - -instance : GetElem (BinaryHeap α le n) (Fin n) α (λ _ _ ↦ True) where - getElem := λ heap index _ ↦ heap.tree.get index - -def forM [Monad m] (heap : BinaryHeap α le n) (f : α → m PUnit) : m PUnit := - match n with - | .zero => pure () - | .succ _ => - let a := heap.tree.root' --this is faster than pop here, in case of a break. - f a >>= λ _ ↦ heap.pop.fst.forM f - -instance : ForM m (BinaryHeap α le n) α where - forM := BinaryHeap.forM - -instance : ForIn m (BinaryHeap α le n) α where - forIn := ForM.forIn - -/--Helper for the common case of using natural numbers for sorting.-/ -theorem nat_ble_to_heap_le_total : total_le Nat.ble := - λa b ↦ Nat.ble_eq.substr $ Nat.ble_eq.substr (Nat.le_total a b) - -/--Helper for the common case of using natural numbers for sorting.-/ -theorem nat_ble_to_heap_transitive_le : transitive_le Nat.ble := - λ a b c ↦ - Nat.le_trans (n := a) (m := b) (k := c) - |> Nat.ble_eq.substr - |> Nat.ble_eq.substr - |> Nat.ble_eq.substr - |> and_imp.mpr +import BinaryHeap.Basic +import BinaryHeap.Aux +import BinaryHeap.Relations diff --git a/BinaryHeap/Aux.lean b/BinaryHeap/Aux.lean new file mode 100644 index 0000000..0aa052d --- /dev/null +++ b/BinaryHeap/Aux.lean @@ -0,0 +1,78 @@ +/- + This file contains some additional functions for a Binary Heap. Things that deal with + converting collections to/from a heap. +-/ +import BinaryHeap.Basic + +namespace BinaryHeap + +def forM [Monad m] (heap : BinaryHeap α le n) (f : α → m PUnit) : m PUnit := + match n with + | .zero => pure () + | .succ _ => + let a := heap.tree.root' --this is faster than pop here, in case of a break. + f a >>= λ _ ↦ heap.pop.snd.forM f + +instance : ForM m (BinaryHeap α le n) α where + forM := BinaryHeap.forM + +instance : ForIn m (BinaryHeap α le n) α where + forIn := ForM.forIn + +/-- Builds a Binary Heap from a list. -/ +def ofList {α : Type u} {le : α → α → Bool} (h₁ : TotalAndTransitiveLe le) (l : List α) : BinaryHeap α le l.length := + let rec worker : (l : List α) → {n : Nat} → (BinaryHeap α le n) → (BinaryHeap α le (n + l.length)) := λ (l : List α) {n : Nat} (heap : BinaryHeap α le n) ↦ + match l with + | [] => heap + | a :: as => (Nat.add_comm_right n as.length 1).subst rfl ▸ worker as (heap.push a) + Nat.zero_add l.length ▸ worker l $ BinaryHeap.new h₁ + +/- Converts the tree to a sorted list. -/ +def toList (heap : BinaryHeap α le n) : List α := + let rec worker : (l : List α) → {n : Nat} → (BinaryHeap α le n) → List α := λ(l : List α) {n : Nat} (heap : BinaryHeap α le n) ↦ + match n with + | 0 => l.reverse + | (_+1) => + let (h, hs) := heap.pop + worker (h :: l) hs + worker [] heap + +private def ofForInAux [ForIn Id ρ α] {le : α → α → Bool} (h₁ : TotalAndTransitiveLe le) (c : ρ) : (h : Nat) ×' BinaryHeap α le h := Id.run do + let mut r : (h : Nat) ×' BinaryHeap α le h := ⟨0, BinaryHeap.new h₁⟩ + for e in c do + r := ⟨r.fst.succ, r.snd.push e⟩ + r + +/-- + Runs a for-loop over the input collection and creates a heap from it. + Warning: Only terminates if the ForIn instance you call it with terminates. + Think of this as a "this doesn't depend on mathlib" alternative to an implementation that uses Traversable +-/ +def ofForIn [ForIn Id ρ α] {le : α → α → Bool} (h₁ : TotalAndTransitiveLe le) (c : ρ) : BinaryHeap α le (ofForInAux h₁ c).fst := PSigma.snd $ ofForInAux h₁ c + +/-- + Folds over the heap, starting at the smallest element and yielding the elements in ascending order. +-/ +def fold (f : α → β → α) (init : α) (heap : BinaryHeap β le n) : α := + match n with + | 0 => init + | (_+1) => + let (a, as) := heap.pop + as.fold f (f init a) + +/-- + Map operation over the heap. + Unlike the regular map operation, this requires you to supply a new ordering relation for the result type. + Needs to create a new heap with the mapped values. +-/ +def map {α : Type u} {le₀ : α → α → Bool } {β : Type u₁} {le : β → β → Bool} (h₁ : TotalAndTransitiveLe le) (f : α → β) : (h : BinaryHeap α le₀ n) → BinaryHeap β le n + | { tree, .. } => + -- no need to do this in-order. + let rec worker : (o p : Nat) → (CompleteTree α o) → (BinaryHeap β le p) → (BinaryHeap β le (p + o)) := λ o p t h ↦ + match o, t with + | 0, .leaf => h + | (q+r+1), .branch v left right _ _ _ => + let left_result := worker q p left h + let right_result := worker r (p+q) right left_result + (Nat.add_assoc _ _ _▸right_result).push (f v) + (Nat.zero_add _)▸worker n 0 tree $ BinaryHeap.new h₁ diff --git a/BinaryHeap/Basic.lean b/BinaryHeap/Basic.lean new file mode 100644 index 0000000..3f4a1f1 --- /dev/null +++ b/BinaryHeap/Basic.lean @@ -0,0 +1,61 @@ +/- + This file contains the Binary Heap type and its basic operations. +-/ +import BinaryHeap.CompleteTree + +abbrev BinaryHeap.TotalAndTransitiveLe (le : α → α → Bool) : Prop := BinaryHeap.transitive_le le ∧ BinaryHeap.total_le le + +structure BinaryHeap (α : Type u) (le : α → α → Bool) (n : Nat) where + tree : BinaryHeap.CompleteTree α n + valid : BinaryHeap.HeapPredicate tree le + wellDefinedLe : BinaryHeap.TotalAndTransitiveLe le +deriving Repr + +namespace BinaryHeap + +/-- Creates an empty heap. O(1) -/ +def new {α : Type u} {le : α → α → Bool} (h₁ : TotalAndTransitiveLe le) : BinaryHeap α le 0 := + { + tree := CompleteTree.empty, + valid := CompleteTree.emptyIsHeap le + wellDefinedLe := h₁ + } + +/-- Adds an element into a heap. O(log(n)) -/ +def push {α : Type u} {le : α → α → Bool} {n : Nat} : α → BinaryHeap α le n → BinaryHeap α le (n+1) +| elem, .mk tree valid wellDefinedLe => + let valid := tree.heapPushIsHeap valid wellDefinedLe.left wellDefinedLe.right + let tree := tree.heapPush le elem + {tree, valid, wellDefinedLe} + +/-- Removes the smallest element from the heap and returns it. O(log(n)) -/ +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 + (result.fst, { tree := result.snd, valid := resultValid, wellDefinedLe}) + +/-- Removes the element at the given (depth-first) index from the heap and returns it. O(log(n)) -/ +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 + (result.fst, { tree := result.snd, valid := resultValid, wellDefinedLe}) + +/-- Updates the element at the given (depth-first) index and returns its previous value. O(log(n)) -/ +def updateAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le n) → (Fin n) → α → (BinaryHeap α le n × α) +| {tree, valid, wellDefinedLe}, index, value => + let result := tree.heapUpdateAt le index value + let resultValid := CompleteTree.heapUpdateAtIsHeap le index value tree valid wellDefinedLe.left wellDefinedLe.right + ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd) + +/-- Searches for an element in the heap and returns its index. **O(n)** -/ +def indexOf {α : Type u} {le : α → α → Bool} {n : Nat} : BinaryHeap α le n → (pred : α → Bool) → Option (Fin n) +| {tree, valid := _, wellDefinedLe := _}, pred => + tree.indexOf pred + +instance : GetElem (BinaryHeap α le n) (Nat) α (λ _ index ↦ index < n) where + getElem := λ heap index h₁ ↦ heap.tree.get ⟨index, h₁⟩ + +instance : GetElem (BinaryHeap α le n) (Fin n) α (λ _ _ ↦ True) where + getElem := λ heap index _ ↦ heap.tree.get index diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean index 09b1450..0fc88df 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean @@ -4,7 +4,7 @@ import BinaryHeap.CompleteTree.AdditionalProofs.HeapUpdateRoot namespace BinaryHeap.CompleteTree.AdditionalProofs -theorem heapPopReturnsRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (le : α → α → Bool) : (tree.heapPop le).snd = tree.root (Nat.succ_pos n) := by +theorem heapPopReturnsRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (le : α → α → Bool) : (tree.heapPop le).fst = tree.root (Nat.succ_pos n) := by unfold heapPop split <;> simp only @@ -22,14 +22,14 @@ theorem heapPopReturnsRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1) case isTrue h₁ => have h₂ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexLeavesRoot tree h₁ have h₃ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameTree tree - simp only [h₃, heapUpdateRootReturnsRoot, h₂] + simp only [heapPop.Prod.swap, h₃, heapUpdateRootReturnsRoot, h₂] /-- Shows that each element contained before removing the root that is not the root is still contained after removing the root. This is not a rigorous proof that the rest of the tree remained unchanged, as (1 (1 (1 1)) (2)).heapPop = (1 (2 (2 _)) (2)) would pass it too... Imho it is still a good indication that there are no obvious bugs. -/ -theorem heapPopOnlyRemovesRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (le: α → α → Bool) (index : Fin (n+1)) (h₁ : index ≠ ⟨0, Nat.succ_pos _⟩) : (tree.heapPop le).fst.contains $ tree.get index := by +theorem heapPopOnlyRemovesRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (le: α → α → Bool) (index : Fin (n+1)) (h₁ : index ≠ ⟨0, Nat.succ_pos _⟩) : (tree.heapPop le).snd.contains $ tree.get index := by unfold heapPop split <;> simp case isFalse h₃ => omega --contradiction. if n == 0 then index cannot be ≠ 0 @@ -39,7 +39,7 @@ theorem heapPopOnlyRemovesRoot {α : Type u} {n : Nat} (tree : CompleteTree α ( rw[←h₂] at h₃ have := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameElement tree rw[←this] at h₃ - simp[h₃, heapUpdateRootContainsUpdatedElement] + simp[heapPop.Prod.swap,h₃, heapUpdateRootContainsUpdatedElement] else have h₄ : (Internal.heapRemoveLastWithIndex tree).snd.snd ≠ 0 := by have a : n ≠ 0 := Nat.ne_of_gt h₃ diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean index dcff870..d8d1de4 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean @@ -5,7 +5,7 @@ import BinaryHeap.CompleteTree.AdditionalProofs.HeapRemoveLast namespace BinaryHeap.CompleteTree.AdditionalProofs -theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : (heap.heapRemoveAt le index).snd = heap.get index := by +theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : (heap.heapRemoveAt le index).fst = heap.get index := by unfold heapRemoveAt if h₁ : index = 0 then simp only [h₁, ↓reduceDIte] @@ -28,7 +28,7 @@ theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → rewrite[←h₄] exact Eq.symm $ heapUpdateAtReturnsElementAt le _ _ _ -theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (removeIndex : Fin (n+1)) (otherIndex : Fin (n+1)) (h₁ : removeIndex ≠ otherIndex) : (heap.heapRemoveAt le removeIndex).fst.contains (heap.get otherIndex) := by +theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (removeIndex : Fin (n+1)) (otherIndex : Fin (n+1)) (h₁ : removeIndex ≠ otherIndex) : (heap.heapRemoveAt le removeIndex).snd.contains (heap.get otherIndex) := by unfold heapRemoveAt if h₂ : removeIndex = 0 then subst removeIndex diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean index aa2eb2c..038a32c 100644 --- a/BinaryHeap/CompleteTree/HeapOperations.lean +++ b/BinaryHeap/CompleteTree/HeapOperations.lean @@ -271,18 +271,19 @@ def heapUpdateAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin ---------------------------------------------------------------------------------------------- -- heapPop -def heapPop {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) : CompleteTree α n × α := +def heapPop {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) : α × CompleteTree α n := let l := Internal.heapRemoveLast heap if p : n > 0 then - heapUpdateRoot p le l.snd l.fst + Prod.swap $ heapUpdateRoot p le l.snd l.fst else - l + Prod.swap l +where Prod.swap := λ(a,b)↦(b,a) ---------------------------------------------------------------------------------------------- -- heapRemoveAt /--Removes the element at a given index. Use `indexOf` to find the respective index.-/ -def heapRemoveAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin (n+1)) (heap : CompleteTree α (n+1)) : CompleteTree α n × α := +def 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 --version from Wikipedia: We first remove the last element, and then update values in the tree --indices are depth first, but "last" means last element of the complete tree. @@ -292,12 +293,13 @@ def heapRemoveAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin else let (remaining_tree, removed_element, removed_index) := Internal.heapRemoveLastWithIndex heap if index = removed_index then - (remaining_tree, removed_element) + (removed_element, remaining_tree) else if index_lt_lastIndex : index ≥ removed_index then let index := index.pred index_ne_zero - heapUpdateAt le index removed_element remaining_tree + Prod.swap $ heapUpdateAt le index removed_element remaining_tree else let h₁ : index < n := by omega let index : Fin n := ⟨index, h₁⟩ - heapUpdateAt le index removed_element remaining_tree + Prod.swap $ heapUpdateAt le index removed_element remaining_tree +where Prod.swap := λ(a,b)↦(b,a) diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapPop.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapPop.lean index df4f9aa..af0593c 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapPop.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapPop.lean @@ -3,7 +3,7 @@ import BinaryHeap.CompleteTree.HeapProofs.HeapUpdateRoot namespace BinaryHeap.CompleteTree -theorem heapPopIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (h₁ : HeapPredicate heap le) (wellDefinedLe : transitive_le le ∧ total_le le) : HeapPredicate (heap.heapPop le).fst le := by +theorem heapPopIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (h₁ : HeapPredicate heap le) (wellDefinedLe : transitive_le le ∧ total_le le) : HeapPredicate (heap.heapPop le).snd le := by have h₂ : HeapPredicate (Internal.heapRemoveLast heap).fst le := CompleteTree.heapRemoveLastIsHeap h₁ wellDefinedLe.left wellDefinedLe.right - unfold heapPop + unfold heapPop heapPop.Prod.swap cases n <;> simp[h₂, heapUpdateRootIsHeap, wellDefinedLe] diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveAt.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveAt.lean index 3d7975c..6e0c9e7 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveAt.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveAt.lean @@ -3,7 +3,7 @@ import BinaryHeap.CompleteTree.HeapProofs.HeapUpdateAt namespace BinaryHeap.CompleteTree -theorem heapRemoveAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin (n+1)) (heap : CompleteTree α (n+1)) (h₁ : HeapPredicate heap le) (wellDefinedLe : transitive_le le ∧ total_le le) : HeapPredicate (heap.heapRemoveAt le index).fst le := by +theorem heapRemoveAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin (n+1)) (heap : CompleteTree α (n+1)) (h₁ : HeapPredicate heap le) (wellDefinedLe : transitive_le le ∧ total_le le) : HeapPredicate (heap.heapRemoveAt le index).snd le := by have h₂ : HeapPredicate (Internal.heapRemoveLastWithIndex heap).fst le := CompleteTree.heapRemoveLastWithIndexIsHeap h₁ wellDefinedLe.left wellDefinedLe.right unfold heapRemoveAt split diff --git a/BinaryHeap/Relations.lean b/BinaryHeap/Relations.lean new file mode 100644 index 0000000..ebf45c6 --- /dev/null +++ b/BinaryHeap/Relations.lean @@ -0,0 +1,19 @@ +/- + This file contains proofs for relations that might be helpful for creating heaps. + -/ +import BinaryHeap.HeapPredicate + +namespace BinaryHeap + +/--Helper for the common case of using natural numbers for sorting.-/ +theorem nat_ble_to_heap_le_total : total_le Nat.ble := + λa b ↦ Nat.ble_eq.substr $ Nat.ble_eq.substr (Nat.le_total a b) + +/--Helper for the common case of using natural numbers for sorting.-/ +theorem nat_ble_to_heap_transitive_le : transitive_le Nat.ble := + λ a b c ↦ + Nat.le_trans (n := a) (m := b) (k := c) + |> Nat.ble_eq.substr + |> Nat.ble_eq.substr + |> Nat.ble_eq.substr + |> and_imp.mpr |