diff options
| -rw-r--r-- | BinaryHeap.lean | 6 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalOperations.lean | 27 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean | 213 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/Find.lean | 4 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/Get.lean | 174 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean | 2 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean | 4 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean | 18 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean | 98 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean | 31 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean | 95 |
11 files changed, 251 insertions, 421 deletions
diff --git a/BinaryHeap.lean b/BinaryHeap.lean index 61ebd42..4c7326f 100644 --- a/BinaryHeap.lean +++ b/BinaryHeap.lean @@ -53,12 +53,10 @@ def indexOf {α : Type u} {le : α → α → Bool} {n : Nat} : BinaryHeap α le tree.indexOf pred instance : GetElem (BinaryHeap α le n) (Nat) α (λ _ index ↦ index < n) where - getElem := λ heap index h₁ ↦ match n, heap, index with - | (_+1), {tree, ..}, index => tree.get' ⟨index, h₁⟩ + getElem := λ heap index h₁ ↦ heap.tree.get ⟨index, h₁⟩ instance : GetElem (BinaryHeap α le n) (Fin n) α (λ _ _ ↦ True) where - getElem := λ heap index _ ↦ match n, heap, index with - | (_+1), {tree, ..}, index => tree.get' index + getElem := λ heap index _ ↦ heap.tree.get index /--Helper for the common case of using natural numbers for sorting.-/ theorem nat_ble_to_heap_le_total : total_le Nat.ble := diff --git a/BinaryHeap/CompleteTree/AdditionalOperations.lean b/BinaryHeap/CompleteTree/AdditionalOperations.lean index ee6b685..8038555 100644 --- a/BinaryHeap/CompleteTree/AdditionalOperations.lean +++ b/BinaryHeap/CompleteTree/AdditionalOperations.lean @@ -32,27 +32,16 @@ def indexOf {α : Type u} (heap : CompleteTree α o) (pred : α → Bool) : Opti ---------------------------------------------------------------------------------------------- -- get -/--Returns the lement at the given index. Indices are depth first.-/ -def get' {α : Type u} {n : Nat} (index : Fin (n+1)) (heap : CompleteTree α (n+1)) : α := - match h₁ : index, h₂ : n, heap with - | 0, (_+_), .branch v _ _ _ _ _ => v - | ⟨j+1,h₃⟩, (o+p), .branch _ l r _ _ _ => - if h₄ : j < o then - match o with - | (oo+1) => get' ⟨j, h₄⟩ l - else - have h₅ : n - o = p := Nat.sub_eq_of_eq_add $ (Nat.add_comm o p).subst h₂ - have : p ≠ 0 := - have h₆ : o < n := Nat.lt_of_le_of_lt (Nat.ge_of_not_lt h₄) (Nat.lt_of_succ_lt_succ h₃) - h₅.symm.substr $ Nat.sub_ne_zero_of_lt h₆ - have h₆ : j - o < p := h₅.subst $ Nat.sub_lt_sub_right (Nat.ge_of_not_lt h₄) $ Nat.lt_of_succ_lt_succ h₃ - have _termination : j - o < index.val := (Fin.val_inj.mpr h₁).substr (Nat.sub_lt_succ j o) - match p with - | (pp + 1) => get' ⟨j - o, h₆⟩ r - +/--Returns the element at the given index. Indices are depth first.-/ def get {α : Type u} {n : Nat} (index : Fin n) (heap : CompleteTree α n) : α := match n, index, heap with - | (_+1), index, heap => heap.get' index + | (_+_+1), 0, .branch v _ _ _ _ _ => v + | (o+p+1), ⟨j+1,h₃⟩, .branch _ l r _ _ _ => + if h₄ : j < o then + get ⟨j, h₄⟩ l + else + have h₄ : j - o < p := Nat.sub_lt_left_of_lt_add (Nat.ge_of_not_lt h₄) $ Nat.lt_of_succ_lt_succ h₃ + get ⟨j - o, h₄⟩ r ---------------------------------------------------------------------------------------------- -- contains - implemented as decidable proposition diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean index 6614210..7a0c893 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean @@ -3,93 +3,46 @@ import BinaryHeap.CompleteTree.AdditionalProofs.Get namespace BinaryHeap.CompleteTree.AdditionalProofs -private theorem if_get_eq_contains {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) (index : Fin (o+1)) : tree.get' index = element → tree.contains element := by - unfold get' contains - simp only [Nat.succ_eq_add_one, Fin.zero_eta, Nat.add_eq, ne_eq] - split - case h_1 p q v l r _ _ _ _ => - intro h₁ - split; omega - rename α => vv - rename_i hsum heq - have h₂ := heqSameRoot (hsum) (Nat.succ_pos (p+q)) heq - rw[root_unfold] at h₂ - rw[root_unfold] at h₂ - simp only [←h₂, h₁, true_or] - case h_2 index p q v l r _ _ _ _ h₃ => - intro h₄ - split ; rename_i hx _; exact absurd hx (Nat.succ_ne_zero _) - case h_2 pp qq vv ll rr _ _ _ h₅ heq => - have : p = pp := heqSameLeftLen h₅ (Nat.succ_pos _) heq - have : q = qq := heqSameRightLen h₅ (Nat.succ_pos _) heq - subst pp qq - simp only [Nat.add_eq, Nat.succ_eq_add_one, heq_eq_eq, branch.injEq] at heq - have : v = vv := heq.left - have : l = ll := heq.right.left - have : r = rr := heq.right.right - subst vv ll rr - revert h₄ - split - all_goals - split - intro h₄ - right +private theorem if_get_eq_contains {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) (index : Fin n) : tree.get index = element → tree.contains element := by + rw[get_unfold] + rw[contains_as_root_left_right] + intro h₁ + split at h₁ + case isTrue => + left + assumption + case isFalse h => + have _termination : index.val ≠ 0 := Fin.val_ne_iff.mpr h + right + simp only at h₁ + split at h₁ case' isTrue => left case' isFalse => right all_goals - revert h₄ + revert h₁ apply if_get_eq_contains - done +termination_by index.val -private theorem if_contains_get_eq_auxl {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) : - ∀(indexl : Fin (tree.leftLen (Nat.succ_pos o))), (tree.left _).get indexl = element → ∃(index : Fin (o+1)), tree.get index = element +private theorem if_contains_get_eq_auxl {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) (h₁ : n > 0): + ∀(indexl : Fin (tree.leftLen h₁)), (tree.left _).get indexl = element → ∃(index : Fin n), tree.get index = element := by intro indexl - let index : Fin (o+1) := indexl.succ.castLT (by - simp only [Nat.succ_eq_add_one, Fin.val_succ, Nat.succ_lt_succ_iff, gt_iff_lt] - exact Nat.lt_of_lt_of_le indexl.isLt $ Nat.le_of_lt_succ $ leftLenLtN tree (Nat.succ_pos o) - ) + let index : Fin n := indexl.succ.castLT (Nat.lt_of_le_of_lt (Nat.succ_le_of_lt indexl.isLt) (leftLenLtN tree h₁)) intro prereq exists index - unfold get - simp - unfold get' - generalize hindex : index = i - split - case h_1 => - have : index.val = 0 := Fin.val_eq_of_eq hindex - contradiction - case h_2 j p q v l r ht1 ht2 ht3 _ _ => - have h₂ : index.val = indexl.val + 1 := rfl - have h₃ : index.val = j.succ := Fin.val_eq_of_eq hindex - have h₄ : j = indexl.val := Nat.succ.inj $ h₃.subst (motive := λx↦ x = indexl.val + 1) h₂ - have : p = (branch v l r ht1 ht2 ht3).leftLen (Nat.succ_pos _) := rfl - have h₅ : j < p := by simp only [this, indexl.isLt, h₄] - simp only [h₅, ↓reduceDIte, Nat.add_eq] - unfold get at prereq - split at prereq - rename_i pp ii ll hel hei heq - split - rename_i ppp lll _ _ _ _ _ _ - have : pp = ppp := by omega - subst pp - simp only [gt_iff_lt, Nat.succ_eq_add_one, Nat.add_eq, heq_eq_eq, Nat.zero_lt_succ] at * - have : j = ii.val := by omega - subst j - simp - rw[←hei] at prereq - rw[left_unfold] at heq - rw[heq] - assumption + have h₂ : index > ⟨0,h₁⟩ := Nat.zero_lt_of_ne_zero $ Fin.val_ne_iff.mpr $ Fin.succ_ne_zero _ + have h₃ : index.val ≤ tree.leftLen h₁ := Nat.succ_le_of_lt indexl.isLt + rw[get_left _ _ h₂ h₃] + exact prereq -private theorem if_contains_get_eq_auxr {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) : - ∀(indexl : Fin (tree.rightLen (Nat.succ_pos o))), (tree.right _).get indexl = element → ∃(index : Fin (o+1)), tree.get index = element +private theorem if_contains_get_eq_auxr {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) (h₁ : n > 0): + ∀(indexr : Fin (tree.rightLen h₁)), (tree.right _).get indexr = element → ∃(index : Fin n), tree.get index = element := by intro indexr - let index : Fin (o+1) := ⟨(tree.leftLen (Nat.succ_pos o) + indexr.val + 1), by - have h₂ : tree.leftLen (Nat.succ_pos _) + tree.rightLen _ + 1 = tree.length := Eq.symm $ lengthEqLeftRightLenSucc tree _ + let index : Fin n := ⟨(tree.leftLen h₁ + indexr.val + 1), by + have h₂ : tree.leftLen h₁ + tree.rightLen _ + 1 = tree.length := Eq.symm $ lengthEqLeftRightLenSucc tree _ rw[length] at h₂ - have h₃ : tree.leftLen (Nat.succ_pos o) + indexr.val + 1 < tree.leftLen (Nat.succ_pos o) + tree.rightLen (Nat.succ_pos o) + 1 := by + have h₃ : tree.leftLen h₁ + indexr.val + 1 < tree.leftLen h₁ + tree.rightLen h₁ + 1 := by apply Nat.succ_lt_succ apply Nat.add_lt_add_left exact indexr.isLt @@ -97,95 +50,39 @@ private theorem if_contains_get_eq_auxr {α : Type u} {o : Nat} (tree : Complete ⟩ intro prereq exists index - unfold get - simp - unfold get' - generalize hindex : index = i - split - case h_1 => - have : index.val = 0 := Fin.val_eq_of_eq hindex - contradiction - case h_2 j p q v l r ht1 ht2 ht3 _ _ => - have h₂ : index.val = (branch v l r ht1 ht2 ht3).leftLen (Nat.succ_pos _) + indexr.val + 1 := rfl - have h₃ : index.val = j.succ := Fin.val_eq_of_eq hindex - have h₄ : j = (branch v l r ht1 ht2 ht3).leftLen (Nat.succ_pos _) + indexr.val := by - rw[h₃] at h₂ - exact Nat.succ.inj h₂ - have : p = (branch v l r ht1 ht2 ht3).leftLen (Nat.succ_pos _) := rfl - have h₅ : ¬(j < p) := by simp_arith [this, h₄] - simp only [h₅, ↓reduceDIte, Nat.add_eq] - unfold get at prereq - split at prereq - rename_i pp ii rr hel hei heq - split - rename_i ppp rrr _ _ _ _ _ _ _ - have : pp = ppp := by rw[rightLen_unfold] at hel; exact Nat.succ.inj hel.symm - subst pp - simp only [gt_iff_lt, ne_eq, Nat.succ_eq_add_one, Nat.add_eq, Nat.reduceEqDiff, heq_eq_eq, Nat.zero_lt_succ] at * - have : j = ii.val + p := by omega - subst this - simp - rw[right_unfold] at heq - rw[heq] - assumption + have h₂ : tree.leftLen h₁ < tree.leftLen h₁ + indexr.val + 1 := Nat.lt_of_le_of_lt (Nat.le_add_right _ _) (Nat.lt_succ_self _) + rw[get_right _ index h₂] + have : index.val - tree.leftLen h₁ - 1 = indexr.val := + have : index.val = tree.leftLen h₁ + indexr.val + 1 := rfl + have : index.val = indexr.val + tree.leftLen h₁ + 1 := (Nat.add_comm indexr.val (tree.leftLen h₁)).substr this + have : index.val - (tree.leftLen h₁ + 1) = indexr.val := Nat.sub_eq_of_eq_add this + (Nat.sub_sub _ _ _).substr this + simp only[this] + assumption -private theorem if_contains_get_eq {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) (h₁ : tree.contains element) : ∃(index : Fin (o+1)), tree.get' index = element := by - revert h₁ - unfold contains - split ; rename_i hx _; exact absurd hx (Nat.succ_ne_zero o) - rename_i n m v l r _ _ _ he heq - intro h₁ +private theorem if_contains_get_eq {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) (h₁ : tree.contains element) : ∃(index : Fin n), tree.get index = element := by + unfold contains at h₁ + match n, tree with + | 0, .leaf => contradiction + | (o+p+1), .branch v l r o_le_p max_height_diff subtree_complete => cases h₁ - case h_2.inl h₂ => - unfold get' + case inl h₂ => exists 0 - split - case h_2 hx => have hx := Fin.val_eq_of_eq hx; simp at hx; - case h_1 vv _ _ _ _ _ _ _ => - have h₃ := heqSameRoot he (Nat.succ_pos _) heq - simp only[root_unfold] at h₃ - simp only[h₃, h₂] - rename_i h - cases h - case h_2.inr.inl h₂ => exact - match hn : n, hl: l with - | 0, .leaf => by contradiction - | (nn+1), l => by - have nn_lt_o : nn < o := by have : o = nn + 1 + m := Nat.succ.inj he; omega --also for termination - have h₃ := if_contains_get_eq l element h₂ - have h₄ := if_contains_get_eq_auxl tree element - simp only at h₄ - simp[get_eq_get'] at h₃ ⊢ - apply h₃.elim - match o, tree with - | (yy+_), .branch _ ll _ _ _ _ => - simp_all[left_unfold, leftLen_unfold] - have : yy = nn+1 := heqSameLeftLen (by omega) (Nat.succ_pos _) heq - have : _ = m := heqSameRightLen (by omega) (Nat.succ_pos _) heq - subst yy m - simp_all - exact h₄ - case h_2.inr.inr h₂ => exact - match hm : m, hr: r with - | 0, .leaf => by contradiction - | (mm+1), r => by - have mm_lt_o : mm < o := by have : o = n + (mm + 1) := Nat.succ.inj he; omega --termination - have h₃ := if_contains_get_eq r element h₂ - have h₄ := if_contains_get_eq_auxr tree element - simp[get_eq_get'] at h₃ ⊢ - apply h₃.elim - match o, tree with - | (_+zz), .branch _ _ rr _ _ _ => - simp_all[right_unfold, rightLen_unfold] - have : _ = n := heqSameLeftLen (by omega) (Nat.succ_pos _) heq - have : zz = mm+1 := heqSameRightLen (by omega) (Nat.succ_pos _) heq - subst n zz - simp_all - exact h₄ - termination_by o + case inr h₂ => + cases h₂ + case inl h₂ => + have h₄ := if_contains_get_eq l element h₂ + have h₅ := if_contains_get_eq_auxl (.branch v l r o_le_p max_height_diff subtree_complete) element (Nat.succ_pos _) + apply h₄.elim + assumption + case inr h₂ => + have h₄ := if_contains_get_eq r element h₂ + have h₅ := if_contains_get_eq_auxr (.branch v l r o_le_p max_height_diff subtree_complete) element (Nat.succ_pos _) + apply h₄.elim + assumption -theorem contains_iff_index_exists' {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) : tree.contains element ↔ ∃ (index : Fin (o+1)), tree.get' index = element := by +theorem contains_iff_index_exists' {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) : tree.contains element ↔ ∃ (index : Fin n), tree.get index = element := by constructor case mpr => simp only [forall_exists_index] diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean index 902afc4..32bf722 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean @@ -44,14 +44,14 @@ private theorem indexOfNoneImpPredFalseAux {α : Type u} {n : Nat} (tree : Compl else have h₃₂ : index > ⟨0,h₁⟩ := Fin.pos_iff_ne_zero.mpr h₃ if h₄ : index ≤ o then - rw[get_left (.branch v l r p_le_o max_height_difference subtree_complete) _ h₁ h₃₂ h₄] + rw[get_left (.branch v l r p_le_o max_height_difference subtree_complete) _ h₃₂ h₄] rw[left_unfold] have := indexOfNoneImpPredFalseAux l pred (currentIndex + 1) simp only [Option.isNone_iff_eq_none, Bool.not_eq_true] at this exact this h₂₂.left _ else have h₄₂ : index > o := Nat.gt_of_not_le h₄ - rw[get_right (.branch v l r p_le_o max_height_difference subtree_complete) _ (Nat.succ_pos _) h₄₂] + rw[get_right (.branch v l r p_le_o max_height_difference subtree_complete) _ h₄₂] rw[right_unfold] have := indexOfNoneImpPredFalseAux r pred (currentIndex + o + 1) simp only [Option.isNone_iff_eq_none, Bool.not_eq_true] at this diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean index f872836..1012ef5 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean @@ -3,64 +3,39 @@ import BinaryHeap.CompleteTree.Lemmas namespace BinaryHeap.CompleteTree.AdditionalProofs -theorem get_eq_get' {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (index : Fin (n+1)) : tree.get' index = tree.get index := rfl +theorem get_zero_eq_root {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n > 0): tree.root h₁ = tree.get ⟨0,h₁⟩ := + match h₂ : n, h₃ : (⟨0,h₁⟩ : Fin n), tree with + | (_+_+1), 0, .branch v _ _ _ _ _ => rfl + | nn+1, ⟨j+1,h₄⟩, _ => by + subst h₂ + simp only [heq_eq_eq, Fin.ext_iff] at h₃ -theorem get_zero_eq_root {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n > 0): tree.root h₁ = tree.get ⟨0,h₁⟩ := by - unfold get - match n with - | nn+1 => - unfold get' - split - case h_2 hx => exact absurd (Fin.mk.inj hx) (Nat.zero_ne_add_one _) - case h_1 => trivial - -theorem get_right {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin n) (h₁ : n > 0) (h₂ : index > tree.leftLen h₁) : - have h₃ : ↑index - tree.leftLen h₁ - 1 < tree.rightLen h₁ := by - revert h₂ - unfold leftLen rightLen length - split - intro h₂ - rename_i o p v l r _ _ _ _ - have h₃ := index.isLt - apply Nat.sub_lt_right_of_lt_add - omega - apply Nat.sub_lt_right_of_lt_add - omega - have : p+1+o = (o.add p).succ := by simp_arith - rw[this] - assumption - tree.get index = (tree.right h₁).get ⟨index.val - (tree.leftLen h₁) - 1, h₃⟩ -:= - match n, tree with - | (o+p+1), .branch v l r _ _ _ => by - simp[right_unfold, leftLen_unfold] - rw[leftLen_unfold] at h₂ - generalize hnew : get ⟨↑index - o - 1, _⟩ r = new - unfold get get' - split - case h_1 => - contradiction - case h_2 j h₃ o2 p2 v2 l2 r2 _ _ _ d1 he₁ he₂ _ => - clear d1 - have : o = o2 := heqSameLeftLen (congrArg Nat.succ he₁) (Nat.succ_pos _) he₂ - have : p = p2 := heqSameRightLen (congrArg Nat.succ he₁) (Nat.succ_pos _) he₂ - subst o2 p2 - simp at he₂ - have : v = v2 := he₂.left - have : l = l2 := he₂.right.left - have : r = r2 := he₂.right.right - subst r2 l2 v2 - simp_all - have : ¬j < o := by simp_arith[h₂] - simp[this] - cases p <;> simp - case zero => - omega - case succ pp _ _ _ _ _ _ => - have : j + 1 - o - 1 = j - o := by omega - simp[this] at hnew - rw[get_eq_get'] - assumption +theorem get_right {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin n) (h₂ : index > tree.leftLen (Nat.zero_lt_of_lt index.isLt)) + : have h₁ : n > 0 := Nat.zero_lt_of_lt index.isLt + have h₃ : ↑index - tree.leftLen h₁ - 1 < tree.rightLen h₁ := by + revert h₂ + unfold leftLen rightLen length + split + intro h₂ + rename_i o p v l r _ _ _ + have h₃ := index.isLt + apply Nat.sub_lt_right_of_lt_add + omega + apply Nat.sub_lt_right_of_lt_add + omega + have : p+1+o = (o.add p).succ := by simp_arith + rw[this] + assumption + tree.get index = (tree.right h₁).get ⟨index.val - (tree.leftLen h₁) - 1, h₃⟩ + := + match n, index, tree with + | (o+p+1), ⟨j+1,h₃⟩, .branch _ _ r _ _ _ => + if h₄ : j < o then + absurd h₄ $ Nat.not_lt_of_ge (Nat.le_of_lt_succ h₂) + else by + simp only[right_unfold, leftLen_unfold] + have : j + 1 - o - 1 = j - o := by omega + simp (config := {autoUnfold := true})[this, h₄] theorem get_right' {α : Type u} {n m : Nat} {v : α} {l : CompleteTree α n} {r : CompleteTree α m} {m_le_n : m ≤ n} {max_height_diff : n < 2 * (m + 1)} {subtree_complete : (n + 1).isPowerOfTwo ∨ (m + 1).isPowerOfTwo} (index : Fin (n + m + 1)) (h₁ : index > n) : have h₂ : ↑index - n - 1 < m := by @@ -74,36 +49,73 @@ theorem get_right' {α : Type u} {n m : Nat} {v : α} {l : CompleteTree α n} {r assumption (branch v l r m_le_n max_height_diff subtree_complete).get index = r.get ⟨index.val - n - 1, h₂⟩ := - get_right (branch v l r m_le_n max_height_diff subtree_complete) index (Nat.succ_pos _) h₁ + get_right (branch v l r m_le_n max_height_diff subtree_complete) index h₁ -theorem get_left {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin n) (h₁ : n > 0) (h₂ : index > ⟨0, h₁⟩) (h₃ : index ≤ tree.leftLen h₁) : +theorem get_left {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin n) (h₂ : index > ⟨0, (Nat.zero_lt_of_lt index.isLt)⟩) (h₃ : index ≤ tree.leftLen (Nat.zero_lt_of_lt index.isLt)) : + have h₁ : n > 0 := Nat.zero_lt_of_lt index.isLt have h₃ : ↑index - 1 < tree.leftLen h₁ := Nat.lt_of_lt_of_le (Nat.pred_lt_self h₂) h₃ tree.get index = (tree.left h₁).get ⟨index.val - 1, h₃⟩ := - match n, tree with - | (o+p+1), .branch v l r _ _ _ => by - simp[left_unfold] - generalize hnew : get ⟨↑index - 1, _⟩ l = new - unfold get get' - split - case h_1 => contradiction - case h_2 j h₃ o2 p2 v2 l2 r2 _ _ _ d1 he₁ he₂ => - clear d1 - have : o = o2 := heqSameLeftLen (congrArg Nat.succ he₁) (Nat.succ_pos _) he₂ - have : p = p2 := heqSameRightLen (congrArg Nat.succ he₁) (Nat.succ_pos _) he₂ - subst o2 p2 - simp[leftLen_unfold] at h₃ - have h₄ : j < o :=Nat.lt_of_succ_le h₃ - simp[h₄] - cases o ; contradiction - case succ oo => - simp at hnew he₂ ⊢ - have := he₂.right.left - subst l2 - assumption + match n, index, tree with + | (o+p+1), ⟨j+1,h₅⟩, .branch _ l _ _ _ _ => + if h₄ : j < o then by + simp only[left_unfold, leftLen_unfold] + have : j + 1 - o - 1 = j - o := by omega + simp (config := {autoUnfold := true})[this, h₄] + else + absurd (Nat.lt_of_succ_le h₃) h₄ theorem get_left' {α : Type u} {n m : Nat} {v : α} {l : CompleteTree α n} {r : CompleteTree α m} {m_le_n : m ≤ n} {max_height_diff : n < 2 * (m + 1)} {subtree_complete : (n + 1).isPowerOfTwo ∨ (m + 1).isPowerOfTwo} (index : Fin (n + m + 1)) (h₁ : index > ⟨0, Nat.succ_pos _⟩) (h₂ : index ≤ n) : have h₃ : ↑index - 1 < n := Nat.lt_of_lt_of_le (Nat.pred_lt_self h₁) h₂ (branch v l r m_le_n max_height_diff subtree_complete).get index = l.get ⟨index.val - 1, h₃⟩ := - get_left (branch v l r m_le_n max_height_diff subtree_complete) index (Nat.succ_pos _) h₁ h₂ + get_left (branch v l r m_le_n max_height_diff subtree_complete) index h₁ h₂ + +theorem get_unfold {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin n) + : + have h₁ : n > 0 := (Nat.zero_lt_of_lt index.isLt) + tree.get index = + if h₂ : index = ⟨0, h₁⟩ then + tree.root h₁ + else if h₃ : index ≤ tree.leftLen h₁ then + have h₃ : ↑index - 1 < tree.leftLen h₁ := Nat.lt_of_lt_of_le (Nat.pred_lt_self $ Nat.zero_lt_of_ne_zero $ Fin.val_ne_iff.mpr h₂) h₃ + (tree.left h₁).get ⟨index.val - 1, h₃⟩ + else + have h₃ : ↑index - tree.leftLen h₁ - 1 < tree.rightLen h₁ := by + revert h₃ + unfold leftLen rightLen length + split + intro h₂ + rename_i o p v l r _ _ _ _ _ + have h₃ := index.isLt + apply Nat.sub_lt_right_of_lt_add + omega + apply Nat.sub_lt_right_of_lt_add + omega + have : p+1+o = (o.add p).succ := by simp_arith + rw[this] + assumption + (tree.right h₁).get ⟨index.val - (tree.leftLen h₁) - 1, h₃⟩ + := + have h₁ : n > 0 := (Nat.zero_lt_of_lt index.isLt) + if h₂ : index = ⟨0, h₁⟩ then by + simp only [h₂] + exact Eq.symm $ get_zero_eq_root _ _ + else if h₃ : index ≤ tree.leftLen h₁ then by + simp [h₂, h₃] + exact get_left tree index (Nat.zero_lt_of_ne_zero $ Fin.val_ne_iff.mpr h₂) h₃ + else by + simp [h₂, h₃] + exact get_right tree index (Nat.gt_of_not_le h₃) + +theorem get_unfold' {α : Type u} {n m : Nat} {v : α} {l : CompleteTree α n} {r : CompleteTree α m} {m_le_n : m ≤ n} {max_height_diff : n < 2 * (m + 1)} {subtree_complete : (n + 1).isPowerOfTwo ∨ (m + 1).isPowerOfTwo} (index : Fin (n + m + 1)) : + (branch v l r m_le_n max_height_diff subtree_complete).get index = if h₂ : index = ⟨0, Nat.zero_lt_of_lt index.isLt⟩ then + v + else if h₃ : index ≤ n then + have h₃ : ↑index - 1 < n := Nat.lt_of_lt_of_le (Nat.pred_lt_self $ Nat.zero_lt_of_ne_zero $ Fin.val_ne_iff.mpr h₂) h₃ + l.get ⟨index.val - 1, h₃⟩ + else + have h₃ : ↑index - n - 1 < m := by omega + r.get ⟨index.val - n - 1, h₃⟩ + := + get_unfold _ _ diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean index 807bdcb..09b1450 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean @@ -37,8 +37,6 @@ theorem heapPopOnlyRemovesRoot {α : Type u} {n : Nat} (tree : CompleteTree α ( if h₂ : index = (Internal.heapRemoveLastWithIndex tree).snd.snd then have h₃ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex tree rw[←h₂] at h₃ - unfold get - simp only have := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameElement tree rw[←this] at h₃ simp[h₃, heapUpdateRootContainsUpdatedElement] diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean index ea2b5a7..62b0e2c 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean @@ -87,7 +87,7 @@ theorem heapPushRetainsHeapValues {α : Type u} {n: Nat} (le : α → α → Boo split case' isFalse => rw[←containsSeesThroughCast] case' isTrue | isFalse => - rw[get_left (.branch v l r p_le_o max_height_difference subtree_complete) index (Nat.succ_pos _) h₂₂ h₃] + rw[get_left (.branch v l r p_le_o max_height_difference subtree_complete) index h₂₂ h₃] rw[contains_as_root_left_right _ _ (Nat.succ_pos _)] right; left rw[left_unfold] @@ -102,7 +102,7 @@ theorem heapPushRetainsHeapValues {α : Type u} {n: Nat} (le : α → α → Boo split case' isFalse => rw[←containsSeesThroughCast] case' isTrue | isFalse => - rw[get_right (.branch v l r p_le_o max_height_difference subtree_complete) index (Nat.succ_pos _) (Nat.gt_of_not_le h₃)] + rw[get_right (.branch v l r p_le_o max_height_difference subtree_complete) index (Nat.gt_of_not_le h₃)] rw[contains_as_root_left_right _ _ (Nat.succ_pos _)] right; right rw[right_unfold] diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean index a8a551f..dcff870 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean @@ -5,11 +5,11 @@ import BinaryHeap.CompleteTree.AdditionalProofs.HeapRemoveLast namespace BinaryHeap.CompleteTree.AdditionalProofs -theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : (heap.heapRemoveAt le index).snd = heap.get' index := by +theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : (heap.heapRemoveAt le index).snd = heap.get index := by unfold heapRemoveAt if h₁ : index = 0 then simp only [h₁, ↓reduceDIte] - rw[get_eq_get', ←Fin.zero_eta, ←get_zero_eq_root] + rw[←Fin.zero_eta, ←get_zero_eq_root] exact heapPopReturnsRoot heap le else simp only [h₁, ↓reduceDIte, ge_iff_le] @@ -20,15 +20,15 @@ theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → if h₃ : (Internal.heapRemoveLastWithIndex heap).2.snd ≤ index then simp only[h₂, h₃, ↓reduceDIte] have h₄ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationGt heap index $ Nat.lt_of_le_of_ne h₃ (Fin.val_ne_iff.mpr (Ne.symm h₂)) - rewrite[get_eq_get', ←h₄] + rewrite[←h₄] exact Eq.symm $ heapUpdateAtReturnsElementAt le _ _ _ else simp only[h₂, h₃, ↓reduceDIte] have h₄ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationLt heap index (Nat.gt_of_not_le h₃) - rewrite[get_eq_get', ←h₄] + rewrite[←h₄] exact Eq.symm $ heapUpdateAtReturnsElementAt le _ _ _ -theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (removeIndex : Fin (n+1)) (otherIndex : Fin (n+1)) (h₁ : removeIndex ≠ otherIndex) : (heap.heapRemoveAt le removeIndex).fst.contains (heap.get' otherIndex) := by +theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (removeIndex : Fin (n+1)) (otherIndex : Fin (n+1)) (h₁ : removeIndex ≠ otherIndex) : (heap.heapRemoveAt le removeIndex).fst.contains (heap.get otherIndex) := by unfold heapRemoveAt if h₂ : removeIndex = 0 then subst removeIndex @@ -45,13 +45,13 @@ theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bo simp only [gt_iff_lt] at h₅ split at h₅ case isTrue h₆ => - rw[get_eq_get', ←h₅] + rw[←h₅] apply heapUpdateAtOnlyUpdatesAt simp only [ne_eq, Fin.pred_inj, h₁, not_false_eq_true] case isFalse h₆ => split at h₅ case isTrue h₇ => - rw[get_eq_get', ←h₅] + rw[←h₅] apply heapUpdateAtOnlyUpdatesAt simp only [ne_eq, Fin.ext_iff, Fin.coe_pred, Fin.coe_castLT] generalize (Internal.heapRemoveLastWithIndex heap).snd.snd = j at * @@ -69,7 +69,7 @@ theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bo simp only [gt_iff_lt] at h₅ split at h₅ case isTrue h₆ => - rw[get_eq_get', ←h₅] + rw[←h₅] apply heapUpdateAtOnlyUpdatesAt simp[Fin.ext_iff] generalize (Internal.heapRemoveLastWithIndex heap).snd.snd = j at * @@ -77,7 +77,7 @@ theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bo case isFalse h₆ => split at h₅ case isTrue h₇ => - rw[get_eq_get', ←h₅] + rw[←h₅] apply heapUpdateAtOnlyUpdatesAt rw[←Fin.val_ne_iff] at h₁ ⊢ exact h₁ diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index 694a0ee..cf0774f 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -7,84 +7,39 @@ import BinaryHeap.CompleteTree.NatLemmas namespace BinaryHeap.CompleteTree.AdditionalProofs /--Shows that the index and value returned by heapRemoveLastWithIndex are consistent.-/ -protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : Nat} (heap : CompleteTree α (o+1)) : heap.get' (Internal.heapRemoveLastWithIndex heap).snd.snd = (Internal.heapRemoveLastWithIndex heap).snd.fst := by +protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : Nat} (heap : CompleteTree α (o+1)) : heap.get (Internal.heapRemoveLastWithIndex heap).snd.snd = (Internal.heapRemoveLastWithIndex heap).snd.fst := by unfold CompleteTree.Internal.heapRemoveLastWithIndex CompleteTree.Internal.heapRemoveLastAux split rename_i n m v l r m_le_n max_height_difference subtree_full simp only [Nat.add_eq, Fin.zero_eta, Fin.isValue, decide_eq_true_eq, Fin.castLE_succ] split case isTrue n_m_zero => - unfold get' - split - case h_1 nn mm vv ll rr mm_le_nn _ _ _ _ he₁ he₂ => - have h₁ : n = 0 := And.left $ Nat.add_eq_zero.mp n_m_zero.symm - have h₂ : m = 0 := And.right $ Nat.add_eq_zero.mp n_m_zero.symm - have h₃ : nn = 0 := And.left (Nat.add_eq_zero.mp $ Eq.symm $ (Nat.zero_add 0).subst (motive := λx ↦ x = nn + mm) $ h₂.subst (motive := λx ↦ 0 + x = nn + mm) (h₁.subst (motive := λx ↦ x + m = nn + mm) he₁)) - have h₄ : mm = 0 := And.right (Nat.add_eq_zero.mp $ Eq.symm $ (Nat.zero_add 0).subst (motive := λx ↦ x = nn + mm) $ h₂.subst (motive := λx ↦ 0 + x = nn + mm) (h₁.subst (motive := λx ↦ x + m = nn + mm) he₁)) - subst n m nn mm - exact And.left $ CompleteTree.branch.inj (eq_of_heq he₂.symm) - case h_2 => - omega -- to annoying to deal with Fin.ofNat... There's a hypothesis that says 0 = ⟨1,_⟩. + have h₁ : n = 0 := And.left $ Nat.add_eq_zero.mp n_m_zero.symm + have h₂ : m = 0 := And.right $ Nat.add_eq_zero.mp n_m_zero.symm + subst n m + rfl case isFalse n_m_not_zero => - unfold get' split - case h_1 nn mm vv ll rr mm_le_nn max_height_difference_2 subtree_full2 _ he₁ he₂ he₃ => - --aaaaaaaaaaaaaaaaaaaaaaaaaaaaaa - --okay, I know that he₁ is False. - --but reducing this wall of text to something the computer understands - I am frightened. - exfalso - revert he₁ - split - case' isTrue => cases l; case leaf hx => exact absurd hx.left $ Nat.not_lt_zero m - all_goals - apply Fin.ne_of_val_ne - simp only [Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat, Nat.add_one_ne_zero, not_false_eq_true] - --okay, this wasn't that bad - case h_2 j j_lt_n_add_m nn mm vv ll rr mm_le_nn max_height_difference_2 subtree_full2 heap he₁ he₂ he₃ => - --he₁ relates j to the other indices. This is the important thing here. - --it should be reducible to j = (l or r).heap.heapRemoveLastWithIndex.snd.snd - --or something like it. - - --but first, let's get rid of mm and nn, and vv while at it. - -- which are equal to m, n, v, but we need to deduce this from he₃... - have : n = nn := heqSameLeftLen (congrArg (·+1) he₂) (Nat.succ_pos _) he₃ - have : m = mm := heqSameRightLen (congrArg (·+1) he₂) (Nat.succ_pos _) he₃ - subst nn mm - simp only [heq_eq_eq, branch.injEq] at he₃ - -- yeah, no more HEq fuglyness! - have : v = vv := he₃.left - have : l = ll := he₃.right.left - have : r = rr := he₃.right.right - subst vv ll rr - split at he₁ - <;> rename_i goLeft - <;> simp only [goLeft, and_self, ↓reduceDIte, Fin.isValue] - case' isTrue => - cases l; - case leaf => exact absurd goLeft.left $ Nat.not_lt_zero m - rename_i o p _ _ _ _ _ _ _ - case' isFalse => - cases r; - case leaf => simp (config := { ground := true }) only [and_true, Nat.not_lt, Nat.le_zero_eq] at goLeft; - exact absurd ((Nat.add_zero n).substr goLeft.symm) n_m_not_zero - all_goals - have he₁ := Fin.val_eq_of_eq he₁ - simp only [Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat, Nat.reduceEqDiff] at he₁ - have : max_height_difference_2 = max_height_difference := rfl - have : subtree_full2 = subtree_full := rfl - subst max_height_difference_2 subtree_full2 - rename_i del1 del2 - clear del1 del2 - case' isTrue => - have : j < o + p + 1 := by omega --from he₁. It has j = (blah : Fin (o+p+1)).val - case' isFalse => - have : ¬j<n := by omega --from he₁. It has j = something + n. - all_goals - simp only [this, ↓reduceDIte, Nat.pred_succ, Fin.isValue] - subst j -- overkill, but unlike rw it works - simp only [Nat.pred_succ, Fin.isValue, Nat.add_sub_cancel, Fin.eta] + case isTrue goLeft => + match _term : n, l, m_le_n, max_height_difference, subtree_full with + | (nn+1), l ,m_le_n, max_height_difference, subtree_full => + dsimp only [Fin.isValue, Nat.succ_eq_add_one] + rw[get_left, left_unfold] + case h₂ => exact Nat.succ_pos _ + case h₃ => exact (Internal.heapRemoveLastAux (β := λ n ↦ α × Fin n) l _ _ _).2.snd.isLt + apply AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex + case isFalse goRight => + dsimp only [Nat.pred_eq_sub_one, Nat.succ_eq_add_one, Fin.isValue] + cases r -- to work around cast + case leaf => simp (config:={ground:=true}) at goRight; exact absurd goRight.symm n_m_not_zero + case branch rv rl rr rm_le_n rmax_height_difference rsubtree_full => + rw[get_right, right_unfold] + case h₂ => simp_arith[leftLen_unfold] + simp only [Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat, leftLen_unfold] + have : ∀(a : Nat), a + n + 1 - n - 1 = a := λa↦(Nat.add_sub_cancel _ _).subst $ (Nat.add_assoc a n 1).subst (motive := λx↦a+n+1-n-1 = x-(n+1)) $ (Nat.sub_sub (a+n+1) n 1).subst rfl + simp only[this] apply AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex - done + protected theorem heapRemoveLastWithIndexLeavesRoot {α : Type u} {n: Nat} (heap : CompleteTree α (n+1)) (h₁ : n > 0) : heap.root (Nat.succ_pos n) = (CompleteTree.Internal.heapRemoveLastWithIndex heap).fst.root h₁ := CompleteTree.heapRemoveLastAuxLeavesRoot heap _ _ _ h₁ @@ -267,7 +222,6 @@ if h₃ : p < o ∧ (p + 1).nextPowerOfTwo = p + 1 then rewrite[←lens_see_through_cast _ leftLen _ (Nat.succ_pos _) _] rewrite[leftLen_unfold] assumption - omega simp only [Nat.add_eq, ne_eq, Fin.zero_eta, Nat.succ_eq_add_one, Nat.pred_eq_sub_one, Fin.coe_pred, Fin.isValue, ← lens_see_through_cast _ leftLen _ (Nat.succ_pos _) _] simp only[leftLen_unfold] @@ -502,10 +456,10 @@ protected theorem heapRemoveLastWithIndexEitherContainsOrReturnsElement {α : Ty else by right have h₂ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex heap - unfold get simp at h₁ subst index - exact h₂.symm + rw[h₂] + rfl /-- Shows that each element contained before removing the last that is not the last is still contained after removing the last. diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean index be82a57..606b687 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean @@ -5,19 +5,18 @@ import BinaryHeap.CompleteTree.AdditionalProofs.Get namespace BinaryHeap.CompleteTree.AdditionalProofs +theorem heapUpdatAtRootEqUpdateRoot {α : Type u} {le : α → α → Bool} : CompleteTree.heapUpdateAt le ⟨0, h₁⟩ = CompleteTree.heapUpdateRoot h₁ le := by + funext + unfold heapUpdateAt heapUpdateAtAux + rfl + theorem heapUpdateAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (val : α) (heap : CompleteTree α n) (index : Fin n) : heap.get index = (heap.heapUpdateAt le index val).snd := by cases index rename_i i isLt cases i case mk.zero => - unfold get get' - split - split - case h_2 hx => - have hx := Fin.val_eq_of_eq hx - contradiction - case h_1 v l r h₂ h₃ h₄ _ _=> - exact Eq.symm $ heapUpdateRootReturnsRoot le val (.branch v l r h₂ h₃ h₄) (Nat.succ_pos _) + rw[←get_zero_eq_root, heapUpdatAtRootEqUpdateRoot] + exact Eq.symm $ heapUpdateRootReturnsRoot le val heap isLt case mk.succ j => unfold heapUpdateAt heapUpdateAtAux generalize hj : (⟨j + 1, isLt⟩ : Fin n) = index -- otherwise split fails... @@ -37,18 +36,12 @@ theorem heapUpdateAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → exact h₂ apply heapUpdateAtReturnsElementAt case isFalse h₂ => - rw[get_right _ _] - case h₁ => exact Nat.succ_pos _ + rw[get_right] case h₂ => simp only [Nat.not_le] at h₂ simp only [leftLen_unfold, gt_iff_lt, h₂] apply heapUpdateAtReturnsElementAt -theorem heapUpdatAtRootEqUpdateRoot {α : Type u} {le : α → α → Bool} : CompleteTree.heapUpdateAt le ⟨0, h₁⟩ = CompleteTree.heapUpdateRoot h₁ le := by - funext - unfold heapUpdateAt heapUpdateAtAux - rfl - theorem heapUpdateAtContainsValue {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α n) (value : α) (index : Fin n) : (heap.heapUpdateAt le index value).fst.contains value := by unfold heapUpdateAt heapUpdateAtAux generalize heapUpdateAt.proof_1 index = h₁ @@ -141,7 +134,7 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo case false.isTrue h₅ | true.isTrue h₅ => if h₆ : otherIndex ≤ o then have : otherIndex ≤ (branch v l r olep mhd stc).leftLen (Nat.succ_pos _) := by simp only [leftLen_unfold, h₆] - rw[get_left _ _ (Nat.succ_pos _) h₄₂ this] + rw[get_left _ _ h₄₂ this] left --rw[left_unfold] have : o < o + p + 1 := Nat.lt_of_le_of_lt (Nat.le_add_right o p) (Nat.lt_succ_self (o+p)) @@ -150,7 +143,7 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo exact (Nat.pred_ne_of_ne (Fin.pos_iff_ne_zero.mpr h₃) (Fin.pos_iff_ne_zero.mpr h₄)).mp $ Fin.val_ne_iff.mpr h₂ else have : otherIndex > (branch v l r olep mhd stc).leftLen (Nat.succ_pos _) := by rw[leftLen_unfold]; exact Nat.gt_of_not_le h₆ - rw[get_right _ _ (Nat.succ_pos _) this] + rw[get_right _ _ this] right --rw[right_unfold] --rw[right_unfold] @@ -164,7 +157,7 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo case false.isFalse h₅ | true.isFalse h₅ => if h₆ : otherIndex ≤ o then have : otherIndex ≤ (branch v l r olep mhd stc).leftLen (Nat.succ_pos _) := by simp only [leftLen_unfold, h₆] - rw[get_left _ _ (Nat.succ_pos _) h₄₂ this] + rw[get_left _ _ h₄₂ this] left --rw[left_unfold] --rw[left_unfold] @@ -175,7 +168,7 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo omega else have h₆ : otherIndex > (branch v l r olep mhd stc).leftLen (Nat.succ_pos _) := by rw[leftLen_unfold]; exact Nat.gt_of_not_le h₆ - rw[get_right _ _ (Nat.succ_pos _) h₆] + rw[get_right _ _ h₆] right --rw[right_unfold] have : p < o + p + 1 := Nat.lt_of_le_of_lt (Nat.le_add_left p o) (Nat.lt_succ_self (o+p)) diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean index cd765bb..1a44da1 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean @@ -18,10 +18,8 @@ abbrev heapUpdateRootReturnsRoot {α : Type u} {n : Nat} (le : α → α → Boo -/ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α → Bool) (tree : CompleteTree α n) (h₁ : n > 0) (index : Fin n) (h₂ : index ≠ ⟨0, h₁⟩) (value : α) : (tree.heapUpdateRoot h₁ le value).fst.contains $ tree.get index := by generalize h₃ : (get index tree) = oldVal - unfold get at h₃ unfold heapUpdateRoot split - simp at h₃ rename_i o p v l r p_le_o _ _ _ cases o case zero => @@ -30,50 +28,46 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α exact absurd (Fin.fin_one_eq_zero index) h₂ case succ oo _ _ _ => simp - unfold get' at h₃ - split at h₃ - case h_1 => omega - case h_2 j _ o2 p2 v2 l2 r2 _ _ _ _ he1 he2 => - have : oo+1 = o2 := heqSameLeftLen (congrArg Nat.succ he1) (by simp_arith) he2 - have : p = p2 := heqSameRightLen (congrArg Nat.succ he1) (by simp_arith) he2 - subst o2 - subst p2 - simp at he2 - have := he2.left - have := he2.right.left - have := he2.right.right - subst v2 l2 r2 - simp at h₃ - cases p - case zero => - have : j < oo + 1 := by omega - simp[this] at h₃ ⊢ - cases le value (l.root _) <;> simp - case false => - cases j - case zero => - rw[heapUpdateRootReturnsRoot] - rw[get_zero_eq_root] - unfold get; simp only - rw[h₃, contains_as_root_left_right _ _ (Nat.succ_pos _)] - left - rw[root_unfold] - case succ jj h₄ => - have h₅ : oo = 0 := by omega - have h₆ : jj < oo := Nat.lt_of_succ_lt_succ this - have h₆ : jj < 0 := h₅.subst h₆ - exact absurd h₆ $ Nat.not_lt_zero jj - case true h₄ _ _ _ _ _=> - rw[contains_as_root_left_right _ _ h₄] - right + rw[get_unfold'] at h₃ + simp only[h₂, reduceDIte] at h₃ + cases p + case zero => + let j := index.val.pred + simp at h₃ ⊢ + have : index.val ≤ oo + 1 := Nat.le_of_lt_succ index.isLt + simp only [this, reduceDIte] at h₃ + cases le value (l.root _) <;> simp + case false => + cases hj : j + case zero => + rw[heapUpdateRootReturnsRoot] + rw[get_zero_eq_root] + rw[contains_as_root_left_right _ _ (Nat.succ_pos _)] left - rewrite[contains_iff_index_exists'] - exists ⟨j,this⟩ - case succ pp _ _ _ _ _ _ _ _ => + rw[root_unfold] + simp only[←hj] + exact h₃ + case succ jj => + have h₅ : oo = 0 := by omega + have h₆ : index.val = jj + 1 + 1 := hj.subst (motive := λx ↦ index.val = x + 1) $ Eq.symm $ Nat.succ_pred (Fin.val_ne_iff.mpr h₂) + have h₇ : jj < 0 := h₅.subst $ Nat.le_of_succ_le_succ $ h₆.subst (motive := λx ↦ x ≤ oo + 1) this + exact absurd h₇ $ Nat.not_lt_zero jj + case true h₄ => + rw[contains_as_root_left_right _ _ h₄] + right + left + rewrite[contains_iff_index_exists'] + exists ⟨j, (Nat.succ_pred (Fin.val_ne_iff.mpr h₂)).substr (p := λx ↦ x ≤ oo + 1) this⟩ + case succ pp _ _ _ => + have h₂ := Fin.val_ne_iff.mpr h₂ + generalize hi : index.val = i at h₂ ⊢ + simp only[hi] at h₃ + cases i; contradiction + case succ j => simp if h : j < oo + 1 then -- index was in l - simp only [h, ↓reduceDIte] at h₃ + simp only [Nat.succ_le_of_lt h, ↓reduceDIte] at h₃ split case isTrue => simp @@ -91,8 +85,6 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α cases j case zero => rw[get_zero_eq_root] - unfold get - simp only rw[h₃, contains_as_root_left_right _ _ (Nat.succ_pos _)] left rw[root_unfold] @@ -104,8 +96,8 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α rw[←h₃, left_unfold] have : oo + 1 < oo + 1 + pp + 1 + 1 := by simp_arith --termination apply heapUpdateRootOnlyUpdatesRoot - apply Fin.ne_of_val_ne - simp only [Nat.add_one_ne_zero, not_false_eq_true] + apply Fin.val_ne_iff.mp + exact Nat.succ_ne_zero _ case isFalse => -- r.root gets moved up rw[contains_as_root_left_right _ _ (Nat.succ_pos _)] @@ -116,9 +108,9 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α exists ⟨j, h⟩ else -- index was in r - simp only [h, ↓reduceDIte] at h₃ - rename_i h₄ _ _ _ _ - have h₄ : j - (oo + 1) < pp + 1 := Nat.sub_lt_left_of_lt_add (Nat.le_of_not_gt h) (Nat.lt_of_succ_lt_succ h₄) + have : j + 1 - (oo + 1) - 1 = j - oo - 1 := (Nat.sub_sub (j+1) 1 oo).substr $ (Nat.add_comm oo 1).substr rfl + simp only [this, Not.intro $ h ∘ Nat.lt_of_succ_le ∘ (Nat.succ_eq_add_one j).substr, ↓reduceDIte] at h₃ + have h₄ : j - (oo + 1) < pp + 1 := Nat.sub_lt_left_of_lt_add (Nat.le_of_not_gt h) (Nat.lt_of_succ_lt_succ $ hi.subst (motive := λx ↦ x < _) index.isLt) split case isTrue h₄ _ _ _ _ _ => simp @@ -141,14 +133,12 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α case isFalse => --r.root gets moved up simp only - generalize h₅ : j - (oo + 1) = jr + generalize h₅ : j - oo - 1 = jr simp only [h₅] at h₃ have h₄ : jr < pp+1 := h₅.subst (motive := λx ↦ x < pp+1) h₄ cases jr case zero => rw[get_zero_eq_root] - unfold get - simp only rw[h₃, contains_as_root_left_right _ _ (Nat.succ_pos _)] left rw[root_unfold] @@ -161,7 +151,6 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α apply heapUpdateRootOnlyUpdatesRoot apply Fin.ne_of_val_ne simp only [Nat.add_one_ne_zero, not_false_eq_true] -termination_by n theorem heapUpdateRootContainsUpdatedElement {α : Type u} {n : Nat} (tree : CompleteTree α n) (le : α → α → Bool) (value : α) (h₁ : n > 0): (tree.heapUpdateRoot h₁ le value).fst.contains value := by unfold heapUpdateRoot |