diff options
Diffstat (limited to 'Common/BinaryHeap.lean')
| -rw-r--r-- | Common/BinaryHeap.lean | 72 |
1 files changed, 59 insertions, 13 deletions
diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean index 1523dea..faac226 100644 --- a/Common/BinaryHeap.lean +++ b/Common/BinaryHeap.lean @@ -173,18 +173,34 @@ private def CompleteTree.heapInsert (le : α → α → Bool) (elem : α) (heap private theorem CompleteTree.rootSeesThroughCast (n m : Nat) - (h₁ : n+1+m+1=n+m+1+1) - (h₂ : 0<n+1+m+1) - (h₃ : 0<n+m+1+1) - (heap : CompleteTree α (n+1+m+1)) : (h₁▸heap).root h₃ = heap.root h₂ := by + (h₁ : n + 1 + m = n + m + 1) + (h₂ : 0 < n + 1 + m) + (h₃ : 0 < n + m + 1) + (heap : CompleteTree α (n+1+m)) : (h₁▸heap).root h₃ = heap.root h₂ := by induction m generalizing n case zero => simp case succ o ho => have h₄ := ho (n+1) - have h₅ : n+1+1+o+1 = n+1+(Nat.succ o)+1 := by simp_arith - rewrite[h₅] at h₄ - have h₆ : n + 1 + o + 1 + 1 = n + (Nat.succ o + 1 + 1) := by simp_arith - rewrite[h₆] at h₄ + have h₅ : n + 1 + 1 + o = n + 1 + (Nat.succ o) := by simp_arith + have h₆ : n + 1 + o + 1 = n + (Nat.succ o + 1) := by simp_arith + rewrite[h₅, h₆] at h₄ + revert heap h₁ h₂ h₃ + assumption + +--- Same as rootSeesThroughCast, but in the other direction. +private theorem CompleteTree.rootSeesThroughCast2 + (n m : Nat) + (h₁ : n + m + 1 = n + 1 + m) + (h₂ : 0 < n + m + 1) + (h₃ : 0 < n + 1 + m) + (heap : CompleteTree α (n+m+1)) : (h₁▸heap).root h₃ = heap.root h₂ := by + induction m generalizing n + case zero => simp + case succ mm mh => + have h₄ := mh (n+1) + have h₅ : n + 1 + mm + 1 = n + Nat.succ mm + 1 := by simp_arith + have h₆ : n + 1 + 1 + mm = n + 1 + Nat.succ mm := by simp_arith + rw[h₅, h₆] at h₄ revert heap h₁ h₂ h₃ assumption @@ -198,7 +214,7 @@ theorem CompleteTree.heapInsertRootSameOrElem (elem : α) (heap : CompleteTree else by unfold CompleteTree.heapInsert simp[h] - rw[rootSeesThroughCast n m (by simp_arith) (by simp_arith) (by simp_arith)] + rw[rootSeesThroughCast n (m+1) (by simp_arith) (by simp_arith) (by simp_arith)] cases (lt elem v) <;> simp[instDecidableEqBool, Bool.decEq, CompleteTree.root] @@ -467,8 +483,33 @@ theorem CompleteTree.popLastLeaf (heap : CompleteTree α 1) : heap.popLast.snd = | .leaf => rfl exact h₁ -theorem CompleteTree.popLastLeavesRoot (heap : CompleteTree α (n+1+1)) : heap.root (by simp_arith) = heap.popLast.snd.root (by simp_arith) := by - sorry +theorem CompleteTree.popLastLeavesRoot (heap : CompleteTree α (n+1)) (h₁ : n > 0) : heap.root (Nat.zero_lt_of_ne_zero $ Nat.succ_ne_zero n) = heap.popLast.snd.root (h₁) := + match h₂ : n, heap with + | (o+p), .branch v l r _ _ _ => by + have h₃ : (0 ≠ o + p) := Ne.symm $ Nat.not_eq_zero_of_lt h₁ + unfold popLast + simp[h₃] + exact + if h₄ : p < o ∧ Nat.nextPowerOfTwo (p + 1) = p + 1 then by + simp[h₄] + cases o + case zero => exact absurd h₄.left $ Nat.not_lt_zero p + case succ oo _ _ _ => + simp -- redundant, but makes goal easier to read + rw[rootSeesThroughCast2 oo p _ (by simp_arith) _] + unfold root + simp + else by + simp[h₄] + cases p + case zero => + simp_arith at h₁ -- basically o ≠ 0 + simp_arith[h₁] at h₄ -- the second term in h₄ is decidable and True. What remains is ¬(0 < o), or o = 0 + case succ pp hp => + simp_arith + unfold root + simp + theorem CompleteTree.popLastIsHeap {heap : CompleteTree α (o+1)} {le : α → α → Bool} (h₁ : HeapPredicate heap le) (h₂ : transitive_le le) (h₃ : total_le le) : HeapPredicate (heap.popLast.snd) le := match o, heap with @@ -496,8 +537,13 @@ theorem CompleteTree.popLastIsHeap {heap : CompleteTree α (o+1)} {le : α → have h₇ : HeapPredicate .leaf le := by trivial have h₈ : HeapPredicate.leOrLeaf le v .leaf := by trivial exact ⟨h₇,h₁.right.left, h₈, h₁.right.right.right⟩ - case a.succ => -- if ll is not zero, then the root element before and after popLast is the same. - sorry + case a.succ nn => -- if ll is not zero, then the root element before and after popLast is the same. + unfold HeapPredicate at * + simp[h₁.right.left, h₁.right.right.right, popLastIsHeap h₁.left h₂ h₃] + unfold HeapPredicate.leOrLeaf + simp + rw[←(popLastLeavesRoot l (Nat.zero_lt_of_ne_zero $ Nat.succ_ne_zero nn))] + exact h₁.right.right.left else by simp[h₅] sorry |