Verify Binary Heap

[fgdorais]

This is a standard textbook algorithm. It is well implemented in Batteries.Data.BinaryHeap but not verified.

If you're looking to get started with formal verification project in Lean, this should be an interesting one to try!

[linesthatinterlace]

I think I know what you want here, but I think a good first step would be to work out what proofs are actually wanted.

[linesthatinterlace]

Also, should BinaryHeap use a typeclass rather than taking an explicit comparator function?

[fgdorais]

Yes, this is also needed. It's a common pattern in Batteries to provide a bare-bones and therefore highly flexible implementation, with the expectation that users will use this as part of the internal state of a more sophisticated API. In this case, at least two basic examples for min-heap and max-heap should be provided (using LE/LT or Ord classes, for example).

[fgdorais]

I think I know what you want here, but I think a good first step would be to work out what proofs are actually wanted.

The basic theorems needed are that the functions provided preserve the max-heap property for the provided relation. The difficulty is that the proofs should ideally make minimal use of the expected properties of the relation.

[cmlsharp]

I started some initial work on this. It's not nearly ready for a PR, but I have managed to verify the basic heap preserving properties of heapifyDown and mkHeap.

The well-formedness properties I'm currently using are:

/-- Checks if the node at index `i` satisfies the max-heap property with respect to its children. -/
-- Not sure if defining this inductively would simplify things or not
-- I do later inductively define a 'inSubtree' relation, maybe these could be merged?
def WF.at [Ord α] (a : Vector α sz) (i : Fin sz) : Prop :=
  let left := 2 * i.val + 1
  let right := left + 1
  (∀ hleft : left < sz, compare a[i] a[left] |>.isGE) ∧
  (∀ hright : right < sz, compare a[i] a[right] |>.isGE)

/-- All indices greater than i are well-formed nodes -/
def WF.below [Ord α] (a : Vector α sz) (i : Nat) : Prop
  := ∀ j : Fin sz, i < j.val → WF.at a j

/-- A vector satisfies the max-heap property. -/
def WF [Ord α] (v : Vector α sz) : Prop
  := ∀ i : Fin sz, WF.at v i

and then I prove

theorem heapifyDown_wf [Ord α] [Std.TransOrd α] [Std.OrientedOrd α] [Std.ReflOrd α] 
    {a : Vector α sz} {i : Fin sz}
    (hbelow : WF.below a i)
  : WF.at (heapifyDown a i) i ∧ WF.below (heapifyDown a i) i

theorem mkHeap_wf [Ord α] [Std.TransOrd α] [Std.OrientedOrd α] [Std.ReflOrd α]
    (a : Vector α sz)
  : WF (mkHeap a)

Maybe there's a way to weaken the requirements on the Ord instance, but I don't see how.

(As part of this, I changed the BinomialHeap interface to take an Ord instance rather than a comparison function, but that's not strictly necessary)

Progress here: https://github.com/cmlsharp/batteries/blob/binomial_heap/Batteries/Data/BinaryHeap/Lemmas.lean