Library Coq.Sorting.Sorted



This file defines two notions of sorted list:
  • a list is locally sorted if any element is smaller or equal than its successor in the list
  • a list is sorted if any element coming before another one is smaller or equal than this other element
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).
Arguments Transitive [U] R.

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.

#[global]
Hint Constructors HdRel : core.
#[global]
Hint Constructors Sorted : core.