Require Import Coq.Lists.List.

Set Implicit Arguments.
Set Strict Implicit.

Section parametric.
  Variable T : Type.

  Lemma nth_error_app_L : forall (A B : list T) n,
    n < length A ->
    nth_error (A ++ B) n = nth_error A n.
  Proof.
(* Goal: forall (A B : list T) (n : nat) (_ : le (@length T A) n), @eq (option T) (@nth_error T (@app T A B) n) (@nth_error T B (Nat.sub n (@length T A))) *)
    induction A; destruct n; simpl; intros; auto.
    { inversion H. }
    { inversion H. }
    { eapply IHA. apply Lt.lt_S_n; assumption. }
  Qed.

  Lemma nth_error_app_R : forall (A B : list T) n,
    length A <= n ->
    nth_error (A ++ B) n = nth_error B (n - length A).
  Proof.
(* Goal: forall (A B : list T) (n : nat) (_ : le (@length T A) n), @eq (option T) (@nth_error T (@app T A B) n) (@nth_error T B (Nat.sub n (@length T A))) *)
    induction A; destruct n; simpl; intros; auto.
(* Goal: lt (S n) O *)
    + inversion H.
    + apply IHA. apply Le.le_S_n; assumption.
  Qed.

  Lemma nth_error_weaken : forall ls' (ls : list T) n v,
    nth_error ls n = Some v ->
    nth_error (ls ++ ls') n = Some v.
  Proof.
(* Goal: forall (ls : list T) (n : nat) (_ : le (@length T ls) n), @eq (option T) (@nth_error T ls n) (@None T) *)
    clear. induction ls; destruct n; simpl; intros; unfold value, error in *; try congruence; auto.
  Qed.

  Lemma nth_error_nil : forall n,
    nth_error nil n = @None T.
  Proof.
(* Goal: forall n : nat, @eq (option T) (@nth_error T (@nil T) n) (@None T) *)
    destruct n; reflexivity.
  Qed.

  Lemma nth_error_past_end : forall (ls : list T) n,
    length ls <= n ->
    nth_error ls n = None.
  Proof.
(* Goal: forall (ls : list T) (n : nat) (_ : le (@length T ls) n), @eq (option T) (@nth_error T ls n) (@None T) *)
    clear. induction ls; destruct n; simpl; intros; auto.
(* Goal: lt (S n) O *)
    + inversion H.
    + apply IHls. apply Le.le_S_n; assumption.
  Qed.

  Lemma nth_error_length : forall (ls ls' : list T) n,
    nth_error (ls ++ ls') (n + length ls) = nth_error ls' n.
  Proof.
(* Goal: forall (ls ls' : list T) (n : nat), @eq (option T) (@nth_error T (@app T ls ls') (Nat.add n (@length T ls))) (@nth_error T ls' n) *)
    induction ls; simpl; intros.
(* Goal: @eq (option T) (@nth_error T ls' (Nat.add n O)) (@nth_error T ls' n) *)
(* Goal: @eq (option T) (@nth_error T (@cons T a (@app T ls ls')) (Nat.add n (S (@length T ls)))) (@nth_error T ls' n) *)
    rewrite Plus.plus_0_r. auto.
(* Goal: @eq (option T) (@nth_error T (@cons T a (@app T ls ls')) (Nat.add n (S (@length T ls)))) (@nth_error T ls' n) *)
    rewrite <- Plus.plus_Snm_nSm.
(* Goal: @eq (option T) (@nth_error T ls n) (@None T) *)
    simpl. eapply IHls.
  Qed.

  Theorem nth_error_length_ge : forall T (ls : list T) n,
    nth_error ls n = None -> length ls <= n.
  Proof.
(* Goal: forall (T : Type) (ls : list T) (n : nat) (_ : @eq (option T) (@nth_error T ls n) (@None T)), le (@length T ls) n *)
    induction ls; destruct n; simpl in *; auto; simpl in *.
    + intro. apply Le.le_0_n.
    + inversion 1.
    + intros. eapply Le.le_n_S. auto.
  Qed.

  Lemma nth_error_length_lt : forall {T} (ls : list T) n val,
    nth_error ls n = Some val -> n < length ls.
  Proof.
(* Goal: forall (T : Type) (ls : list T) (n : nat) (val : T) (_ : @eq (option T) (@nth_error T ls n) (@Some T val)), lt n (@length T ls) *)
    induction ls; destruct n; simpl; intros; auto.
(* Goal: lt (S n) O *)
    + inversion H.
(* Goal: lt (S n) O *)
    + inversion H.
    + apply Lt.lt_0_Sn.
    + apply Lt.lt_n_S. eauto.
  Qed.


  Theorem nth_error_map : forall U (f : T -> U) ls n,
    nth_error (map f ls) n = match nth_error ls n with
                               | None => None
                               | Some x => Some (f x)
                             end.
  Proof.
(* Goal: le (@length T0 ls) n *)
    induction ls; destruct n; simpl; auto.
  Qed.

End parametric.
