(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* Made by Hugo Herbelin *)

Require Import List Relations Relations_1.

(* Set Universe Polymorphism. *)

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.

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

  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.
A:Type
R:A -> A -> Prop
forall (a b : A) (l : list A),
HdRel a (b :: l) -> R a b
  Proof.
A:Type
R:A -> A -> Prop
forall (a b : A) (l : list A),
HdRel a (b :: l) -> R a b
    inversion 1; auto.
  Qed.

  Lemma Sorted_inv :
    forall a l, Sorted (a :: l) -> Sorted l /\ HdRel a l.
A:Type
R:A -> A -> Prop
forall (a : A) (l : list A),
Sorted (a :: l) -> Sorted l /\ HdRel a l
  Proof.
A:Type
R:A -> A -> Prop
forall (a : A) (l : list A),
Sorted (a :: l) -> Sorted l /\ HdRel a l
    intros a l H; inversion H; auto.
  Qed.

  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.
A:Type
R:A -> A -> Prop
forall P : list A -> Type,
P [ ] ->
(forall (a : A) (l : list A),
 Sorted l -> P l -> HdRel a l -> P (a :: l)) ->
forall l : list A, Sorted l -> P l
  Proof.
A:Type
R:A -> A -> Prop
forall P : list A -> Type,
P [ ] ->
(forall (a : A) (l : list A),
 Sorted l -> P l -> HdRel a l -> P (a :: l)) ->
forall l : list A, Sorted l -> P l
    induction l.
A:Type
R:A -> A -> Prop
P:list A -> Type
X:P [ ]
X0:forall (a : A) (l : list A),
Sorted l -> P l -> HdRel a l -> P (a :: l)
Sorted [ ] -> P [ ]
A:Type
R:A -> A -> Prop
P:list A -> Type
X:P [ ]
X0:forall (a0 : A) (l0 : list A),
Sorted l0 -> P l0 -> HdRel a0 l0 -> P (a0 :: l0)
a:A
l:list A
IHl:Sorted l -> P l
Sorted (a :: l) -> P (a :: l) firstorder using Sorted_inv.
A:Type
R:A -> A -> Prop
P:list A -> Type
X:P [ ]
X0:forall (a0 : A) (l0 : list A),
Sorted l0 -> P l0 -> HdRel a0 l0 -> P (a0 :: l0)
a:A
l:list A
IHl:Sorted l -> P l
Sorted (a :: l) -> P (a :: l) firstorder using Sorted_inv.
  Qed.

  Lemma Sorted_LocallySorted_iff : forall l, Sorted l <-> LocallySorted l.
A:Type
R:A -> A -> Prop
forall l : list A, Sorted l <-> LocallySorted l
  Proof.
A:Type
R:A -> A -> Prop
forall l : list A, Sorted l <-> LocallySorted l
    split; [induction 1 as [|a l [|]]| induction 1];
      auto using Sorted, LocallySorted, HdRel.
A:Type
R:A -> A -> Prop
a:A
l:list A
a0:A
l0:list A
H:Sorted l0
H0:HdRel a0 l0
H1:HdRel a (a0 :: l0)
IHSorted:LocallySorted (a0 :: l0)
LocallySorted (a :: a0 :: l0)
    inversion H1; subst; auto using LocallySorted.
  Qed.

  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.
A:Type
R:A -> A -> Prop
forall (a : A) (l : list A),
StronglySorted (a :: l) ->
StronglySorted l /\ Forall (R a) l
  Proof.
A:Type
R:A -> A -> Prop
forall (a : A) (l : list A),
StronglySorted (a :: l) ->
StronglySorted l /\ Forall (R a) l
    intros; inversion H; auto.
  Defined.

  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.
A:Type
R:A -> A -> Prop
forall P : list A -> Type,
P [ ] ->
(forall (a : A) (l : list A),
 StronglySorted l ->
 P l -> Forall (R a) l -> P (a :: l)) ->
forall l : list A, StronglySorted l -> P l
  Proof.
A:Type
R:A -> A -> Prop
forall P : list A -> Type,
P [ ] ->
(forall (a : A) (l : list A),
 StronglySorted l ->
 P l -> Forall (R a) l -> P (a :: l)) ->
forall l : list A, StronglySorted l -> P l
    induction l; firstorder using StronglySorted_inv.
  Defined.

  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.
A:Type
R:A -> A -> Prop
forall P : list A -> Type,
P [ ] ->
(forall (a : A) (l : list A),
 StronglySorted l ->
 P l -> Forall (R a) l -> P (a :: l)) ->
forall l : list A, StronglySorted l -> P l
  Proof.
A:Type
R:A -> A -> Prop
forall P : list A -> Type,
P [ ] ->
(forall (a : A) (l : list A),
 StronglySorted l ->
 P l -> Forall (R a) l -> P (a :: l)) ->
forall l : list A, StronglySorted l -> P l
    firstorder using StronglySorted_rect.
  Qed.

  Lemma StronglySorted_Sorted : forall l, StronglySorted l -> Sorted l.
A:Type
R:A -> A -> Prop
forall l : list A, StronglySorted l -> Sorted l
  Proof.
A:Type
R:A -> A -> Prop
forall l : list A, StronglySorted l -> Sorted l
    induction 1 as [|? ? ? ? HForall]; constructor; trivial.
A:Type
R:A -> A -> Prop
a:A
l:list A
H:StronglySorted l
HForall:Forall (R a) l
IHStronglySorted:Sorted l
HdRel a l
    destruct HForall; constructor; trivial.
  Qed.

  Lemma Sorted_extends :
    Transitive R -> forall a l, Sorted (a::l) -> Forall (R a) l.
A:Type
R:A -> A -> Prop
Transitive R ->
forall (a : A) (l : list A),
Sorted (a :: l) -> Forall (R a) l
  Proof.
A:Type
R:A -> A -> Prop
Transitive R ->
forall (a : A) (l : list A),
Sorted (a :: l) -> Forall (R a) l
    intros.
A:Type
R:A -> A -> Prop
H:Transitive R
a:A
l:list A
H0:Sorted (a :: l)
Forall (R a) l change match a :: l with [] => True | a :: l => Forall (R a) l end.
A:Type
R:A -> A -> Prop
H:Transitive R
a:A
l:list A
H0:Sorted (a :: l)
match a :: l with
| [ ] => True
| a0 :: l0 => Forall (R a0) l0
end
    induction H0 as [|? ? ? ? H1]; [trivial|].
A:Type
R:A -> A -> Prop
H:Transitive R
a:A
l:list A
a0:A
l0:list A
H0:Sorted l0
H1:HdRel a0 l0
IHSorted:match l0 with
| [ ] => True
| a1 :: l1 => Forall (R a1) l1
end
Forall (R a0) l0
    destruct H1; constructor; trivial.
A:Type
R:A -> A -> Prop
H:Transitive R
a:A
l:list A
a0, b:A
l0:list A
H0:Sorted (b :: l0)
H1:R a0 b
IHSorted:Forall (R b) l0
Forall (R a0) l0
    eapply Forall_impl; [|eassumption].
A:Type
R:A -> A -> Prop
H:Transitive R
a:A
l:list A
a0, b:A
l0:list A
H0:Sorted (b :: l0)
H1:R a0 b
IHSorted:Forall (R b) l0
forall a1 : A, R b a1 -> R a0 a1
    firstorder.
  Qed.

  Lemma Sorted_StronglySorted :
    Transitive R -> forall l, Sorted l -> StronglySorted l.
A:Type
R:A -> A -> Prop
Transitive R ->
forall l : list A, Sorted l -> StronglySorted l
  Proof.
A:Type
R:A -> A -> Prop
Transitive R ->
forall l : list A, Sorted l -> StronglySorted l
    induction 2; constructor; trivial.
A:Type
R:A -> A -> Prop
H:Transitive R
a:A
l:list A
H0:Sorted l
H1:HdRel a l
IHSorted:StronglySorted l
Forall (R a) l
    apply Sorted_extends; trivial.
A:Type
R:A -> A -> Prop
H:Transitive R
a:A
l:list A
H0:Sorted l
H1:HdRel a l
IHSorted:StronglySorted l
Sorted (a :: l)
    constructor; trivial.
  Qed.

End defs.

Hint Constructors HdRel : core.
Hint Constructors Sorted : core.

(* begin hide *)
(* Compatibility with deprecated file Sorting.v *)
Notation lelistA := HdRel (only parsing).
Notation nil_leA := HdRel_nil (only parsing).
Notation cons_leA := HdRel_cons (only parsing).

Notation sort := Sorted (only parsing).
Notation nil_sort := Sorted_nil (only parsing).
Notation cons_sort := Sorted_cons (only parsing).

Notation lelistA_inv := HdRel_inv (only parsing).
Notation sort_inv := Sorted_inv (only parsing).
Notation sort_rect := Sorted_rect (only parsing).
(* end hide *)