Library Copland.More_lists



More facts about lists.

Require Import List Omega.
Import List.ListNotations.
Open Scope list_scope.

Set Implicit Arguments.

Section More_lists.

  Variable A: Type.

This is the analog of firstn_app from the List library.

  Lemma skipn_app n:
     l1 l2: list A,
      skipn n (l1 ++ l2) = (skipn n l1) ++ (skipn (n - length l1) l2).

  Lemma firstn_append:
     l l': list A,
      firstn (length l) (l ++ l') = l.

  Lemma skipn_append:
     l l': list A,
      skipn (length l) (l ++ l') = l'.

  Lemma skipn_all:
     l: list A,
      skipn (length l) l = [].

  Lemma skipn_nil:
     i,
      @skipn A i [] = [].

  Lemma firstn_all_n:
     (l: list A) n,
      length l n
      firstn n l = l.

  Lemma skipn_all_n:
     (l: list A) n,
      length l n
      skipn n l = [].

  Lemma firstn_in:
     x i (l: list A),
      In x (firstn i l)
      In x l.

  Lemma skipn_in:
     x i (l: list A),
      In x (skipn i l)
      In x l.

  Lemma skipn_zero:
     l: list A,
      skipn 0 l = l.

  Lemma in_skipn_cons:
     i x y (l: list A),
      In x (skipn i l)
      In x (skipn i (y :: l)).

Do l and l' share no elements?

  Definition disjoint_lists (l l': list A): Prop :=
     x, In x l In x l' False.

  Lemma nodup_append:
     l l': list A,
      NoDup l NoDup l'
      disjoint_lists l l'
      NoDup (l ++ l').

  Lemma in_cons_app_cons:
     x y z (l: list A),
      In x (y :: l ++ [z])
      x = y In x l x = z.

Earlier

Is x earlier than y in list l? This definition is used in contexts in which l has no duplicates.

  Definition earlier (l: list A) (x y: A) :=
     n,
      In x (firstn n l)
      In y (skipn n l).

  Lemma earlier_in_left:
     l x y,
      earlier l x y In x l.

  Lemma earlier_in_right:
     l x y,
      earlier l x y In y l.

x is earlier than y in p ++ q if x is earlier than y in p.

  Lemma earlier_left:
     p q x y,
      earlier p x y earlier (p ++ q) x y.

x is earlier than y in p ++ q if x is earlier than y in q.

  Lemma earlier_right:
     p q x y,
      earlier q x y earlier (p ++ q) x y.

  Lemma earlier_append:
     p q x y,
      In x p In y q
      earlier (p ++ q) x y.

  Lemma earlier_append_iff:
     x y (l l': list A),
      earlier (l ++ l') x y
      earlier l x y In x l In y l' earlier l' x y.

  Lemma earlier_cons:
     p x y,
      In y p
      earlier (x :: p) x y.

  Lemma earlier_cons_shift:
     p x y z,
      earlier p x y
      earlier (z :: p) x y.

End More_lists.

Unset Implicit Arguments.