Fix Heap Insert preserves Heap Proof. Preconditions were wrong.

And with wrong I mean "unfulfillable if any elements in the heap should
be equal to each other".

I'm still not fully happy with this, as it relies on lt being compatible
with Eq, but yeah, it works for now.

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₉