From 61c5d52ffa7775cbad85b6f9daf99f8a901c6bb1 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Sun, 28 Jul 2024 22:08:00 +0200 Subject: Finish left half of heapRemoveLastWithIndexOnlyRemovesOneElement. --- BinaryHeap/CompleteTree/AdditionalProofs.lean | 99 +++++++++++++++++++-------- 1 file changed, 69 insertions(+), 30 deletions(-) diff --git a/BinaryHeap/CompleteTree/AdditionalProofs.lean b/BinaryHeap/CompleteTree/AdditionalProofs.lean index 8ef5473..442c2d3 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs.lean @@ -324,7 +324,7 @@ private theorem left_sees_through_cast {α : Type u} {p q : Nat} (h₁ : q+p+1 = assumption /--Helper for heapRemoveLastWithIndexOnlyRemovesOneElement_Auxllength to allow splitting the goal-/ -private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_Auxllength2 {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (h₁ : n > 0) +private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLLengthAux {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (h₁ : n > 0) : let o := tree.leftLen' let p := tree.rightLen' @@ -349,11 +349,11 @@ private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_Auxllength2 {α : T 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)) +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_Auxllength2 (branch v l r h₁ h₂ h₃) (Nat.lt_add_right p $ Nat.succ_pos o) + 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₄ @@ -434,29 +434,43 @@ private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxL {α : Type u} have h₅ : (branch v l r h₁ h₂ h₃).leftLen' > 0 := Nat.succ_pos o heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLAux _ _ h₅ 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 +/--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' @@ -479,10 +493,8 @@ private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxL2Aux {α : Type -- okay, dealing with p.pred.succ is a guarantee for pain. "Stuck at solving universe constraint" cases p case zero => - have : ((0 + 1).nextPowerOfTwo = 0 + 1) := by simp! (config := {ground := true}) - have : decide ((0 + 1).nextPowerOfTwo = 0 + 1) = true := by simp[this] - simp[this] at h₃ - simp at h₄ + 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... @@ -498,6 +510,29 @@ private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxL2 {α : Type u} := heapRemoveLastWithIndexOnlyRemovesOneElement_AuxL2Aux (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... @@ -544,14 +579,18 @@ protected theorem heapRemoveLastWithIndexOnlyRemovesOneElement {α : Type u} {n let rightIsFull : Bool := ((p + 1).nextPowerOfTwo = p + 1) 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₇ := 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₅ - sorry + 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 _ _ _ h₄ h₅ -- cgit v1.2.3