Require Import Coq.Lists.List.
Require Import Coq.omega.Omega.

Fixpoint delete_nth {A} (n: nat) (xs: list A) {struct n} : list A :=
 match n, xs with
 | O, y::ys => ys
 | S n', y::ys =>y :: delete_nth n' ys
 | _ , _ => nil
 end.

Inductive find_nth_preds_rec {A: Type} (pred: A -> Prop): nat -> list A -> option (nat * A) -> Prop :=
| find_nth_preds_rec_cons_head: forall n R0 R, pred R0 -> find_nth_preds_rec pred n (R0 :: R) (Some (n, R0))
| find_nth_preds_rec_cons_tail: forall n R0 R R_res, find_nth_preds_rec pred (S n) R R_res -> find_nth_preds_rec pred n (R0 :: R) R_res
| find_nth_preds_rec_nil: forall n, find_nth_preds_rec pred n nil None.

Local Unset Elimination Schemes. (* ensure that we avoid name collision with the above *)
Inductive find_nth_preds {A: Type} (pred: A -> Prop): list A -> option (nat * A) -> Prop :=
| find_nth_preds_constr: forall R R_res, find_nth_preds_rec pred 0 R R_res -> find_nth_preds pred R R_res.
Scheme Minimality for find_nth_preds Sort Prop.
Local Set Elimination Schemes.

Lemma find_nth_preds_Some: forall {A: Type} (pred: A -> Prop) R n R0, find_nth_preds pred R (Some (n, R0)) ->
  nth_error R n = Some R0 /\ pred R0.
Proof.
(* Goal: forall (A : Type) (pred : forall _ : A, Prop) (z : nat) (R : list A) (n : nat) (Rn : A) (_ : @find_nth_preds_rec A pred z R (@Some (prod nat A) (@pair nat A n Rn))), @find_nth_preds_rec A pred (S z) R (@Some (prod nat A) (@pair nat A (S n) Rn)) *)
  intros.
(* Goal: @ex nat (fun n : nat => @find_nth_preds A pred R (@Some (prod nat A) (@pair nat A n Rn))) *)
  inversion H; subst; clear H.
(* Goal: and (@eq (option A) (@nth_error A R n) (@Some A R0)) (pred R0) *)
  replace n with (n - 0)%nat by omega.
(* Goal: and (@eq (option A) (@nth_error A R (Init.Nat.sub n O)) (@Some A R0)) (pred R0) *)
  assert ((n >= 0)%nat /\ nth_error R (n - 0) = Some R0 /\ pred R0); [| tauto].
(* Goal: forall (A : Type) (pred : forall _ : A, Prop) (z : nat) (R : list A) (n : nat) (Rn : A) (_ : @find_nth_preds_rec A pred z R (@Some (prod nat A) (@pair nat A n Rn))), @find_nth_preds_rec A pred (S z) R (@Some (prod nat A) (@pair nat A (S n) Rn)) *)
  revert H0; generalize 0%nat as m; intros.
(* Goal: and (ge n m) (and (@eq (option A) (@nth_error A R (Init.Nat.sub n m)) (@Some A R0)) (pred R0)) *)
  remember (Some (n, R0)) as R_res eqn:?H in H0.
(* Goal: and (ge n m) (and (@eq (option A) (@nth_error A R (Init.Nat.sub n m)) (@Some A R0)) (pred R0)) *)
  induction H0.
(* Goal: @ex nat (fun n : nat => @find_nth_preds A pred R (@Some (prod nat A) (@pair nat A n Rn))) *)
  + inversion H; subst; clear H.
(* Goal: and (ge n n) (and (@eq (option A) (@nth_error A (@cons A R0 R) (Init.Nat.sub n n)) (@Some A R0)) (pred R0)) *)
    replace (n - n)%nat with 0%nat by omega.
(* Goal: and (@eq (option A) (@nth_error A (@cons A R1 R) (S (Init.Nat.sub n (S n0)))) (@Some A R0)) (pred R0) *)
    simpl; auto.
  + apply IHfind_nth_preds_rec in H.
(* Goal: and (ge n n0) (and (@eq (option A) (@nth_error A (@cons A R1 R) (Init.Nat.sub n n0)) (@Some A R0)) (pred R0)) *)
    destruct H as [? [? ?]].
(* Goal: and (ge n n0) (and (@eq (option A) (@nth_error A (@cons A R1 R) (Init.Nat.sub n n0)) (@Some A R0)) (pred R0)) *)
    replace (n - n0)%nat with (S (n - S n0)) by omega.
(* Goal: and (ge n n0) (and (@eq (option A) (@nth_error A (@cons A R1 R) (S (Init.Nat.sub n (S n0)))) (@Some A R0)) (pred R0)) *)
    split; [omega |].
(* Goal: and (@eq (option A) (@nth_error A (@cons A R1 R) (S (Init.Nat.sub n (S n0)))) (@Some A R0)) (pred R0) *)
    simpl; auto.
  + inversion H.
Qed.

(* Current not used. *)
Lemma find_nth_preds_rec_S: forall {A: Type} (pred: A -> Prop) z R n Rn,
  find_nth_preds_rec pred z R (Some (n, Rn)) ->
  find_nth_preds_rec pred (S z) R (Some (S n, Rn)).
Proof.
(* Goal: forall (A : Type) (pred : forall _ : A, Prop) (z : nat) (R : list A) (n : nat) (Rn : A) (_ : @find_nth_preds_rec A pred z R (@Some (prod nat A) (@pair nat A n Rn))), @find_nth_preds_rec A pred (S z) R (@Some (prod nat A) (@pair nat A (S n) Rn)) *)
  intros.
(* Goal: @find_nth_preds_rec A pred (S z) R (@Some (prod nat A) (@pair nat A (S n) Rn)) *)
  remember (Some (n, Rn)) as Res eqn:?H.
(* Goal: forall (A : Type) (pred : forall _ : A, Prop) (z : nat) (R : list A) (n : nat) (Rn : A) (_ : @find_nth_preds_rec A pred z R (@Some (prod nat A) (@pair nat A n Rn))), @find_nth_preds_rec A pred (S z) R (@Some (prod nat A) (@pair nat A (S n) Rn)) *)
  revert n Rn H0; induction H; intros.
  + inversion H0; subst; clear H0.
(* Goal: @find_nth_preds_rec A pred (S n0) (@cons A Rn R) (@Some (prod nat A) (@pair nat A (S n0) Rn)) *)
    eapply find_nth_preds_rec_cons_head; eauto.
  + subst R_res.
(* Goal: @find_nth_preds_rec A pred (S n) (@cons A R0 R) (@Some (prod nat A) (@pair nat A (S n0) Rn)) *)
    apply find_nth_preds_rec_cons_tail; auto.
  + inversion H0.
Qed.

(* Current not used. *)
Lemma find_nth_preds_rec_delete_nth: forall {A: Type} (pred: A -> Prop) z m R Rn,
  (exists n, find_nth_preds_rec pred z (delete_nth m R) (Some (n, Rn))) ->
  (exists n, find_nth_preds_rec pred z R (Some (n, Rn))).
Proof.
(* Goal: forall (A : Type) (pred : forall _ : A, Prop) (z : nat) (R : list A) (n : nat) (Rn : A) (_ : @find_nth_preds_rec A pred z R (@Some (prod nat A) (@pair nat A n Rn))), @find_nth_preds_rec A pred (S z) R (@Some (prod nat A) (@pair nat A (S n) Rn)) *)
  intros.
  revert z R H; induction m; intros; destruct R; auto.
  + simpl in *.
(* Goal: @ex nat (fun n : nat => @find_nth_preds A pred R (@Some (prod nat A) (@pair nat A n Rn))) *)
    destruct H as [n ?].
    eexists.
    eapply find_nth_preds_rec_cons_tail.
    apply find_nth_preds_rec_S.
    exact H.
  + simpl in *.
(* Goal: @ex nat (fun n : nat => @find_nth_preds A pred R (@Some (prod nat A) (@pair nat A n Rn))) *)
    destruct H as [n ?].
(* Goal: @ex nat (fun n : nat => @find_nth_preds A pred R (@Some (prod nat A) (@pair nat A n Rn))) *)
    inversion H; subst; clear H.
    - eexists; apply find_nth_preds_rec_cons_head; auto.
    - specialize (IHm (S z) _ (ex_intro _ _ H4)).
      clear n H4; destruct IHm as [n ?].
(* Goal: @ex nat (fun n : nat => @find_nth_preds A pred R (@Some (prod nat A) (@pair nat A n Rn))) *)
      exists n.
(* Goal: @find_nth_preds_rec A pred (S n) (@cons A R0 R) (@Some (prod nat A) (@pair nat A (S n0) Rn)) *)
      apply find_nth_preds_rec_cons_tail; auto.
Qed.

(* Current not used. *)
Lemma find_nth_preds_delete_nth: forall {A: Type} (pred: A -> Prop) m R Rn,
  (exists n, find_nth_preds pred (delete_nth m R) (Some (n, Rn))) ->
  (exists n, find_nth_preds pred R (Some (n, Rn))).
Proof.
(* Goal: forall (A : Type) (pred : forall _ : A, Prop) (m : nat) (R : list A) (Rn : A) (_ : @ex nat (fun n : nat => @find_nth_preds A pred (@delete_nth A m R) (@Some (prod nat A) (@pair nat A n Rn)))), @ex nat (fun n : nat => @find_nth_preds A pred R (@Some (prod nat A) (@pair nat A n Rn))) *)
  intros ? ? ? ? ? [n ?].
(* Goal: @ex nat (fun n : nat => @find_nth_preds A pred R (@Some (prod nat A) (@pair nat A n Rn))) *)
  inversion H; subst; clear H.
(* Goal: @ex nat (fun n : nat => @find_nth_preds A pred R (@Some (prod nat A) (@pair nat A n Rn))) *)
  pose proof (ex_intro _ n H0): exists n, find_nth_preds_rec pred 0 (delete_nth m R) (Some (n, Rn)).
(* Goal: @ex nat (fun n : nat => @find_nth_preds A pred R (@Some (prod nat A) (@pair nat A n Rn))) *)
  apply find_nth_preds_rec_delete_nth in H.
(* Goal: @ex nat (fun n : nat => @find_nth_preds A pred R (@Some (prod nat A) (@pair nat A n Rn))) *)
  clear n H0.
(* Goal: @ex nat (fun n : nat => @find_nth_preds A pred R (@Some (prod nat A) (@pair nat A n Rn))) *)
  destruct H as [n ?].
(* Goal: @ex nat (fun n : nat => @find_nth_preds A pred R (@Some (prod nat A) (@pair nat A n Rn))) *)
  exists n.
(* Goal: @find_nth_preds A pred R (@Some (prod nat A) (@pair nat A n Rn)) *)
  apply find_nth_preds_constr; auto.
Qed.

Ltac find_nth_rec tac :=
  first [ simple eapply find_nth_preds_rec_cons_head; tac
        | simple eapply find_nth_preds_rec_cons_tail; find_nth_rec tac
        | simple eapply find_nth_preds_rec_nil].

Ltac find_nth tac :=
  eapply find_nth_preds_constr; find_nth_rec tac.
(* The reason to use "eapply" instead of "simple eapply" is because "find_nth" may be buried in definitions. *)
