# 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 xs → P y → P (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 _ nil ⇒ constructor

| |- Forall _ (_ :: _) ⇒ constructor

| H : Forall _ (?xs ++ ?ys) |- Forall _ ?xs ⇒ apply (IHxs ys)

| H : Forall _ (?xs ++ ?ys) |- Forall _ ?ys ⇒ apply (IHxs ys)

| |- Forall _ (_ ++ ?ys) ⇒ apply (IHxs ys)

end; auto).

Qed.

Lemma Forall_map : ∀ A B (h : A → Prop) f (g : B → Prop), (∀ 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 : A → Prop) f (g : B → Prop), (∀ x, h x → g (f x)) →

∀ xs, Forall h xs → Forall 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.

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 xs → P y → P (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 _ nil ⇒ constructor

| |- Forall _ (_ :: _) ⇒ constructor

| H : Forall _ (?xs ++ ?ys) |- Forall _ ?xs ⇒ apply (IHxs ys)

| H : Forall _ (?xs ++ ?ys) |- Forall _ ?ys ⇒ apply (IHxs ys)

| |- Forall _ (_ ++ ?ys) ⇒ apply (IHxs ys)

end; auto).

Qed.

Lemma Forall_map : ∀ A B (h : A → Prop) f (g : B → Prop), (∀ 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 : A → Prop) f (g : B → Prop), (∀ x, h x → g (f x)) →

∀ xs, Forall h xs → Forall 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.