Require Export lists.

Section Dep_lists.
  Variable A : Type.
  Variable T : A → Type.

  Definition dep_prop : Type := ∀(a : A), T a → Prop.

  Definition subset_dep_prop(P Q : dep_prop) : Prop :=
    ∀(a : A)(ta : T a), P a ta → Q a ta.

  Inductive dep_list : list A → Type :=
    | dep_nil : dep_list []
    | dep_cons : ∀(a : A)(al : list A),
        T a → dep_list al → dep_list (a :: al).

  Fixpoint dep_nth(al : list A)(tal : dep_list al)(n : nat)
                             (inside : n < length al) : T (nth al n inside) :=
    match tal
      in (dep_list l)
      return (∀ inside0 : n < length l, T (nth l n inside0))
    with
      | dep_nil ⇒ fun(inside0 : n < length []) ⇒
        nth_0_nil_tcc n inside0 _
      | dep_cons a al0 ta tal0 ⇒ fun(inside0 : n < length (a :: al0)) ⇒
          match n
            return (∀(inside1 : n < length (a :: al0)),
                                          T (nth (a :: al0) n inside1))
          with
            | 0 ⇒ fun _ ⇒ ta
            | S n0 ⇒ fun(inside1 : S n0 < length (a :: al0)) ⇒
              dep_nth al0 tal0 n0 (nth_succ_tcc n0 a al0 inside1)
          end inside0
    end inside.

  Lemma nth_dep_nth_tcc_irr :
    ∀(B : Type)(f : ∀(a : A), T a → B)
          (al : list A)(tal : dep_list al)
          (n : nat)(n_less_1 n_less_2 : n < length al),
      f (nth al n n_less_1) (dep_nth al tal n n_less_1) =
      f (nth al n n_less_2) (dep_nth al tal n n_less_2).

  Definition every_dep_nth(P : dep_prop)(al : list A)(tal : dep_list al)
                                                                      : Prop :=
    ∀(n : nat)(n_less : n < length al),
      P (nth al n n_less) (dep_nth al tal n n_less).

  Lemma every_dep_nth_empty : ∀(P : dep_prop),
    every_dep_nth P [] dep_nil.

  Lemma every_dep_nth_cons :
    ∀(P : dep_prop)(a : A)(ta : T a)(l : list A)(tl : dep_list l),
      P a ta →
      every_dep_nth P l tl →
        every_dep_nth P (a :: l) (dep_cons a l ta tl).

  Lemma every_dep_nth_head :
    ∀(P : dep_prop)(a : A)(ta : T a)(l : list A)(tl : dep_list l),
      every_dep_nth P (a :: l) (dep_cons a l ta tl) →
        P a ta.

  Lemma every_dep_nth_tail :
    ∀(P : dep_prop)(a : A)(ta : T a)(l : list A)(tl : dep_list l),
      every_dep_nth P (a :: l) (dep_cons a l ta tl) →
        every_dep_nth P l tl.

  Fixpoint dep_map_const_dep(f : ∀(a : A), T a)(al : list A)
                                                              : dep_list al :=
    match al with
      | [] ⇒ dep_nil
      | a :: al ⇒ dep_cons a al (f a) (dep_map_const_dep f al)
    end.

  Fixpoint dep_map_dep_const(B : Type)(f : ∀(a : A), T a → B)
                                (al : list A)(tal : dep_list al) : list B :=
    match tal with
      | dep_nil ⇒ []
      | dep_cons a al ta tal ⇒
          (f a ta) :: (dep_map_dep_const B f al tal)
    end.

  Lemma length_dep_map_dep_const :
    ∀(B : Type)(f : ∀(a : A), T a → B)
          (al : list A)(tal : dep_list al),
      length (dep_map_dep_const B f al tal) = length al.

  Lemma nth_dep_map_dep_const_tcc :
    ∀(B : Type)(f : ∀(a : A), T a → B)
          (al : list A)(tal : dep_list al)(n : nat),
      n < length (dep_map_dep_const B f al tal) →
        n < length al.

  Lemma nth_dep_map_dep_const :
    ∀(B : Type)(f : ∀(a : A), T a → B)
          (al : list A)(tal : dep_list al)
          (n : nat)(n_less : n < length (dep_map_dep_const B f al tal)),
      nth (dep_map_dep_const B f al tal) n n_less =
        f (nth al n (nth_dep_map_dep_const_tcc B f al tal n n_less))
          (dep_nth al tal n (nth_dep_map_dep_const_tcc B f al tal n n_less)).

  Lemma nth_dep_map_dep_const_inv_tcc :
    ∀(B : Type)(f : ∀(a : A), T a → B)
          (al : list A)(tal : dep_list al)(n : nat),
      n < length al →
        n < length (dep_map_dep_const B f al tal).

  Lemma nth_dep_map_dep_const_inv :
    ∀(B : Type)(f : ∀(a : A), T a → B)
          (al : list A)(tal : dep_list al)
          (n : nat)(n_less : n < length al),
      f (nth al n n_less) (dep_nth al tal n n_less) =
        nth (dep_map_dep_const B f al tal) n
            (nth_dep_map_dep_const_inv_tcc B f al tal n n_less).

  Lemma every_dep_nth_dep_map_const :
    ∀(B : Type)(f : ∀(a : A), T a → B)(P : B → Prop)
          (al : list A)(tal : dep_list al),
      every_nth P (dep_map_dep_const B f al tal) →
        every_dep_nth (fun(a : A)(ta : T a) ⇒ P (f a ta)) al tal.

  Lemma every_nth_exists :
    ∀(Q : dep_prop)(l : list A),
      every_nth (fun(a : A) ⇒ ∃(b : T a), Q a b) l →
        ∃(dl : dep_list l), every_dep_nth Q l dl.

  Lemma every_nth_exists_apply :
    ∀(P : A → Prop)(Q : dep_prop)(l : list A),
      every_nth (fun(a : A) ⇒ P a → ∃(b : T a), Q a b) l →
      every_nth P l →
        ∃(dl : dep_list l), every_dep_nth Q l dl.

  Lemma every_nth_exists_inv :
    ∀(Q : dep_prop)(l : list A)(dl : dep_list l),
      every_dep_nth Q l dl →
        every_nth (fun(a : A) ⇒ ∃(b : T a), Q a b) l.

End Dep_lists.

Implicit Arguments dep_nil [A T].
Implicit Arguments dep_cons [A T].
Implicit Arguments dep_nth [A T].
Implicit Arguments every_dep_nth [A T].
Implicit Arguments every_dep_nth_empty [A T].
Implicit Arguments every_dep_nth_cons [A T].
Implicit Arguments every_dep_nth_head [A T].
Implicit Arguments every_dep_nth_tail [A T].
Implicit Arguments dep_map_const_dep [A T].
Implicit Arguments dep_map_dep_const [A T B].
Implicit Arguments nth_dep_map_dep_const_tcc [A T B f al tal n].
Implicit Arguments every_nth_exists [A T].
Implicit Arguments every_nth_exists_apply [A T].

Fixpoint dep_map_dep_dep{A : Type}{T1 T2 : A → Type}
                        (f : ∀(a : A), T1 a → T2 a)
                        (al : list A)(dal : dep_list A T1 al)
                                                          : dep_list A T2 al :=
  match dal with
    | dep_nil ⇒ dep_nil
    | dep_cons a al da dal ⇒ dep_cons a al (f a da) (dep_map_dep_dep f al dal)
  end.

Fixpoint dep_list_proj_left{A : Type}{T : A → Type}{B : Type}
           (al : list A)(tsal : dep_list A (fun(a : A) ⇒ sum (T a) B) al) :
                                                     (dep_list A T al) + B :=
  match tsal with
    | dep_nil ⇒ inl dep_nil
    | dep_cons a al (inr b) _ ⇒ inr b
    | dep_cons a al (inl ta) tsal ⇒
      match dep_list_proj_left al tsal with
        | inr b ⇒ inr b
        | inl tal ⇒ inl (dep_cons a al ta tal)
      end
  end.

Lemma dep_list_proj_left_dep_map :
  ∀(A : Type)(T : A → Type)(B : Type)
        (f : ∀(a : A), sum (T a) B)(al : list A)(b : B),
    dep_list_proj_left al (dep_map_const_dep f al) = inr b →
      ∃ n : nat,
        n_less # n < length al /#\ f (nth al n n_less) = inr b.

Fixpoint list_of_dep_list{A B : Type}(l : list A)
                         (dl : dep_list A (fun _ ⇒ B) l) : list B :=
  match dl with
    | dep_nil ⇒ []
    | dep_cons _ l b dl ⇒ b :: (list_of_dep_list l dl)
  end.

Lemma list_of_dep_list_dep_map_dep_dep :
  ∀(A : Type)(T : A → Type)(B : Type)
        (f : ∀(a : A), T a → B)
        (al : list A)(tal : dep_list A T al),
    list_of_dep_list al (dep_map_dep_dep f al tal)
      = dep_map_dep_const f al tal.

Lemma every_nth_of_dep_list :
  ∀{A : Type}{P : A → Prop}(l : list A),
    (∃ pl : dep_list A P l, True) → every_nth P l.

Fixpoint dep_list_of_every_nth{A : Type}{P : A → Prop}(l : list A)
                                    (p_l : every_nth P l) : dep_list A P l :=
  match l return every_nth P l → dep_list A P l with
    | [] ⇒ fun _ ⇒ dep_nil
    | a :: l ⇒ fun(H : every_nth P (a :: l)) ⇒
      dep_cons a l (every_nth_head _ _ _ H)
        (dep_list_of_every_nth l (every_nth_tail _ _ _ H))
  end p_l.