Library LambdaTamer.ListT
Require Import Eqdep List TheoryList.
Set Implicit Arguments.
Theorem eq_rec_r_ident : forall (A : Type) (x : A) (P : A -> Set)
(H : P x) (H0 : x = x), eq_rec_r P H H0 = H.
Theorem eq_rect_r_ident : forall (A : Type) (x : A) (P : A -> Type)
(H : P x) (H0 : x = x), eq_rect_r P H H0 = H.
Theorem eq_rect_ident : forall (A : Type) (x : A) (P : A -> Type)
(H : P x) (H0 : x = x), eq_rect _ P H _ H0 = H.
Theorem eq_rect_reverse : forall (A : Type) (x : A) (P : A -> Type)
(H : P x) (y : A) (H0 : x = y) (H1 : y = x),
eq_rect _ P (eq_rect _ P H _ H0) _ H1 = H.
Ltac clear_all :=
repeat match goal with
| [ H : _ |- _ ] => clear H
end.
Ltac base_ident := unfold eq_rec_r, eq_rect_r; simpl.
Section optionT.
Variable A : Type.
Inductive optionT : Type :=
| NoneT : optionT
| SomeT : A -> optionT.
Theorem option_inj : forall (v1 v2 : A),
SomeT v1 = SomeT v2
-> v1 = v2.
End optionT.
Section listT.
Variable A : Type.
Inductive listT : Type :=
| nilT : listT
| consT : A -> listT -> listT.
Fixpoint lengthT (ls : listT) : nat :=
match ls with
| nilT => O
| consT _ ls' => S (lengthT ls')
end.
Fixpoint appT (ls1 ls2 : listT) {struct ls1} : listT :=
match ls1 with
| nilT => ls2
| consT x ls1' => consT x (appT ls1' ls2)
end.
Fixpoint InT (x : A) (ls : listT) {struct ls} : Prop :=
match ls with
| nilT => False
| consT x' ls' => x = x' \/ InT x ls'
end.
Fixpoint nthT (n : nat) (ls : listT) {struct ls} : optionT A :=
match ls with
| nilT => NoneT _
| consT v ls' =>
match n with
| O => SomeT v
| S n' => nthT n' ls'
end
end.
Inductive elemT : listT -> A -> Type :=
| firstT : forall v ts,
elemT (consT v ts) v
| nextT : forall v ts v',
elemT ts v'
-> elemT (consT v ts) v'.
Hint Constructors elemT.
Lemma elemT_invert'
: forall P : forall t' l t, elemT (consT t' l) t -> Prop,
(forall G t, P t G t (firstT t G)) ->
(forall G t t' v,
P t' G t (nextT t' v)) ->
forall l t v,
match l return (elemT l t -> Prop) with
| nilT => fun _ => True
| _ => fun v => P _ _ _ v
end v.
Theorem elemT_invert
: forall P : forall t' l t, elemT (consT t' l) t -> Prop,
(forall G t, P t G t (firstT t G)) ->
(forall G t t' v,
P t' G t (nextT t' v)) ->
forall t' l t v, P t' l t v.
Definition retype_elemT : forall x p, x = p
-> forall ls, elemT ls x -> elemT ls p.
Lemma retype_elemT_ident : forall x (Heq : x = x)
ls (elm : elemT ls x), retype_elemT Heq elm = elm.
Lemma elemT_split : forall x ls p (elm : elemT (consT x ls) p),
(x = p /\ forall Heq : x = p, elm = retype_elemT Heq (firstT _ _))
\/ exists elm', elm = nextT _ elm'.
End listT.
Ltac inversion_elemT elm :=
let Heq := fresh "Heq"
with His := fresh "His"
with elm' := fresh "elm'" in
(destruct (elemT_split elm) as [[Heq His] | [elm' His]];
[subst; generalize (His (refl_equal _)); clear His; intro His;
repeat rewrite retype_elemT_ident in His
| idtac];
subst; simpl in *).
Ltac inversion_elemT_any :=
match goal with
| [ elm : elemT _ _ |- _ ] => inversion elm; fail
| [ elm : elemT _ _ |- _ ] => inversion_elemT elm
end.
Section mapT.
Variables A B : Type.
Variable f : A -> B.
Fixpoint mapT (ls : listT A) : listT B :=
match ls with
| nilT => nilT _
| consT h t => consT (f h) (mapT t)
end.
Fixpoint mapElemT (ls : listT A) v (elm : elemT ls v) {struct elm}
: elemT (mapT ls) (f v) :=
match elm in (elemT ls v) return (elemT (mapT ls) (f v)) with
| firstT _ _ => firstT _ _
| nextT _ _ _ elm' => nextT _ (mapElemT elm')
end.
Theorem mapT_InT : forall (ts : listT A) x,
InT x ts
-> InT (f x) (mapT ts).
End mapT.
Section mapT2.
Variable A : Type.
Variable f : A -> A.
Hypothesis idempotent : forall x, f x = x.
Theorem mapIdempotent : forall ls, mapT f ls = ls.
End mapT2.
Section mapT3.
Variables A B C : Type.
Variable f : A -> B.
Variable g : B -> C.
Theorem mapCompose : forall ls,
mapT g (mapT f ls)
= mapT (fun x => g (f x)) ls.
End mapT3.
Section listF.
Variable A : Type.
Variable B : A -> Type.
Inductive listF : listT A -> Type :=
| nilF : listF (nilT _)
| consF : forall v ls,
B v -> listF ls -> listF (consT v ls).
Fixpoint lengthF ts (ls : listF ts) {struct ls} : nat :=
match ls with
| nilF => O
| consF _ _ _ ls' => S (lengthF ls')
end.
Fixpoint appF ts1 (ls1 : listF ts1) ts2 (ls2 : listF ts2) {struct ls1}
: listF (appT ts1 ts2) :=
match ls1 in (listF ts1) return (listF (appT ts1 ts2)) with
| nilF => ls2
| consF _ _ v ls1' => consF v (appF ls1' ls2)
end.
Definition headF' : forall (Tss : listT A)
T ss, Tss = consT T ss
-> listF Tss -> B T.
Definition headF : forall (T : A) (ss : listT A) (ls : listF (consT T ss)), B T.
Definition tailF' : forall (Tss : listT A)
T ss, Tss = consT T ss
-> listF Tss -> listF ss.
Definition tailF : forall (T : A) (ss : listT A) (ls : listF (consT T ss)),
listF ss.
Fixpoint get_elemT ts T (ls : elemT ts T) {struct ls} : listF ts -> B T :=
match ls in (elemT ts T) return (listF ts -> B T) with
| firstT _ _ => fun vals => headF vals
| nextT _ _ _ ls' => fun vals => get_elemT ls' (tailF vals)
end.
Theorem get_elemT_map : forall (l : listT A) p p0,
elemT l p
-> listF (mapT p0 l)
-> B (p0 p).
Section listF_prover.
Variable prover : forall (x : A), B x.
Hint Constructors listF.
Theorem listF_prover : forall ls, listF ls.
Theorem getElemT_listF_prover : forall ls x (elm : elemT ls x),
get_elemT elm (listF_prover ls) = prover x.
End listF_prover.
Section listF_prover'.
Variable ls : listT A.
Variable prover : forall x, elemT ls x -> B x.
Hint Constructors listF elemT.
Lemma listF_prover'' : forall ls', (forall x, elemT ls' x -> elemT ls x) -> listF ls'.
Lemma get_elemT_listF_prover'' : forall ls' (Hinc : forall x, elemT ls' x -> elemT ls x)
x (elm : elemT ls' x),
get_elemT elm (listF_prover'' Hinc) = prover (Hinc _ elm).
Theorem listF_prover' : listF ls.
Theorem getElemT_listF_prover' : forall x (elm : elemT ls x),
get_elemT elm listF_prover' = prover elm.
End listF_prover'.
Variable f : forall (T : A), B T -> Type.
Inductive AllF : forall (ts : listT A), listF ts -> Type :=
| AllF_nil : AllF nilF
| AllF_cons : forall t ts (x : B t) (ls : listF ts),
f x
-> AllF ls
-> AllF (consF x ls).
Hint Constructors AllF.
Theorem head_AllF' : forall ts (ls : listF ts)
(Hall : AllF ls),
match ts return (forall (ls : listF ts), AllF ls -> Type) with
| nilT => fun _ _ => True
| consT _ _ => fun ls _ => f (headF ls)
end ls Hall.
Theorem head_AllF : forall v ts (ls : listF (consT v ts)),
AllF ls
-> f (headF ls).
Theorem tail_AllF' : forall ts (ls : listF ts)
(Hall : AllF ls),
match ts return (forall (ls : listF ts), AllF ls -> Type) with
| nilT => fun _ _ => True
| consT _ _ => fun ls _ => AllF (tailF ls)
end ls Hall.
Theorem tail_AllF : forall v ts (ls : listF (consT v ts)),
AllF ls
-> AllF (tailF ls).
Theorem get_AllF' : forall ts p (elm : elemT ts p)
(ls : listF ts), AllF ls -> f (get_elemT elm ls).
Section get_AllF.
Variable A' : Type.
Variable g : A' -> A.
Definition get_AllF ts p (elm : elemT ts p) ls :=
get_elemT (mapElemT g elm) ls.
Theorem prover_AllF : forall ts p (elm : elemT ts p)
(ls : listF (mapT g ts)), AllF ls
-> f (get_AllF elm ls).
Variable ts : listT A'.
Variable prover : forall x, elemT (mapT g ts) x -> B x.
Lemma get_AllF_listF_prover'' : forall ts' (Hinc : forall x, elemT (mapT g ts') x -> elemT (mapT g ts) x)
p (elm : elemT ts' p),
get_AllF elm (listF_prover'' prover Hinc)
= prover (Hinc _ (mapElemT g elm)).
Theorem get_AllF_listF_prover' : forall p (elm : elemT ts p),
get_AllF elm (listF_prover' prover)
= prover (mapElemT g elm).
End get_AllF.
Section AllF_prover.
Variable prover : forall v (b : B v), f b.
Theorem AllF_prover : forall ts (ls : listF ts),
AllF ls.
Theorem get_AllF'_AllF_prover : forall ts p (elm : elemT ts p) ls,
get_AllF' elm (AllF_prover ls) = prover (get_elemT elm ls).
End AllF_prover.
Lemma fromNilF' : forall (P : listF (nilT _) -> Type) ts
(ls : listF ts),
match ts return (listF ts -> Type) with
| nilT => fun ls => P nilF -> P ls
| _ => fun _ => unit
end ls.
Theorem fromNilF : forall (P : listF (nilT _) -> Type),
P nilF -> forall ls, P ls.
Lemma fromConsF' : forall ts (P : listF ts -> Type)
(ls : listF ts),
match ts return ((listF ts -> Type) -> listF ts -> Type) with
| nilT => fun _ _ => unit
| _ => fun P ls => P (consF (headF ls) (tailF ls)) -> P ls
end P ls.
Theorem fromConsF : forall T ts (P : listF (consT T ts) -> Type)
(ls : listF (consT T ts)), P (consF (headF ls) (tailF ls)) -> P ls.
Theorem invert_listF_nil : forall (ls : listF (nilT _)),
ls = nilF.
Theorem invert_listF_cons : forall T ts (ls : listF (consT T ts)),
exists h, exists t, ls = consF h t.
End listF.
Definition set := fun T : Set => T.
Definition listS := listF set.
Definition nilS : listS (nilT _) := nilF _.
Definition consS (T : Set) ts (x : T) (ls : listS ts) : listS (consT T ts) := consF (B:= set) _ x ls.
Ltac inversion_listF_nil ls :=
let His := fresh "His" in
(generalize (invert_listF_nil ls); intro His;
subst; simpl; unfold eq_rect_r; simpl).
Ltac inversion_listF_cons ls :=
let His := fresh "His"
with h := fresh "h"
with t := fresh "t" in
(destruct (invert_listF_cons ls) as [h [t His]];
subst; simpl;
unfold eq_rect_r; simpl).
Ltac inversion_listF ls := inversion_listF_nil ls || inversion_listF_cons ls.
Ltac inversion_listF_any :=
match goal with
| [ ls : listF _ _ |- _ ] => inversion_listF ls
| [ ls : listS _ |- _ ] => inversion_listF ls
end.
Section mapF.
Variable A : Type.
Variables B1 B2 : A -> Type.
Variable convert : forall x, B1 x -> B2 x.
Fixpoint mapF ts (ls : listF B1 ts) {struct ls} : listF B2 ts :=
match ls in (listF _ ts) return (listF B2 ts) with
| nilF => nilF _
| consF _ _ x ls' => consF _ (convert x) (mapF ls')
end.
Variable A' : Set.
Variable g : A' -> A.
Theorem get_mapF : forall ts (ls : listF B1 (mapT g ts))
p (elm : elemT ts p),
get_AllF g elm (mapF ls)
= convert (get_AllF g elm ls).
End mapF.
Section mapF'.
Variable A : Type.
Variable B1 : A -> Type.
Variable B2 : Set.
Variable convert : forall x, B1 x -> B2.
Fixpoint mapF' ts (ls : listF B1 ts) {struct ls} : list B2 :=
match ls with
| nilF => nil
| consF _ _ x ls' => convert x :: mapF' ls'
end.
Hypothesis convert_neutral : forall x1 x2 (Heq : B1 x1 = B1 x2) (y : B1 x1),
convert y = convert (eq_rect _ (fun x => x) y _ Heq).
Theorem mapF'_In : forall ts (ls : listF B1 ts) x (elm : elemT ts x),
In (convert (get_elemT elm ls)) (mapF' ls).
End mapF'.
Section mapF'_2.
Variable A : Type.
Variables B1 B2 : A -> Type.
Variable B3 : Set.
Variable f1 : forall x, B1 x -> B2 x.
Variable f2 : forall x, B2 x -> B3.
Theorem mapF'_compose : forall ts (ls : listF B1 ts),
mapF' (fun x (y : B1 x) => f2 (f1 y)) ls
= mapF' f2 (mapF _ f1 ls).
End mapF'_2.
Definition headS' : forall (Tss : listT Set)
T ss, Tss = consT T ss
-> listS Tss -> T.
Definition headS : forall (T : Set) (ss : listT Set) (ls : listS (consT T ss)), T.
Definition tailS' : forall (Tss : listT Set)
T ss, Tss = consT T ss
-> listS Tss -> listS ss.
Definition tailS : forall (T : Set) (ss : listT Set) (ls : listS (consT T ss)),
listS ss.
Hint Constructors listF AllF.
Section listF_AllF.
Variable A : Type.
Variables B1 B2 : A -> Set.
Variable f : forall (T : A), B1 T -> Type.
Variable translate : forall (T : A) (x : B1 T), f x -> B2 T.
Theorem listF_AllF : forall ts (terms : listF B1 ts),
AllF f terms
-> listF B2 ts.
End listF_AllF.
Section AllF_map.
Variable A : Type.
Variable B1 : A -> Set.
Variable B2 : Set.
Variable f : forall (T : A), B1 T -> Type.
Variable translate : forall (T : A) (x : B1 T), f x -> B2.
Theorem map_AllF : forall ts (terms : listF B1 ts),
AllF f terms
-> list B2.
Variable prover : forall (v : A) (b : B1 v), f b.
Theorem map_AllF_prover : forall ts (terms : listF B1 ts),
map_AllF (AllF_prover f prover terms)
= mapF' (B2:= B2) (fun (x : A) (y : B1 x) => translate (prover y)) terms.
End AllF_map.
Section get_AllF_prover.
Variables A A' : Type.
Variable g : A' -> A.
Variables B1 B2 : A -> Set.
Variable f : forall (T : A), B1 T -> Type.
Variable translate : forall (T : A) (x : B1 T), f x -> B2 T.
Variable prover : forall v (b : B1 v), f b.
Definition retype_listF : forall (B : A -> Set) ts1 ts2, ts1 = ts2 -> listF B ts1 -> listF B ts2.
Theorem retype_listF_ident : forall B ts (Heq : ts = ts) ls,
retype_listF (B:= B) Heq ls = ls.
Theorem get_AllF_prover' : forall ts' (ls : listF B1 ts')
ts (Heq : ts' = mapT g ts)
p (elm : elemT ts p),
get_AllF g elm (retype_listF Heq (listF_AllF _ translate (AllF_prover f prover ls)))
= translate (prover (get_AllF g elm (retype_listF Heq ls))).
Theorem get_AllF_prover : forall ts (ls : listF B1 (mapT g ts))
p (elm : elemT ts p),
get_AllF g elm (listF_AllF _ translate (AllF_prover f prover ls))
= translate (prover (get_AllF g elm ls)).
End get_AllF_prover.
Definition elemT_absurd : forall (A : Type) (T : A),
elemT (nilT _) T
-> forall (T' : Type), T'.
Ltac simpl_ListT := repeat progress
(repeat inversion_elemT_any;
repeat inversion_listF_any;
simpl in *; intuition).
Ltac trivial_ListT :=
intros;
repeat inversion_elemT_any;
repeat inversion_listF_any;
trivial.
Index
This page has been generated by coqdoc