From Coq Require Export List Arith Relations Lia.
From Coq Require Import Sorting.Sorted Compare_dec Sorting.Sorted.

Fixpoint iota_from i n :=
  match n with 0 ⇒ nil
            | S p ⇒ i :: iota_from (S i) p
  end.

Definition interval i j := iota_from i (S j - i).

Definition bounded_by (n:nat)(s: list nat) :=
  List.Forall (fun i ⇒ i≤n)%nat s.


Definition shift (l: list nat) := List.map S l.

Fixpoint unshift (l : list nat) : list nat :=
  match l with
      nil ⇒ nil
    | 0 :: l' ⇒ unshift l'
    | S i :: l' ⇒ i :: unshift l'
  end.

Inductive sorted_ge (n: nat) : list nat → Prop :=
| sorted_ge_nil : sorted_ge n nil
| sorted_ge_one : ∀ p, n≤p → sorted_ge n (p::nil)
| sorted_ge_cons: ∀ p q s,
    n ≤ p → p < q → sorted_ge p (q::s) →
    sorted_ge n (p::q::s).

Fixpoint simple_last {A} (x:A) s :=
  match s with
      nil ⇒ x
    | i::s' ⇒ simple_last i s'
  end.

Fixpoint but_last {A:Type}(x:A) (s : list A) :=
  match s with
  | nil ⇒ nil
  | y::s' ⇒ x :: but_last y s'
  end.

Lemma but_last_iota_from : ∀ l i,
      but_last i (iota_from (S i) (S l)) = i::iota_from (S i) l.

Lemma interval_length i j : length (interval i j) = S j - i.

Lemma but_last_interval i j:
  i < j →
  but_last i (interval (S i) (S j)) = i:: interval (S i) j.

Lemma but_last_shift' s : ∀ x,
     but_last (S x) (shift s) = shift (but_last x s).

Lemma unshift_but_last s : ∀ x,
    ¬ In 0 (x::s) →
    unshift (but_last x s) = but_last (Nat.pred x) (unshift s).

Lemma unshift_app : ∀ s t, unshift (s ++ t) = unshift s ++ unshift t.

Lemma unshift_not_nil : ∀ s, ¬ In 0 s → s ≠ nil → unshift s ≠ nil.

Lemma but_last_app {A} : ∀ s (x:A),
  but_last x s ++ simple_last x s :: nil = x::s.

Lemma but_last_iota_from' j : ∀ i, but_last i (iota_from (S i) (S j)) =
                                       iota_from i (S j).

Definition ptwise_le: list nat → list nat → Prop := Forall2 le.

Lemma empty_interval i j : (j < i)%nat → interval i j = nil.

Lemma shift_iota_from : ∀ i l, shift (iota_from i l) = iota_from (S i) l.

Lemma shift_interval (i j: nat): shift (interval i j) = interval (S i) (S j).

Lemma unshift_iota_from : ∀ i l, unshift (iota_from (S i) l) =
                                       iota_from i l.

Lemma unshift_interval (i j: nat): unshift (interval (S i) (S j)) =
                                   interval i j.

Lemma unshift_interval_pred (i j:nat) : 0 < j →
  unshift (interval (S i) j) = interval i (Nat.pred j).

Lemma shift_no_zero l : ¬ In 0 (shift l).

Lemma shift_unshift l : unshift (shift l) = l.

Lemma unshift_shift l (H: ¬ In 0 l): shift (unshift l) = l.

Lemma unshift_pred : ∀ (s: list nat), ¬ In 0 s →
                                            unshift s = List.map Nat.pred s.


Lemma sorted_ge_Forall (n:nat) : ∀ l, sorted_ge n l →
                                           Forall (fun x ⇒ n ≤ x) l.

Lemma sorted_ge_trans n p l : n ≤ p → sorted_ge p l → sorted_ge n l.

Lemma sorted_ge_not_In (n:nat) : ∀ l, sorted_ge (S n) l →
                                           ¬ In n l.

#[global] Hint Constructors sorted_ge : lists.

Lemma sorted_inv_gt : ∀ n p s, sorted_ge n (p::s) →
                                    (p < n)%nat → False.

Lemma iota_from_app n p :
  iota_from n (S p) = iota_from n p ++ (n+p::nil)%nat.

Lemma iota_from_plus : ∀ k i j, iota_from i (k+j) =
                                     iota_from i k ++ iota_from (k+i) j.

Lemma interval_not_empty : ∀ i j, i ≤ j → interval i j ≠ nil.

Lemma interval_not_empty_iff (n p : nat) :
  interval n p ≠ nil ↔ (n ≤ p)%nat.

Lemma interval_singleton (i:nat) : interval i i = i::nil.

Lemma interval_app (i j k:nat):
  (i ≤ j)%nat → (j ≤ k)%nat →
  interval i k = interval i j ++ interval (S j) k.

Lemma iota_from_unroll i l : iota_from i (S l) = i :: iota_from (S i) l.

Lemma interval_unroll : ∀ i j:nat , (i < j)%nat →
                                       interval i j = i :: interval (S i) j.

Lemma iota_from_sorted_ge : ∀ p n q : nat,
    (q ≤ n)%nat →
    sorted_ge q (iota_from n p).

Lemma interval_sorted_ge: ∀ p n q : nat, (q ≤ n)%nat →
                                                sorted_ge q (interval n p).

Lemma iota_from_lt_not_In i j l : i < j → ¬ In i (iota_from j l).

Lemma interval_lt_not_In :
  ∀ i j k, i < j → ¬ In i (interval j k).

Section Forall2_right_induction.

Inductive Forall2R {A B: Type} (R: A → B → Prop) : list A → list B → Prop :=
  Forall2R_nil : Forall2R R nil nil
| Forall2R_last : ∀ l l' x y l1 l'1, Forall2R R l l' →
                                          R x y →
                                          l1 = l++(x::nil) →
                                          l'1 = l' ++ (y::nil) →
                                          Forall2R R l1 l'1.

Remark Forall2R_cons {A B: Type} (R: A → B → Prop):
  ∀ l l', Forall2R R l l' → ∀ x y, R x y → Forall2R R (x::l) (y:: l').


Remark Forall2_R {A B: Type} (R: A → B → Prop) :
  ∀ l l', Forall2 R l l' → Forall2R R l l'.

Remark Forall2_RR {A B: Type} (R: A → B → Prop) :
  ∀ l l', Forall2R R l l' → Forall2 R l l'.

Lemma Forall2R_iff {A B: Type} (R: A → B → Prop) :
  ∀ l l', Forall2R R l l' ↔ Forall2 R l l'.

Lemma Forall2_indR {A B : Type} (R : A → B → Prop) (P : list A → list B → Prop):
P nil nil →
(∀ (l : list A) (l' : list B) (x : A) (y : B)
   (l1 : list A) (l'1 : list B),
 Forall2 R l l' → P l l' →
 R x y → l1 = l ++ x :: nil → l'1 = l' ++ y :: nil → P l1 l'1) →
  ∀ (l : list A) (l0 : list B), Forall2 R l l0 → P l l0.

End Forall2_right_induction.

Lemma sorted_le : ∀ i j X, i ≤ j →
                                sorted_ge j X →
                                sorted_ge i X.


Lemma sorted_tail : ∀ i j X, sorted_ge i (j::X) →
                                  sorted_ge i X.

Lemma sorted_tail' : ∀ i j X, sorted_ge i (j::X) →
                                   sorted_ge j X.

Lemma sorted_head : ∀ n m s, sorted_ge n (m::s)
                                  → n≤m.

Lemma Sorted_mono {A:Type}(R S : relation A)
      (Hincl : ∀ x y, R x y → S x y):
  ∀ l, Sorted R l → Sorted S l.

Lemma sorted_ge_iff0 : ∀ l n, sorted_ge n l ↔
                                    LocallySorted Peano.lt l ∧
                                    List.Forall (fun i ⇒ n ≤ i) l.

Lemma sorted_ge_iff : ∀ l n, sorted_ge n l ↔
                                    Sorted lt l ∧
                                    List.Forall (fun i ⇒ n ≤ i) l.

Lemma sorted_ge_prefix :
  ∀ l1 n l2, sorted_ge n (l1 ++ l2) → sorted_ge n l1.

Lemma sorted_In : ∀ i X, Sorted lt (i::X) → ∀ j, In j X → i < j.

Lemma sorted_not_in_tail : ∀ i j X, Sorted lt (i::X) → j≤i →
                                           ¬ (In j X).

Remark simple_last_correct {A}: ∀ s (x:A), simple_last x s = last s x.

Lemma In_sorted_ge_inv : ∀ x y s,
                             In x (y::s) →
                             sorted_ge y s →
                             y < x ∧ In x s ∨ y = x.

Lemma incl_inv : ∀ x y l1 l2, Sorted lt (x::l1) →
                                    Sorted lt (y::l2) →
                                    incl (x::l1)(y::l2) →
                                    y ≤ x ∧ incl l1 l2.

Lemma incl_decomp : ∀ l1 l2, Sorted lt l1 →
                                   Sorted lt l2 →
                                   incl l1 l2 →
                                   ∃ l3 l4, l2 = l3 ++ l4 ∧
                                                  ptwise_le l3 l1.

  Lemma simple_last_app {A}: ∀ l l1 (x y:A), simple_last x (l++(y::l1)) =
                                     simple_last y l1 .

Lemma simple_last_app1 {A}: ∀ l (x y:A), simple_last x (l++(y::nil)) = y.

Lemma sorted_max_1 : ∀ s n, sorted_ge n s →
                                 (n ≤ simple_last n s)%nat.

Lemma sorted_cut :∀ l1 n x l2, sorted_ge n (l1++(x::l2)) →
                                    simple_last n l1 ≤ x.

Lemma sorted_max_2 : ∀ s n, sorted_ge n s →
                                 Forall (fun i ⇒
                                           (i ≤ simple_last n s)%nat)
                                        s.

Lemma sorted_ge_suffix :
  ∀ l1 n l2, sorted_ge n (l1 ++ l2) → sorted_ge (simple_last n l1) l2.