Library Coq.Sorting.Heap



A development of Treesort on Heap trees


Require Import List Multiset Permutation Relations Sorting.

Section defs.

Trees and heap trees


Definition of trees over an ordered set


  Variable A : Type.
  Variable leA : relation A.
  Variable eqA : relation A.

  Let gtA (x y:A) := ~ leA x y.

  Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
  Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
  Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
  Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
  Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.

  Hint Resolve leA_refl.
  Hint Immediate eqA_dec leA_dec leA_antisym.

  Let emptyBag := EmptyBag A.
  Let singletonBag := SingletonBag _ eqA_dec.

  Inductive Tree :=
    | Tree_Leaf : Tree
    | Tree_Node : A -> Tree -> Tree -> Tree.

a is lower than a Tree T if T is a Leaf or T is a Node holding b>a

  Definition leA_Tree (a:A) (t:Tree) :=
    match t with
      | Tree_Leaf => True
      | Tree_Node b T1 T2 => leA a b
    end.

  Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf.

  Lemma leA_Tree_Node :
    forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D).

The heap property


  Inductive is_heap : Tree -> Prop :=
    | nil_is_heap : is_heap Tree_Leaf
    | node_is_heap :
      forall (a:A) (T1 T2:Tree),
        leA_Tree a T1 ->
        leA_Tree a T2 ->
        is_heap T1 -> is_heap T2 -> is_heap (Tree_Node a T1 T2).

  Lemma invert_heap :
    forall (a:A) (T1 T2:Tree),
      is_heap (Tree_Node a T1 T2) ->
      leA_Tree a T1 /\ leA_Tree a T2 /\ is_heap T1 /\ is_heap T2.

  Lemma is_heap_rect :
    forall P:Tree -> Type,
      P Tree_Leaf ->
      (forall (a:A) (T1 T2:Tree),
        leA_Tree a T1 ->
        leA_Tree a T2 ->
        is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
      forall T:Tree, is_heap T -> P T.

  Lemma is_heap_rec :
    forall P:Tree -> Set,
      P Tree_Leaf ->
      (forall (a:A) (T1 T2:Tree),
        leA_Tree a T1 ->
        leA_Tree a T2 ->
        is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
      forall T:Tree, is_heap T -> P T.

  Lemma low_trans :
    forall (T:Tree) (a b:A), leA a b -> leA_Tree b T -> leA_Tree a T.

From trees to multisets


contents of a tree as a multiset

Nota Bene : In what follows the definition of SingletonBag in not used. Actually, we could just take as postulate: Parameter SingletonBag : A->multiset.

  Fixpoint contents (t:Tree) : multiset A :=
    match t with
      | Tree_Leaf => emptyBag
      | Tree_Node a t1 t2 =>
        munion (contents t1) (munion (contents t2) (singletonBag a))
    end.

equivalence of two trees is equality of corresponding multisets
  Definition equiv_Tree (t1 t2:Tree) := meq (contents t1) (contents t2).

From lists to sorted lists


Specification of heap insertion


  Inductive insert_spec (a:A) (T:Tree) : Type :=
    insert_exist :
    forall T1:Tree,
      is_heap T1 ->
      meq (contents T1) (munion (contents T) (singletonBag a)) ->
      (forall b:A, leA b a -> leA_Tree b T -> leA_Tree b T1) ->
      insert_spec a T.

  Lemma insert : forall T:Tree, is_heap T -> forall a:A, insert_spec a T.

Building a heap from a list


  Inductive build_heap (l:list A) : Type :=
    heap_exist :
    forall T:Tree,
      is_heap T ->
      meq (list_contents _ eqA_dec l) (contents T) -> build_heap l.

  Lemma list_to_heap : forall l:list A, build_heap l.

Building the sorted list


  Inductive flat_spec (T:Tree) : Type :=
    flat_exist :
    forall l:list A,
      sort leA l ->
      (forall a:A, leA_Tree a T -> lelistA leA a l) ->
      meq (contents T) (list_contents _ eqA_dec l) -> flat_spec T.

  Lemma heap_to_list : forall T:Tree, is_heap T -> flat_spec T.

Specification of treesort


  Theorem treesort :
    forall l:list A, {m : list A | sort leA m & permutation _ eqA_dec l m}.

End defs.