stdlib/pigeon.mlw

   1
   2 (** {1 Pigeon hole principle} *)
   3
   4 module Pigeonhole
   5
   6   use int.Int
   7   use map.Map
   8
   9   let rec lemma pigeonhole (n m: int) (f: int -> int)
  10     requires { 0 <= m < n }
  11     requires { forall i. 0 <= i < n -> 0 <= f i < m }
  12     ensures  { exists i1, i2. 0 <= i1 < i2 < n /\ f i1 = f i2 }
  13     variant  { m }
  14   = for i = 0 to n - 1 do
  15       invariant { forall k. 0 <= k < i -> f k < m - 1 }
  16       if f i = m - 1 then begin
  17         for j = i + 1 to n - 1 do
  18           invariant { forall k. i < k < j -> f k < m - 1 }
  19           if f j = m - 1 then return
  20         done;
  21         let function g k = if k < i then f k else f (k + 1) in
  22         pigeonhole (n - 1) (m - 1) g;
  23         return end
  24     done;
  25     pigeonhole n (m - 1) f
  26
  27 end
  28
  29 (** An instance where a list is included into a set with fewer elements.
  30
  31    Contributed by Yuto Takei (University of Tokyo) *)
  32
  33 module ListAndSet
  34
  35   use int.Int
  36   use list.List
  37   use list.Length
  38   use list.Append
  39   use list.Mem as Mem
  40   use set.Fset
  41
  42   type t
  43
  44   predicate pigeon_set (s: fset t) =
  45     forall l: list t.
  46     (forall e: t. Mem.mem e l -> mem e s) ->
  47     (length l > cardinal s) ->
  48     exists e: t, l1 l2 l3: list t.
  49     l = l1 ++ (Cons e (l2 ++ (Cons e l3)))
  50
  51   clone set.FsetInduction as FSI with
  52     type t = t, predicate p = pigeon_set
  53
  54   lemma corner:
  55     forall s: fset t, l: list t.
  56     (length l = cardinal s) ->
  57     (forall e: t. Mem.mem e l -> mem e s) ->
  58     (exists e: t, l1 l2 l3: list t.
  59     l = l1 ++ (Cons e (l2 ++ (Cons e l3)))) \/
  60     (forall e: t. mem e s -> Mem.mem e l)
  61
  62   lemma pigeon_0:
  63     pigeon_set empty
  64
  65   lemma pigeon_1:
  66     forall s: fset t. pigeon_set s ->
  67     forall t: t. pigeon_set (add t s)
  68
  69   lemma pigeon_2:
  70     forall s: fset t. pigeon_set s
  71
  72   lemma pigeonhole:
  73     forall s: fset t, l: list t.
  74     (forall e: t. Mem.mem e l -> mem e s) ->
  75     (length l > cardinal s) ->
  76     exists e: t, l1 l2 l3: list t.
  77     l = l1 ++ (Cons e (l2 ++ (Cons e l3)))
  78
  79 end