diff options
Diffstat (limited to 'Common/BinaryHeap.lean')
| -rw-r--r-- | Common/BinaryHeap.lean | 62 |
1 files changed, 40 insertions, 22 deletions
diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean index d7568ab..1801122 100644 --- a/Common/BinaryHeap.lean +++ b/Common/BinaryHeap.lean @@ -573,36 +573,54 @@ def BinaryHeap.popLast {α : Type u} {le : α → α → Bool} {n : Nat} : (Bina -/ def CompleteTree.replaceElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : n > 0) : α × CompleteTree α n := if h₂ : index = ⟨0,h₁⟩ then - match h₃ : n, heap with - | (o+p+1), .branch v l r h₄ h₅ h₆ => - match l, r with - | .leaf, .leaf => sorry - | .branch lv ll lr _ _ _, .leaf => sorry - | .branch lv ll lr _ _ _, .branch rv rl rr _ _ _ => sorry - | .leaf, .branch _ _ _ _ _ _ => by contradiction + match _h : n, heap with --without assigning the proof, this does not eliminate the zero-case + | (o+p+1), .branch v l r h₃ h₄ h₅ => + if h₆ : o = 0 then + -- have : p = 0 := (Nat.le_zero_eq p).mp $ h₇.subst h₃ --not needed, left here for reference + (v, .branch value l r h₃ h₄ h₅) + else + have h₇ : o > 0 := Nat.zero_lt_of_ne_zero h₆ + let lr := l.root h₇ + if h₈ : p = 0 then + if le value lr then + (v, .branch value l r h₃ h₄ h₅) + else + let ln := replaceElementAt le ⟨0, h₇⟩ value l h₇ + (v, .branch ln.fst ln.snd r h₃ h₄ h₅) + else + have h₉ : p > 0 := Nat.zero_lt_of_ne_zero h₈ + let rr := r.root h₉ + if le value lr ∧ le value rr then + (v, .branch value l r h₃ h₄ h₅) + else if le lr rr then -- value is gt either left or right root. Move it down accordingly + let ln := replaceElementAt le ⟨0, h₇⟩ value l h₇ + (v, .branch ln.fst ln.snd r h₃ h₄ h₅) + else + let rn := replaceElementAt le ⟨0, h₉⟩ value r h₉ + (v, .branch rn.fst l rn.snd h₃ h₄ h₅) else - match h₃ : n, heap with - | (o+p+1), .branch v l r h₄ h₅ h₆ => + match n, heap with + | (o+p+1), .branch v l r h₃ h₄ h₅ => let (v, value) := if le v value then (v, value) else (value, v) - if h₇ : index ≤ o then - have h₈ : Nat.pred index.val < o := Nat.lt_of_lt_of_le (Nat.pred_lt $ Fin.val_ne_of_ne h₂) h₇ - let index_in_left : Fin o := ⟨index.val.pred, h₈⟩ - have h₉ : 0 < o := Nat.zero_lt_of_lt h₈ - let result := replaceElementAt le index_in_left value l h₉ - (result.fst, .branch v result.snd r h₄ h₅ h₆) + if h₆ : index ≤ o then + have h₇ : Nat.pred index.val < o := Nat.lt_of_lt_of_le (Nat.pred_lt $ Fin.val_ne_of_ne h₂) h₆ + let index_in_left : Fin o := ⟨index.val.pred, h₇⟩ + have h₈ : 0 < o := Nat.zero_lt_of_lt h₇ + let result := replaceElementAt le index_in_left value l h₈ + (result.fst, .branch v result.snd r h₃ h₄ h₅) else - have h₈ : index.val - (o + 1) < p := + have h₇ : index.val - (o + 1) < p := -- tactic rewrite failed, result is not type correct. - have h₉ : index.val < p + o + 1 := index.isLt + have h₈ : index.val < p + o + 1 := index.isLt |> (Nat.add_assoc o p 1).subst |> (Nat.add_comm p 1).subst (motive := λx ↦ index.val < o + x) |> (Nat.add_assoc o 1 p).symm.subst |> (Nat.add_comm (o+1) p).subst - Nat.sub_lt_of_lt_add h₉ $ (Nat.not_le_eq index.val o).mp h₇ - let index_in_right : Fin p := ⟨index.val - o - 1, h₈⟩ - have h₉ : 0 < p := Nat.zero_lt_of_lt h₈ - let result := replaceElementAt le index_in_right value r h₉ - (result.fst, .branch v l result.snd h₄ h₅ h₆) + Nat.sub_lt_of_lt_add h₈ $ (Nat.not_le_eq index.val o).mp h₆ + let index_in_right : Fin p := ⟨index.val - o - 1, h₇⟩ + have h₈ : 0 < p := Nat.zero_lt_of_lt h₇ + let result := replaceElementAt le index_in_right value r h₈ + (result.fst, .branch v l result.snd h₃ h₄ h₅) /--Removes the element at a given index. Use `CompleteTree.indexOf` to find the respective index.-/ def CompleteTree.heapRemoveAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin (n+1)) (heap : CompleteTree α (n+1)) : α × CompleteTree α n := |