From 376e4bf573f754aa7cb8c5d6ed652f1efece3050 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Thu, 19 Dec 2024 00:01:53 +0100
Subject: Add BinaryHeap.pushList function.

---
 BinaryHeap/Aux.lean | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/BinaryHeap/Aux.lean b/BinaryHeap/Aux.lean
index 0aa052d..1b23bbf 100644
--- a/BinaryHeap/Aux.lean
+++ b/BinaryHeap/Aux.lean
@@ -27,7 +27,7 @@ def ofList {α : Type u} {le : α → α → Bool} (h₁ : TotalAndTransitiveLe
     | 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. -/
+/-- 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
@@ -37,6 +37,14 @@ def toList (heap : BinaryHeap α le n) : List α :=
       worker (h :: l) hs
   worker [] heap
 
+/-- Adds all elements in a list -/
+def pushList {α : Type u} {n : Nat} {le : α → α → Bool} (heap : BinaryHeap α le n) (l : List α) : BinaryHeap α le (n+l.length) :=
+  match l with
+  | [] => heap
+  | a :: as =>
+    have : n + 1 + as.length = n + (a :: as).length := by simp_arith[List.length_cons a as]
+    this▸pushList (heap.push a) as
+
 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
-- 
cgit v1.2.3