[Merged by Bors] - feat: binary heaps

[digama0]

The main addition is a type BinaryHeap α lt of binary max-heaps stored in an array.

Also some cleanup:

• Fix line length and formatting in Data.Fin.Basic
• Add Mathlib.Init.WF for some more tools for proving well foundedness
• Use termination_by instead of manual termination compilation for String.toAsciiByteArray and ByteSlice.forIn

I originally wrote heapifyDown et al without the embedded postcondition, but proving facts about definitions like heapifyDown is incredibly painful right now.

[gebner]

Should these maybe be in the WellFoundedRelation namespace?

And aren't these in Init.WF already?

[digama0]

They are annoying to use if they are namespaced. Hopefully leanprover/lean4#879 will be handled at some point, which will make this unnecessary in most cases.

There is a similar definition in Init.WF, but it is nondependent. Here the idea is to introduce the parameter to skip as a variable in the context so it can be used in later relations (e.g. in Fin.upRel).

[gebner]

They are annoying to use if they are namespaced.

Really? open PSigma works just fine (for the core function). (I completely agree that leanprover/lean4#849 is the proper fix here though.)

There is a similar definition in Init.WF, but it is nondependent.

I am not sure if this makes it better; we now have two functions with the same name, same purpose, but different types. At least a prime would be good here for disambiguation.

[digama0]

It wouldn't be good to have open PSigma at the top level because the user probably isn't doing anything related to PSigma except for the specification of the well founded relation (they didn't ask for it, it is just how the compilation works). If we really want to put these in the PSigma namespace then termination_by should automatically open this namespace (or perhaps some other namespace dedicated to termination relations), because it is so different from everything else in the user's file.

[gebner]

Here's a simpler termination argument:

/-- Core operation for binary heaps, expressed directly on arrays.
Given an array which is a max-heap, push item `i` down to restore the max-heap property. -/
def heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
  {a' : Array α // a'.size = a.size} :=
  let left := 2 * i.1 + 1
  let right := left + 1
  have left_le : i ≤ left := Nat.le_trans
    (by rw [Nat.succ_mul, Nat.one_mul]; exact Nat.le_add_left i i)
    (Nat.le_add_right ..)
  have right_le : i ≤ right := Nat.le_trans left_le (Nat.le_add_right ..)
  have i_le : i ≤ i := Nat.le_refl _
  have j : {j : Fin a.size // i ≤ j} := if h : left < a.size then
    if lt (a.get i) (a.get ⟨left, h⟩) then ⟨⟨left, h⟩, left_le⟩ else ⟨i, i_le⟩ else ⟨i, i_le⟩
  have j := if h : right < a.size then
    if lt (a.get j) (a.get ⟨right, h⟩) then ⟨⟨right, h⟩, right_le⟩ else j else j
  if h : i.1 = j then ⟨a, rfl⟩ else
    let a' := a.swap i j
    let j' := ⟨j, by rw [a.size_swap i j]; exact j.1.2⟩
    have : a.size - j < a.size - i :=
      Nat.sub_lt_sub_left i.2 <| Nat.lt_of_le_and_ne j.2 h
    let ⟨a₂, h₂⟩ := heapifyDown lt a' j'
    ⟨a₂, h₂.trans (a.size_swap i j)⟩
termination_by measure fun ⟨α, lt, a, i⟩ => a.size - i
decreasing_by simp [measure, invImage, InvImage]; assumption

BTW, instead of Fin.upRel I think it would be more ergonomic to talk about -i and use the standard order. (alas, this doesn't work directly because you then have two versions of -: one in Fin a.size and one in Fin a'.size...)

[digama0]

The whole point of Nat.upRel and Fin.upRel is so that you don't have to do this a - x < a - y argument all the time. I think we should try to make this kind of proof more ergonomic, there is no reason to always be doing downward induction. I'm not too happy with the skipLeft stuff, I think more should be automated than currently, but I do think that the original proof is in the right direction.

[gebner]

Personally I find the measure version much easier to read compared to explicitly specifying the relations. Although ideally measure would accept functions into any well-ordered type. Then you could write measure fun ⟨α, lt, a, i⟩ => (⟨a.size, -i⟩ : (n : ℕ) ×' Fin n) or measure fun ⟨α, lt, a, i⟩ => (⟨a.size, i⟩ : (n : ℕ) ×' OrderDual (Fin n)). The OrderDual version also works for any finite type, not just Fin n.

[gebner]

I originally wrote heapifyDown et al without the embedded postcondition, but proving facts about definitions like heapifyDown is incredibly painful right now.

This is true, as far as I can tell Lean doesn't even generate an equational lemma for WF definitions at the moment. And if you make one yourself you still need to deal with the huge if-then-else soup and use well-founded induction.

[gebner]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build