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.