Data structures

Stream: Program verification

[Michael George]

I am interested in specifying properties of various basic data structures, such as priority queues, sorted enumerations, dictionaries, etc. I see that there are some data structures, such as Std.Data.PairingHeap, Mathlib.Data.BinaryHeap, etc, but as far as I can tell, there are no interfaces defining the expected operations and their behavior. For example, I would imagine something like:

class PollableCollection (α β) extends Collection α β where
    peek  : β → Option α
    poll  : β → Option (α × β)
    empty : β → bool
    ...

    poll_correct (pq : β) : pq = {fst (poll β)} ∪ snd (poll β)
    peek_correct (pq : β) : peek pq = fst (poll pq)
    ...

instance : PollableCollection α (List α)

/- PriorityQueue.lean -/
class PriorityQueue (α β) [PartialOrder α] extends PollableCollection α β where
    peek_minimal (pq : β) : ∀ a ∈ pq, peek pq ≤ a

/- PairingHeap.lean -/
instance [PartialOrder α] : PriorityQueue α (PairingHeap α)

/- BinaryHeap.lean -/
instance [PartialOrder α] : PriorityQueue α (BinomialHeap α)

The details here are off, but the point is that I would like a concise definition of correctness for a priority queue which I could program against.

I'm curious whether such a library exists, or if anyone has suggestions or pointers that would be helpful in the design.

[Henrik Böving]

You probably want to talk to the #std4 people about designing practical abstractions for verified data structures.

[Karl Palmskog]

since people translate Coq<->Lean all the time, maybe this is of interest:

• https://softwarefoundations.cis.upenn.edu/vfa-current/Priqueue.html
• https://github.com/clayrat/fav-ssr/blob/trunk/src/priority.v

[Mario Carneiro]

I've been trying to follow the model of the rust standard library where the data structures have a lot of operations and proved properties but it is relatively light on unifying abstractions (traits / typeclasses) over them. It should be relatively simple for a third party library like @James Gallicchio 's LeanColls to add such a typeclass and wrap all existing relevant data structures with the operations and laws.

[Martin Dvořák]

Karl Palmskog said:

since people translate Coq<->Lean all the time, maybe this is of interest:

• https://softwarefoundations.cis.upenn.edu/vfa-current/Priqueue.html
• https://github.com/clayrat/fav-ssr/blob/trunk/src/priority.v

Do people really translate stuff between Coq and Lean on daily basis?

[Karl Palmskog]

I was thinking of examples like https://github.com/kaicho8636/GeoLean and https://github.com/uncomputable/natural-number-game

[Karl Palmskog]

and not least https://coq.discourse.group/t/alpha-announcement-coq-is-a-lean-typechecker/581