The Coq Proof Assistant

# 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.