diff options
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs.lean | 71 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapOperations.lean | 4 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapProofs.lean | 12 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/Lemmas.lean | 2 | ||||
| -rw-r--r-- | TODO | 2 |
5 files changed, 79 insertions, 12 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs.lean b/BinaryHeap/CompleteTree/AdditionalProofs.lean index 43927f5..db0b258 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs.lean @@ -1,9 +1,13 @@ import BinaryHeap.CompleteTree.Lemmas import BinaryHeap.CompleteTree.AdditionalOperations import BinaryHeap.CompleteTree.HeapOperations +import BinaryHeap.CompleteTree.HeapProofs namespace BinaryHeap.CompleteTree.AdditionalProofs +---------------------------------------------------------------------------------------------- +-- contains + 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] @@ -199,7 +203,7 @@ private theorem if_contains_get_eq {α : Type u} {o : Nat} (tree : CompleteTree termination_by o -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} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) : tree.contains element ↔ ∃ (index : Fin (o+1)), tree.get' index = element := by constructor case mpr => simp only [forall_exists_index] @@ -207,9 +211,16 @@ theorem contains_iff_index_exists {α : Type u} {o : Nat} (tree : CompleteTree case mp => exact if_contains_get_eq tree element +theorem contains_iff_index_exists {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) (h₁ : n > 0): tree.contains element ↔ ∃ (index : Fin n), tree.get index h₁ = element := + match n, tree with + | _+1, tree => contains_iff_index_exists' tree element + +---------------------------------------------------------------------------------------------- +-- heapRemoveLast + /--Shows that the index and value returned by heapRemoveLastWithIndex are consistent.-/ -protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : Nat} (heap : CompleteTree α (o+1)) : heap.get' heap.heapRemoveLastWithIndex.snd.snd = heap.heapRemoveLastWithIndex.snd.fst := by - unfold CompleteTree.heapRemoveLastWithIndex CompleteTree.Internal.heapRemoveLastAux +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] @@ -286,3 +297,57 @@ protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : N simp only [Nat.pred_succ, Fin.isValue, Nat.add_sub_cancel, Fin.eta] apply AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex done + +private 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₁ + +/--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, removedValue, 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₄ := 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 + split + case isTrue j_lt_o => + split + rename_i o d1 d2 d3 d4 d5 oo l _ _ _ h₄ + clear d1 d2 d3 d4 d5 + revert h₁ + unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux + unfold contains --without this split fails... + simp only + intro h₁ + have : 0 ≠ oo.succ+p := by simp_arith + simp only[this, reduceDite] at h₁ + simp [this] + split + case h_1 hx _ => exact absurd hx (Nat.ne_of_gt $ Nat.lt_add_right p $ Nat.succ_pos oo) + case h_2 => + rename_i heq + sorry + case isFalse j_ge_o => + split + rename_i pp r _ _ _ _ + sorry diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean index 1c9a27e..f3ff41c 100644 --- a/BinaryHeap/CompleteTree/HeapOperations.lean +++ b/BinaryHeap/CompleteTree/HeapOperations.lean @@ -188,7 +188,7 @@ protected def Internal.heapRemoveLast {α : Type u} {o : Nat} (heap : CompleteTr Also returns the index of the removed element. -/ -protected def heapRemoveLastWithIndex {α : Type u} {o : Nat} (heap : CompleteTree α (o+1)) : (CompleteTree α o × α × Fin (o+1)) := +protected def Internal.heapRemoveLastWithIndex {α : Type u} {o : Nat} (heap : CompleteTree α (o+1)) : (CompleteTree α o × α × Fin (o+1)) := Internal.heapRemoveLastAux heap (β := λn ↦ α × Fin n) (λ(a : α) ↦ (a, Fin.mk 0 (Nat.succ_pos 0))) (λ(a, prev_idx) h₁ ↦ (a, prev_idx.succ.castLE $ Nat.succ_le_of_lt h₁) ) @@ -287,7 +287,7 @@ def heapRemoveAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin if index_ne_zero : index = 0 then heapPop le heap else - let (remaining_tree, removed_element, removed_index) := heap.heapRemoveLastWithIndex + let (remaining_tree, removed_element, removed_index) := Internal.heapRemoveLastWithIndex heap if p : index = removed_index then (remaining_tree, removed_element) else diff --git a/BinaryHeap/CompleteTree/HeapProofs.lean b/BinaryHeap/CompleteTree/HeapProofs.lean index a41f963..2946c30 100644 --- a/BinaryHeap/CompleteTree/HeapProofs.lean +++ b/BinaryHeap/CompleteTree/HeapProofs.lean @@ -202,7 +202,7 @@ private theorem CompleteTree.heapRemoveLastAuxLeaf | .leaf => rfl exact h₁ -private theorem CompleteTree.heapRemoveLastAuxLeavesRoot +protected theorem CompleteTree.heapRemoveLastAuxLeavesRoot {α : Type u} {β : Nat → Type u} (heap : CompleteTree α (n+1)) @@ -274,7 +274,7 @@ private theorem CompleteTree.heapRemoveLastAuxIsHeap simp only [heapRemoveLastAuxIsHeap aux0 auxl auxr h₁.left h₂ h₃, h₁.right.left, h₁.right.right.right, and_true, true_and] unfold HeapPredicate.leOrLeaf simp only - rw[←heapRemoveLastAuxLeavesRoot] + rw[←CompleteTree.heapRemoveLastAuxLeavesRoot] exact h₁.right.right.left else by simp[h₅] @@ -290,14 +290,14 @@ private theorem CompleteTree.heapRemoveLastAuxIsHeap | 0 => rfl | o+1 => have h₉ : le v ((Internal.heapRemoveLastAux r _ _ _).fst.root (Nat.zero_lt_succ o)) := by - rw[←heapRemoveLastAuxLeavesRoot] + rw[←CompleteTree.heapRemoveLastAuxLeavesRoot] exact h₁.right.right.right h₉ private theorem CompleteTree.heapRemoveLastIsHeap {α : Type u} {heap : CompleteTree α (o+1)} {le : α → α → Bool} (h₁ : HeapPredicate heap le) (h₂ : transitive_le le) (h₃ : total_le le) : HeapPredicate (Internal.heapRemoveLast heap).fst le := heapRemoveLastAuxIsHeap _ _ _ h₁ h₂ h₃ -private theorem CompleteTree.heapRemoveLastWithIndexIsHeap {α : Type u} {heap : CompleteTree α (o+1)} {le : α → α → Bool} (h₁ : HeapPredicate heap le) (h₂ : transitive_le le) (h₃ : total_le le) : HeapPredicate (heap.heapRemoveLastWithIndex.fst) le := +private theorem CompleteTree.heapRemoveLastWithIndexIsHeap {α : Type u} {heap : CompleteTree α (o+1)} {le : α → α → Bool} (h₁ : HeapPredicate heap le) (h₂ : transitive_le le) (h₃ : total_le le) : HeapPredicate ((Internal.heapRemoveLastWithIndex heap).fst) le := heapRemoveLastAuxIsHeap _ _ _ h₁ h₂ h₃ ---------------------------------------------------------------------------------------------- @@ -676,12 +676,12 @@ theorem CompleteTree.heapPopIsHeap {α : Type u} {n : Nat} (le : α → α → B -- heapRemoveAt theorem CompleteTree.heapRemoveAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin (n+1)) (heap : CompleteTree α (n+1)) (h₁ : HeapPredicate heap le) (wellDefinedLe : transitive_le le ∧ total_le le) : HeapPredicate (heap.heapRemoveAt le index).fst le := by - have h₂ : HeapPredicate heap.heapRemoveLastWithIndex.fst le := heapRemoveLastWithIndexIsHeap h₁ wellDefinedLe.left wellDefinedLe.right + have h₂ : HeapPredicate (Internal.heapRemoveLastWithIndex heap).fst le := heapRemoveLastWithIndexIsHeap h₁ wellDefinedLe.left wellDefinedLe.right unfold heapRemoveAt split case isTrue => exact heapPopIsHeap le heap h₁ wellDefinedLe case isFalse h₃ => - cases h: (index = heap.heapRemoveLastWithIndex.snd.snd : Bool) + cases h: (index = (Internal.heapRemoveLastWithIndex heap).snd.snd : Bool) <;> simp_all split <;> apply heapUpdateAtIsHeap <;> simp_all diff --git a/BinaryHeap/CompleteTree/Lemmas.lean b/BinaryHeap/CompleteTree/Lemmas.lean index 1841111..602c0bc 100644 --- a/BinaryHeap/CompleteTree/Lemmas.lean +++ b/BinaryHeap/CompleteTree/Lemmas.lean @@ -29,6 +29,8 @@ theorem CompleteTree.rightLen_unfold {α : Type u} {o p : Nat} (v : α) (l : Com /-- 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 +theorem CompleteTree.contains_unfold {α : Type u} {o p : Nat} (element : α) (v : α) (l : CompleteTree α o) (r : CompleteTree α p) (h₁ : p ≤ o) (h₂ : o < 2 * (p + 1)) (h₃ : (o + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) : (CompleteTree.branch v l r h₁ h₂ h₃).contains element = (v=element ∨ l.contains element ∨ r.contains element) := rfl + theorem CompleteTree.heqSameLeftLen {α : Type u} {n m : Nat} {a : CompleteTree α n} {b : CompleteTree α m} (h₁ : n = m) (h₂ : n > 0) (h₃ : HEq a b) : a.leftLen h₂ = b.leftLen (h₁.subst h₂) := by subst n have h₃ : a = b := eq_of_heq h₃ @@ -5,7 +5,7 @@ This is a rough outline of upcoming tasks: [ ] Prove that CompleteTree.heapUpdateAt returns the element at the given index [ ] Prove that CompleteTree.heapRemoveLastWithIndex and CompleteTree.heapRemoveLast yield the same tree [ ] Prove that CompleteTree.heapRemoveLastWithIndex and CompleteTree.heapRemoveLast yield the same element -[ ] Prove that CompleteTree.heapRemoveLastWithIndex indeed removes the last element +[ ] Prove that CompleteTree.heapRemoveLastWithIndex only removes one element and leaves the rest unchanged - This automatically serves as a proof for CompleteTree.heapRemoveLast, once it is shown that they yield the same tree - A potential approach is to show that any index in the resulting tree can be converted into an index |