binomial_heap: proof in progress (only lemmas missing now)

examples/in_progress/binomial_heap.mlw

@@ -34,8 +34,8 @@ module BinomialHeap
   (* [l] is a list of heaps *)
   predicate heaps (l: list tree) =
     match l with
-    | Nil                         -> true
-    | Cons {elem=e; children=c} r -> le_roots e c && heaps c && heaps r
+    | Nil                               -> true
+    | Cons { elem = e; children = c } r -> le_roots e c && heaps c && heaps r
     end
 
   lemma heaps_reverse:
@@ -50,12 +50,6 @@ module BinomialHeap
     else
       { t2 with children = Cons t1 t2.children }
 
-  (* predicate mem (x: elt) (l: list tree) = *)
-  (*   match l with *)
-  (*   | Nil      -> false *)
-  (*   | Cons { elem = y; children = c } r -> x = y || mem x c || mem x r *)
-  (*   end *)
-
   function occ (x: elt) (l: list tree) : int =
     match l with
     | Nil      -> 0
@@ -91,52 +85,41 @@ module BinomialHeap
     | Cons { children = c } r -> has_order (k-1) c && has_order (k-1) r
     end
 
-  function size (l: list tree) : int =
-    match l with
-    | Nil                     -> 0
-    | Cons { children = c } r -> 1 + size c + size r
-    end
+  predicate binomial_tree (t: tree) =
+    has_order (rank t) t.children
 
   (* a binomial heap is a list of trees *)
   type heap = list tree
 
-(*
-  predicate inv (t: t) = match t with
-  | Empty      -> true
-  | Node l _ r -> (size l = size r || size l = size r + 1) && inv l && inv r
-  end
-*)
+  (* h is a list of binomial trees in strict increasing order of ranks
+     no smaller than m *)
+  predicate inv (m: int) (h: heap) =
+    match h with
+    | Nil -> true
+    | Cons t r -> let k = rank t in m <= k && binomial_tree t && inv (k + 1) r
+    end
+
+  lemma inv_reverse:
+    forall t. binomial_tree t -> inv 0 (reverse t.children)
 
   let empty () : heap
     ensures { heaps result }
-    (* ensures { inv result } *)
-    (* ensures { size result = 0 } *)
+    ensures { inv 0 result }
     ensures { forall e. not (mem e result) }
-    = Nil
-
-(*
-  function minimum (list tree) : elt
-
-  axiom minimum_def: forall l x r. minimum (Node l x r) = x
-
-  predicate is_minimum (x: elt) (l: list tree) =
-    mem x t && forall e. mem e t -> le x e
-*)
+    =
+    Nil
 
-(*
   let is_empty (h: heap) : bool
-    ensures { result <-> size h = 0 }
-  =
+    ensures { result <-> h = Nil }
+    =
     h = Nil
-*)
 
   let get_min (h: heap) : elt
     requires { heaps h }
-    (* requires { 0 < size h } *)
     requires { h <> Nil }
     ensures  { mem result h }
     ensures  { forall x. mem x h -> le result x }
-  =
+    =
     match h with
       | Nil      -> absurd
       | Cons t l ->
@@ -155,9 +138,12 @@ module BinomialHeap
 
   let rec add_tree (t: tree) (h: heap)
     requires { heaps (Cons t Nil) }
+    requires { binomial_tree t }
     requires { heaps h }
+    requires { inv (rank t) h }
     variant  { h }
     ensures  { heaps result }
+    ensures  { inv (rank t) result }
     ensures  { forall x. occ x result = occ x (Cons t Nil) + occ x h }
     =
     match h with
@@ -166,67 +152,89 @@ module BinomialHeap
     | Cons hd tl ->
         if rank t < rank hd then
           Cons t h
-        else if rank t = rank hd then
+        else begin
+          assert { rank t = rank hd };
           add_tree (link t hd) tl
-        else
-         (* this case will never be used with usual binomial heaps *)
-          Cons hd (add_tree t tl)
+        end
     end
 
   let add (x: elt) (h: heap) : heap
     requires { heaps h }
-    (* requires { inv t } *)
+    requires { inv 0 h }
     ensures  { heaps result }
-    (* ensures  { inv result } *)
+    ensures  { inv 0 result }
     ensures  { occ x result = occ x h + 1 }
     ensures  { forall e. e <> x -> occ e result = occ e h }
-    (* ensures  { size result = size h + 1 } *)
-  =
+    =
     add_tree { elem = x; children = Nil } h
 
-  let rec merge (h1 h2: heap)
+  let rec merge (ghost k: int) (h1 h2: heap)
     requires { heaps h1 }
+    requires { inv k h1 }
     requires { heaps h2 }
-    variant  { h2 }
+    requires { inv k h2 }
+    variant  { h1, h2 }
     ensures  { heaps result }
+    ensures  { inv k result }
     ensures  { forall x. occ x result = occ x h1 + occ x h2 }
-  = match h2 with
-    | Nil -> h1
-    | Cons hd2 tl2 -> merge (add_tree hd2 h1) tl2
+    =
+    match h1, h2 with
+    | Nil, _ -> h2
+    | _, Nil -> h1
+    | Cons t1 tl1, Cons t2 tl2 ->
+        if rank t1 < rank t2 then
+          Cons t1 (merge (rank t1 + 1) tl1 h2)
+        else if rank t2 < rank t1 then
+          Cons t2 (merge (rank t2 + 1) h1 tl2)
+        else
+          add_tree (link t1 t2) (merge (rank t1 + 1) tl1 tl2)
     end
 
-  let rec extract_min_tree (h: heap) : (tree, heap)
+  let rec extract_min_tree (ghost k: int) (h: heap) : (tree, heap)
     requires { heaps h }
-    (* requires { 0 < size h } *)
+    requires { inv k h }
     requires { h <> Nil }
     variant  { h }
     ensures  { let (t, h') = result in
-               heaps (Cons t Nil) && heaps h' &&
-               le_roots t.elem h &&
-               (* inv t' && size h' = size h - 1 && *)
+               heaps (Cons t Nil) && heaps h' && inv k h' &&
+               le_roots t.elem h && binomial_tree t &&
                forall x. occ x h = occ x (Cons t Nil) + occ x h' }
-  = match h with
+    =
+    match h with
     | Nil ->
         absurd
     | Cons t Nil ->
         (t, Nil)
     | Cons t tl ->
-        let (t', tl') = extract_min_tree tl in
+        let (t', tl') = extract_min_tree (rank t + 1) tl in
         if le t.elem t'.elem then (t, tl) else (t', Cons t tl')
     end
 
   let rec extract_min (h: heap) : (elt, heap)
     requires { heaps h }
-    (* requires { inv h } *)
-    (* requires { 0 < size h } *)
+    requires { inv 0 h }
     requires { h <> Nil }
     variant  { h }
     ensures  { let (e, h') = result in
-               heaps h' && (* inv t' && size h' = size h - 1 && *)
+               heaps h' && inv 0 h' &&
                occ e h' = occ e h - 1 &&
                forall x. x <> e -> occ x h' = occ x h }
-  =
-    let (t, h') = extract_min_tree h in
-    (t.elem, merge (reverse t.children) h')
+    =
+    let (t, h') = extract_min_tree 0 h in
+    (t.elem, merge 0 (reverse t.children) h')
+
+  (* complexity analysis *)
+
+  use import int.Power
+
+  function size (l: list tree) : int =
+    match l with
+    | Nil                     -> 0
+    | Cons { children = c } r -> 1 + size c + size r
+    end
+
+  lemma binomial_tree_size:
+    forall k t. has_order k t.children -> size t.children = power 2 k - 1
+
 
 end