Leftist heaps as indexed data types in Agda

LeftistHeap.agda

{-# OPTIONS --postfix-projections #-}
{-# OPTIONS --termination-depth=2 #-}

-- Leftist heaps (Knuth 1973).
-- An implementation of priority queues.

-- Tested with Agda v2.6.2 and agda-stdlib v1.7.

-- The module is parametrized over the type of the elements
-- stored in the heap.  These elements need to be totally ordered,
-- otherwise the concept of a priority queue does not make sense
-- for them.

open import Level using () renaming (zero to lzero)
open import Relation.Binary.Bundles using (DecTotalOrder)

module LeftistHeap (O : DecTotalOrder lzero lzero lzero) where

-- We create a module for record O (with the same name, O).
-- This allows us to use the content of O conveniently
-- when constructing new records.

module O = DecTotalOrder O
open O
  using    (_≤_; total)
  renaming (Carrier to A)

-- Imports

open import Data.Unit.Polymorphic using (⊤)
open import Data.Sum              using (inj₁; inj₂)
open import Data.Product          using (∃; ∃₂; _,_)
open import Data.Maybe            using (Maybe; nothing; just)

open import Data.Nat.Base using (ℕ; zero; suc; _⊓_) hiding (module ℕ)
module ℕ where
  open import Data.Nat.Base public
  open import Data.Nat.Properties public

open import Function using (case_of_)

open import Relation.Binary.Lattice.Definitions using (Infimum)
open import Relation.Binary.Lattice.Bundles     using (MeetSemilattice)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; subst; cong)

-- Minimum operation
------------------------------------------------------------------------

-- Variables x and y range over elements of A.

variable
  x x' x₁ x₂ : A
  y y' y₁ y₂ : A

-- Infimum from decidable total order on A.
-- Why is this not in the standard library?  Or where is it?

min : A → A → A
min x y = case total x y of λ where
  (inj₁ x≤y) → x
  (inj₂ y≤x) → y

infimum : Infimum _≤_ min
infimum x y with total x y
... | inj₁ x≤y = O.refl , x≤y , λ _ z≤x _ → z≤x
... | inj₂ y≤x = y≤x , O.refl , λ _ _ z≤y → z≤y

meetSemilattice : MeetSemilattice _ _ _
meetSemilattice = record
  { O
  ; _∧_ = min
  ; isMeetSemilattice = record { O ; infimum = infimum }
  }

------------------------------------------------------------------------

-- Adding a top element to A

A∞ = Maybe A
pattern ∞ = nothing

-- Variables a and b range over elements of A∞

variable
  a a' a₁ a₂ : A∞
  b b' b₁ b₂ : A∞

-- A∞ is a bounded inf-semilattice.

_≤∞_ : A → A∞ → Set _
x ≤∞ ∞ = ⊤
x ≤∞ just y = x ≤ y

min∞ : A∞ → A∞ → A∞
min∞ ∞ b = b
min∞ (just x) ∞ = just x
min∞ (just x) (just y) = just (min x y)

lb∞ : x ≤∞ a₁ → x ≤∞ a₂ → x ≤∞ min∞ a₁ a₂
lb∞ {a₁ = just x} {a₂ = just y} p q = let _ , _ , H = infimum x y in H _ p q
lb∞ {a₁ = just x} {a₂ = ∞}      p q = p
lb∞ {a₁ = ∞}      {a₂ = just y} p q = q
lb∞ {a₁ = ∞}      {a₂ = ∞}      p q = _

------------------------------------------------------------------------

-- Let variable k range over ranks.

variable
  k k' k₁ k₂ : ℕ

-- Leftist heaps with static invariants.
--
-- * Heap invariant: root is smallest element, for each subtree
-- * Rank is depth of rightmost element.
-- * Right subtree never has higher rank than left subtree.

data LHeap : (min : A∞) (rank : ℕ) → Set where
  empty : LHeap ∞ 0
  node  : (x : A) (h₁ : LHeap a₁ k₁) (h₂ : LHeap a₂ k₂)
        → (x≤a₁ : x ≤∞ a₁) (x≤a₂ : x ≤∞ a₂) (k₂≤k₁ : k₂ ℕ.≤ k₁)
        → LHeap (just x) (suc k₂)

-- Singleton heap

sg : (x : A) → LHeap (just x) 1
sg x = node x empty empty _ _ ℕ.≤-refl

-- Smart version of node constructor that establishes the rank invariant.

mkNode :
  (x : A) (h₁ : LHeap a₁ k₁) (h₂ : LHeap a₂ k₂)
  (x≤a₁ : x ≤∞ a₁) (x≤a₂ : x ≤∞ a₂)
  → LHeap (just x) (suc (k₁ ⊓ k₂))
mkNode {k₁ = k₁} {k₂ = k₂} x h₁ h₂ x≤a₁ x≤a₂ with ℕ.≤-total k₁ k₂
... | inj₁ k₁≤k₂ = subst (LHeap _) (cong suc (≡.sym (ℕ.m≤n⇒m⊓n≡m k₁≤k₂))) (node x h₂ h₁ x≤a₂ x≤a₁ k₁≤k₂)
... | inj₂ k₂≤k₁ = subst (LHeap _) (cong suc (≡.sym (ℕ.m≥n⇒m⊓n≡n k₂≤k₁))) (node x h₁ h₂ x≤a₁ x≤a₂ k₂≤k₁)

-- Merging heaps.

-- Because of `with', this mutual definition needs termination depth 2.
mutual

  -- Merging two leftist heaps.
  -- Returns also the rank of the result heap, which depends on the decisions taken during merge.

  merge : LHeap a₁ k₁ → LHeap a₂ k₂ → ∃ λ k → LHeap (min∞ a₁ a₂) k
  merge {k₂ = k} empty h                    = k , h
  merge {k₁ = k} h@(node _ _ _ _ _ _) empty = k , h
  merge h₁@(node x₁ _ _ _ _ _) h₂@(node x₂ _ _ _ _ _) with total x₁ x₂
  ... | inj₁ x₁≤x₂ = merge' x₁≤x₂ h₁ h₂
  ... | inj₂ x₂≤x₁ = merge' x₂≤x₁ h₂ h₁
    -- N.B.: We cannot simply replace the `with' by `case'.

  -- Merging the second heap into the right subheap of the first.

  merge' : x₁ ≤ x₂ → LHeap (just x₁) k₁ → LHeap (just x₂) k₂ → ∃ λ k → LHeap (just x₁) k
  merge' x₁≤x₂ (node {k₁ = k₁} {a₂ = a₂} x₁ l₁ r₁ x₁≤l₁ x₁≤r₁ _) h =
    let k , h' = merge r₁ h
    in  suc (k₁ ⊓ k) , mkNode x₁ l₁ h' x₁≤l₁ (lb∞ {a₁ = a₂} x₁≤r₁ x₁≤x₂)
    -- Goal: x₁ ≤∞ min∞ a₂ (just x₂)
    --  x₁ ≤ x₂
    --  x₁ ≤∞ a₂

-- Other heap operations
------------------------------------------------------------------------

-- Insert an element.

insert : ∀ x → LHeap a k → ∃ (LHeap (min∞ (just x) a))
insert x h = merge (sg x) h

-- Delete the root.

deleteMin : LHeap (just x) k → ∃₂ LHeap
deleteMin (node {a₁ = a₁} {a₂ = a₂} _ l r _ _ _) = min∞ a₁ a₂ , merge l r