Require Import Coq.Lists.List.
Require Import Coq.ZArith.ZArith.

Lemma firstn_app_L : forall T n (a b : list T),
  n <= length a ->
  firstn n (a ++ b) = firstn n a.
Proof.
(* Goal: forall (T : Type) (n : nat) (a : list T) (_ : le (@length T a) n), @eq (list T) (@skipn T n a) (@nil T) *)
  induction n; destruct a; simpl in *; intros; auto.
(* Goal: @eq (list T) (@cons T t a) (@nil T) *)
(* Goal: @eq (list T) (@skipn T n a) (@nil T) *)
  exfalso; omega.
(* Goal: @eq (list T) (@cons T t (@firstn T n a)) (@cons T t a) *)
  f_equal. eapply IHn; eauto. omega.
Qed.

Lemma firstn_app_R : forall T n (a b : list T),
  length a <= n ->
  firstn n (a ++ b) = a ++ firstn (n - length a) b.
Proof.
(* Goal: forall (T : Type) (n : nat) (a : list T) (_ : le (@length T a) n), @eq (list T) (@skipn T n a) (@nil T) *)
  induction n; destruct a; simpl in *; intros; auto.
(* Goal: @eq (list T) (@cons T t a) (@nil T) *)
(* Goal: @eq (list T) (@skipn T n a) (@nil T) *)
  exfalso; omega.
(* Goal: @eq (list T) (@cons T t (@firstn T n a)) (@cons T t a) *)
  f_equal. eapply IHn; eauto. omega.
Qed.

Lemma firstn_all : forall T n (a : list T),
  length a <= n ->
  firstn n a = a.
Proof.
(* Goal: forall (T : Type) (n : nat) (a : list T) (_ : le (@length T a) n), @eq (list T) (@firstn T n a) a *)
  induction n; destruct a; simpl; intros; auto.
(* Goal: @eq (list T) (@cons T t a) (@nil T) *)
(* Goal: @eq (list T) (@skipn T n a) (@nil T) *)
  exfalso; omega.
(* Goal: @eq (list T) (@cons T t (@firstn T n a)) (@cons T t a) *)
  simpl. f_equal. eapply IHn; omega.
Qed.

Lemma firstn_0 : forall T n (a : list T),
  n = 0 ->
  firstn n a = nil.
Proof.
(* Goal: forall (T : Type) (n : nat) (a : list T) (_ : @eq nat n O), @eq (list T) (@skipn T n a) a *)
  intros; subst; auto.
Qed.

Lemma firstn_cons : forall T n a (b : list T),
  0 < n ->
  firstn n (a :: b) = a :: firstn (n - 1) b.
Proof.
(* Goal: forall (T : Type) (n : nat) (a : T) (b : list T) (_ : lt O n), @eq (list T) (@skipn T n (@cons T a b)) (@skipn T (Init.Nat.sub n (S O)) b) *)
  destruct n; intros.
(* Goal: @eq (list T) (@skipn T O (@cons T a b)) (@skipn T (Init.Nat.sub O (S O)) b) *)
(* Goal: @eq (list T) (@skipn T (S n) (@cons T a b)) (@skipn T (Init.Nat.sub (S n) (S O)) b) *)
  omega.
(* Goal: @eq (list T) (@skipn T (S n) (@cons T a b)) (@skipn T (Init.Nat.sub (S n) (S O)) b) *)
  simpl. cutrewrite (n - 0 = n); [ | omega ]. reflexivity.
Qed.

Hint Rewrite firstn_app_L firstn_app_R firstn_all firstn_0 firstn_cons using omega : list_rw.

Lemma skipn_app_R : forall T n (a b : list T),
  length a <= n ->
  skipn n (a ++ b) = skipn (n - length a) b.
Proof.
(* Goal: forall (T : Type) (n : nat) (a : list T) (_ : le (@length T a) n), @eq (list T) (@skipn T n a) (@nil T) *)
  induction n; destruct a; simpl in *; intros; auto.
(* Goal: @eq (list T) (@cons T t a) (@nil T) *)
(* Goal: @eq (list T) (@skipn T n a) (@nil T) *)
  exfalso; omega.
(* Goal: @eq (list T) (@skipn T O (@cons T a b)) (@skipn T (Init.Nat.sub O (S O)) b) *)
(* Goal: @eq (list T) (@skipn T (S n) (@cons T a b)) (@skipn T (Init.Nat.sub (S n) (S O)) b) *)
  eapply IHn. omega.
Qed.

Lemma skipn_app_L : forall T n (a b : list T),
  n <= length a ->
  skipn n (a ++ b) = (skipn n a) ++ b.
Proof.
(* Goal: forall (T : Type) (n : nat) (a : list T) (_ : le (@length T a) n), @eq (list T) (@skipn T n a) (@nil T) *)
  induction n; destruct a; simpl in *; intros; auto.
(* Goal: @eq (list T) (@cons T t a) (@nil T) *)
(* Goal: @eq (list T) (@skipn T n a) (@nil T) *)
  exfalso; omega.
(* Goal: @eq (list T) (@skipn T O (@cons T a b)) (@skipn T (Init.Nat.sub O (S O)) b) *)
(* Goal: @eq (list T) (@skipn T (S n) (@cons T a b)) (@skipn T (Init.Nat.sub (S n) (S O)) b) *)
  eapply IHn. omega.
Qed.

Lemma skipn_0 : forall T n (a : list T),
  n = 0 ->
  skipn n a = a.
Proof.
(* Goal: forall (T : Type) (n : nat) (a : list T) (_ : @eq nat n O), @eq (list T) (@skipn T n a) a *)
  intros; subst; auto.
Qed.

Lemma skipn_all : forall T n (a : list T),
  length a <= n ->
  skipn n a = nil.
Proof.
(* Goal: forall (T : Type) (n : nat) (a : list T) (_ : le (@length T a) n), @eq (list T) (@skipn T n a) (@nil T) *)
  induction n; destruct a; simpl in *; intros; auto.
(* Goal: @eq (list T) (@cons T t a) (@nil T) *)
(* Goal: @eq (list T) (@skipn T n a) (@nil T) *)
  exfalso; omega.
(* Goal: @eq (list T) (@skipn T O (@cons T a b)) (@skipn T (Init.Nat.sub O (S O)) b) *)
(* Goal: @eq (list T) (@skipn T (S n) (@cons T a b)) (@skipn T (Init.Nat.sub (S n) (S O)) b) *)
  apply IHn; omega.
Qed.

Lemma skipn_cons : forall T n a (b : list T),
  0 < n ->
  skipn n (a :: b) = skipn (n - 1) b.
Proof.
(* Goal: forall (T : Type) (n : nat) (a : T) (b : list T) (_ : lt O n), @eq (list T) (@skipn T n (@cons T a b)) (@skipn T (Init.Nat.sub n (S O)) b) *)
  destruct n; intros.
(* Goal: @eq (list T) (@skipn T O (@cons T a b)) (@skipn T (Init.Nat.sub O (S O)) b) *)
(* Goal: @eq (list T) (@skipn T (S n) (@cons T a b)) (@skipn T (Init.Nat.sub (S n) (S O)) b) *)
  omega.
(* Goal: @eq (list T) (@skipn T (S n) (@cons T a b)) (@skipn T (Init.Nat.sub (S n) (S O)) b) *)
  simpl. cutrewrite (n - 0 = n); [ | omega ]. reflexivity.
Qed.

Hint Rewrite skipn_app_L skipn_app_R skipn_0 skipn_all skipn_cons using omega : list_rw.