PADEC - Coq Library

Library Padec.Tools.PigeonHole

A Framework for Certified Self-Stabilization
PADEC Coq Library

March 2017

Global Imports

From Coq Require Import Finite_sets.
From Coq Require Import Finite_sets_facts.
From Coq Require Import Lia.
From Coq Require List.
From Coq Require SetoidList.

Section PigeonHole.

A variation on the Pigeon Hole principle with coq Ensembles

Let n and k be natural numbers such that k is greater or equal to n and n is greater or equal to 2. Let s be a finite set with cardinal less or equal to n-1, then there exists an natural number x such that x is less or equal to k-1 and x is not in s.

Open Scope nat.

We start by demonstrating that if the set of all natural numbers smaller or equal to n is included in s and s is finite then the cardinal of s is greater than n+1. s is finite to ensure the fact that it has a cardinal, See coq Finite sets library for more details.

  Lemma Pigeon_hole_cardinal_le:
    forall (n:nat), n >0->
                     forall (s:Ensemble nat),
                       Finite nat s ->
                       (forall x, x <=n ->In nat s x )->
                       exists c , cardinal nat s c /\ (S n ) <= c.

We then show that for two sets A and B either B is included in A or there exists an x which belongs to B but not to A. This is conditionned by the finiteness of B and the decidability of belonging to A.

  Remark Included_or_exists_outside: forall A B, Finite nat B ->
                          (forall x,{A x }+{~A x })->
                          (Included nat B A )\/(exists x , In nat B x /\~ In nat A x ).

For all natural numbers n, the sets of all natural numbers smaller or equal to n is finite.

Remark Finite_le: forall n, Finite nat (fun x=>x <=n).

The final principle

  Theorem Pigeon_hole: forall n k s c, 2<=n ->n <=k ->
                                   Finite nat s ->
                                   (forall x,{s x }+{~ s x })->
                                   cardinal nat s c ->
                                   c <= n -1->
                                   (exists x , x <=k -1/\~ In nat s x ).

  Import List.
  Import SetoidList.

  Fixpoint Set_from_list (l:list nat):=
    match l with
    | nil => Empty_set nat
    | a::l' =>Ensembles.Add nat (Set_from_list l') a
    end.

  Lemma Finite_Set_from_list : forall l, Finite nat (Set_from_list l).

  Lemma Set_from_list_equiv:
    forall l x, Ensembles.In nat (Set_from_list l) x <->In x l.

  Lemma Set_from_list_dec: forall l x,
      {Ensembles.In nat (Set_from_list l ) x }+{~Ensembles.In nat (Set_from_list l ) x }.

  Lemma cardinal_Set_from_list:
    forall l c A, NoDupA eq l ->(forall x, Ensembles.In nat A x <->In x l )->cardinal nat A c ->c = (length l ).

    Theorem Pigeon_hole_list: forall n k
                                     (l:list nat) c,
      NoDupA eq l ->
      2<=n ->n <=k ->
      length l = c ->
      c <= n -1->
      (exists x , x <=k -1/\~ List.In x l ).

End PigeonHole.