diff options
| -rw-r--r-- | Common/BinaryHeap.lean | 77 |
1 files changed, 59 insertions, 18 deletions
diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean index 143b47b..324a3d6 100644 --- a/Common/BinaryHeap.lean +++ b/Common/BinaryHeap.lean @@ -16,9 +16,10 @@ inductive CompleteTree (α : Type u) : Nat → Type u def CompleteTree.root (tree : CompleteTree α n) (_ : 0 < n) : α := match tree with | .branch a _ _ _ _ _ => a -structure WellDefinedLt (lt : α → α → Bool) : Prop where - antisymm : ∀ (a b : α), lt a b ↔ ¬lt b a +structure TotalOrder (lt : α → α → Bool) : Prop where + asymmetric : ∀ (a b : α), lt a b → ¬lt b a transitive : ∀ (a b c : α), lt a b ∧ lt b c → lt a c + connected : ∀ (a b : α), a = b ∨ lt a b ∨ lt b a -- equivalently: a ≠ b → lt a b ∨ lt b a def HeapPredicate {α : Type u} {n : Nat} (heap : CompleteTree α n) (lt : α → α → Bool) : Prop := match heap with @@ -32,7 +33,42 @@ def HeapPredicate {α : Type u} {n : Nat} (heap : CompleteTree α n) (lt : α structure BinaryHeap (α : Type u) (lt : α → α → Bool) (n : Nat) where tree : CompleteTree α n valid : HeapPredicate tree lt - wellDefinedLt : WellDefinedLt lt + wellDefinedLt : TotalOrder lt + +theorem TotalOrder.irreflexive (a : α) {lt : α → α → Bool} (h₁ : TotalOrder lt) : lt a a = false := + if hc : lt a a = true then by + simp[h₁.asymmetric a a hc] + else by + simp[hc] + +theorem TotalOrder.not_lt_eq_or_lt {lt : α → α → Bool} (h₁ : TotalOrder lt) (h₂ : ¬lt a b) : a = b ∨ lt b a := by + have h₃ := h₁.connected a b + simp[h₂] at h₃ + assumption + +theorem TotalOrder.not_lt_trans {lt : α → α → Bool} (h₁ : TotalOrder lt) : ∀ (a b c : α), ¬lt a b ∧ ¬lt b c → ¬lt a c := by + intros a b c h₂ + have h₃ := h₁.asymmetric + have h₄ := h₁.transitive + have h₆ := not_lt_eq_or_lt h₁ h₂.left + have h₇ := not_lt_eq_or_lt h₁ h₂.right + cases h₆ + case inl h₈ => + cases h₇ + case inl h₉ => + have h₁₀ : a = c := h₈.substr h₉ + simp[h₁₀] + exact (h₁.irreflexive c) + case inr h₉ => + apply h₃ + simp[*] + case inr h₈ => + cases h₇ + case inl h₉ => + apply h₃ + simp[←h₉,h₈] + case inr h₉ => + exact h₃ c a $ h₄ c b a ⟨h₉, h₈⟩ /--Please do not use this for anything meaningful. It's a debug function, with horrible performance.-/ instance {α : Type u} [ToString α] : ToString (CompleteTree α n) where @@ -201,18 +237,19 @@ theorem CompleteTree.heapInsertEmptyElem (elem : α) (heap : CompleteTree α o) match o, heap with | 0, .leaf => by simp[CompleteTree.heapInsert, root] -private theorem HeapPredicate.notSmallerOrLeaf_transitive (h₁ : WellDefinedLt lt) : lt a b → HeapPredicate.notSmallerOrLeaf lt b h → HeapPredicate.notSmallerOrLeaf lt a h := by - have h₂ := h₁.antisymm - have h₁ := h₁.transitive + +private theorem HeapPredicate.notSmallerOrLeaf_transitive (h₁ : TotalOrder lt) : lt a b → HeapPredicate.notSmallerOrLeaf lt b h → HeapPredicate.notSmallerOrLeaf lt a h := by + have h₂ := h₁.asymmetric + have h₁ := h₁.not_lt_trans unfold notSmallerOrLeaf rename_i n _ cases n <;> simp rename_i n simp at h₂ intros h₃ h₄ - rw[←h₂] at * - have h₅ := h₁ a b (h.root (by simp_arith)) - exact h₅ ⟨h₃, h₄⟩ + have h₅ := h₂ a b h₃ + simp at * + exact h₁ _ _ _ ⟨h₄, h₅⟩ private theorem HeapPredicate.seesThroughCast (n m : Nat) @@ -234,7 +271,7 @@ private theorem HeapPredicate.seesThroughCast revert heap h₁ h₂ h₃ assumption -theorem CompleteTree.heapInsertIsHeap {elem : α} {heap : CompleteTree α o} {lt : α → α → Bool} (h₁ : HeapPredicate heap lt) (h₂ : WellDefinedLt lt) : HeapPredicate (heap.heapInsert lt elem) lt := +theorem CompleteTree.heapInsertIsHeap {elem : α} {heap : CompleteTree α o} {lt : α → α → Bool} (h₁ : HeapPredicate heap lt) (h₂ : TotalOrder lt) : HeapPredicate (heap.heapInsert lt elem) lt := match o, heap with | 0, .leaf => by trivial | (n+m+1), .branch v l r m_le_n _ _ => @@ -248,22 +285,24 @@ theorem CompleteTree.heapInsertIsHeap {elem : α} {heap : CompleteTree α o} {lt have h₅ : (HeapPredicate (CompleteTree.heapInsert lt v r) lt) := CompleteTree.heapInsertIsHeap h₁.right.left h₂ simp[h₁, h₅] simp[HeapPredicate.notSmallerOrLeaf_transitive h₂ h₄ h₁.right.right.left] - have h₇ := h₂.antisymm + have h₇ := h₂.asymmetric simp at h₇ cases m case zero => have h₆ := heapInsertEmptyElem v r lt (by simp_arith) simp[HeapPredicate.notSmallerOrLeaf, h₆] - rw[←h₇] + apply h₇ assumption case succ _ => simp[HeapPredicate.notSmallerOrLeaf] cases heapInsertRootSameOrElem v r lt (by simp_arith) <;> rename_i h₆ <;> simp[h₆] - <;> rw[←h₇] + apply h₇ . assumption - apply h₂.transitive (b := v) + have h₈ := h₂.not_lt_trans + simp at h₈ + apply h₈ _ v elem simp[h₄, h₇] have h₉ := h₁.right.right.right unfold HeapPredicate.notSmallerOrLeaf at h₉ @@ -302,22 +341,24 @@ theorem CompleteTree.heapInsertIsHeap {elem : α} {heap : CompleteTree α o} {lt have h₅ : (HeapPredicate (CompleteTree.heapInsert lt v l) lt) := CompleteTree.heapInsertIsHeap h₁.left h₂ simp[h₁, h₅] simp[HeapPredicate.notSmallerOrLeaf_transitive h₂ h₄ h₁.right.right.right] - have h₇ := h₂.antisymm + have h₇ := h₂.asymmetric simp at h₇ cases n case zero => have h₆ := heapInsertEmptyElem v l lt (by simp_arith) simp[HeapPredicate.notSmallerOrLeaf, h₆] - rw[←h₇] + apply h₇ assumption case succ _ => simp[HeapPredicate.notSmallerOrLeaf] cases heapInsertRootSameOrElem v l lt (by simp_arith) <;> rename_i h₆ <;> simp[h₆] - <;> rw[←h₇] + apply h₇ . assumption - apply h₂.transitive (b := v) + have h₈ := h₂.not_lt_trans + simp at h₈ + apply h₈ _ v elem simp[h₄, h₇] have h₉ := h₁.right.right.left unfold HeapPredicate.notSmallerOrLeaf at h₉ |