add leftist heaps

README.md

@@ -23,7 +23,7 @@ Besides Mathcomp, this also requires the [Equations](https://mattam82.github.io/
 13. [Huffman’s Algorithm](src/huffman.v)
 ### Part III: Priority Queues
 14. [Priority Queues](src/priority.v)
-15. Leftist Heaps
+15. [Leftist Heaps](src/leftist.v)
 16. Priority Queues via Braun Trees
 17. Binomial Heaps
 ### Part IV: Advanced Design and Analysis Techniques

_CoqProject

@@ -16,4 +16,5 @@ src/beyond.v
 src/braun.v
 src/trie.v
 src/huffman.v
-src/priority.v
+src/priority.v
+src/leftist.v

src/bintree.v

@@ -488,14 +488,19 @@ End AlmostCompleteTrees.
 Section AugmentedTrees.
 Context {A B : Type}.
 
-Fixpoint inorder_a (t : tree (A * B)) : seq A :=
+Fixpoint preorder_a (t : tree (A*B)) : seq A :=
+  if t is Node l (x,_) r
+    then x :: preorder_a l ++ preorder_a r
+  else [::].
+
+Fixpoint inorder_a (t : tree (A*B)) : seq A :=
   if t is Node l (x, _) r
     then inorder_a l ++ [:: x] ++ inorder_a r
   else [::].
 
-Definition inorder_a' (t : tree (A * B)) : seq A := map fst (inorder t).
+Definition inorder_a' (t : tree (A*B)) : seq A := map fst (inorder t).
 
-Definition inorder_a'' (t : tree (A * B)) : seq A := inorder (map_tree fst t).
+Definition inorder_a'' (t : tree (A*B)) : seq A := inorder (map_tree fst t).
 
 Lemma in_a : inorder_a =1 inorder_a'.
 Proof.
@@ -531,6 +536,13 @@ Context {A : eqType} {B : Type}.
 Lemma inorder_a_empty_pred : inorder_a (@Leaf (A*B)) =i pred0.
 Proof. by []. Qed.
 
+Lemma perm_pre_in (t : tree (A*B)) : perm_eq (inorder_a t) (preorder_a t).
+Proof.
+elim: t=>//=l IHl [a _] r IHr.
+rewrite perm_catC /= perm_cons perm_catC.
+by apply: perm_cat.
+Qed.
+
 End AugmentedTreesEq.
 
 (* generalized form *)

src/leftist.v

@@ -0,0 +1,324 @@
+From Coq Require Import ssreflect ssrbool ssrfun.
+From mathcomp Require Import eqtype order ssrnat seq path prime.
+From favssr Require Import prelude bintree priority.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Import Order.POrderTheory.
+Import Order.TotalTheory.
+Open Scope order_scope.
+
+Section Intro.
+Context {disp : unit} {T : orderType disp}.
+
+Definition lheap T := tree (T * nat).
+
+Definition mht (h : lheap T) : nat :=
+  if h is Node _ (_,n) _ then n else 0.
+
+Fixpoint heap_a {B} (t : tree (T*B)) : bool :=
+  if t is Node l (m,_) r
+    then [&& all (>= m) (inorder_a l ++ inorder_a r), heap_a l & heap_a r]
+    else true.
+
+Fixpoint ltree (h : lheap T) : bool :=
+  if h is Node l (_, n) r
+    then [&& min_height r <= min_height l,
+             n == (min_height r).+1,
+             ltree l &
+             ltree r]
+  else true.
+
+(* Exercise 15.1 *)
+
+Fixpoint rank {A} (t : tree A) : nat :=
+  if t is Node _ _ r then (rank r).+1 else 0.
+
+Lemma ltree_rank_min t : ltree t -> rank t = min_height t.
+Proof.
+Admitted.
+
+End Intro.
+
+Section ImplementationPQM.
+Context {disp : unit} {T : orderType disp}.
+
+Definition empty_lheap : lheap T := leaf.
+
+Definition get_min_lheap (x0 : T) (t : lheap T) : T :=
+  if t is Node _ (a, _) _
+    then a else x0.
+
+Definition node (l : lheap T) (a : T) (r : lheap T) : lheap T :=
+  let mhl := mht l in
+  let mhr := mht r in
+  if mhr <= mhl then Node l (a, mhr.+1) r
+                else Node r (a, mhl.+1) l.
+
+Fixpoint merge_lheap (h1 : lheap T) : lheap T -> lheap T :=
+  if h1 is Node l1 (a1,_) r1 then
+    let fix merge_lheap_h1 (h2 : lheap T) :=
+      if h2 is Node l2 (a2,_) r2 then
+        if a1 <= a2 then node l1 a1 (merge_lheap r1 h2)
+                    else node l2 a2 (merge_lheap_h1 r2)
+      else h1 in
+    merge_lheap_h1
+  else id.
+
+Definition insert x h : lheap T :=
+  merge_lheap (Node leaf (x,1%N) leaf) h.
+
+Definition del_min (t : lheap T) : lheap T :=
+  if t is Node l _ r then merge_lheap l r else leaf.
+
+End ImplementationPQM.
+
+Section Correctness.
+Context {disp : unit} {T : orderType disp}.
+
+Definition mset_lheap (h : lheap T) : seq T := preorder_a h.
+
+Definition invar (h : lheap T) : bool := heap_a h && ltree h.
+
+Lemma mht_min_height (t : lheap T) :
+  ltree t -> mht t = min_height t.
+Proof.
+case: t=>//=l [_ n] r /and4P [H /eqP -> _ _].
+apply/eqP; rewrite -addn1 eqn_add2r eq_sym.
+by apply/eqP/minn_idPr.
+Qed.
+
+Lemma mset_node (l : lheap T) a r :
+  perm_eq (mset_lheap (node l a r)) (a :: mset_lheap l ++ mset_lheap r).
+Proof. by rewrite /node; case: ifP=>//= _; rewrite perm_cons perm_catC. Qed.
+
+Lemma ltree_node (l : lheap T) a r :
+  ltree (node l a r) <-> ltree l /\ ltree r.
+Proof.
+rewrite /node; split.
+- by case: ifP=>/= _ /and4P [_ _ -> ->].
+case=>Hl Hr; case: ifP=>/=.
+- by move=>H; rewrite -!mht_min_height // H eq_refl Hl Hr.
+move/negbT; rewrite -ltNge=>H.
+rewrite -!mht_min_height // eq_refl Hl Hr /= andbT.
+by apply: ltW.
+Qed.
+
+Lemma heap_node (l : lheap T) a r :
+  heap_a (node l a r) <-> [/\ all (>= a) (inorder_a l ++ inorder_a r), heap_a l & heap_a r].
+Proof.
+rewrite /node; split.
+- case: ifP=>/= _ /and3P // [Ha Hlr Hr]; split=>//.
+  by rewrite !all_cat in Ha *; case/andP: Ha=>->->.
+case=>Ha Hl Hr; case: ifP=>/= _; rewrite Hl Hr /= andbT //.
+by rewrite !all_cat in Ha *; case/andP: Ha=>->->.
+Qed.
+
+Lemma all_foldl_a {B} (x : T) (t : tree (T*B)) :
+  all (>= x) (inorder_a t) ->
+  foldl Order.min x (preorder_a t) = x.
+Proof.
+elim: t x =>//=l IHl [a _] r IHr x; rewrite all_cat /=.
+case/and3P=>Hal Hxa Har; rewrite foldl_cat.
+by rewrite min_l // IHl // IHr.
+Qed.
+
+Lemma get_min_mins_heap (h : lheap T) x0 :
+  heap_a h ->
+  get_min_lheap x0 h = mins x0 (mset_lheap h).
+Proof.
+case: h=>//=l [a n] r /and3P [+ Hl Hr].
+by rewrite all_cat /mins foldl_cat; case/andP=>/all_foldl_a->/all_foldl_a->.
+Qed.
+
+Corollary get_min_mins (h : lheap T) x0 :
+  invar h ->
+  get_min_lheap x0 h = mins x0 (mset_lheap h).
+Proof. by rewrite /invar => /andP [+ _]; exact: get_min_mins_heap. Qed.
+
+Lemma mset_merge_heap (h1 h2 : lheap T) :
+  perm_eq (mset_lheap (merge_lheap h1 h2)) (mset_lheap h1 ++ mset_lheap h2).
+Proof.
+elim: h1 h2=>//= l1 _ [a1 n1] r1 IHr1; elim=>/= [|l2 _ [a2 n2] r2 IHr2].
+- by rewrite cats0 /=.
+case: ifP=>/= _; apply: perm_trans; try by apply: mset_node.
+- rewrite perm_cons perm_sym -catA perm_cat2l perm_sym.
+  by apply: IHr1=>//=; rewrite H2 Hl2 Hr2.
+rewrite perm_sym -!cat_cons perm_catCA perm_cat2l /= perm_sym.
+by apply: IHr2.
+Qed.
+
+Lemma ltree_merge_heap (l r : lheap T) :
+  ltree l -> ltree r -> ltree (merge_lheap l r).
+Proof.
+elim: l r=>//= l1 _ [a1 n1] r1 IHr1; elim=>//= l2 _ [a2 n2] r2 IHr2.
+case/and4P=>Eh1 En1 Hl1 Hr1; case/and4P=>Eh2 En2 Hl2 Hr2.
+case: ifP=>/= _; apply/ltree_node; split=>//.
+- by apply: IHr1=>//=; rewrite Eh2 En2 Hl2 Hr2.
+by apply: IHr2=>//; rewrite Eh1 En1 Hl1 Hr1.
+Qed.
+
+Lemma heap_merge_heap (l r : lheap T) :
+  heap_a l -> heap_a r -> heap_a (merge_lheap l r).
+Proof.
+elim: l r=>//= l1 _ [a1 n1] r1 IHr1; elim=>//= l2 _ [a2 n2] r2 IHr2.
+case/and3P=>Ha1 Hl1 Hr1; case/and3P=>Ha2 Hl2 Hr2.
+case: ifP=>/= Ha; apply/heap_node; split=>//.
+- rewrite !all_cat in Ha1 *; case/andP: Ha1=>-> Ha1 /=.
+  rewrite (perm_all _ (perm_pre_in _)) (perm_all _ (mset_merge_heap _ _))
+    all_cat /= all_cat -!(perm_all _ (perm_pre_in _)) Ha Ha1 /=.
+  rewrite all_cat in Ha2; case/andP: Ha2=>Hal2 Har2.
+  apply/andP; split.
+  - by apply/sub_all/Hal2=>z Hz; apply/le_trans/Hz.
+  by apply/sub_all/Har2=>z Hz; apply/le_trans/Hz.
+- by apply: IHr1=>//=; rewrite Ha2 Hl2 Hr2.
+- move/negbT: Ha; rewrite -ltNge=>Ha.
+  rewrite !all_cat in Ha2 *; case/andP: Ha2=>-> Ha2 /=.
+  move: (@mset_merge_heap (Node l1 (a1, n1) r1) r2)=>/= H'.
+  rewrite (perm_all _ (perm_pre_in _)) (perm_all _ H') /= !all_cat
+    -!(perm_all _ (perm_pre_in _)) (ltW Ha) Ha2 /= andbT.
+  rewrite all_cat in Ha1; case/andP: Ha1=>Hal1 Har1.
+  apply/andP; split.
+  - by apply/sub_all/Hal1=>z Hz; apply/ltW/lt_le_trans/Hz.
+  by apply/sub_all/Har1=>z Hz; apply/ltW/lt_le_trans/Hz.
+by apply: IHr2=>//; rewrite Ha1 Hl1 Hr1.
+Qed.
+
+Corollary invar_merge h1 h2 :
+  invar h1 -> invar h2 -> invar (merge_lheap h1 h2).
+Proof.
+rewrite /invar; case/andP=>Hh1 Hl1; case/andP=>Hh2 Hl2.
+apply/andP; split.
+- by apply: heap_merge_heap.
+by apply: ltree_merge_heap.
+Qed.
+
+Corollary mset_merge h1 h2 :
+  invar h1 -> invar h2 ->
+  perm_eq (mset_lheap (merge_lheap h1 h2)) (mset_lheap h1 ++ mset_lheap h2).
+Proof. by move=>_ _; exact: mset_merge_heap. Qed.
+
+Lemma invar_empty : invar empty_lheap.
+Proof. by []. Qed.
+
+Lemma mset_empty : mset_lheap empty_lheap = [::].
+Proof. by []. Qed.
+
+Corollary invar_insert x h :
+  invar h -> invar (insert x h).
+Proof. by exact: invar_merge. Qed.
+
+Corollary mset_insert x h :
+  invar h -> perm_eq (mset_lheap (insert x h)) (x :: mset_lheap h).
+Proof. by move=>_; apply: mset_merge_heap. Qed.
+
+Corollary invar_delmin h :
+  invar h -> ~~ nilp (mset_lheap h) -> invar (del_min h).
+Proof.
+rewrite /invar; case: h=>//= l [a n] r /and5P [/and3P [_ Hhl Hhr] _ _ Hll Hlr] _.
+by apply/andP; split; [apply: heap_merge_heap | apply: ltree_merge_heap].
+Qed.
+
+Corollary mset_delmin x0 h :
+  invar h -> ~~ nilp (mset_lheap h) ->
+  perm_eq (mset_lheap (del_min h)) (rem (get_min_lheap x0 h) (mset_lheap h)).
+Proof.
+rewrite /invar; case: h=>//= l [a n] r /and5P [/and3P [_ Hhl Hhr] _ _ Hll Hlr] _.
+apply: perm_trans; first by apply: mset_merge_heap.
+by rewrite rem_cons eq_refl.
+Qed.
+
+Definition LHeapPQM :=
+  @APQM.make _ _ (lheap T)
+    empty_lheap insert del_min get_min_lheap merge_lheap
+    mset_lheap invar
+    invar_empty mset_empty
+    invar_insert mset_insert
+    invar_delmin mset_delmin
+    get_min_mins
+    invar_merge mset_merge.
+
+End Correctness.
+
+Section RunningTimeAnalysis.
+Context {disp : unit} {T : orderType disp}.
+
+Fixpoint T_merge (h1 : lheap T) : lheap T -> nat :=
+  if h1 is Node l1 (a1,_) r1 then
+    let fix T_merge_h1 (h2 : lheap T) :=
+      if h2 is Node l2 (a2,_) r2 then
+        if a1 <= a2 then T_merge r1 h2
+                    else T_merge_h1 r2
+      else 1%N in
+    T_merge_h1
+  else fun=>1%N.
+
+Definition T_insert x h :=
+  T_merge (Node leaf (x,1%N) leaf) h + 1.
+
+Definition T_del_min (t : lheap T) : nat :=
+  if t is Node l _ r then T_merge l r + 1 else 1%N.
+
+Lemma T_merge_bound l r :
+  ltree l -> ltree r ->
+  T_merge l r <= min_height l + min_height r + 1.
+Proof.
+elim: l r=>/=; first by move=>r _ _; rewrite add0n; apply: leq_addl.
+move=>l1 _ [a1 n1] r1 IHr1; elim=>/=; first by move=>_ _; rewrite addn0 addn1.
+move=>l2 _ [a2 n2] r2 IHr2.
+case/and4P=>Hm1 En1 Hl1 Hr1; case/and4P=>Hm2 En2 Hl2 Hr2.
+case: ifP=>/= Ha.
+- apply: leq_trans; first by apply: IHr1=>//=; rewrite Hm2 En2 Hl2 Hr2.
+  rewrite /= !addnA !leq_add2r addn1.
+  by apply: ltnW; rewrite ltnS leq_min -leEnat Hm1 lexx.
+apply: leq_trans; first by apply: IHr2=>//=; rewrite Hm1 En1 Hl1 Hr1.
+rewrite /=  leq_add2r leq_add2l addn1.
+by apply: ltnW; rewrite ltnS leq_min -leEnat Hm2 lexx.
+Qed.
+
+Corollary T_merge_log l r :
+  ltree l -> ltree r ->
+  T_merge l r <= trunc_log 2 (size1_tree l) + trunc_log 2 (size1_tree r) + 1.
+Proof.
+move=>Hl Hr; apply: leq_trans; first by by apply: T_merge_bound.
+by rewrite leq_add2r; apply: leq_add; apply: trunc_log_max=>//; apply: exp_mh_leq.
+Qed.
+
+Corollary T_insert_log t x :
+  ltree t -> T_insert x t <= trunc_log 2 (size1_tree t) + 3.
+Proof.
+move=>H; rewrite /T_insert (_ : 3 = 2 + 1) // addnA leEnat leq_add2r.
+apply: leq_trans; first by apply: T_merge_log.
+by rewrite addnAC addnC.
+Qed.
+
+Lemma trunc_log2_ltD x y :
+  (0 < x -> 0 < y ->
+  trunc_log 2 x + trunc_log 2 y + 1 < 2 * up_log 2 (x + y))%N.
+Proof.
+move=>Hx Hy.
+have H: (2 ^ (trunc_log 2 x + trunc_log 2 y + 1) <= 2*x*y)%N.
+- rewrite !expnD expn1 mulnC -mulnA leq_pmul2l //.
+  by apply: leq_mul; apply: trunc_logP.
+have H' : (2*x*y < (x+y)^2)%N.
+- by rewrite sqrnD mulnA -[X in (X < _)%N]add0n ltn_add2r addn_gt0 !sqrn_gt0 Hx Hy.
+have H'': ((x+y)^2 <= 2 ^ (2 * up_log 2 (x + y)))%N.
+- rewrite (mulnC 2) expnM leq_exp2r //.
+  by apply: up_logP.
+rewrite -(ltn_exp2l _ _ (isT : (1 < 2)%N)).
+by apply: (leq_ltn_trans H); apply: (leq_trans H').
+Qed.
+
+Lemma T_del_min_log t :
+  ltree t -> T_del_min t <= 2 * up_log 2 (size1_tree t) + 1.
+Proof.
+case: t=>//= l [a n] r /and4P [Hm En Hl Hr]; rewrite leEnat leq_add2r.
+apply: leq_trans; first by by apply: T_merge_bound.
+apply: (leq_trans (n:=trunc_log 2 (size1_tree l) + trunc_log 2 (size1_tree r) + 1)).
+- by rewrite leq_add2r; apply: leq_add; apply: trunc_log_max=>//; apply: exp_mh_leq.
+by apply/ltnW/trunc_log2_ltD; rewrite size1_size addn1.
+Qed.
+
+End RunningTimeAnalysis.