# Library list

Require Import Omega.
Require Import List.

Require Import ext.

Lemma cut_length : A i (xys : list A) j, length xys = i + j xs ys,
xys = xs ++ ys length xs = i length ys = j.
Proof.
induction i; simpl; intros xys j l; [ nil, xys; auto|].
destruct xys as [|x xys]; inversion l.
destruct IHi with (j := j) (xys := xys) as [? [? [? [? ?]]]]; auto.
(x :: x0), x1; simpl; split; [|split]; auto.
rewrite H; auto.
Qed.

Lemma Forall_nth : A P xs (y : A) n, Forall P xsP yP (nth n xs y).
Proof. induction xs; intros y [|n] Pxs Py; inversion Pxs; simpl in *; auto. Qed.

Lemma Forall_app : A C (xs ys : list A), Forall C (xs ++ ys) Forall C xs Forall C ys.
Proof.
induction xs; simpl; split; intros Cxys;
repeat (simpl; match goal with
| H : _ _ |- _destruct H
| H : Forall _ (_ :: _) |- _inversion H; clear H
| |- _ _split
| |- Forall _ nilconstructor
| |- Forall _ (_ :: _) ⇒ constructor
| H : Forall _ (?xs ++ ?ys) |- Forall _ ?xsapply (IHxs ys)
| H : Forall _ (?xs ++ ?ys) |- Forall _ ?ysapply (IHxs ys)
| |- Forall _ (_ ++ ?ys) ⇒ apply (IHxs ys)
end; auto).
Qed.

Lemma Forall_map : A B (h : AProp) f (g : BProp), ( x, g (f x) = h x) →
xs, Forall g (map f xs) = Forall h xs.
Proof.
induction xs; intros; simpl; apply propositional_extensionality; split; constructor; inversion H0; subst.
rewrite H in H3; auto.
rewrite IHxs in H4; auto.
rewrite <- H in H3; auto.
rewrite <- IHxs in H4; auto.
Qed.

Lemma Forall_map_impl : A B (h : AProp) f (g : BProp), ( x, h xg (f x)) →
xs, Forall h xsForall g (map f xs).
Proof. induction xs; intros; simpl; constructor; inversion H0; subst; auto. Qed.

Lemma replicate : A (a : A) n, xs, length xs = n i, nth i xs a = a.
Proof.
induction n.
nil; split; auto.
intros i; destruct i; auto.
destruct IHn as [xs [? ?]].
(cons a xs).
split; simpl; try omega.
intros i; destruct i; auto.
Qed.