Why3 Standard Library index

# Pigeon hole principle

```module Pigeonhole

use int.Int
use map.Map

let rec lemma pigeonhole (n m: int) (f: int -> int)
requires { 0 <= m < n }
requires { forall i. 0 <= i < n -> 0 <= f i < m }
ensures  { exists i1, i2. 0 <= i1 < i2 < n /\ f i1 = f i2 }
variant  { m }
= for i = 0 to n - 1 do
invariant { forall k. 0 <= k < i -> f k < m - 1 }
if f i = m - 1 then begin
for j = i + 1 to n - 1 do
invariant { forall k. i < k < j -> f k < m - 1 }
if f j = m - 1 then return
done;
let function g k = if k < i then f k else f (k + 1) in
pigeonhole (n - 1) (m - 1) g;
return end
done;
pigeonhole n (m - 1) f

end

(* An instance where a list is included into a set with fewer elements.

Contributed by Yuto Takei (University of Tokyo) *)

module ListAndSet

use int.Int
use list.List
use list.Length
use list.Append
use list.Mem as Mem
use set.Fset

type t

predicate pigeon_set (s: fset 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 as FSI with
type t = t, predicate p = pigeon_set

lemma corner:
forall s: fset 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: fset t. pigeon_set s ->
forall t: t. pigeon_set (add t s)

lemma pigeon_2:
forall s: fset t. pigeon_set s

lemma pigeonhole:
forall s: fset 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 1.4.0