Dependent lists
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.