Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrbool ssrfun ssrnat eqtype fintype choice seq.
From mathcomp Require Import path.

Set Implicit Arguments.

Open Scope N.

Module LeqGeqOrder.

Definition geq_refl : reflexive geq :=
  fun x => leqnn x.
Definition geq_total : total geq :=
  fun x y => leq_total y x.
Definition geq_trans : transitive geq :=
  fun x y z H1 H2 => leq_trans H2 H1.
Definition anti_geq : antisymmetric geq :=
  fun x y H => esym (anti_leq H).
Definition ltn_irr : irreflexive ltn :=
  fun x => ltnn x.
Definition gtn_trans : transitive gtn :=
  fun x y z H1 H2 => ltn_trans H2 H1.
Definition gtn_irr : irreflexive gtn :=
  fun x => ltnn x.

#[export] Hint Resolve leq_total leq_trans anti_leq : core.
#[export] Hint Resolve geq_refl geq_total geq_trans anti_geq : core.
#[export] Hint Resolve ltn_trans ltn_irr gtn_trans gtn_irr : core.

End LeqGeqOrder.

Import LeqGeqOrder.

Section Sorted.

Variable T : eqType.
Variable Z : T.
Variable R : rel T.

Implicit Type l : T.
Implicit Type r : seq T.

#[local] Notation sorted r := (sorted R r).
#[local] Notation "x <=R y" := (R x y) (at level 70, y at next level).

Lemma sorted_consK l r : sorted (cons l r) -> sorted r.

Lemma sorted_rconsK l r : sorted (rcons r l) -> sorted r.

Lemma sorted_rcons l r : sorted r -> (last l r <=R l) -> sorted (rcons r l).

Hypothesis Rtrans : transitive R.

Lemma incr_equiv r :
  (forall (i j : nat), i < j < (size r) -> nth Z r i <=R nth Z r j)
  <->
  (forall (i : nat), i.+1 < (size r) -> nth Z r i <=R nth Z r i.+1).

Lemma sorted_strictP r :
  reflect
    (forall (i j : nat), i < j < (size r) -> (nth Z r i <=R nth Z r j))
    (sorted r).

Hypothesis Rrefl : reflexive R.

Lemma non_decr_equiv r :
  (forall (i j : nat), i <= j < (size r) -> nth Z r i <=R nth Z r j)
  <->
  (forall (i : nat), i.+1 < (size r) -> nth Z r i <=R nth Z r i.+1).

Lemma sorted2P r :
  reflect
    (forall (i j : nat), i <= j < (size r) -> (nth Z r i <=R nth Z r j))
    (sorted r).

Lemma sorted_cons l r : sorted (cons l r) -> (l <=R head l r) /\ sorted r.

Lemma sorted_last l r : sorted (rcons r l) -> (last l r <=R l).

Lemma head_leq_last_sorted l r : sorted (l :: r) -> (l <=R last l r).

Hypothesis Hanti : antisymmetric R.

Lemma sorted_lt_by_pos r p q :
  sorted r -> p < size r -> q < size r ->
   (nth Z r p != nth Z r q) && (nth Z r p <=R nth Z r q) -> p < q.

End Sorted.

Require Import tools.

Lemma enum_ord_sorted_ltn N :
  sorted (fun i j : 'I_N => i < j) (enum 'I_N).

Lemma enum_ord_sorted N :
  sorted (fun i j : 'I_N => i <= j) (enum 'I_N).

Lemma sorted_ltn_ind s :
  sorted ltn s -> sumn (iota 0 (size s)) <= sumn s /\ last 0 s >= (size s).-1.

Lemma sorted_sumn_iotaE s :
  sorted ltn s -> sumn s = sumn (iota 0 (size s)) -> s = iota 0 (size s).