diff options
| -rw-r--r-- | BinaryHeap/Aux.lean | 35 |
1 files changed, 26 insertions, 9 deletions
diff --git a/BinaryHeap/Aux.lean b/BinaryHeap/Aux.lean index b57130a..16d7e94 100644 --- a/BinaryHeap/Aux.lean +++ b/BinaryHeap/Aux.lean @@ -21,11 +21,13 @@ instance : ForIn m (BinaryHeap α le n) α where /-- 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) ↦ + let rec worker : (l : List α) → {n : Nat} → (BinaryHeap α le n) → (BinaryHeap α le (l.length + n)) := λ (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₁ + | [] => Nat.zero_add _ ▸ heap + | a :: as => + have : (a :: as).length + n = as.length + n + 1 := by simp +arith + this ▸ worker as (heap.push a) + worker l $ BinaryHeap.new h₁ /-- Converts the tree to a sorted list. -/ def toList (heap : BinaryHeap α le n) : List α := @@ -76,11 +78,26 @@ def fold (f : α → β → α) (init : α) (heap : BinaryHeap β le n) : α := 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 ↦ + let rec worker : (o p : Nat) → (CompleteTree α o) → (BinaryHeap β le p) → (BinaryHeap β le (o+p)) := λ o p t h ↦ match o, t with - | 0, .leaf => h + | 0, .leaf => (Nat.add_comm _ _)▸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₁ + let right_result := worker r (q+p) right left_result + have : r + (q + p) + 1 = q+r+1+p := by simp +arith + this▸(right_result).push (f v) + worker n 0 tree $ BinaryHeap.new h₁ + +private theorem toList.worker.len_const (l : List α) {n : Nat} (h : BinaryHeap α le n) : (BinaryHeap.toList.worker l h).length = l.length + n := + match n with + | 0 => List.length_reverse.subst rfl + | (m+1) => (toList.worker.len_const (h.pop.fst :: l) (h.pop.snd)) + |> List.length_cons.subst (motive := λx ↦ _ = x + _) + |> (Nat.add_assoc l.length 1 m).subst + |> (Nat.add_comm 1 m).subst (motive := λx ↦ _ = _ + (x)) + +theorem toList_len_eq (h : BinaryHeap α le n) : h.toList.length = n := + match n with + | 0 => rfl + | (m+1) => toList.worker.len_const [h.pop.fst] h.pop.snd + |> (Nat.add_comm 1 m).subst |