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 int.Int, set.Fset, ref.Ref

  let rec ghost below (n: int) : fset 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
    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 return;
      s := add (f i) !s
    done;
    let b = below m in assert { subset !s b };
    absurd

end

download ZIP archive

Why3 Proof Results for Project "pigeonhole"

Theory "pigeonhole.Pigeonhole": fully verified

ObligationsAlt-Ergo 2.1.0
VC for below0.02
VC for pigeonhole---
split_goal_right
loop invariant init0.01
loop invariant init0.00
postcondition0.00
loop invariant preservation0.00
loop invariant preservation0.01
precondition0.00
assertion0.00
unreachable point0.00
out of loop bounds0.00