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.

#[local]
Set Warnings "-deprecated".

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

  #[deprecated(since="8.3", note="Use mergesort.v")]
  Definition leA_Tree (a:A) (t:Tree) :=
    match t with
      | Tree_Leaf => True
      | Tree_Node b T1 T2 => leA a b
    end.

  #[deprecated(since="8.3", note="Use mergesort.v")]
  Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf.

  #[deprecated(since="8.3", note="Use mergesort.v")]
  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).

  #[deprecated(since="8.3", note="Use mergesort.v")]
  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.

  #[deprecated(since="8.3", note="Use mergesort.v")]
  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.

  #[deprecated(since="8.3", note="Use mergesort.v")]
  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.

  #[deprecated(since="8.3", note="Use mergesort.v")]
  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).

  #[deprecated(since="8.3", note="Use mergesort.v")]
  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.

  #[deprecated(since="8.3", note="Use mergesort.v")]
  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

#[deprecated(since="8.3", note="Use mergesort.v")]
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.

  #[deprecated(since="8.3", note="Use mergesort.v")]
  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.

  #[deprecated(since="8.3", note="Use mergesort.v")]
  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.

  #[deprecated(since="8.3", note="Use mergesort.v")]
  Lemma heap_to_list : forall T:Tree, is_heap T -> flat_spec T.

Specification of treesort

  #[deprecated(since="8.3", note="Use mergesort.v")]
  Theorem treesort :
    forall l:list A,
    {m : list A | Sorted leA m & permutation _ eqA_dec l m }.

End defs.