Library Coq.Sorting.Sorted
This file defines two notions of sorted list:
The two notions are equivalent if the order is transitive.
- 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
Preambule
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 : core.
Hint Constructors Sorted : core.