Skip to content

Instantly share code, notes, and snippets.

@josh-hs-ko

josh-hs-ko/BinomialHeap.agda

Last active August 29, 2015 14:04
Show Gist options
  • Save josh-hs-ko/39ccd95af603d628b56b to your computer and use it in GitHub Desktop.
Save josh-hs-ko/39ccd95af603d628b56b to your computer and use it in GitHub Desktop.
Download ZIP
Insertion and extraction in coherence with increment and decrement, and minimum extraction (proved correct, of course).
Raw
BinomialHeap.agda
open import Data.Sum
module BinomialHeap (V : Set)
(_≤_ : V → V → Set) (≤-refl : {x : V} → x ≤ x) (≤-trans : {x y z : V} → x ≤ y → y ≤ z → x ≤ z)
(_≤?_ : (x y : V) → x ≤ y ⊎ y ≤ x) where
open import Level using (Level; _⊔_)
open import Function
open import Data.Empty
open import Data.Unit
open import Data.Bool using (Bool; false; true)
open import Data.Maybe renaming (map to mapMaybe)
open import Data.Product renaming (map to _**_; <_,_> to split)
open import Data.Nat using (ℕ; zero; suc)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality using (_≅_; ≅-to-≡; ≡-to-≅; ≡-subst-removable)
renaming (refl to hrefl; sym to fsym; trans to htrans; cong to hcong)
- : {l : Level} {A : Set l} {{_ : A}} → A
- {{a}} = a
-- See Conor McBride's "How to keep your neighbours in order" (ICFP'14)
if_then_else_ : {A B C : Set} → A ⊎ B → ({{_ : A}} → C) → ({{_ : B}} → C) → C
if inj₁ a then t else u = t
if inj₂ b then t else u = u
if-elim : {A B C : Set} (c : A ⊎ B) (ca : {{_ : A}} → C) (cb : {{_ : B}} → C) →
(P : C → Set) → ({{_ : A}} → P ca) → ({{_ : B}} → P cb) → P (if c then ca else cb)
if-elim (inj₁ a) ca cb P pa pb = pa
if-elim (inj₂ b) ca cb P pa pb = pb
pattern <_> b = _ , b
pattern <_>' h = h , _
pattern <_>ʳ h = h , refl
Exists : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
Exists = Σ _
syntax Exists (λ x → P) = ∃[ x ] P
--------
-- binary numbers
data Bin : Set where -- specialisation of List Bool
nul : Bin
zero : Bin → Bin
one : Bin → Bin
incr : Bin → Bin
incr nul = one nul
incr (zero b) = one b
incr (one b) = zero (incr b)
--------
-- binomial trees
_^_ : (ℕ → Set) → ℕ → Set
X ^ zero = ⊤
X ^ (suc n) = X n × (X ^ n)
data BTree : V → ℕ → Set where
node : {x : V} {r : ℕ} (y : V) {{ord : x ≤ y}} (ts : BTree y ^ r) → BTree x r
root : {x : V} {r : ℕ} → BTree x r → V
root (node a ts) = a
link : {x y : V} {r : ℕ} (t : BTree x r) (u : BTree y r) {{leq : root u ≤ root t}} → BTree y (suc r)
link (node a ts) (node b us) = node b (node a ts , us)
link-root : {x y : V} {r : ℕ} (t : BTree x r) (u : BTree y r) {{leq : root u ≤ root t}}
{l : V} → l ≤ root u → l ≤ root (link t u)
link-root (node a ts) (node b us) l≤b = l≤b
attach' : {x y : V} {r : ℕ} → BTree x r → BTree y r → ∃[ z ] BTree z (suc r)
attach' t u = if root t ≤? root u then < link u t > else < link t u >
attach : {x y : V} {r : ℕ} (t : BTree x r) (u : BTree y r) → BTree (proj₁ (attach' t u)) (suc r)
attach t u = proj₂ (attach' t u)
bound-root : {x : V} {r : ℕ} (t : BTree x r) {y : V} → y ≤ x → y ≤ root t
bound-root (node a {{x≤a}} ts) y≤x = ≤-trans y≤x x≤a
attach-root : {x y : V} {r : ℕ} (t : BTree x r) (u : BTree y r)
{l : V} → l ≤ root t → l ≤ root u → l ≤ root (attach t u)
attach-root {x} {y} {r} t u {l} l≤t l≤u =
if-elim {C = ∃[ z ] BTree z (suc r)} (root t ≤? root u) < link u t > < link t u >
(λ v → l ≤ root (proj₂ v)) (link-root u t l≤t) (link-root t u l≤u)
--------
-- binomial heaps
-- ornamentation of Bin
data BHeap : ℕ → Set where
nul : {r : ℕ} → BHeap r
zero : {r : ℕ} (h : BHeap (suc r)) → BHeap r
one : {r : ℕ} {x : V} (t : BTree x r) (h : BHeap (suc r)) → BHeap r
-- free
toBin : {r : ℕ} → BHeap r → Bin
toBin nul = nul
toBin (zero h) = zero (toBin h)
toBin (one x h) = one (toBin h)
-- free
data BHeap' : ℕ → Bin → Set where
nul : {r : ℕ} → BHeap' r nul
zero : {r : ℕ} {b : Bin} (h : BHeap' (suc r) b) → BHeap' r (zero b)
one : {r : ℕ} {b : Bin} {x : V} (t : BTree x r) (h : BHeap' (suc r) b) → BHeap' r (one b)
insT' : {x : V} {r : ℕ} {b : Bin} → BTree x r → BHeap' r b → BHeap' r (incr b)
insT' t nul = one t nul
insT' t (zero h) = one t h
insT' t (one u h) = zero (insT' (attach t u) h)
-- free
toBHeap : {r : ℕ} {b : Bin} → BHeap' r b → BHeap r
toBHeap nul = nul
toBHeap (zero h) = zero (toBHeap h)
toBHeap (one t h) = one t (toBHeap h)
-- free
fromBHeap : {r : ℕ} (h : BHeap r) → BHeap' r (toBin h)
fromBHeap nul = nul
fromBHeap (zero h) = zero (fromBHeap h)
fromBHeap (one t h) = one t (fromBHeap h)
-- free
insT : {x : V} {r : ℕ} → BTree x r → BHeap r → BHeap r
insT t h = toBHeap (insT' t (fromBHeap h))
-- free
recomputation : {r : ℕ} {b : Bin} (h : BHeap' r b) → toBin (toBHeap h) ≡ b
recomputation nul = refl
recomputation (zero h) = cong zero (recomputation h)
recomputation (one t h) = cong one (recomputation h)
-- free
incr-insT-coherence : {x : V} {r : ℕ} (t : BTree x r) (h : BHeap r) → toBin (insT t h) ≡ incr (toBin h)
incr-insT-coherence t h = recomputation (insT' t (fromBHeap h))
--------
-- refinements and upgrades
elim-≡ : ∀ {a b} {A : Set a} {x : A} (P : {y : A} → x ≡ y → Set b) → P refl → {y : A} (eq : x ≡ y) → P eq
elim-≡ P p refl = p
record Iso (A B : Set) : Set₁ where
field
to : A → B
from : B → A
from-to-inverse : (x : A) → from (to x) ≡ x
to-from-inverse : (y : B) → to (from y) ≡ y
record Refinement (X Y : Set) : Set₁ where
field
P : X → Set
i : Iso Y (Σ X P)
forget : Y → X
forget = proj₁ ∘ Iso.to i
canonRef : {X Y : Set} → (Y → X) → Refinement X Y
canonRef {X} {Y} f =
record { P = λ x → Σ[ y ∈ Y ] f y ≡ x
; i = record { to = split f (split id (λ _ → refl))
; from = proj₁ ∘ proj₂
; to-from-inverse = λ { (._ , y , refl) → refl }
; from-to-inverse = λ _ → refl } }
prom-change : {X Y : Set} (r s : Refinement X Y) → ((y : Y) → Refinement.forget r y ≡ Refinement.forget s y) →
∀ x → Refinement.P r x → Refinement.P s x
prom-change r s eq x p =
subst (Refinement.P s)
(trans (sym (eq (Iso.from (Refinement.i r) (x , p)))) (cong proj₁ (Iso.to-from-inverse (Refinement.i r) (x , p))))
(proj₂ (Iso.to (Refinement.i s) (Iso.from (Refinement.i r) (x , p))))
prom-inverse : {X Y : Set} (r s : Refinement X Y)
(rseq : (y : Y) → Refinement.forget r y ≡ Refinement.forget s y)
(sreq : (y : Y) → Refinement.forget s y ≡ Refinement.forget r y) →
∀ x (p : Refinement.P r x) → prom-change s r sreq x (prom-change r s rseq x p) ≡ p
prom-inverse r s rseq sreq x p =
let xp = (x , subst (Refinement.P s)
(trans (sym (rseq (Iso.from (Refinement.i r) (x , p))))
(cong proj₁ (Iso.to-from-inverse (Refinement.i r) (x , p))))
(proj₂ (Iso.to (Refinement.i s) (Iso.from (Refinement.i r) (x , p)))))
in ≅-to-≡ (htrans (≡-subst-removable (Refinement.P r)
(trans (sym (sreq (Iso.from (Refinement.i s) xp)))
(cong proj₁ (Iso.to-from-inverse (Refinement.i s) xp)))
(proj₂ (Iso.to (Refinement.i r) (Iso.from (Refinement.i s) xp))))
(elim-≡ (λ {x'} eq' →
proj₂ (Iso.to (Refinement.i r) (Iso.from (Refinement.i s)
(x' , subst (Refinement.P s) eq'
(proj₂ (Iso.to (Refinement.i s) (Iso.from (Refinement.i r) (x , p)))))))
≅ p)
(htrans (hcong (proj₂ ∘ Iso.to (Refinement.i r))
(≡-to-≅ (Iso.from-to-inverse (Refinement.i s) (Iso.from (Refinement.i r) (x , p)))))
(hcong proj₂ (≡-to-≅ (Iso.to-from-inverse (Refinement.i r) (x , p)))))
(trans (sym (rseq (Iso.from (Refinement.i r) (x , p))))
(cong proj₁ (Iso.to-from-inverse (Refinement.i r) (x , p))))))
promIso : {X Y : Set} (r s : Refinement X Y) → ((y : Y) → Refinement.forget r y ≡ Refinement.forget s y) →
∀ x → Iso (Refinement.P r x) (Refinement.P s x)
promIso r s eq x =
record { to = prom-change r s eq x
; from = prom-change s r (sym ∘ eq) x
; to-from-inverse = prom-inverse s r (sym ∘ eq) eq x
; from-to-inverse = prom-inverse r s eq (sym ∘ eq) x }
coherence : {X Y : Set} (r : Refinement X Y) → ∀ x → Iso (Refinement.P r x) (Σ[ y ∈ Y ] Refinement.forget r y ≡ x)
coherence {X} {Y} r = promIso r (canonRef (Refinement.forget r)) (λ _ → refl)
record Upgrade (X Y : Set) : Set₁ where
field
P : X → Set
C : X → Y → Set
u : ∀ x → P x → Y
c : ∀ x → (p : P x) → C x (u x p)
toUpgrade : ∀ {X Y} → Refinement X Y → Upgrade X Y
toUpgrade r = record { P = Refinement.P r
; C = λ x y → Refinement.forget r y ≡ x
; u = λ x → proj₁ ∘ Iso.to (coherence r x)
; c = λ x → proj₂ ∘ Iso.to (coherence r x) }
_⇀_ : {X Y Z W : Set} → Refinement X Y → Upgrade Z W → Upgrade (X → Z) (Y → W)
r ⇀ s = record { P = λ f → ∀ x → (p : Refinement.P r x) → Upgrade.P s (f x)
; C = λ f g → ∀ x y → Upgrade.C (toUpgrade r) x y → Upgrade.C s (f x) (g y)
; u = λ f h → Upgrade.u s _ ∘ uncurry h ∘ Iso.to (Refinement.i r)
; c = λ { f h ._ y refl → let xp = (Iso.to (Refinement.i r) y)
in Upgrade.c s (f (proj₁ xp)) (uncurry h xp) } }
infixr 2 _⇀_
new : {X : Set} (I : Set) {Y : I → Set} → (∀ i → Upgrade X (Y i)) → Upgrade X ((i : I) → Y i)
new I r = record { P = λ x → ∀ i → Upgrade.P (r i) x
; C = λ x y → ∀ i → Upgrade.C (r i) x (y i)
; u = λ x p i → Upgrade.u (r i) x (p i)
; c = λ x p i → Upgrade.c (r i) x (p i) }
syntax new I (λ i → r) = ∀⁺[ i ∈ I ] r
new' : {X : Set} (I : Set) {Y : I → Set} → (∀ i → Upgrade X (Y i)) → Upgrade X ({i : I} → Y i)
new' I r = record { P = λ x → ∀ {i} → Upgrade.P (r i) x
; C = λ x y → ∀ {i} → Upgrade.C (r i) x (y {i})
; u = λ x p {i} → Upgrade.u (r i) x (p {i})
; c = λ x p {i} → Upgrade.c (r i) x (p {i}) }
syntax new' I (λ i → r) = ∀⁺[[ i ∈ I ]] r
fixed : (I : Set) {X : I → Set} {Y : I → Set} → (∀ i → Upgrade (X i) (Y i)) → Upgrade ((i : I) → X i) ((i : I) → Y i)
fixed I u = record { P = λ f → ∀ i → Upgrade.P (u i) (f i)
; C = λ f g → ∀ i → Upgrade.C (u i) (f i) (g i)
; u = λ f h i → Upgrade.u (u i) (f i) (h i)
; c = λ f h i → Upgrade.c (u i) (f i) (h i) }
syntax fixed I (λ i → u) = ∀[ i ∈ I ] u
fixed' : (I : Set) {X : I → Set} {Y : I → Set} → (∀ i → Upgrade (X i) (Y i)) → Upgrade ({i : I} → X i) ({i : I} → Y i)
fixed' I u = record { P = λ f → ∀ {i} → Upgrade.P (u i) (f {i})
; C = λ f g → ∀ {i} → Upgrade.C (u i) (f {i}) (g {i})
; u = λ f h {i} → Upgrade.u (u i) (f {i}) (h {i})
; c = λ f h {i} → Upgrade.c (u i) (f {i}) (h {i}) }
syntax fixed' I (λ i → u) = ∀[[ i ∈ I ]] u
fixed'' : (I : Set) {X : I → Set} {Y : I → Set} → (∀ i → Upgrade (X i) (Y i)) → Upgrade ((i : I) → X i) ({i : I} → Y i)
fixed'' I u = record { P = λ f → (i : I) → Upgrade.P (u i) (f i)
; C = λ f g → (i : I) → Upgrade.C (u i) (f i) (g {i})
; u = λ f h {i} → Upgrade.u (u i) (f i) (h i)
; c = λ f h i → Upgrade.c (u i) (f i) (h i) }
record FUpgrade (X Y : Set) : Set₁ where
field
P : X → Set
forget : Y → X
u : ∀ x → P x → Y
c : ∀ x → (p : P x) → forget (u x p) ≡ x
fromFUpgrade : {X Y : Set} → FUpgrade X Y → Upgrade X Y
fromFUpgrade fupg = record
{ P = FUpgrade.P fupg
; C = λ x y → FUpgrade.forget fupg y ≡ x
; u = FUpgrade.u fupg
; c = FUpgrade.c fupg }
toFUpgrade : {X Y : Set} → Refinement X Y → FUpgrade X Y
toFUpgrade ref = record
{ P = Refinement.P ref
; forget = Refinement.forget ref
; u = curry (Iso.from (Refinement.i ref))
; c = curry (cong proj₁ ∘ Iso.to-from-inverse (Refinement.i ref)) }
_⁺×_ : (X : Set) {Y Z : Set} → FUpgrade Y Z → FUpgrade Y (X × Z)
X ⁺× fupg = record { P = λ y → X × FUpgrade.P fupg y
; forget = FUpgrade.forget fupg ∘ proj₂
; u = λ { y (x , p) → x , FUpgrade.u fupg y p }
; c = λ { y (x , p) → FUpgrade.c fupg y p } }
--------
-- refinement from Bin to BHeap
toBHeap-fromBHeap-inverse : {r : ℕ} (h : BHeap r) → toBHeap (fromBHeap h) ≡ h
toBHeap-fromBHeap-inverse nul = refl
toBHeap-fromBHeap-inverse (zero h) = cong zero (toBHeap-fromBHeap-inverse h)
toBHeap-fromBHeap-inverse (one t h) = cong (one t) (toBHeap-fromBHeap-inverse h)
fromBHeap-toBHeap-inverse :
{r : ℕ} (b : Bin) (h' : BHeap' r b) →
let h = toBHeap h' in (toBin h , fromBHeap h) ≡ (Σ Bin (BHeap' r) ∋ b , h')
fromBHeap-toBHeap-inverse nul nul = refl
fromBHeap-toBHeap-inverse (zero b) (zero h') = cong (zero ** zero) (fromBHeap-toBHeap-inverse b h')
fromBHeap-toBHeap-inverse (one b) (one t h') = cong (one ** one t) (fromBHeap-toBHeap-inverse b h')
Bin-BHeap : (r : ℕ) → Refinement Bin (BHeap r)
Bin-BHeap r = record
{ P = BHeap' r
; i = record { to = split toBin fromBHeap
; from = toBHeap ∘ proj₂
; from-to-inverse = toBHeap-fromBHeap-inverse
; to-from-inverse = uncurry fromBHeap-toBHeap-inverse } }
--------
-- decrement and extraction
decr : Bin → Maybe Bin
decr nul = nothing
decr (zero b) = mapMaybe one (decr b)
decr (one b) = just (zero b)
data Maybe' {A : Set} (B : A → Set) : Maybe A → Set where
nothing : Maybe' B nothing
just : {a : A} (b : B a) → Maybe' B (just a)
toMaybe : {A : Set} {B : A → Set} {ma : Maybe A} → Maybe' B ma → Maybe (Σ A B)
toMaybe nothing = nothing
toMaybe (just b) = just < b >
mapMaybe' : {A B : Set} {C : A → Set} {D : B → Set} {f : A → B} → ({a : A} → C a → D (f a)) →
{ma : Maybe A} → Maybe' C ma → Maybe' D (mapMaybe f ma)
mapMaybe' f' nothing = nothing
mapMaybe' f' (just c) = just (f' c)
maybeFU : {A B : Set} → FUpgrade A B → FUpgrade (Maybe A) (Maybe B)
maybeFU {A} {B} fupg = record
{ P = Maybe' (FUpgrade.P fupg)
; forget = mapMaybe (FUpgrade.forget fupg)
; u = λ _ → mapMaybe proj₂ ∘ toMaybe ∘ mapMaybe' {f = id} (λ {a} → FUpgrade.u fupg a)
; c = λ { nothing nothing → refl
; (just a) (just p) → cong just (FUpgrade.c fupg a p) } }
decr-extract-upg : Upgrade (Bin → Maybe Bin) ({r : ℕ} → BHeap r → Maybe ((∃[ x ] BTree x r) × BHeap r))
decr-extract-upg = ∀⁺[[ r ∈ ℕ ]] Bin-BHeap r ⇀ fromFUpgrade (maybeFU ((∃[ x ] BTree x r) ⁺× toFUpgrade (Bin-BHeap r)))
extract' : {r : ℕ} (b : Bin) → BHeap' r b → Maybe' (λ b' → (∃[ x ] BTree x r) × BHeap' r b') (decr b)
extract' ._ nul = nothing
extract' ._ (zero h) = mapMaybe' (λ { ((x , node a (t , ts)) , h) → < node {x} a ts > , one t h }) (extract' _ h)
extract' ._ (one t h) = just (< t > , zero h)
extract : {r : ℕ} → BHeap r → Maybe ((∃[ x ] BTree x r) × BHeap r)
extract = Upgrade.u decr-extract-upg decr extract'
decr-extract-coherence : {r : ℕ} (h : BHeap r) → mapMaybe (toBin ∘ proj₂) (extract h) ≡ decr (toBin h)
decr-extract-coherence h = Upgrade.c decr-extract-upg decr extract' _ h refl
first : {r : ℕ} → BHeap r → Maybe (∃[ x ] ∃[ r' ] BTree x r')
first nul = nothing
first (zero h) = first h
first (one t h) = just < < t > >
extract-first : {r : ℕ} (h : BHeap r) → mapMaybe (root ∘ proj₂ ∘ proj₁) (extract h) ≡ mapMaybe (root ∘ proj₂ ∘ proj₂) (first h)
extract-first nul = refl
extract-first (zero h) with extract-first h
extract-first (zero h) | eq with extract' (toBin h) (fromBHeap h)
extract-first (zero h) | eq | _ with decr (toBin h)
extract-first (zero h) | eq | nothing | nothing = eq
extract-first (zero h) | eq | just ((x , node a (t , ts)) , h') | just b = eq
extract-first (one t h) = refl
--------
-- minimum extraction
{-
replace : {x y : V} {r : ℕ} (k : ℕ) → BTree x r → BTree y (k + r) → BTree y r × (∃[ z ] BTree z (k + r))
replace zero t u = u , < t >
replace (suc k) t (node b (u , us)) = (id ** (attach' u ∘ proj₂)) (replace k t (node b us))
replace-lemma : {x y : V} {r : ℕ} (k : ℕ) (t : BTree x r) (u : BTree y (k + r)) → root (proj₁ (replace k t u)) ≡ root u
replace-lemma zero t u = refl
replace-lemma (suc k) t (node b (u , us)) = replace-lemma k t (node b us)
-}
-- ornamentation of BHeap
data BHeap'' : ℕ → Maybe V → Set where
nul : {r : ℕ} → BHeap'' r nothing
zero : {r : ℕ} {ma : Maybe V} (h : BHeap'' (suc r) ma) → BHeap'' r ma
oneᶠ : {r : ℕ} {x : V} (t : BTree x r) (h : BHeap'' (suc r) nothing) → BHeap'' r (just (root t))
oneᵗʰ : {r : ℕ} {x : V} (t : BTree x r) {a : V} (h : BHeap'' (suc r) (just a)) {{leq : root t ≤ a}} → BHeap'' r (just (root t))
oneᵗᵗ : {r : ℕ} {x : V} (t : BTree x r) {a : V} (h : BHeap'' (suc r) (just a)) {{leq : a ≤ root t}} → BHeap'' r (just a)
-- free
fromBHeap'' : {r : ℕ} {ma : Maybe V} → BHeap'' r ma → BHeap r
fromBHeap'' nul = nul
fromBHeap'' (zero h) = zero (fromBHeap'' h)
fromBHeap'' (oneᶠ t h) = one t (fromBHeap'' h)
fromBHeap'' (oneᵗʰ t h) = one t (fromBHeap'' h)
fromBHeap'' (oneᵗᵗ t h) = one t (fromBHeap'' h)
_∈ᵀ_ : V → {r : ℕ} → BHeap r → Set
a ∈ᵀ nul = ⊥
a ∈ᵀ zero h = a ∈ᵀ h
a ∈ᵀ one u h = a ≡ root u ⊎ a ∈ᵀ h
empty-heap : {r : ℕ} (h : BHeap'' r nothing) → {a : V} → ¬ (a ∈ᵀ fromBHeap'' h)
empty-heap nul ()
empty-heap (zero h) i = empty-heap h i
root-element : {r : ℕ} {a : V} (h : BHeap'' r (just a)) → a ∈ᵀ fromBHeap'' h
root-element (zero h) = root-element h
root-element (oneᶠ t h) = inj₁ refl
root-element (oneᵗʰ t h) = inj₁ refl
root-element (oneᵗᵗ t h) = inj₂ (root-element h)
_≤ᵀ_ : (a : V) {r : ℕ} (h : BHeap r) → Set
a ≤ᵀ h = {b : V} → b ∈ᵀ h → a ≤ b
lower-bound : {r : ℕ} {a : V} (h : BHeap'' r (just a)) → a ≤ᵀ fromBHeap'' h
lower-bound (zero h) i = lower-bound h i
lower-bound (oneᶠ t h) (inj₁ refl) = ≤-refl
lower-bound (oneᶠ t h) (inj₂ i ) = ⊥-elim (empty-heap h i)
lower-bound (oneᵗʰ t h) (inj₁ refl) = ≤-refl
lower-bound (oneᵗʰ t h) (inj₂ i ) = ≤-trans - (lower-bound h i)
lower-bound (oneᵗᵗ t h) (inj₁ refl) = -
lower-bound (oneᵗᵗ t h) (inj₂ i ) = lower-bound h i
_IsMinRootOf_ : (a : V) {r : ℕ} (h : BHeap r) → Set
a IsMinRootOf h = a ∈ᵀ h × a ≤ᵀ h
minimum-root : {r : ℕ} {a : V} (h : BHeap'' r (just a)) → a IsMinRootOf (fromBHeap'' h)
minimum-root h = root-element h , lower-bound h
toBHeap'' : {r : ℕ} → BHeap r → ∃[ ma ] BHeap'' r ma
toBHeap'' nul = < nul >
toBHeap'' (zero h) = (id ** zero) (toBHeap'' h)
toBHeap'' (one t h) with toBHeap'' h
toBHeap'' (one t h) | nothing , h' = < oneᶠ t h' >
toBHeap'' (one t h) | just a , h' = if root t ≤? a then < oneᵗʰ t h' > else < oneᵗᵗ t h' >
-- free, if toBHeap'' is defined in terms of the optimised predicate
fromBHeap''-toBHeap''-inverse : {r : ℕ} (h : BHeap r) → fromBHeap'' (proj₂ (toBHeap'' h)) ≡ h
fromBHeap''-toBHeap''-inverse nul = refl
fromBHeap''-toBHeap''-inverse (zero h) = cong zero (fromBHeap''-toBHeap''-inverse h)
fromBHeap''-toBHeap''-inverse (one t h) with fromBHeap''-toBHeap''-inverse h
fromBHeap''-toBHeap''-inverse (one t h) | eq with toBHeap'' h
fromBHeap''-toBHeap''-inverse (one t h) | eq | nothing , h' = cong (one t) eq
fromBHeap''-toBHeap''-inverse {r} (one t h) | eq | just a , h' =
if-elim {C = ∃[ ma ] BHeap'' r ma} (root t ≤? a) < oneᵗʰ t h' > < oneᵗᵗ t h' >
(λ w → fromBHeap'' (proj₂ w) ≡ one t h) (cong (one t) eq) (cong (one t) eq)
regular : {r : ℕ} {ma : Maybe V} → BHeap'' r ma → Bool
regular nul = true
regular (zero h) = regular h
regular (oneᶠ t h) = true
regular (oneᵗʰ t h) = true
regular (oneᵗᵗ t h) = false
{-
postulate
regularise-aux : {r : ℕ} {a : V} (h : BHeap'' (suc r) (just a)) →
Σ (Σ (∃[ x ] BTree x r) (λ { < u > → root u ≡ a }))
(λ { < < u > >' → {x : V} (t : BTree x r) {{leq : a ≤ root t}} → ∃[ b ] BHeap'' (suc r) (just b) × a ≤ b })
-}
attach'' : {x y : V} {r : ℕ} (t : BTree x r) (u : BTree y r) {{leq : x ≤ root u}} → Σ[ t ∈ BTree _ (suc r) ] x ≤ root t
attach'' t u = attach t u , attach-root t u (bound-root t ≤-refl) -
-- takes a (relatively) long time to typecheck
regularise-aux : {r : ℕ} {a : V} (h : BHeap'' (suc r) (just a)) →
Σ (Σ (∃[ x ] BTree x r) (λ { < u > → root u ≡ a }))
(λ { < < u > >' → {x : V} (t : BTree x r) {{leq : a ≤ root t}} → ∃[ b ] BHeap'' (suc r) (just b) × a ≤ b })
regularise-aux (zero h) with regularise-aux h
regularise-aux (zero h) | < x , node a (u , us) >ʳ , f = < x , node a us >ʳ ,
λ t → let < t' >' = attach'' u t
< < h' >' > = f t'
in < zero h' , - >
regularise-aux (oneᶠ {x = x} (node c (v , vs)) h) = < x , node c vs >ʳ ,
λ t → let < t' >' = attach'' v t
in < oneᶠ t' h , - >
regularise-aux (oneᵗʰ {x = x} (node c (v , vs)) {a} h) = < x , node c vs >ʳ ,
λ t → let < t' >' = attach'' v t
in if root t' ≤? a then < oneᵗʰ t' h , - >
else < oneᵗᵗ t' h , - >
regularise-aux (oneᵗᵗ v h) with regularise-aux h
regularise-aux (oneᵗᵗ v h) | < x , node a (u , us) >ʳ , f = < x , node a us >ʳ ,
λ t → let < t' >' = attach'' u t
(b , < h' >') = f t'
in if root v ≤? b then < oneᵗʰ v h' , - >
else < oneᵗᵗ v h' , - >
regularise : {r : ℕ} {ma : Maybe V} → BHeap'' r ma → Σ[ h ∈ BHeap'' r ma ] regular h ≡ true
regularise nul = < nul >ʳ
regularise (zero h) = (zero ** id) (regularise h)
regularise (oneᶠ t h) = < oneᶠ t h >ʳ
regularise (oneᵗʰ t h) = < oneᵗʰ t h >ʳ
regularise (oneᵗᵗ t h) with regularise-aux h
regularise (oneᵗᵗ t h) | < x , node a us >ʳ , f = let < < h' >' > = f t in < oneᵗʰ {x = x} (node a us) h' >ʳ
regular-first : {r : ℕ} {ma : Maybe V} (h : BHeap'' r ma) → regular h ≡ true →
mapMaybe (root ∘ proj₂ ∘ proj₂) (first (fromBHeap'' h)) ≡ ma
regular-first nul eq = refl
regular-first (zero h) eq = regular-first h eq
regular-first (oneᶠ t h) eq = refl
regular-first (oneᵗʰ t h) eq = refl
regular-first (oneᵗᵗ t h) ()
extractMin : {r : ℕ} → BHeap r → Maybe ((∃[ x ] BTree x r) × BHeap r)
extractMin = extract ∘ fromBHeap'' ∘ proj₁ ∘ regularise ∘ proj₂ ∘ toBHeap''
extractMin-nothing : {r : ℕ} (h : BHeap r) → mapMaybe (root ∘ proj₂ ∘ proj₁) (extractMin h) ≡ nothing → {a : V} → ¬ (a ∈ᵀ h)
extractMin-nothing h eq with fromBHeap''-toBHeap''-inverse h
extractMin-nothing h eq | eq' with toBHeap'' h
extractMin-nothing h eq | eq' | ma , h'' with trans (sym (regular-first (proj₁ (regularise h'')) (proj₂ (regularise h''))))
(trans (sym (extract-first (fromBHeap'' (proj₁ (regularise h''))))) eq)
extractMin-nothing ._ eq | refl | nothing , h'' | _ = empty-heap h''
extractMin-nothing h eq | eq' | just a , h'' | ()
extractMin-just : {r : ℕ} (h : BHeap r) {a : V} → mapMaybe (root ∘ proj₂ ∘ proj₁) (extractMin h) ≡ just a → a IsMinRootOf h
extractMin-just h eq with fromBHeap''-toBHeap''-inverse h
extractMin-just h eq | eq' with toBHeap'' h
extractMin-just h eq | eq' | ma , h'' with trans (sym (regular-first (proj₁ (regularise h'')) (proj₂ (regularise h''))))
(trans (sym (extract-first (fromBHeap'' (proj₁ (regularise h''))))) eq)
extractMin-just h eq | eq' | nothing , h'' | ()
extractMin-just ._ eq | refl | just a , h'' | refl = minimum-root h''
{-
_∈ᵀ_ : {x : V} {r : ℕ} → BTree x r → {r' : ℕ} → BHeap r' → Set
t ∈ᵀ nul = ⊥
t ∈ᵀ zero h = t ∈ᵀ h
t ∈ᵀ one u h = (((Σ[ x ∈ V ] Σ[ r ∈ ℕ ] BTree x r) ∋ < < t > >) ≡ < < u > >) ⊎ t ∈ᵀ h
_Below_ : {x : V} {r : ℕ} (t : BTree x r) {r' : ℕ} (h : BHeap r') → Set
t Below h = {y : V} {r'' : ℕ} {u : BTree y r''} → u ∈ᵀ h → root t ≤ root u
findMin : {r : ℕ} (h : BHeap r) →
Maybe (Σ (Σ[ x ∈ V ] Σ[ r' ∈ ℕ ] BTree x r') λ { < < t > > → t ∈ᵀ h × t Below h })
findMin nul = nothing
findMin (zero h) = findMin h
findMin (one t h) = mapMaybe (λ { (< < u > > , i , leqs) →
if root t ≤? root u
then (λ {{leq}} → < < t > > , inj₁ refl ,
λ { {._} {._} {._} (inj₁ refl) → ≤-refl
; (inj₂ j) → ≤-trans leq (leqs j) })
else (λ {{leq}} → < < u > > , inj₂ i ,
λ { {._} {._} {._} (inj₁ refl) → leq; (inj₂ j) → leqs j}) })
(findMin h)
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment