(** [member] is the proof relevant version of [In] **)
Require Import Coq.Lists.List.
Require Import Relations RelationClasses.
Require Import ExtLib.Core.Type.
Require Import ExtLib.Core.RelDec.
Require Import ExtLib.Data.SigT.
Require Import ExtLib.Data.ListNth.
Require Import ExtLib.Data.Option.
Require Import ExtLib.Structures.Proper.
Require Import ExtLib.Tactics.Injection.
Require Import ExtLib.Tactics.EqDep.

Set Implicit Arguments.
Set Strict Implicit.
Set Asymmetric Patterns.

Section member.
  Context {T : Type}.

  Inductive member (a : T) : list T -> Type :=
  | MZ : forall ls, member a (a :: ls)
  | MN : forall l ls, member a ls -> member a (l :: ls).

  Section to_nat.
    Variable a : T.

(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
    Fixpoint to_nat {ls} (m : member a ls) : nat :=
      match m with
        | MZ _ => 0
        | MN _ _ m => S (to_nat m)
      end.
  End to_nat.

  Lemma member_eta
  : forall x ls (m : member x ls),
      m = match m in member _ ls
                return member x ls
          with
            | MZ ls => MZ x ls
            | MN _ _ n => MN _ n
          end.
  Proof.
(* Goal: forall (x : T) (ls : list T) (m : member x ls), @eq (member x ls) m match m in (member _ ls0) return (member x ls0) with | @MZ _ ls0 => MZ x ls0 | @MN _ l ls0 n => @MN x l ls0 n end *)
    destruct m; auto.
  Qed.

  Lemma member_case
  : forall x ls (m : member x ls),
      match ls as ls return member x ls -> Prop with
        | nil => fun _ => False
        | l :: ls' => fun m =>
                        (exists (pf : l = x),
                           m = match pf in _ = z return member z (l :: ls') with
                                 | eq_refl => MZ _ ls'
                               end)
                        \/ exists m' : member x ls',
                             m = MN _ m'
      end m.
  Proof.
(* Goal: iff (@eq (option (@sigT T (fun x : T => member x ls))) (nth_member ls (@to_nat x ls m)) (@Some (@sigT T (fun x : T => member x ls)) (@existT T (fun x : T => member x ls) x m))) (@eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x)) *)
    induction m.
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
    { left. exists eq_refl. reflexivity. }
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
    { right. eauto. }
  Qed.

  Lemma to_nat_eq_member_eq
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
  : forall {_ : EqDec T (@eq T)} x ls (a b : member x ls),
      to_nat a = to_nat b ->
      a = b.
  Proof.
(* Goal: forall (_ : @EqDec T (@eq T) (@eq_equivalence T)) (x : T) (ls : list T) (a b : member x ls) (_ : @eq nat (@to_nat x ls a) (@to_nat x ls b)), @eq (member x ls) a b *)
    induction a; intros.
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
    { destruct (member_case b).
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
      { destruct H0. subst.
(* Goal: @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
        rewrite (UIP_refl x0). reflexivity. }
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
      { destruct H0. subst.
        simpl in *. congruence. } }
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
    { destruct (member_case b).
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
      { exfalso. destruct H0. subst. simpl in *. congruence. }
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
      { destruct H0. subst. simpl in *.
(* Goal: @eq (option T) (@nth_error T ls (@to_nat x0 ls m)) (@Some T x0) *)
        inversion H; clear H; subst.
        eapply IHa in H1. f_equal. assumption. } }
  Qed.

(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
  Fixpoint nth_member (ls : list T) (n : nat) {struct n}
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
  : option { x : T & member x ls } :=
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
    match ls as ls return option { x : T & member x ls } with
      | nil => None
      | l :: ls =>
        match n with
          | 0 => Some (@existT _ (fun x => member x (l :: ls)) l (MZ _ _))
          | S n =>
            match nth_member ls n with
              | Some (existT v m) => Some (@existT _ _ v (MN _ m))
              | None => None
            end
        end
    end.

  Definition get_next ls y x (m : member x (y :: ls))
  : option (member x ls) :=
    match m in member _ ls'
          return match ls' with
                   | nil => unit
                   | l' :: ls' => option (member x ls')
                 end
    with
      | MZ _ => None
      | MN _ _ m => Some m
    end.

  Instance Injective_MN x y ls m m' : Injective (@MN x y ls m = @MN x y ls m').
  Proof.
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
  refine {| result := m = m' |}.
(* Goal: forall _ : @eq (member x (@cons T y ls)) (@MN x y ls m) (@MN x y ls m'), @eq (member x ls) m m' *)
    intro.
(* Goal: @eq (member x ls) m m' *)
    assert (get_next (MN y m) = get_next (MN y m')).
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
    { rewrite H. reflexivity. }
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
    { simpl in *. inversion H0. reflexivity. }
  Defined.

  Lemma nth_member_nth_error
  : forall ls p,
      nth_member ls (to_nat (projT2 p)) = Some p <->
      nth_error ls (to_nat (projT2 p)) = Some (projT1 p).
  Proof.
(* Goal: iff (@eq (option (@sigT T (fun x : T => member x ls))) (nth_member ls (@to_nat (@projT1 T (fun x : T => member x ls) (@existT T (fun x : T => member x ls) x m)) ls (@projT2 T (fun x : T => member x ls) (@existT T (fun x : T => member x ls) x m)))) (@Some (@sigT T (fun x : T => member x ls)) (@existT T (fun x : T => member x ls) x m))) (@eq (option T) (@nth_error T ls (@to_nat (@projT1 T (fun x : T => member x ls) (@existT T (fun x : T => member x ls) x m)) ls (@projT2 T (fun x : T => member x ls) (@existT T (fun x : T => member x ls) x m)))) (@Some T (@projT1 T (fun x : T => member x ls) (@existT T (fun x : T => member x ls) x m)))) *)
    destruct p. simpl in *.
(* Goal: iff (@eq (option (@sigT T (fun x : T => member x ls))) (nth_member ls (@to_nat x ls m)) (@Some (@sigT T (fun x : T => member x ls)) (@existT T (fun x : T => member x ls) x m))) (@eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x)) *)
    induction m.
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
    { simpl. split; auto. }
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
    { simpl. split.
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
      { intros. destruct (nth_member ls (to_nat m)); try congruence.
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
        { destruct s.
(* Goal: @eq (option T) (@nth_error T ls (@to_nat x0 ls m)) (@Some T x0) *)
          inv_all. subst. inv_all. subst.
(* Goal: @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
          apply IHm. reflexivity. } }
(* Goal: forall _ : @eq (option T) (@nth_error T ls (@to_nat x ls m)) (@Some T x), @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) match nth_member ls (@to_nat x ls m) with | Some (@existT _ _ v m as s) => @Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) v (@MN v l ls m)) | None => @None (@sigT T (fun x : T => member x (@cons T l ls))) end (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
      { intros.
(* Goal: @eq (option (@sigT T (fun x : T => member x (@cons T l ls)))) (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) (@Some (@sigT T (fun x : T => member x (@cons T l ls))) (@existT T (fun x : T => member x (@cons T l ls)) x (@MN x l ls m))) *)
        eapply IHm in H. rewrite H. reflexivity. } }
  Qed.

  Lemma member_In : forall ls (t : T), member t ls -> List.In t ls.
  Proof.
(* Goal: forall (ls : list T) (t : T) (_ : member t ls), @In T t ls *)
    induction 1; simpl; auto.
  Qed.

End member.