Library Coq.Sorting.Sorted



This file defines two notions of sorted list:
The two notions are equivalent if the order is transitive.

Require Import List Relations Relations_1.

Preambule

Set Implicit Arguments.
Local Notation "[ ]" := nil (at level 0).
Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) (at level 0).

Section defs.

  Variable A : Type.
  Variable R : A -> A -> Prop.

Locally sorted: consecutive elements of the list are ordered

  Inductive LocallySorted : list A -> Prop :=
    | LSorted_nil : LocallySorted []
    | LSorted_cons1 a : LocallySorted [a]
    | LSorted_consn a b l :
        LocallySorted (b :: l) -> R a b -> LocallySorted (a :: b :: l).

Alternative two-step definition of being locally sorted

  Inductive HdRel a : list A -> Prop :=
    | HdRel_nil : HdRel a []
    | HdRel_cons b l : R a b -> HdRel a (b :: l).

  Inductive Sorted : list A -> Prop :=
    | Sorted_nil : Sorted []
    | Sorted_cons a l : Sorted l -> HdRel a l -> Sorted (a :: l).

  Lemma HdRel_inv : forall a b l, HdRel a (b :: l) -> R a b.

  Lemma Sorted_inv :
    forall a l, Sorted (a :: l) -> Sorted l /\ HdRel a l.

  Lemma Sorted_rect :
    forall P:list A -> Type,
      P [] ->
      (forall a l, Sorted l -> P l -> HdRel a l -> P (a :: l)) ->
      forall l:list A, Sorted l -> P l.

  Lemma Sorted_LocallySorted_iff : forall l, Sorted l <-> LocallySorted l.

Strongly sorted: elements of the list are pairwise ordered

  Inductive StronglySorted : list A -> Prop :=
    | SSorted_nil : StronglySorted []
    | SSorted_cons a l : StronglySorted l -> Forall (R a) l -> StronglySorted (a :: l).

  Lemma StronglySorted_inv : forall a l, StronglySorted (a :: l) ->
    StronglySorted l /\ Forall (R a) l.

  Lemma StronglySorted_rect :
    forall P:list A -> Type,
      P [] ->
      (forall a l, StronglySorted l -> P l -> Forall (R a) l -> P (a :: l)) ->
      forall l, StronglySorted l -> P l.

  Lemma StronglySorted_rec :
    forall P:list A -> Type,
      P [] ->
      (forall a l, StronglySorted l -> P l -> Forall (R a) l -> P (a :: l)) ->
      forall l, StronglySorted l -> P l.

  Lemma StronglySorted_Sorted : forall l, StronglySorted l -> Sorted l.

  Lemma Sorted_extends :
    Transitive R -> forall a l, Sorted (a::l) -> Forall (R a) l.

  Lemma Sorted_StronglySorted :
    Transitive R -> forall l, Sorted l -> StronglySorted l.

End defs.

Hint Constructors HdRel.
Hint Constructors Sorted.