Verifying BinaryHeap (PR Review)

Stream: batteries

[cmlsharp]

I tried my hand at verifying Batteries.BinaryHeap. The PR is still a work in progress but the biggest pieces are there (heapifyDown, heapifyUp, and mkHeap). Any comments/suggestions/critiques would be greatly appreciated!

batteries#1602

[Kim Morrison]

Can you update to current main? There are downstream users of BinaryHeap, so we'll have to make sure the API change here is viable for them.

[cmlsharp]

I have synced my branch with the current main

[cmlsharp]

As a side note:

The original API functions were not @[expose]. I temporarily marked the whole public section as @[expose] so I could access the definitions in my lemma module. Is there a way to expose definitions but only to some other internal module and not to external users?

[Robin Arnez]

cmlsharp schrieb:

Is there a way to expose definitions but only to some other internal module and not to external users?

import all MyModule imports all private declarations and all declaration bodies. For your lemmas you'll probably need both public import Batteries.Data.BinaryHeap.Basic and import all Batteries.Data.BinaryHeap.Basic.

[Robin Arnez]

And don't forget to put your lemmas into a public section!

[cmlsharp]

Thank you for the tip! I'm experiencing a slightly odd issue when I remove the @[expose] annotations from the BinaryHeap functions and instead use 'import all' in my Lemmas module. This mostly works, but it causes a couple lemmas I'm currently using grind for to fail (separately, I need to be using grind less for performance reasons, but I don't understand why this break happens)

For example.

module
import all Batteries.Data.BinaryHeap.Basic
public import Batteries.Data.BinaryHeap.Basic
-- ...
theorem heapifyDown_preserves_prefix [Ord α] (a : Vector α sz) (i k : Fin sz) (hk : k < i) :
    (heapifyDown a i)[k] = a[k] := by
  induction a, i using heapifyDown.induct <;> grind [heapifyDown]

'heapifyDown.induct' works fine, and I can unfold heapifyDown so the definition is in scope, however I get the following failure from grind

▼ 237:47-237:66: error:
invalid pattern(s) for `heapifyDown.match_1.congr_eq_2`
  [@Batteries.BinaryHeap.heapifyDown.match_1✝ #6 #5 #4 #3 #2]
the following theorem parameters cannot be instantiated:
  j : Fin sz
  heq_1 : x✝ = some j

This is resolved by marking heapifyDown as @[expose] (this is the state of the repo at present)

[Kim Morrison]

It would be super helpful if you could produce a standalone example of this (i.e. something where you use import all and public import, but grind fails unless you add @[expose] to a definition in the imported file), so we can diganose.

[cmlsharp]

Ok, I will try to come up with a minimal example

[Notification Bot]

A message was moved from this topic to #batteries > Strange 'import all' bug by cmlsharp.

[cmlsharp]

Update: I was able to prove that Array.heapSort is a sorted permutation of the original array. I think modulo the aforementioned bug requiring some definitions (specifically heapifyDown) to be exposed that oughtn't the main set of lemmas one would want to have about a binary heap are there.