pigeonhole.mlw 987 Bytes
Newer Older
1

2 3 4
(** Pigeonhole principle (also know as Dirichlet's drawer principle)

    Proved using a lemma function. *)
5

6
module Pigeonhole
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21

  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))

22
  let lemma pigeonhole (n m: int) (f: int -> int)
23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
    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