Wiki Agenda Contact Version française

Pigeonhole principle

Pigeonhole principle (aka Dirichlet's drawer principle) proved using a lemma function.


Authors: Jean-Christophe Filliâtre

Topics: Mathematics / Ghost code

Tools: Why3

see also the index (by topic, by tool, by reference, by year)



Pigeonhole principle (also know as Dirichlet's drawer principle)

Proved using a lemma function.

module Pigeonhole

  use import HighOrd
  use import int.Int
  use import set.Fset
  use import ref.Ref

  exception Exit

  let rec below (n: int) : set int
    requires { 0 <= n }
    ensures  { forall i. mem i result <-> 0 <= i < n }
    ensures  { cardinal result = n }
    variant  { n }
  = if n = 0 then empty else add (n-1) (below (n-1))

  let 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 }
  =
    let s = ref empty in
    try
    for i = 0 to n-1 do
      invariant { cardinal !s = i }
      invariant { forall x. mem x !s <-> (exists j. 0 <= j < i /\ x = f j) }
      if mem (f i) !s then raise Exit;
      s := add (f i) !s
    done;
    let b = below m in assert { subset !s b };
    absurd
    with Exit -> () end

end

download ZIP archive

Why3 Proof Results for Project "pigeonhole"

Theory "pigeonhole.Pigeonhole": fully verified in 0.16 s

ObligationsAlt-Ergo (0.99.1)
VC for below0.01
VC for pigeonhole---
split_goal_wp
  1. precondition0.02
2. assertion0.01
3. unreachable point0.02
4. loop invariant init0.01
5. loop invariant init0.01
6. postcondition0.02
7. loop invariant preservation0.01
8. loop invariant preservation0.02
9. precondition0.00
10. assertion0.02
11. unreachable point0.01