Library list

Require Import Omega.
Require Import List.

Require Import ext.

Inductive list_v := .

Links: Index_v Table of contents Main page

This file defines some lemmas for lists.

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.
(* 2: 0 *)
   nil; split; auto.
  intros i; destruct i; auto.
(* 1: 1+ *)
  destruct IHn as [xs [? ?]].
   (cons a xs).
  split; simpl; try omega.
  intros i; destruct i; auto.
Qed.

Lemma skipn_overflow : A d h, length h < dskipn d h = @nil A.
Proof.
induction d; destruct h; simpl; intros; auto.
inversion H.
apply IHd.
omega.
Qed.

Lemma skipn_app_length : A (h2 h1 : list A),
  skipn (length h1) (h1 ++ h2) = h2.
Proof. induction h1; simpl; auto. Qed.