Why3 Standard Library index

# 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
```

Generated by why3doc 0.88.0