diff options
Diffstat (limited to 'BinaryHeap')
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean | 55 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean | 589 |
2 files changed, 81 insertions, 563 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean index af03076..937e6d0 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean @@ -38,26 +38,35 @@ theorem heapPopOnlyRemovesRoot {α : Type u} {n : Nat} (tree : CompleteTree α ( rw[←this] at h₃ simp[h₃, heapUpdateRootContainsUpdatedElement] else - sorry - - -theorem heapPopOnlyRemovesRoot2 {α : 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 (Nat.succ_pos _) := by - unfold heapPop - have h₂ := CompleteTree.AdditionalProofs.heapRemoveLastEitherContainsOrReturnsElement tree index - simp only at h₂ - split <;> simp - case isFalse h₃ => omega --contradiction. if n == 0 then index cannot be ≠ 0 - case isTrue h₃ => - cases h₂ - case inr h₂ => - rw[h₂] - exact heapUpdateRootContainsUpdatedElement (Internal.heapRemoveLast tree).fst le (get index tree (Nat.succ_pos _)) h₃ - case inl h₂ => - generalize h₄ : (Internal.heapRemoveLast tree).fst = withoutLast - have h₅ := CompleteTree.AdditionalProofs.heapRemoveLastLeavesRoot tree h₃ - rw[h₄] at h₂ h₅ - have := heapUpdateRootOnlyUpdatesRoot le withoutLast h₃ - rw[contains_iff_index_exists _ _ h₃] at h₂ - -- to use h₂.elim we need to rewrite this into - -- ∀ (a : Fin n), get a withoutLast h₃ = get index tree ⋯ → something - sorry + have h₄ : (Internal.heapRemoveLastWithIndex tree).snd.snd ≠ 0 := by + have a : n ≠ 0 := Nat.ne_of_gt h₃ + have b := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexIndexNeZeroForNGt1 tree + simp only [ne_eq, ←b] at a + exact a + if h₅ : index < (Internal.heapRemoveLastWithIndex tree).snd.snd then + have h₆ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationLt tree index h₅ + simp only at h₆ + have h₇ : index.val < n := by omega + have : (⟨↑index, h₇⟩ : Fin n) ≠ ⟨0, h₃⟩ := by + rewrite[←Fin.val_ne_iff] at h₁ + simp only [ne_eq, Fin.mk.injEq] at h₁ ⊢ + assumption + have h₈ := heapUpdateRootOnlyUpdatesRoot le (Internal.heapRemoveLastWithIndex tree).fst h₃ ⟨↑index, h₇⟩ this $ (Internal.heapRemoveLastWithIndex tree).snd.fst + rewrite[h₆] at h₈ + rewrite[←CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameElement] at h₈ + rewrite[←CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameTree] at h₈ + exact h₈ + else + have h₅ : index > (Internal.heapRemoveLastWithIndex tree).snd.snd := by omega + have h₆ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationGt tree index h₅ + simp only at h₆ + have : index.pred h₁ ≠ ⟨0, h₃⟩ := by + have h₄ : (Internal.heapRemoveLastWithIndex tree).snd.snd.val > 0 := Nat.zero_lt_of_ne_zero (Fin.val_ne_of_ne h₄) + rewrite[←Fin.val_ne_iff] + simp only [Fin.coe_pred, ne_eq] + omega + have h₈ := heapUpdateRootOnlyUpdatesRoot le (Internal.heapRemoveLastWithIndex tree).fst h₃ (index.pred h₁) this $ (Internal.heapRemoveLastWithIndex tree).snd.fst + rewrite[h₆] at h₈ + rewrite[←CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameElement] at h₈ + rewrite[←CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameTree] at h₈ + exact h₈ diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index 0aa9481..c29fc3f 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -100,520 +100,6 @@ private theorem lens_see_through_cast {α : Type u} {p q : Nat} (h₁ : q+p+1 = revert hb ha heap h₁ assumption -private theorem left_sees_through_cast {α : Type u} {p q : Nat} (h₁ : q+p+1 = q+1+p) (heap : CompleteTree α (q+p+1)) (ha : q+p+1 > 0) (hb : q+1+p > 0): HEq (heap.left ha) ((h₁▸heap).left hb) := by - induction p generalizing q - case zero => simp only [Nat.add_zero, heq_eq_eq] - case succ pp hp => - have h₂ := hp (q := q+1) - have h₃ : (q + 1 + pp + 1) = q + (pp + 1) + 1 := Nat.add_comm_right q 1 (pp + 1) - have h₄ : (q + 1 + 1 + pp) = q + 1 + (pp + 1) := (Nat.add_comm_right (q+1) 1 pp).substr $ Nat.add_assoc (q+1) pp 1 - rw[h₃, h₄] at h₂ - revert hb ha heap h₁ - assumption - -private theorem right_sees_through_cast {α : Type u} {p q : Nat} (h₁ : q+p+1 = q+1+p) (heap : CompleteTree α (q+p+1)) (ha : q+p+1 > 0) (hb : q+1+p > 0): HEq (heap.right ha) ((h₁▸heap).right hb) := by - induction p generalizing q - case zero => simp only [Nat.add_zero, heq_eq_eq] - case succ pp hp => - have h₂ := hp (q := q+1) - have h₃ : (q + 1 + pp + 1) = q + (pp + 1) + 1 := Nat.add_comm_right q 1 (pp + 1) - have h₄ : (q + 1 + 1 + pp) = q + 1 + (pp + 1) := (Nat.add_comm_right (q+1) 1 pp).substr $ Nat.add_assoc (q+1) pp 1 - rw[h₃, h₄] at h₂ - revert hb ha heap h₁ - assumption - -/--Helper for heapRemoveLastWithIndexOnlyRemovesOneElement_Auxllength to allow splitting the goal-/ -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLLengthAux {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (h₁ : n > 0) -: - let o := tree.leftLen' - let p := tree.rightLen' - (h₂ : p < o ∧ (p+1).nextPowerOfTwo = p+1) → (Internal.heapRemoveLastWithIndex tree).fst.leftLen h₁ = o.pred -:= by - simp only - intro h₂ - unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux - split --finally - rename_i del1 del2 o p v l r o_le_p max_height_difference subtree_complete - clear del2 del1 - unfold rightLen' leftLen' at h₂ - simp only [leftLen_unfold, rightLen_unfold] at h₂ - have : 0 ≠ o + p := Nat.ne_of_lt h₁ - simp only [this, ↓reduceDite, h₂, decide_True, and_self] - match o, l, o_le_p, max_height_difference, subtree_complete, this, h₂ with - | (q+1), l, o_le_p, max_height_difference, subtree_complete, this, h₂ => - simp only [Nat.add_eq, Fin.zero_eta, Fin.isValue, Nat.succ_eq_add_one, Nat.pred_eq_sub_one] - rw[←lens_see_through_cast _ leftLen _ (Nat.succ_pos (q+p))] - unfold leftLen' - rw[leftLen_unfold] - rw[leftLen_unfold] - rfl - -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLLength {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α (o+1)) (r : CompleteTree α p) (h₁ : p ≤ (o+1)) (h₂ : (o+1) < 2 * (p + 1)) (h₃ : (o + 1 + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : p < (o+1) ∧ ((p+1).nextPowerOfTwo = p+1 : Bool)) -: - (Internal.heapRemoveLastWithIndex (branch v l r h₁ h₂ h₃)).fst.leftLen (Nat.lt_add_right p $ Nat.succ_pos o) = o -:= by - apply heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLLengthAux (branch v l r h₁ h₂ h₃) (Nat.lt_add_right p $ Nat.succ_pos o) - unfold leftLen' rightLen' - simp only [leftLen_unfold, rightLen_unfold] - simp only [decide_eq_true_eq] at h₄ - assumption - -/--Helper for heapRemoveLastWithIndexOnlyRemovesOneElement_Auxllength to allow splitting the goal-/ -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxRLengthAux {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (h₁ : n > 0) -: - let o := tree.leftLen' - let p := tree.rightLen' - (h₂ : ¬(p < o ∧ ((p+1).nextPowerOfTwo = p+1 : Bool))) → (Internal.heapRemoveLastWithIndex tree).fst.rightLen h₁ = p.pred -:= by - simp only - intro h₂ - unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux - split --finally - rename_i del1 del2 o p v l r o_le_p max_height_difference subtree_complete - clear del2 del1 - unfold rightLen' leftLen' at h₂ - simp only [leftLen_unfold, rightLen_unfold] at h₂ - have : 0 ≠ o + p := Nat.ne_of_lt h₁ - simp only [this, ↓reduceDite, h₂, decide_True, and_self] - cases p - case zero => - simp at h₂ h₁ - simp (config := {ground:=true})[h₁] at h₂ - case succ pp => - simp[rightLen', rightLen_unfold] - -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxRLength {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α o) (r : CompleteTree α (p+1)) (h₁ : p+1 ≤ o) (h₂ : o < 2 * (p + 1 + 1)) (h₃ : (o + 1).isPowerOfTwo ∨ (p + 1 + 1).isPowerOfTwo) (h₄ : ¬(p + 1 < o ∧ ((p+1+1).nextPowerOfTwo = p+1+1 : Bool))) -: - (Internal.heapRemoveLastWithIndex (branch v l r h₁ h₂ h₃)).fst.rightLen (Nat.lt_add_left o $ Nat.succ_pos p) = p -:= by - apply heapRemoveLastWithIndexOnlyRemovesOneElement_AuxRLengthAux (branch v l r h₁ h₂ h₃) (Nat.lt_add_left o $ Nat.succ_pos p) - unfold leftLen' rightLen' - simp only [leftLen_unfold, rightLen_unfold] - assumption - -private def heapRemoveLastWithIndex' {α : Type u} {o : Nat} (heap : CompleteTree α o) (_ : o > 0) : (CompleteTree α o.pred × α × Fin o) := - match o, heap with - | _+1, heap => Internal.heapRemoveLastWithIndex heap - -private theorem heapRemoveLastWithIndex'_unfold {α : Type u} {o : Nat} (heap : CompleteTree α o) (h₁ : o > 0) -: - match o, heap with - | (oo+1), heap => (heapRemoveLastWithIndex' heap h₁) = (Internal.heapRemoveLastWithIndex heap) -:= by - split - rfl - -/--Helper for heapRemoveLastWithIndexOnlyRemovesOneElement_Auxl to allow splitting the goal-/ -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLAux {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (h₁ : n > 0) -: - let o := tree.leftLen' - let p := tree.rightLen' - (h₂ : o > 0) → - (h₃ : p < o ∧ ((p+1).nextPowerOfTwo = p+1 : Bool)) → - HEq ((Internal.heapRemoveLastWithIndex tree).fst.left h₁) (heapRemoveLastWithIndex' (tree.left') h₂).fst -:= by - simp only - intro h₂ h₃ - --sorry for this wild mixture of working on the LHS and RHS of the goal. - --this function is trial and error, I'm fighting an uphill battle agains tactics mode here, - --which keeps randomly failing on me if I do steps in what the tactics - --percieve to be the "wrong" order. - have h₄ := heapRemoveLastWithIndex'_unfold tree.left' h₂ - split at h₄ - rename_i d3 d2 d1 oo l o_gt_0 he1 he2 he3 - clear d1 d2 d3 - --okay, I have no clue why generalizing here is needed. - --I mean, why does unfolding and simplifying work if it's a separate hypothesis, - --but not within the goal? - generalize hi : (Internal.heapRemoveLastWithIndex tree).fst = input - unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux at hi - split at hi - rename_i o2 p vv ll rr _ _ _ - unfold left' leftLen' rightLen' at * - rw[left_unfold] at * - rw[leftLen_unfold, rightLen_unfold] at * - subst o2 - simp at he2 - subst ll - rw[h₄] - have : (0 ≠ oo.succ + p) := by simp_arith - simp[this, h₃] at hi - have : (p+1).isPowerOfTwo := by - have h₃ := h₃.right - simp at h₃ - exact (Nat.power_of_two_iff_next_power_eq (p+1)).mpr h₃ - have := left_sees_through_cast (by simp_arith) (branch vv - (Internal.heapRemoveLastAux (β := λn ↦ α × Fin n) l (fun a => (a, 0)) - (fun {prev_size curr_size} x h₁ => (x.fst, Fin.castLE (Nat.succ_le_of_lt h₁) x.snd.succ)) - fun {prev_size curr_size} x left_size h₁ => (x.fst, Fin.castLE (by omega) (x.snd.addNat left_size).succ)).fst - rr (by omega) (by omega) (Or.inr this)) - rw[hi] at this - clear hi - have := this (by simp) (by simp_arith) - simp only [left_unfold] at this - unfold Internal.heapRemoveLastWithIndex - simp - exact this.symm - -/--Shows that if the removal happens in the left tree, the new left-tree is the old left-tree with the last element removed.-/ -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxL {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α (o+1)) (r : CompleteTree α p) (h₁ : p ≤ (o+1)) (h₂ : (o+1) < 2 * (p + 1)) (h₃ : (o + 1 + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : p < (o+1) ∧ ((p+1).nextPowerOfTwo = p+1 : Bool)) -: - HEq ((Internal.heapRemoveLastWithIndex (branch v l r h₁ h₂ h₃)).fst.left (Nat.lt_add_right p $ Nat.succ_pos o)) (Internal.heapRemoveLastWithIndex l).fst -:= - --okay, let me be frank here: I have absolutely no clue why I need heapRemoveLastWithIndexOnlyRemovesOneElement_Auxl2. - --from the looks of it, I should just be able to generalize the LHS, and unfold things and be happy. - --However, tactic unfold fails. So, let's just forward this to the helper. - have h₅ : (branch v l r h₁ h₂ h₃).leftLen' > 0 := Nat.succ_pos o - heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLAux _ _ h₅ h₄ - -/--Helper for heapRemoveLastWithIndexOnlyRemovesOneElement_AuxR to allow splitting the goal-/ -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxRAux {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (h₁ : n > 0) -: - let o := tree.leftLen' - let p := tree.rightLen' - (h₂ : p > 0) → - (h₃ : ¬(p < o ∧ ((p+1).nextPowerOfTwo = p+1 : Bool))) → - HEq ((Internal.heapRemoveLastWithIndex tree).fst.right h₁) (heapRemoveLastWithIndex' (tree.right') h₂).fst -:= by - simp only - intro h₂ h₃ - --sorry for this wild mixture of working on the LHS and RHS of the goal. - --this function is trial and error, I'm fighting an uphill battle agains tactics mode here, - --which keeps randomly failing on me if I do steps in what the tactics - --percieve to be the "wrong" order. - have h₄ := heapRemoveLastWithIndex'_unfold tree.right' h₂ - split at h₄ - rename_i d3 d2 d1 pp l o_gt_0 he1 he2 he3 - clear d1 d2 d3 - --okay, I have no clue why generalizing here is needed. - --I mean, why does unfolding and simplifying work if it's a separate hypothesis, - --but not within the goal? - generalize hi : (Internal.heapRemoveLastWithIndex tree).fst = input - unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux at hi - split at hi - rename_i o p2 vv ll rr m_le_n max_height_difference subtree_complete - unfold right' leftLen' rightLen' at * - rw[right_unfold] at * - rw[leftLen_unfold, rightLen_unfold] at * - subst p2 - simp at he2 - subst rr - rw[h₄] - have : (0 ≠ o + pp.succ) := by simp_arith - simp[this] at hi - have : ¬(pp + 1 < o ∧ (pp + 1 + 1).nextPowerOfTwo = pp + 1 + 1) := by simp; simp at h₃; assumption - simp[this] at hi - subst input - simp[right_unfold, Internal.heapRemoveLastWithIndex] - done - -/--Shows that if the removal happens in the left tree, the new left-tree is the old left-tree with the last element removed.-/ -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxR {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α o) (r : CompleteTree α (p+1)) (h₁ : (p+1) ≤ o) (h₂ : o < 2 * (p + 1 + 1)) (h₃ : (o + 1).isPowerOfTwo ∨ (p + 1 + 1).isPowerOfTwo) (h₄ : ¬(p + 1 < o ∧ ((p + 1 + 1).nextPowerOfTwo = p + 1 + 1 : Bool))) -: - HEq ((Internal.heapRemoveLastWithIndex (branch v l r h₁ h₂ h₃)).fst.right (Nat.lt_add_left o $ Nat.succ_pos p)) (Internal.heapRemoveLastWithIndex r).fst -:= - --okay, let me be frank here: I have absolutely no clue why I need heapRemoveLastWithIndexOnlyRemovesOneElement_Auxl2. - --from the looks of it, I should just be able to generalize the LHS, and unfold things and be happy. - --However, tactic unfold fails. So, let's just forward this to the helper. - have h₅ : (branch v l r h₁ h₂ h₃).rightLen' > 0 := Nat.succ_pos p - heapRemoveLastWithIndexOnlyRemovesOneElement_AuxRAux _ _ h₅ h₄ - -/--Helper for heapRemoveLastWithIndexOnlyRemovesOneElement_Auxllength to allow splitting the goal-/ -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLLength2Aux {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (h₁ : n > 0) -: - let o := tree.leftLen' - let p := tree.rightLen' - (h₂ : ¬(p < o ∧ ((p+1).nextPowerOfTwo = p+1 : Bool))) → (Internal.heapRemoveLastWithIndex tree).fst.leftLen h₁ = o -:= by - simp only - intro h₂ - unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux - split --finally - rename_i del1 del2 o p v l r o_le_p max_height_difference subtree_complete - clear del2 del1 - unfold rightLen' leftLen' at h₂ - simp only [leftLen_unfold, rightLen_unfold] at h₂ - have h₄ : 0 ≠ o + p := Nat.ne_of_lt h₁ - simp only [h₄, ↓reduceDite, h₂, decide_True, and_self] - cases p - case zero => - have : decide ((0 + 1).nextPowerOfTwo = 0 + 1) = true := by simp (config := { ground := true }) only [decide_True, Nat.zero_add] - simp only [this, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂ - exact absurd h₂.symm h₄ - case succ pp => - unfold leftLen' - simp[leftLen_unfold] - done - -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLLength2 {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α (o+1)) (r : CompleteTree α p) (h₁ : p ≤ (o+1)) (h₂ : (o+1) < 2 * (p + 1)) (h₃ : (o + 1 + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : ¬(p < (o+1) ∧ ((p+1).nextPowerOfTwo = p+1 : Bool))) -: - (Internal.heapRemoveLastWithIndex (branch v l r h₁ h₂ h₃)).fst.leftLen (Nat.lt_add_right p $ Nat.succ_pos o) = o + 1 -:= by - apply heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLLength2Aux (branch v l r h₁ h₂ h₃) (Nat.lt_add_right p $ Nat.succ_pos o) - unfold leftLen' rightLen' - simp only [leftLen_unfold, rightLen_unfold] - assumption - - -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxL2Aux {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (h₁ : n > 0) -: - let o := tree.leftLen' - let p := tree.rightLen' - (h₂ : o > 0) → - (h₃ : ¬(p < o ∧ ((p+1).nextPowerOfTwo = p+1 : Bool))) → - HEq ((Internal.heapRemoveLastWithIndex tree).fst.left h₁) tree.left' -:= by - simp only - intro h₂ h₃ - generalize hi : (Internal.heapRemoveLastWithIndex tree).fst = input - unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux at hi - split at hi - rename_i d1 d2 o2 p vv ll rr m_le_n max_height_difference subtree_complete - clear d1 d2 - unfold leftLen' rightLen' at* - rw[leftLen_unfold, rightLen_unfold] at * - have h₄ : 0 ≠ o2+p := Nat.ne_of_lt h₁ - simp only [h₄, h₃, reduceDite] at hi - -- okay, dealing with p.pred.succ is a guarantee for pain. "Stuck at solving universe constraint" - cases p - case zero => - have : decide ((0 + 1).nextPowerOfTwo = 0 + 1) = true := by simp (config := { ground := true }) only [decide_True, Nat.zero_add] - simp only [this, and_true, Nat.not_lt, Nat.le_zero_eq] at h₃ - exact absurd h₃.symm h₄ - case succ pp => - simp at hi --whoa, how easy this gets if one just does cases p... - unfold left' - rewrite[←hi, left_unfold] - rewrite[left_unfold] - exact heq_of_eq rfl - -/--Shows that if the removal happens in the right subtree, the left subtree remains unchanged.-/ -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxL2 {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α (o+1)) (r : CompleteTree α p) (h₁ : p ≤ (o+1)) (h₂ : (o+1) < 2 * (p + 1)) (h₃ : (o + 1 + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : ¬ (p < (o+1) ∧ ((p+1).nextPowerOfTwo = p+1 : Bool))) -: - HEq ((Internal.heapRemoveLastWithIndex (branch v l r h₁ h₂ h₃)).fst.left (Nat.lt_add_right p $ Nat.succ_pos o)) l -:= - heapRemoveLastWithIndexOnlyRemovesOneElement_AuxL2Aux (branch v l r h₁ h₂ h₃) (by omega) (Nat.succ_pos _) h₄ - -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxRLength2Aux {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (h₁ : n > 0) -: - let o := tree.leftLen' - let p := tree.rightLen' - (h₂ : (p < o ∧ ((p+1).nextPowerOfTwo = p+1 : Bool))) → (Internal.heapRemoveLastWithIndex tree).fst.rightLen h₁ = p -:= by - simp only - intro h₂ - unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux - split --finally - rename_i del1 del2 o p v l r o_le_p max_height_difference subtree_complete - clear del2 del1 - unfold rightLen' leftLen' at h₂ - simp only [leftLen_unfold, rightLen_unfold] at h₂ - have h₄ : 0 ≠ o + p := Nat.ne_of_lt h₁ - simp only [h₄, ↓reduceDite, h₂, decide_True, and_self] - cases o - case zero => exact absurd h₂.left $ Nat.not_lt_zero p - case succ oo => - simp at h₂ ⊢ - have : (p+1).isPowerOfTwo := by simp[Nat.power_of_two_iff_next_power_eq, h₂.right] - have := lens_see_through_cast ( by simp_arith : oo + p + 1 = oo + 1 + p) rightLen (branch v - (Internal.heapRemoveLastAux (β := λn ↦ α × Fin n) l (fun a => (a, 0)) - (fun {prev_size curr_size} x h₁ => (x.fst, Fin.castLE (by omega) x.snd.succ)) - fun {prev_size curr_size} x left_size h₁ => (x.fst, Fin.castLE (by omega) (x.snd.addNat left_size).succ)).fst - r (Nat.le_of_lt_succ h₂.left) (Nat.lt_of_succ_lt max_height_difference) (Or.inr this)) (Nat.succ_pos _) h₁ - rw[←this] - simp[rightLen', rightLen_unfold] - done - -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxRLength2 {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α o) (r : CompleteTree α (p + 1)) (h₁ : (p + 1) ≤ o) (h₂ : o < 2 * (p + 1 + 1)) (h₃ : (o + 1).isPowerOfTwo ∨ (p + 1 + 1).isPowerOfTwo) (h₄ : ((p + 1) < o ∧ ((p+1+1).nextPowerOfTwo = p+1+1 : Bool))) -: - (Internal.heapRemoveLastWithIndex (branch v l r h₁ h₂ h₃)).fst.rightLen (Nat.lt_add_left o $ Nat.succ_pos p) = p + 1 -:= by - apply heapRemoveLastWithIndexOnlyRemovesOneElement_AuxRLength2Aux (branch v l r h₁ h₂ h₃) (Nat.lt_add_left o $ Nat.succ_pos p) - unfold leftLen' rightLen' - simp only [leftLen_unfold, rightLen_unfold] - assumption - -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxR2Aux {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (h₁ : n > 0) -: - let o := tree.leftLen' - let p := tree.rightLen' - (h₂ : p > 0) → - (h₃ : (p < o ∧ ((p+1).nextPowerOfTwo = p+1 : Bool))) → - HEq ((Internal.heapRemoveLastWithIndex tree).fst.right h₁) tree.right' -:= by - simp only - intro h₂ h₃ - generalize hi : (Internal.heapRemoveLastWithIndex tree).fst = input - unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux at hi - split at hi - rename_i d1 d2 o2 p vv ll rr m_le_n max_height_difference subtree_complete - clear d1 d2 - unfold leftLen' rightLen' at* - rw[leftLen_unfold, rightLen_unfold] at * - have h₄ : 0 ≠ o2+p := Nat.ne_of_lt h₁ - simp only [h₄, h₃, and_true, reduceDite] at hi - -- okay, dealing with p.pred.succ is a guarantee for pain. "Stuck at solving universe constraint" - cases o2 - case zero => - exact absurd h₂ $ Nat.not_lt_of_le m_le_n - case succ oo => - simp at hi --whoa, how easy this gets if one just does cases o2... - unfold right' - rewrite[right_unfold] - simp at h₃ - have : (p+1).isPowerOfTwo := by simp[Nat.power_of_two_iff_next_power_eq, h₃.right] - have h₅ := right_sees_through_cast (by simp_arith: oo + p + 1 = oo + 1 + p) (branch vv - (Internal.heapRemoveLastAux (β := λn ↦ α × Fin n) ll (fun a => (a, 0)) - (fun {prev_size curr_size} x h₁ => (x.fst, Fin.castLE (by omega) x.snd.succ)) - fun {prev_size curr_size} x left_size h₁ => (x.fst, Fin.castLE (by omega) (x.snd.addNat left_size).succ)).fst - rr (Nat.le_of_lt_succ h₃.left) (Nat.lt_of_succ_lt max_height_difference) (Or.inr this)) (Nat.succ_pos _) h₁ - rw[right_unfold, hi] at h₅ - exact h₅.symm - -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxR2 {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α o) (r : CompleteTree α (p+1)) (h₁ : (p+1) ≤ o) (h₂ :o < 2 * (p + 1 + 1)) (h₃ : (o + 1).isPowerOfTwo ∨ (p + 1 + 1).isPowerOfTwo) (h₄ : ((p+1) < o ∧ ((p+1+1).nextPowerOfTwo = p+1+1 : Bool))) -: - HEq ((Internal.heapRemoveLastWithIndex (branch v l r h₁ h₂ h₃)).fst.right (Nat.lt_add_left o $ Nat.succ_pos p)) r -:= - heapRemoveLastWithIndexOnlyRemovesOneElement_AuxR2Aux (branch v l r h₁ h₂ h₃) (by omega) (Nat.succ_pos _) h₄ - - -/--Helper for heapRemoveLastWithIndexOnlyRemovesOneElement_AuxlIndexNe-/ -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLIndexNeAux {α : Type u} {n j : Nat} (tree : CompleteTree α (n+1)) (h₁ : (n+1) > 0) (h₂ : j < tree.leftLen h₁) (h₃ : j.succ < (n+1)) (h₄ : tree.rightLen' < tree.leftLen' ∧ ((tree.rightLen'+1).nextPowerOfTwo = tree.rightLen'+1 : Bool)) (h₅ : ⟨j.succ, h₃⟩ ≠ (Internal.heapRemoveLastWithIndex tree).2.snd) : ⟨j, h₂⟩ ≠ (heapRemoveLastWithIndex' (tree.left h₁) (Nat.zero_lt_of_lt h₂)).snd.snd := by - have h₆ := heapRemoveLastWithIndex'_unfold tree.left' $ Nat.zero_lt_of_lt h₂ - split at h₆ - rename_i d3 d2 d1 oo l o_gt_0 he1 he2 he3 - clear d1 d2 d3 - unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux at h₅ - split at h₅ - rename_i o2 p vv ll rr _ _ _ - unfold left' rightLen' leftLen' at * - rw[left_unfold] at * - rw[leftLen_unfold, rightLen_unfold] at * - subst he1 - simp at he2 - subst he2 - rw[h₆] - have : ¬ 0 = oo.succ + p := by omega - simp only [this, h₄, and_true, reduceDite] at h₅ - rw[←Fin.val_ne_iff] at h₅ ⊢ - simp at h₅ - unfold Internal.heapRemoveLastWithIndex - assumption - -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLIndexNe {α : Type u} {o p j : Nat} (v : α) (l : CompleteTree α (o+1)) (r : CompleteTree α p) (h₁ : p ≤ (o+1)) (h₂ : (o+1) < 2 * (p + 1)) (h₃ : (o + 1 + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : j < o+1) (h₅ : p < (o+1) ∧ ((p+1).nextPowerOfTwo = p+1 : Bool)) (h₆ : ⟨j.succ, (by omega)⟩ ≠ (Internal.heapRemoveLastWithIndex (branch v l r h₁ h₂ h₃)).2.snd) : ⟨j,h₄⟩ ≠ (Internal.heapRemoveLastWithIndex l).snd.snd := - --splitting at h₅ does not work. Probably because we have o+1... - --helper function it is... - heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLIndexNeAux (branch v l r h₁ h₂ h₃) (Nat.succ_pos _) _ (by omega) h₅ h₆ - -/--Helper for heapRemoveLastWithIndexOnlyRemovesOneElement_AuxlIndexNe-/ -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxRIndexNeAux {α : Type u} {n j : Nat} (tree : CompleteTree α (n+1)) (h₁ : (n+1) > 0) (h₂ : j - tree.leftLen h₁ < tree.rightLen h₁) (h₃ : j.succ < (n+1)) (h₄ : tree.leftLen' ≤ j) (h₅ : ¬(tree.rightLen' < tree.leftLen' ∧ ((tree.rightLen'+1).nextPowerOfTwo = tree.rightLen'+1 : Bool))) (h₆ : ⟨j.succ, h₃⟩ ≠ (Internal.heapRemoveLastWithIndex tree).2.snd) : ⟨j - tree.leftLen h₁, h₂⟩ ≠ (heapRemoveLastWithIndex' (tree.right h₁) (Nat.zero_lt_of_lt h₂)).snd.snd := by - have h₇ := heapRemoveLastWithIndex'_unfold tree.right' (Nat.zero_lt_of_lt h₂) - split at h₇ - rename_i d3 d2 d1 pp r o_gt_0 he1 he2 he3 - clear d1 d2 d3 - unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux at h₆ - split at h₆ - rename_i o p2 vv ll rr _ _ _ - unfold right' rightLen' leftLen' at * - rw[right_unfold] at * - rw[leftLen_unfold, rightLen_unfold] at * - subst he1 - simp at he2 - subst he2 - rw[h₇] - have : ¬0 = o + pp.succ := by omega - simp only [this, h₅, and_true, reduceDite] at h₆ - rw[←Fin.val_ne_iff] at h₆ ⊢ - simp at h₆ - unfold Internal.heapRemoveLastWithIndex - simp[leftLen_unfold] - rw[Nat.sub_eq_iff_eq_add h₄] - assumption - - -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxRIndexNe {α : Type u} {o p j : Nat} (v : α) (l : CompleteTree α o) (r : CompleteTree α (p+1)) (h₁ : p+1 ≤ o) (h₂ : o < 2 * (p + 1 + 1)) (h₃ : (o + 1).isPowerOfTwo ∨ (p + 1 + 1).isPowerOfTwo) (h₄ : j - o < p + 1) (h₅ : o ≤ j) (h₆ : ¬(p + 1 < o ∧ ((p+1+1).nextPowerOfTwo = p+1+1 : Bool))) (h₇ : ⟨j.succ, (by omega)⟩ ≠ (Internal.heapRemoveLastWithIndex (branch v l r h₁ h₂ h₃)).2.snd) : ⟨j-o,h₄⟩ ≠ (Internal.heapRemoveLastWithIndex r).snd.snd := - --splitting at h₅ does not work. Probably because we have o+1... - --helper function it is... - heapRemoveLastWithIndexOnlyRemovesOneElement_AuxRIndexNeAux (branch v l r h₁ h₂ h₃) (Nat.succ_pos _) _ _ h₅ h₆ h₇ - -/--If the resulting tree contains all elements except the removed one, and contains one less than the original, well, you get the idea.-/ -protected theorem heapRemoveLastWithIndexOnlyRemovesOneElement {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : - let (newHeap, _, removedIndex) := Internal.heapRemoveLastWithIndex heap - (h₁ : index ≠ removedIndex) → newHeap.contains (heap.get index (Nat.succ_pos n)) := by - simp only - intro h₁ - have h₂ : n > 0 := by omega --cases on n, zero -> h₁ = False as Fin 1 only has one value. - unfold get get' - split - case h_1 o p v l r m_le_n max_height_difference subtree_complete del => - -- this should be reducible to heapRemoveLastWithIndexLeavesRoot - clear del - unfold contains - split - case h_1 _ hx _ => exact absurd hx (Nat.ne_of_gt h₂) - case h_2 del2 del1 oo pp vv ll rr _ _ _ he heq => - clear del1 del2 - left - have h₃ := heqSameRoot he h₂ heq - have h₄ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexLeavesRoot ((branch v l r m_le_n max_height_difference subtree_complete)) h₂ - rw[←h₄] at h₃ - rw[root_unfold] at h₃ - rw[root_unfold] at h₃ - exact h₃.symm - case h_2 j o p v l r m_le_n max_height_difference subtree_complete del h₃ => - -- this should be solvable by recursion - clear del - simp - let rightIsFull : Bool := ((p + 1).nextPowerOfTwo = p + 1) - split - case isTrue j_lt_o => - split - rename_i o d1 d2 d3 d4 d5 oo l ht1 ht2 ht3 _ - clear d1 d2 d3 d4 d5 - rw[contains_as_root_left_right _ _ (Nat.lt_add_right p $ Nat.succ_pos oo)] - right - left - --unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux - --unfolding fails. Need a helper, it seems. - if h₅ : p < oo + 1 ∧ rightIsFull then - have h₆ := heapRemoveLastWithIndexOnlyRemovesOneElement_AuxL v l r ht1 ht2 ht3 h₅ - have h₇ := heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLLength v l r ht1 ht2 ht3 h₅ - have h₈ := heqContains h₇ h₆ - rw[h₈] - have h₉ : ⟨j,j_lt_o⟩ ≠ (Internal.heapRemoveLastWithIndex l).snd.snd := heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLIndexNe v l r ht1 ht2 ht3 j_lt_o h₅ h₁ - exact CompleteTree.AdditionalProofs.heapRemoveLastWithIndexOnlyRemovesOneElement _ _ h₉ - else - have h₆ := heapRemoveLastWithIndexOnlyRemovesOneElement_AuxL2 v l r ht1 ht2 ht3 h₅ - have h₇ := heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLLength2 v l r ht1 ht2 ht3 h₅ - have h₈ := heqContains h₇ h₆ - rw[h₈] - rw[contains_iff_index_exists _ _ (Nat.succ_pos oo)] - exists ⟨j, j_lt_o⟩ - case isFalse j_ge_o => - split - rename_i p d1 d2 d3 d4 d5 h₆ pp r ht1 ht2 ht3 _ h₅ - clear d1 d2 d3 d4 d5 - rw[contains_as_root_left_right _ _ (Nat.lt_add_left o $ Nat.succ_pos pp)] - right - right - -- this should be the same as the left side, with minor adaptations... Let's see. - if h₇ : pp + 1 < o ∧ rightIsFull then - have h₈ := heapRemoveLastWithIndexOnlyRemovesOneElement_AuxR2 v l r ht1 ht2 ht3 h₇ - have h₉ := heapRemoveLastWithIndexOnlyRemovesOneElement_AuxRLength2 v l r ht1 ht2 ht3 h₇ - have h₁₀ := heqContains h₉ h₈ - rw[h₁₀] - rw[contains_iff_index_exists _ _ (Nat.succ_pos pp)] - have : p = pp.succ := (Nat.add_sub_cancel pp.succ o).subst $ (Nat.add_comm o (pp.succ)).subst (motive := λx ↦ p = x-o ) h₅.symm - exists ⟨j-o,this.subst h₆⟩ - else - have h₈ := heapRemoveLastWithIndexOnlyRemovesOneElement_AuxR v l r ht1 ht2 ht3 h₇ - have h₉ := heapRemoveLastWithIndexOnlyRemovesOneElement_AuxRLength v l r ht1 ht2 ht3 h₇ - have h₁₀ := heqContains h₉ h₈ - rw[h₁₀] - have : p = pp.succ := (Nat.add_sub_cancel pp.succ o).subst $ (Nat.add_comm o (pp.succ)).subst (motive := λx ↦ p = x-o ) h₅.symm - have h₉ : ⟨j-o,this.subst h₆⟩ ≠ (Internal.heapRemoveLastWithIndex r).snd.snd := heapRemoveLastWithIndexOnlyRemovesOneElement_AuxRIndexNe v l r ht1 ht2 ht3 (this.subst h₆) (by omega) h₇ h₁ - exact CompleteTree.AdditionalProofs.heapRemoveLastWithIndexOnlyRemovesOneElement _ _ h₉ - protected theorem heapRemoveLastWithIndexHeapRemoveLastSameTree {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) : (CompleteTree.Internal.heapRemoveLast tree).fst = (CompleteTree.Internal.heapRemoveLastWithIndex tree).fst := by unfold Internal.heapRemoveLast Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux split @@ -679,35 +165,10 @@ protected theorem heapRemoveLastWithIndexHeapRemoveLastSameElement {α : Type u} unfold Internal.heapRemoveLast Internal.heapRemoveLastWithIndex at h₃ rw[h₃] -protected theorem heapRemoveLastWithIndexEitherContainsOrReturnsElement {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : - let (newHeap, removedElement, _) := Internal.heapRemoveLastWithIndex heap - newHeap.contains (heap.get index (Nat.succ_pos n)) ∨ removedElement = heap.get index (Nat.succ_pos n) -:= - let removedIndex := (Internal.heapRemoveLastWithIndex heap).snd.snd - if h₁ : index ≠ removedIndex then - Or.inl $ CompleteTree.AdditionalProofs.heapRemoveLastWithIndexOnlyRemovesOneElement heap index h₁ - else by - right - have h₂ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex heap - unfold get - simp at h₁ - subst index - exact h₂.symm - -protected theorem heapRemoveLastEitherContainsOrReturnsElement {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : - let (newHeap, removedElement) := Internal.heapRemoveLast heap - newHeap.contains (heap.get index (Nat.succ_pos n)) ∨ removedElement = heap.get index (Nat.succ_pos n) -:= by - have h₁ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexEitherContainsOrReturnsElement heap index - simp at h₁ ⊢ - rewrite[CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameElement] - rewrite[CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameTree] - assumption - protected theorem heapRemoveLastLeavesRoot {α : Type u} {n: Nat} (heap : CompleteTree α (n+1)) (h₁ : n > 0) : heap.root (Nat.succ_pos n) = (CompleteTree.Internal.heapRemoveLast heap).fst.root h₁ := CompleteTree.heapRemoveLastAuxLeavesRoot heap _ _ _ h₁ -private theorem heapRemoveLastWithIndexIndexNeZeroForNGt1 {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) : (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd = 0 ↔ n = 0 := by +protected theorem heapRemoveLastWithIndexIndexNeZeroForNGt1 {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) : (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd = 0 ↔ n = 0 := by constructor case mp => unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux @@ -1000,3 +461,51 @@ protected theorem heapRemoveLastWithIndexRelation {α : Type u} {n : Nat} (heap CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex heap |> h₃.substr |> Eq.symm + + +/--If the resulting tree contains all elements except the removed one, and contains one less than the original, well, you get the idea.-/ +protected theorem heapRemoveLastWithIndexOnlyRemovesOneElement {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : + let (newHeap, _, removedIndex) := Internal.heapRemoveLastWithIndex heap + (h₁ : index ≠ removedIndex) → newHeap.contains (heap.get index (Nat.succ_pos n)) +:= by + simp only [ne_eq] + intro h₁ + have h₂ : n > 0 := by omega + rw[contains_iff_index_exists] + case h₁ => exact h₂ + have h₃ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelation heap index + simp at h₃ + split at h₃ + case isTrue h₄ => + exists (index.pred (Fin.ne_zero_of_gt h₄)) + case isFalse h₄ => + split at h₃ + case isTrue h₅ => + exists (index.castLT (by omega : ↑index < n)) + case isFalse h₅ => + omega --contradiction + +protected theorem heapRemoveLastWithIndexEitherContainsOrReturnsElement {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : + let (newHeap, removedElement, _) := Internal.heapRemoveLastWithIndex heap + newHeap.contains (heap.get index (Nat.succ_pos n)) ∨ removedElement = heap.get index (Nat.succ_pos n) +:= + let removedIndex := (Internal.heapRemoveLastWithIndex heap).snd.snd + if h₁ : index ≠ removedIndex then + Or.inl $ CompleteTree.AdditionalProofs.heapRemoveLastWithIndexOnlyRemovesOneElement heap index h₁ + else by + right + have h₂ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex heap + unfold get + simp at h₁ + subst index + exact h₂.symm + +protected theorem heapRemoveLastEitherContainsOrReturnsElement {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : + let (newHeap, removedElement) := Internal.heapRemoveLast heap + newHeap.contains (heap.get index (Nat.succ_pos n)) ∨ removedElement = heap.get index (Nat.succ_pos n) +:= by + have h₁ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexEitherContainsOrReturnsElement heap index + simp at h₁ ⊢ + rewrite[CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameElement] + rewrite[CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameTree] + assumption |