Commit 2021-12-16 18:00 6276f24a

View on Github →

feat: binary heaps (#136) 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.

Estimated changes

added def Array.heapSort
added def BinaryHeap.empty
added def BinaryHeap.max
added def BinaryHeap.size
added theorem BinaryHeap.size_insert
added theorem BinaryHeap.size_mkHeap
added theorem BinaryHeap.size_popMax
added structure BinaryHeap
modified theorem Fin.add_def
modified theorem Fin.checked_add_spec
modified theorem Fin.checked_mul_spec
modified theorem Fin.checked_sub_spec
added theorem Fin.gt_wf
modified theorem Fin.mod_def
modified theorem Fin.modn_def
modified theorem Fin.mul_def
deleted theorem Fin.one_def:
added theorem Fin.one_def
modified theorem Fin.sub_def
added def Fin.upRel
added def Nat.upRel