(** {1 Pigeon hole principle} Contributed by Yuto Takei (University of Tokyo) *) theory Pigeonhole use import int.Int use import list.List use import list.Length use import list.Append use list.Mem use import set.Fset type t predicate pigeon_set (s: set t) = forall l: list t. (forall e: t. Mem.mem e l -> mem e s) -> (length l > cardinal s) -> exists e: t, l1 l2 l3: list t. l = l1 ++ (Cons e (l2 ++ (Cons e l3))) clone set.FsetInduction with type t = t, predicate p = pigeon_set lemma corner: forall s: set t, l: list t. (length l = cardinal s) -> (forall e: t. Mem.mem e l -> mem e s) -> (exists e: t, l1 l2 l3: list t. l = l1 ++ (Cons e (l2 ++ (Cons e l3)))) \/ (forall e: t. mem e s -> Mem.mem e l) lemma pigeon_0: pigeon_set empty lemma pigeon_1: forall s: set t. pigeon_set s -> forall t: t. pigeon_set (add t s) lemma pigeon_2: forall s: set t. pigeon_set s lemma pigeonhole: forall s: set t, l: list t. (forall e: t. Mem.mem e l -> mem e s) -> (length l > cardinal s) -> exists e: t, l1 l2 l3: list t. l = l1 ++ (Cons e (l2 ++ (Cons e l3))) end