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.