Binomial trees

Stream: general

[Sebastian Zivota]

A binomial tree of order n has a root element and n subtrees of orders n-1, …, 0. I'm struggling with how to model this type in Lean. To begin with, should the type be indexed by the order? The point of binomial trees is to make binomial heaps, which contain trees of arbitrary orders, so I was working under the assumption that it would be more convenient if the order were not part of the type. This leads me to want to express the list of subtrees as

def subTrees (α : Type) : Type :=
  { ts : List (Tree α) // subTreeProp Tree.order ts }

def subTreeProp (f : α -> Nat) (ts : List α) : Prop :=
  ∀ i, f (ts.get i) = ts.length - i - 1

(subTreeProp is indexed by a function to make it easier to play around with before actually defining binomial trees)
But this way even simple, concrete cases of subTreeProp aren't provable automatically (i.e. by simp or similar). I think the universal quantifier
over Fin (List.length ts) presents a difficulty here.

Should I formulate the property differently? Should I create a bespoke type for the list of subtrees of a tree instead of using a subtype?

[Shreyas Srinivas]

You'll find an isabelle version in chapter 16 of functional algorithms verified : https://functional-algorithms-verified.org/functional_data_structures_algorithms.pdf

[Shreyas Srinivas]

Subtypes in general have two annoyances:

1. You can't pattern match on them.
2. You have to redefine induction principles on them because proofs are not carried over or some such thing. For an example see PNat. To do proofs by induction, it might be useful to define your tree type inductively. At least that is what I find convenient.

[Jannis Limperg]

Std has this for Lean 4: docs4#Std.BinomialHeapImp.HeapNode. There's probably also a Lean 3 version in mathlib.

[Sebastian Zivota]

Oh, it didn't even occur to me to check if it already existed. Thanks, that's very helpful!

[Mario Carneiro]

There's probably also a Lean 3 version in mathlib.

Nope, this is a lean 4 original