Lvc.Infra.Drop

Require Import Arith Coq.Lists.List Setoid Coq.Lists.SetoidList.
Require Export Infra.Option EqDec AutoIndTac Util Get.

Set Implicit Arguments.

Fixpoint drop {X} (n : nat) (xs : list X) : list X :=
  match n with
    | 0 ⇒ xs
    | S n ⇒ drop n (tl xs)
  end.

Fixpoint drop_error {X} (n : nat) (xs : list X) : option (list X) :=
  match n with
    | 0 ⇒ Some xs
    | S n ⇒ match xs with
               | nil ⇒ None
               | _::xs ⇒ drop_error n xs
             end
  end.

Lemma drop_get X (L:list X) k n v
  : get L (k+n) v → get (drop k L) n v.

Lemma get_drop_eq X (L L´:list X) n x y
  : get L n x → y::L´ = drop n L → x = y.

Lemma drop_get_nil X k n (v:X)
  : get (drop k nil) n v → False.

Lemma get_drop X (L:list X) k n v
  : get (drop k L) n v → get L (k+n) v.

Lemma length_drop_cons X (L:list X) k a x
  : k ≤ length L → length (drop k L) = a → length (drop k (x::L)) = S a.

Lemma length_drop X (L:list X) a
  : a ≤ length L → length (drop (length L - a) (L)) = a.

Lemma drop_nil X k
  : drop k nil = (@nil X).

Lemma length_drop_minus X (L:list X) k
  : length (drop k L) = length L - k.

Lemma drop_app X (L L´:list X) n
  : drop (length L + n) (L++L´) = drop n L´.

Lemma drop_tl X (L:list X) n
  : tl (drop n L) = drop n (tl L).

Lemma drop_drop X (L:list X) n n´
  : drop n (drop n´ L) = drop (n+n´) L.


Lemma drop_swap X m n (L:list X)
  : drop m (drop n L) = drop n (drop m L).

Lemma drop_nth X k L (x:X) L´ d
  : drop k L = x::L´ → nth k L d = x.

Lemma drop_map X Y (L:list X) n (f:X → Y)
  : List.map f (drop n L) = drop n (List.map f L).

Lemma drop_length_eq X (L L´ :list X)
: drop (length L´) (L´ ++ L) = L.

Lemma drop_length X (L L´ :list X) n
: n < length L´ → drop n (L´ ++ L) = (drop n L´ ++ L)%list.

Lemma drop_length_gr X (L L´ :list X) n x
: n > length L´ → drop n (L´ ++ x::L) = (drop (n - S(length L´)) L)%list.

Lemma drop_eq X (L L´:list X) n y
: y::L´ = drop n L → get L n y.

Lemma drop_shift_1 X (L:list X) y YL i
: y :: YL = drop i L
  → YL = drop (S i) L.

Lemma drop_length_stable X Y (L:list X) (L´:list Y) i
: length L = length L´
  → length (drop i L) = length (drop i L´).

Lemma get_eq_drop X (L :list X) n x
: get L n x → x::drop (S n) L = drop n L.