Library ListFacts


Assorted facts about lists that are not in Coq's standard library.

Implicit arguments are declared by default in this library.


Require Import Coq.Lists.List.
Require Import Coq.Lists.SetoidList.

Open Scope list_scope.

List structure


Lemma cons_eq_app : ∀ (A : Type) (z : A) (xs ys zs : list A),
  z :: zs = xs ++ ys
  (∃ qs, xs = z :: qszs = qs ++ ys) ∨
  (xs = nilys = z :: zs).

Lemma app_eq_cons : ∀ (A : Type) (z : A) (xs ys zs : list A),
  xs ++ ys = z :: zs
  (∃ qs, xs = z :: qszs = qs ++ ys) ∨
  (xs = nilys = z :: zs).

Lemma nil_eq_app : ∀ (A : Type) (xs ys : list A),
  nil = xs ++ ys
  xs = nilys = nil.

Lemma app_cons_not_nil : ∀ (A : Type) (y : A) (xs ys : list A),
  xs ++ y :: ysnil.


List membership


Lemma In_map : ∀ (A B : Type) (xs : list A) (x : A) (f : AB),
  In x xs
  In (f x) (map f xs).

Setoid facts


Lemma InA_In : ∀ (A : Type) (x : A) (xs : list A),
  InA (@eq _) x xsIn x xs.

Lemma InA_iff_In : ∀ (A : Type) (x : A) (xs : list A),
  InA (@eq _) x xsIn x xs.

This page has been generated by coqdoc