Library Coq.Sorting.Heap

This file is deprecated, for a tree on list, use Mergesort.v.

A development of Treesort on Heap trees. It has an average complexity of O(n.log n) but of O(n²) in the worst case (e.g. if the list is already sorted)

Require Import List Multiset PermutSetoid 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.

  #[local]
  Hint Resolve leA_refl : core.
  #[local]
  Hint Immediate eqA_dec leA_dec leA_antisym : core.

  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.

Merging two sorted lists

   Inductive merge_lem (l1 l2:list A) : Type :=
    merge_exist :
    forall l:list A,
      Sorted leA l ->
      meq (list_contents _ eqA_dec l)
      (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
      (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l ) ->
      merge_lem l1 l2.
  Import Morphisms.

  Instance: Equivalence (@meq A).

  Instance: Proper (@meq A ++> @meq _ ++> @meq _) (@munion A).

  Lemma merge :
    forall l1:list A, Sorted leA l1 ->
    forall l2:list A, Sorted leA l2 -> merge_lem l1 l2.

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,
      Sorted leA l ->
      (forall a:A, leA_Tree a T -> HdRel 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 | Sorted leA m & permutation _ eqA_dec l m }.

End defs.