# Library CoLoR.Util.List.ListOccur

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2007-02-08
number of occurrences of an element in a list proof of the pigeon-hole principle

Set Implicit Arguments.

number of occurrences

Section occur.

Variables (A : Type) (eq_dec : forall x y : A, {x=y}+{~x=y}).

Definition delta x y :=
match eq_dec x y with
| left _ => 1
| right _ => 0
end.

Lemma eq_delta : forall x, delta x x = 1.

Lemma neq_delta : forall x y, x <> y -> delta x y = 0.

Fixpoint occur x (l : list A) : nat :=
match l with
| nil => O
| y :: m => delta x y + occur x m
end.

Lemma occur_app : forall x l m, occur x (l ++ m) = occur x l + occur x m.

Lemma in_occur : forall x l, In x l -> occur x l > 0.

Lemma notin_occur : forall x l, ~In x l -> occur x l = 0.

Lemma occur_in : forall x l, occur x l > 0 -> In x l.

Lemma occur_notin : forall x l, occur x l = 0 -> ~In x l.

Lemma occur_S : forall x l n, occur x l = S n ->
exists m, exists p, l = m ++ x :: p /\ ~In x m /\ occur x p = n.

End occur.

pigeon-hole principle

Section pigeon_hole.

Variables (A : Type) (eq_dec : forall x y : A, {x=y}+{~x=y}).

Notation occur := (occur eq_dec).
Notation delta := (delta eq_dec).

Lemma pigeon_hole : forall s l,
incl l s -> length l > length s -> exists x : A, occur x l >= 2.

End pigeon_hole.