examples/pigeonhole.mlw

   1
   2 (** Pigeonhole principle (also know as Dirichlet's drawer principle)
   3
   4     Proved using a lemma function. *)
   5
   6 module Pigeonhole
   7
   8   use int.Int, set.Fset, ref.Ref
   9
  10   let rec ghost below (n: int) : fset int
  11     requires { 0 <= n }
  12     ensures  { forall i. mem i result <-> 0 <= i < n }
  13     ensures  { cardinal result = n }
  14     variant  { n }
  15   = if n = 0 then empty else add (n-1) (below (n-1))
  16
  17   let lemma pigeonhole (n m: int) (f: int -> int)
  18     requires { 0 <= m < n }
  19     requires { forall i. 0 <= i < n -> 0 <= f i < m }
  20     ensures  { exists i1, i2. 0 <= i1 < i2 < n /\ f i1 = f i2 }
  21   =
  22     let s = ref empty in
  23     for i = 0 to n-1 do
  24       invariant { cardinal !s = i }
  25       invariant { forall x. mem x !s <-> (exists j. 0 <= j < i /\ x = f j) }
  26       if mem (f i) !s then return;
  27       s := add (f i) !s
  28     done;
  29     let b = below m in assert { subset !s b };
  30     absurd
  31
  32 end