Leftist heaps (Clark Allan Crane, 1972 && Donald E. Knuth, 1973).

Purely applicative implementation, following Okasaki's implementation in his book "Purely Functional Data Structures" (Section 3.1).

Author: Mário Pereira (Université Paris Sud)

module Heap

  use int.Int

  type elt
  predicate le elt elt

  clone relations.TotalPreOrder with
    type t = elt, predicate rel = le, axiom .

  type heap

  val function size heap : int

  function occ elt heap : int

  predicate mem (x: elt) (h: heap) = occ x h > 0

  function minimum heap : elt

  predicate is_minimum (x: elt) (h: heap) =
    mem x h && forall e. mem e h -> le x e

  axiom min_def:
    forall h. 0 < size h -> is_minimum (minimum h) h

  val empty : heap
    ensures { size result = 0 }
    ensures { forall x. occ x result = 0 }

  val is_empty (h: heap) : bool
    ensures { result <-> size h = 0 }

  val merge (h1 h2: heap) : heap
    ensures { forall x. occ x result = occ x h1 + occ x h2 }
    ensures { size result = size h1 + size h2 }

  val insert (x: elt) (h: heap) : heap
    ensures { occ x result = occ x h + 1 }
    ensures { forall y. y <> x -> occ y h = occ y result }
    ensures { size result = size h + 1 }

  val find_min (h: heap) : elt
    requires { size h > 0 }
    ensures  { result = minimum h }

  val delete_min (h: heap) : heap
    requires { size h > 0 }
    ensures  { let x = minimum h in occ x result = occ x h - 1 }
    ensures  { forall y. y <> minimum h -> occ y result = occ y h }
    ensures  { size result = size h - 1 }

end

module TreeRank

  type tree 'a = E | N int (tree 'a) 'a (tree 'a)

end

module Size

  use TreeRank
  use int.Int

  let rec function size (t: tree 'a) : int = match t with
    | E -> 0
    | N _ l _ r -> 1 + size l + size r
    end

  lemma size_nonneg: forall t: tree 'a. 0 <= size t
  lemma size_empty: forall t: tree 'a. 0 = size t <-> t = E

end

module Occ

  use TreeRank
  use int.Int

  function occ (x: 'a) (t: tree 'a) : int = match t with
    | E -> 0
    | N _ l e r -> (if x = e then 1 else 0) + occ x l + occ x r
    end

  lemma occ_nonneg:
    forall x:'a, t. 0 <= occ x t

  predicate mem (x: 'a) (t: tree 'a) =
    0 < occ x t

end

module LeftistHeap

  type elt
  val predicate le elt elt
  clone relations.TotalPreOrder with
    type t = elt, predicate rel = le, axiom .

  use TreeRank
  use export Size
  use export Occ
  use int.Int
  use int.MinMax

  type t = tree elt

  (* [e] is no greater than the root of [h], if any *)
  predicate le_root (e: elt) (h: t) = match h with
    | E -> true
    | N _ _ x _ -> le e x
    end

  lemma le_root_trans:
    forall x y h. le x y -> le_root y h -> le_root x h

  (* [h] is a heap *)
  predicate is_heap (h: t) = match h with
    | E -> true
    | N _ l x r -> le_root x l && is_heap l && le_root x r && is_heap r
    end

  function minimum t : elt
  axiom minimum_def: forall l x r s. minimum (N s l x r) = x

  predicate is_minimum (x: elt) (h: t) =
    mem x h && forall e. mem e h -> le x e

  let rec lemma root_is_miminum (h: t) : unit
    requires { is_heap h && 0 < size h }
    ensures  { is_minimum (minimum h) h }
    variant  { h }
  = match h with
    | E -> absurd
    | N _ l _ r ->
       match l with E -> () | _ -> root_is_miminum l end;
       match r with E -> () | _ -> root_is_miminum r end
    end

  function rank (h: t) : int = match h with
    | E -> 0
    | N _ l _ r -> 1 + min (rank l) (rank r)
    end

  predicate leftist (h: t) = match h with
    | E -> true
    | N s l _ r ->
       s = rank h &&
       leftist l && leftist r &&
       rank l >= rank r
    end

   predicate leftist_heap (h: t) =
    is_heap h && leftist h

  let empty : t = E
    ensures { size result = 0 }
    ensures { forall x. occ x result = 0 }
    ensures { leftist_heap result }

  let is_empty (h: t) : bool
    ensures { result <-> size h = 0 }
  = match h with E -> true | N _ _ _ _ -> false end

  let rank (h: t) : int
    requires { leftist_heap h }
    ensures  { result = rank h }
  = match h with
    | E -> 0
    | N r _ _ _ -> r
    end

  let make_n (x: elt) (l r: t) : t
    requires { leftist_heap r && leftist_heap l }
    requires { le_root x l && le_root x r }
    ensures  { leftist_heap result }
    ensures  { minimum result = x }
    ensures  { size result = 1 + size l + size r }
    ensures  { occ x result = 1 + occ x l + occ x r }
    ensures  { forall y. x <> y -> occ y result = occ y l + occ y r }
  = if rank l >= rank r then N (rank r + 1) l x r
    else N (rank l + 1) r x l

  let rec merge (h1 h2: t) : t
    requires { leftist_heap h1 && leftist_heap h2 }
    ensures  { size result = size h1 + size h2 }
    ensures  { forall x. occ x result = occ x h1 + occ x h2 }
    ensures  { leftist_heap result }
    variant  { size h1 + size h2 }
  = match h1, h2 with
    | h, E | E, h -> h
    | N _ l1 x1 r1, N _ l2 x2 r2 ->
       if le x1 x2 then make_n x1 l1 (merge r1 h2)
       else make_n x2 l2 (merge h1 r2)
    end

  let insert (x: elt) (h: t) : t
    requires { leftist_heap h }
    ensures  { leftist_heap result }
    ensures  { occ x result = occ x h + 1 }
    ensures  { forall y. x <> y -> occ y result = occ y h }
    ensures  { size result = size h + 1 }
  = merge (N 1 E x E) h

  let find_min (h: t) : elt
    requires { leftist_heap h }
    requires { 0 < size h }
    ensures  { result = minimum h }
  = match h with
    | E -> absurd
    | N _ _ x _ -> x
    end

  let delete_min (h: t) : t
    requires { 0 < size h }
    requires { leftist_heap h }
    ensures  { occ (minimum h) result = occ (minimum h) h - 1 }
    ensures  { forall x. x <> minimum h -> occ x result = occ x h }
    ensures  { size result = size h - 1 }
    ensures  { leftist_heap result }
  = match h with
    | E -> absurd
    | N _ l _ r -> merge l r
    end

end