diff options
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs.lean | 87 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/Lemmas.lean | 15 |
2 files changed, 92 insertions, 10 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs.lean b/BinaryHeap/CompleteTree/AdditionalProofs.lean index 1b3ef50..43927f5 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs.lean @@ -91,6 +91,53 @@ private theorem if_contains_get_eq_auxl {α : Type u} {o : Nat} (tree : Complete rw[heq] assumption +private theorem if_contains_get_eq_auxr {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) (h₁ : tree.rightLen (Nat.succ_pos o) > 0) : + ∀(indexl : Fin (tree.rightLen (Nat.succ_pos o))), (tree.right _).get indexl h₁ = element → ∃(index : Fin (o+1)), tree.get index (Nat.succ_pos o) = 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 _ + 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 + apply Nat.succ_lt_succ + apply Nat.add_lt_add_left + exact indexr.isLt + exact Nat.lt_of_lt_of_eq h₃ 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 = (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 + 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 @@ -113,22 +160,42 @@ private theorem if_contains_get_eq {α : Type u} {o : Nat} (tree : CompleteTree 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 - have blah := if_contains_get_eq l element h₂ - have blupp := if_contains_get_eq_auxl tree element $ Nat.zero_lt_of_lt nn_lt_o - simp at blupp - simp[get_eq_get'] at blah ⊢ - apply blah.elim + 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 $ Nat.zero_lt_of_lt nn_lt_o + 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 - subst yy have : _ = m := heqSameRightLen (by omega) (Nat.succ_pos _) heq - subst m + 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 : tree.rightLen (Nat.succ_pos o) > 0 := by + have := heqSameRightLen (he) (Nat.succ_pos o) heq + simp[rightLen_unfold] at this + rw[this] + exact Nat.succ_pos mm + have h₄ := if_contains_get_eq_auxr tree element this + 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 blupp - case h_2.inr.inr h₂ => sorry + exact h₄ termination_by o diff --git a/BinaryHeap/CompleteTree/Lemmas.lean b/BinaryHeap/CompleteTree/Lemmas.lean index dc26dd5..1841111 100644 --- a/BinaryHeap/CompleteTree/Lemmas.lean +++ b/BinaryHeap/CompleteTree/Lemmas.lean @@ -24,6 +24,8 @@ theorem CompleteTree.left_unfold {α : Type u} {o p : Nat} (v : α) (l : Complet theorem CompleteTree.leftLen_unfold {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α o) (r : CompleteTree α p) (h₁ : p ≤ o) (h₂ : o < 2 * (p + 1)) (h₃ : (o + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : o + p + 1 > 0): (CompleteTree.branch v l r h₁ h₂ h₃).leftLen h₄ = o := rfl +theorem CompleteTree.rightLen_unfold {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α o) (r : CompleteTree α p) (h₁ : p ≤ o) (h₂ : o < 2 * (p + 1)) (h₃ : (o + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : o + p + 1 > 0): (CompleteTree.branch v l r h₁ h₂ h₃).rightLen h₄ = p := rfl + /-- Helper to rw away right, because Lean 4.9 makes it unnecessarily hard to deal with match in tactics mode... -/ theorem CompleteTree.right_unfold {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α o) (r : CompleteTree α p) (h₁ : p ≤ o) (h₂ : o < 2 * (p + 1)) (h₃ : (o + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : o + p + 1 > 0): (CompleteTree.branch v l r h₁ h₂ h₃).right h₄ = r := rfl @@ -50,3 +52,16 @@ theorem CompleteTree.leftLenLtN {α : Type u} {n : Nat} (tree : CompleteTree α rw[length] rename_i o p _ _ _ _ _ _ _ exact Nat.lt_of_le_of_lt (Nat.le_add_right o p) (Nat.lt_succ_self (o+p)) + +theorem CompleteTree.rightLenLtN {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n>0) : tree.rightLen h₁ < n := by + unfold rightLen + split + rw[length] + rename_i o p _ _ _ _ _ _ _ + exact Nat.lt_of_le_of_lt (Nat.le_add_left p o) (Nat.lt_succ_self (o+p)) + +theorem CompleteTree.lengthEqLeftRightLenSucc {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n>0) : tree.length = tree.leftLen h₁ + tree.rightLen h₁ + 1 := by + unfold leftLen rightLen + split + unfold length + rfl |