# 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

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

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.