[WIP] Verification of binary heap

[cmlsharp]

This PR is still a work in progress, but I wanted to get it out there.

This PR begins the process of addressing #1442. Thus far I have managed to prove that heapifyDown, heapifyUp, and mkHeap preserve the binary heap correctness property, These should be the lions share of the difficulty, as the remaining operations are largely wrappers around the former two.

As suggested in that thread, this PR also alters the definition of BinaryHeap to use an Ord instance on the contained type rather than a comparison function. The proofs additionally rely on Std.OrientedOrd and Std.TransOrd.

The core correctness property is encoded as:

@[expose]
public def WF.children [Ord α] (a : Vector α sz) (i : Fin sz) : Prop :=
  let left := 2 * i.val + 1
  let right := left + 1
  (∀ _ : left < sz, compare a[i] a[left] |>.isGE) ∧
  (∀ _ : right < sz, compare a[i] a[right] |>.isGE)


@[expose]
public def WF [Ord α] (v : Vector α sz) : Prop :=
  ∀ i : Fin sz, WF.children v i

However, for proving heapifyUp it was more convenient to use a "bottom up" version of a correctness property

def WF.parent [Ord α] (a : Vector α sz) (i : Fin sz) : Prop :=
  ∀ _ : 0 < i.val, compare a[i] a[(i.val - 1)/2] |>.isLE
  
def WF.bottomUp [Ord α] (v : Vector α sz) : Prop :=
  ∀ i : Fin sz, WF.parent v i

I provide a theorem that WF is equivalent to WF.bottomUp.

[cmlsharp]

WIP

[cmlsharp]

(I will say, I'm currently overusing grind so compilation is slow at the moment)

[fgdorais]

Please merge main to clarify API changes.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❌ Mathlib branch batteries-pr-testing-1602 built against this PR, but testing failed. (2026-01-07 04:13:07) View Log

[cmlsharp]

awaiting-review

[cmlsharp]

Summary of changes:

• Modified the BinaryHeap interface to use an Ord instance rather than a comparison function
• Added an instance of Membership for the binary heap
• Defined well-formedness property and proved that the following operations preserve it: heapifyDown, heapifyUp, mkHeap, Array.toBinaryHeap, Batteries.Vector.toBinaryHeap, popMax, insert, increaseKey, decreaseKey, empty, singleton under the additional assumptions Std.TransOrd and Std.OrientedOrd. Additionally I provide theorems that self.max gives you the maximal element.
• Defined additional theorems relating to membership such as mem_insert and mem_iff_get

There is still more work to do, but this PR is already getting quite large.

Issues with the current PR:

• Some of the definitions in Basic.lean currently need to be tagged with @[expose] because of this issue mentioned in Zulip.
• I do not yet have theorems for insertExtractMax, replaceMax or heapSort. For the former two, to fully prove their spec you might need e.g. a setoid instance, though less ambitious theorems could still be proven about them. The membership lemmas should be useful here.
• Compile times are still slow. I've tried at least replacing all uses of grind with grind only and replacing particularly slow cases with more explicit proofs, but I'd appreciate any additional advice. At a bare minimum it might be good to try to extract a smaller set of useful lemmas that don't depend on the rest of the well-formedness machinery so people can import just those easier lemmas if that's all they need.